-
Notifications
You must be signed in to change notification settings - Fork 6
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
3b8ec20
commit c185c8a
Showing
9 changed files
with
169 additions
and
107 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,31 +1,60 @@ | ||
| import Mathlib.Analysis.RCLike.Basic | ||
| import Mathlib.Data.Complex.Basic | ||
| import LeanAPAP.Prereqs.Expect.Basic | ||
|
|
||
| open Finset | ||
| open scoped BigOperators NNReal | ||
|
|
||
| section | ||
| variable {ι K E : Type*} [RCLike K] [NormedField E] [CharZero E] [NormedSpace K E] | ||
|
|
||
| include K in | ||
| @[bound] | ||
| lemma norm_expect_le {s : Finset ι} {f : ι → E} : ‖𝔼 i ∈ s, f i‖ ≤ 𝔼 i ∈ s, ‖f i‖ := | ||
| s.le_expect_of_subadditive norm norm_zero norm_add_le (fun _ _ ↦ by rw [RCLike.norm_nnqsmul K]) f | ||
|
|
||
| end | ||
|
|
||
| namespace NNReal | ||
| variable {ι : Type*} | ||
|
|
||
| @[simp, norm_cast] | ||
| lemma coe_expect (s : Finset ι) (a : ι → ℝ≥0) : 𝔼 i ∈ s, a i = 𝔼 i ∈ s, (a i : ℝ) := | ||
| map_expect toRealHom _ _ | ||
| lemma coe_expect (s : Finset ι) (f : ι → ℝ≥0) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : ℝ) := | ||
| map_expect toRealHom .. | ||
|
|
||
| end NNReal | ||
|
|
||
| namespace Complex | ||
| variable {ι : Type*} | ||
|
|
||
| @[simp, norm_cast] | ||
| lemma ofReal_expect (s : Finset ι) (a : ι → ℝ) : 𝔼 i ∈ s, a i = 𝔼 i ∈ s, (a i : ℂ) := | ||
| map_expect ofReal _ _ | ||
| lemma ofReal_expect (s : Finset ι) (f : ι → ℝ) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : ℂ) := | ||
| map_expect ofReal .. | ||
|
|
||
| @[simp] lemma ofReal_comp_balance [Fintype ι] (f : ι → ℝ) : | ||
| ofReal ∘ balance f = balance (ofReal ∘ f) := by simp [balance] | ||
|
|
||
| @[simp] lemma ofReal'_comp_balance [Fintype ι] (f : ι → ℝ) : | ||
| ofReal' ∘ balance f = balance (ofReal' ∘ f) := ofReal_comp_balance _ | ||
|
|
||
| end Complex | ||
|
|
||
| namespace RCLike | ||
| variable {ι 𝕜 : Type*} [RCLike 𝕜] | ||
|
|
||
| @[simp, norm_cast] | ||
| lemma coe_expect (s : Finset ι) (a : ι → ℝ) : 𝔼 i ∈ s, a i = 𝔼 i ∈ s, (a i : 𝕜) := | ||
| map_expect (algebraMap _ _) _ _ | ||
| lemma coe_expect (s : Finset ι) (f : ι → ℝ) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : 𝕜) := | ||
| map_expect (algebraMap ..) .. | ||
|
|
||
| variable [Fintype ι] (f : ι → ℝ) (a : ι) | ||
|
|
||
| @[simp, norm_cast] | ||
| lemma coe_balance : (↑(balance f a) : 𝕜) = balance ((↑) ∘ f) a := map_balance (algebraMap ..) .. | ||
|
|
||
| @[simp] lemma coe_comp_balance : ((↑) : ℝ → 𝕜) ∘ balance f = balance ((↑) ∘ f) := | ||
| funext $ coe_balance _ | ||
|
|
||
| @[simp] lemma ofReal_comp_balance : ofReal ∘ balance f = balance (ofReal ∘ f : ι → 𝕜) := by | ||
| simp [balance] | ||
|
|
||
| end RCLike |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,73 @@ | ||
| import Mathlib.Analysis.RCLike.Basic | ||
| import Mathlib.Data.Complex.Basic | ||
| import Mathlib.Data.Complex.Module | ||
| import LeanAPAP.Prereqs.Function.Indicator.Defs | ||
|
|
||
| open Finset Function | ||
| open Fintype (card) | ||
| open scoped ComplexConjugate Pointwise NNRat | ||
|
|
||
| /-! ### Indicator -/ | ||
|
|
||
| variable {ι α β γ : Type*} [DecidableEq α] | ||
|
|
||
| section Semiring | ||
| variable [Semiring β] [Semiring γ] {s : Finset α} | ||
|
|
||
| variable (β) | ||
| variable {β} | ||
| variable [StarRing β] | ||
|
|
||
| lemma indicate_isSelfAdjoint (s : Finset α) : IsSelfAdjoint (𝟭_[β] s) := | ||
| Pi.isSelfAdjoint.2 fun g ↦ by rw [indicate]; split_ifs <;> simp | ||
|
|
||
| end Semiring | ||
|
|
||
| namespace NNReal | ||
| open scoped NNReal | ||
|
|
||
| @[simp, norm_cast] lemma coe_indicate (s : Finset α) (x : α) : ↑(𝟭_[ℝ≥0] s x) = 𝟭_[ℝ] s x := | ||
| map_indicate NNReal.toRealHom _ _ | ||
|
|
||
| @[simp] lemma coe_comp_indicate (s : Finset α) : (↑) ∘ 𝟭_[ℝ≥0] s = 𝟭_[ℝ] s := by | ||
| ext; exact coe_indicate _ _ | ||
|
|
||
| end NNReal | ||
|
|
||
| namespace Complex | ||
|
|
||
| @[simp, norm_cast] lemma ofReal_indicate (s : Finset α) (x : α) : ↑(𝟭_[ℝ] s x) = 𝟭_[ℂ] s x := | ||
| map_indicate ofReal _ _ | ||
|
|
||
| @[simp] lemma ofReal_comp_indicate (s : Finset α) : (↑) ∘ 𝟭_[ℝ] s = 𝟭_[ℂ] s := by | ||
| ext; exact ofReal_indicate _ _ | ||
|
|
||
| end Complex | ||
|
|
||
| /-! ### Normalised indicator -/ | ||
|
|
||
| namespace Complex | ||
| variable (s : Finset α) (a : α) | ||
|
|
||
| @[simp, norm_cast] lemma ofReal_mu : ↑(μ_[ℝ] s a) = μ_[ℂ] s a := map_mu (algebraMap ℝ ℂ) .. | ||
| @[simp] lemma ofReal_comp_mu : (↑) ∘ μ_[ℝ] s = μ_[ℂ] s := funext $ ofReal_mu _ | ||
|
|
||
| end Complex | ||
|
|
||
| namespace RCLike | ||
| variable {𝕜 : Type*} [RCLike 𝕜] (s : Finset α) (a : α) | ||
|
|
||
| @[simp, norm_cast] lemma coe_mu : ↑(μ_[ℝ] s a) = μ_[𝕜] s a := map_mu (algebraMap ℝ 𝕜) _ _ | ||
| @[simp] lemma coe_comp_mu : (↑) ∘ μ_[ℝ] s = μ_[𝕜] s := funext $ coe_mu _ | ||
|
|
||
| end RCLike | ||
|
|
||
| namespace NNReal | ||
| open scoped NNReal | ||
|
|
||
| @[simp, norm_cast] | ||
| lemma coe_mu (s : Finset α) (x : α) : ↑(μ_[ℝ≥0] s x) = μ_[ℝ] s x := map_mu NNReal.toRealHom _ _ | ||
|
|
||
| @[simp] lemma coe_comp_mu (s : Finset α) : (↑) ∘ μ_[ℝ≥0] s = μ_[ℝ] s := funext $ coe_mu _ | ||
|
|
||
| end NNReal |
Oops, something went wrong.