diff --git a/LeanAPAP.lean b/LeanAPAP.lean index d21e1ee554..d66dc57613 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -20,6 +20,7 @@ import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef import LeanAPAP.Mathlib.MeasureTheory.Measure.Typeclasses import LeanAPAP.Mathlib.Order.Filter.Basic import LeanAPAP.Mathlib.Order.LiminfLimsup +import LeanAPAP.Mathlib.Probability.ConditionalProbability import LeanAPAP.Mathlib.Tactic.Positivity import LeanAPAP.Physics.AlmostPeriodicity import LeanAPAP.Physics.DRC @@ -46,7 +47,8 @@ import LeanAPAP.Prereqs.Function.Indicator.Basic import LeanAPAP.Prereqs.Function.Indicator.Defs import LeanAPAP.Prereqs.Function.Translate import LeanAPAP.Prereqs.LargeSpec -import LeanAPAP.Prereqs.LpNorm.Compact +import LeanAPAP.Prereqs.LpNorm.Compact.Defs +import LeanAPAP.Prereqs.LpNorm.Compact.Inner import LeanAPAP.Prereqs.LpNorm.Discrete.Basic import LeanAPAP.Prereqs.LpNorm.Discrete.Defs import LeanAPAP.Prereqs.LpNorm.Discrete.Inner diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean index cd8f961d45..fc529b49fa 100644 --- a/LeanAPAP/FiniteField/Basic.lean +++ b/LeanAPAP/FiniteField/Basic.lean @@ -33,14 +33,14 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ) _ ≤ _ := div_le_div_of_nonneg_right hAC (card G).cast_nonneg _ = |⟪balance (μ A) ∗ balance (μ A), μ C⟫_[ℝ]| := ?_ _ ≤ ‖balance (μ_[ℝ] A) ∗ balance (μ A)‖_[p] * ‖μ_[ℝ] C‖_[NNReal.conjExponent p] := - abs_l2Inner_le_dLpNorm_mul_dLpNorm hp'' _ _ + abs_dL2Inner_le_dLpNorm_mul_dLpNorm hp'' _ _ _ ≤ ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[p] * (card G ^ (-(p : ℝ)⁻¹) * γ ^ (-(p : ℝ)⁻¹)) := mul_le_mul (dLpNorm_conv_le_dLpNorm_dconv' (by positivity) (even_two_mul _) _) ?_ (by positivity) (by positivity) _ = ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[↑(2 * ⌈γ.curlog⌉₊), const _ (card G)⁻¹] * γ ^ (-(p : ℝ)⁻¹) := ?_ _ ≤ _ := mul_le_mul_of_nonneg_left ?_ $ by positivity - · rw [← balance_conv, balance, l2Inner_sub_left, l2Inner_const_left, expect_conv, sum_mu ℝ hA, + · rw [← balance_conv, balance, dL2Inner_sub_left, dL2Inner_const_left, expect_conv, sum_mu ℝ hA, expect_mu ℝ hA, sum_mu ℝ hC, conj_trivial, one_mul, mul_one, ← mul_inv_cancel₀, ← mul_sub, abs_mul, abs_of_nonneg, mul_div_cancel_left₀] <;> positivity · rw [dLpNorm_mu hp''.symm.one_le hC, hp''.symm.coe.inv_sub_one, NNReal.coe_natCast, ← mul_rpow] @@ -88,7 +88,7 @@ lemma ap_in_ff (hS : S.Nonempty) (hα₀ : 0 < α) (hε₀ : 0 < ε) (hε₁ : calc _ = ⟪μ V', μ A₁ ∗ μ A₂ ○ 𝟭 S⟫_[ℝ] := by sorry - -- rw [conv_assoc, conv_l2Inner, ← conj_l2Inner] + -- rw [conv_assoc, conv_dL2Inner, ← conj_dL2Inner] -- simp _ = _ := sorry @@ -209,7 +209,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty) _ ≤ 2 := by norm_num · positivity all_goals positivity - rw [hB.l2Inner_mu_conv_mu_mu_two_smul_mu] at hBV + rw [hB.dL2Inner_mu_conv_mu_mu_two_smul_mu] at hBV suffices h : (q ^ (n - 65 * curlog α ^ 9) : ℝ) ≤ q ^ (n / 2) by rw [rpow_le_rpow_left_iff ‹_›, sub_le_comm, sub_half, div_le_iff₀' zero_lt_two, ← mul_assoc] at h norm_num at h diff --git a/LeanAPAP/Mathlib/Algebra/Algebra/Rat.lean b/LeanAPAP/Mathlib/Algebra/Algebra/Rat.lean new file mode 100644 index 0000000000..73291f6f08 --- /dev/null +++ b/LeanAPAP/Mathlib/Algebra/Algebra/Rat.lean @@ -0,0 +1,19 @@ +import Mathlib.Algebra.Algebra.Rat + +variable {α : Type*} + +instance [Semiring α] [Module ℚ≥0 α] : SMulCommClass ℚ≥0 α α where + smul_comm q a b := sorry + +instance [Semiring α] [Module ℚ≥0 α] : SMulCommClass α ℚ≥0 α := .symm .. + +instance [Semiring α] [Module ℚ≥0 α] : IsScalarTower ℚ≥0 α α where + smul_assoc q a b := sorry + +instance [Ring α] [Module ℚ α] : SMulCommClass ℚ α α where + smul_comm q a b := sorry + +instance [Ring α] [Module ℚ α] : SMulCommClass α ℚ α := .symm .. + +instance [Ring α] [Module ℚ α] : IsScalarTower ℚ α α where + smul_assoc q a b := sorry diff --git a/LeanAPAP/Mathlib/Algebra/Star/Basic.lean b/LeanAPAP/Mathlib/Algebra/Star/Basic.lean new file mode 100644 index 0000000000..2c54b306b2 --- /dev/null +++ b/LeanAPAP/Mathlib/Algebra/Star/Basic.lean @@ -0,0 +1,12 @@ +import Mathlib.Algebra.Star.Basic + +/-! +# TODO + +Swap arguments to `star_nsmul`/`star_zsmul` +-/ + +variable {α : Type*} + +instance StarAddMonoid.toStarModuleInt [AddCommGroup α] [StarAddMonoid α] : StarModule ℤ α where + star_smul _ _ := star_zsmul _ _ diff --git a/LeanAPAP/Mathlib/Algebra/Star/Rat.lean b/LeanAPAP/Mathlib/Algebra/Star/Rat.lean new file mode 100644 index 0000000000..cb9e712090 --- /dev/null +++ b/LeanAPAP/Mathlib/Algebra/Star/Rat.lean @@ -0,0 +1,16 @@ +import Mathlib.Algebra.Module.Defs +import Mathlib.Algebra.Star.Rat + +variable {α : Type*} + +@[simp] lemma star_nnqsmul [AddCommMonoid α] [Module ℚ≥0 α] [StarAddMonoid α] (q : ℚ≥0) (a : α) : + star (q • a) = q • star a := sorry + +@[simp] lemma star_qsmul [AddCommGroup α] [Module ℚ α] [StarAddMonoid α] (q : ℚ) (a : α) : + star (q • a) = q • star a := sorry + +instance StarAddMonoid.toStarModuleNNRat [AddCommMonoid α] [Module ℚ≥0 α] [StarAddMonoid α] : + StarModule ℚ≥0 α where star_smul := star_nnqsmul + +instance StarAddMonoid.toStarModuleRat [AddCommGroup α] [Module ℚ α] [StarAddMonoid α] : + StarModule ℚ α where star_smul := star_qsmul diff --git a/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean b/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean new file mode 100644 index 0000000000..f2b432f493 --- /dev/null +++ b/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean @@ -0,0 +1,13 @@ +import Mathlib.Probability.ConditionalProbability + +open ENNReal MeasureTheory MeasureTheory.Measure MeasurableSpace Set + +variable {Ω Ω' α : Type*} {m : MeasurableSpace Ω} {m' : MeasurableSpace Ω'} (μ : Measure Ω) + {s t : Set Ω} + +namespace ProbabilityTheory + +@[simp] lemma cond_apply_self (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) : μ[|s] s = 1 := by + simpa [cond] using ENNReal.inv_mul_cancel hs₀ hs + +end ProbabilityTheory diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean index f25a43a371..2385a88286 100644 --- a/LeanAPAP/Physics/DRC.lean +++ b/LeanAPAP/Physics/DRC.lean @@ -19,7 +19,7 @@ private lemma lemma_0 (p : ℕ) (B₁ B₂ A : Finset G) (f : G → ℝ) : ∑ s, ⟪𝟭_[ℝ] (B₁ ∩ c p A s) ○ 𝟭 (B₂ ∩ c p A s), f⟫_[ℝ] = (B₁.card * B₂.card) • ∑ x, (μ_[ℝ] B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x := by simp_rw [mul_assoc] - simp only [l2Inner_eq_sum, RCLike.conj_to_real, mul_sum, sum_mul, smul_sum, + simp only [dL2Inner_eq_sum, RCLike.conj_to_real, mul_sum, sum_mul, smul_sum, @sum_comm _ _ (Fin p → G), sum_dconv_mul, dconv_apply_sub, Fintype.sum_pow, map_indicate] congr with b₁ congr with b₂ @@ -82,7 +82,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ have hg : ∀ s, 0 ≤ g s := fun s ↦ by rw [hg_def]; dsimp; positivity have hgB : ∑ s, g s = B₁.card * B₂.card * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p := by have hAdconv : 0 ≤ 𝟭_[ℝ] A ○ 𝟭 A := dconv_nonneg indicate_nonneg indicate_nonneg - simpa only [wLpNorm_pow_eq_sum hp₀, l2Inner_eq_sum, sum_dconv, sum_indicate, Pi.one_apply, + simpa only [wLpNorm_pow_eq_sum hp₀, dL2Inner_eq_sum, sum_dconv, sum_indicate, Pi.one_apply, RCLike.inner_apply, RCLike.conj_to_real, norm_of_nonneg (hAdconv _), mul_one, nsmul_eq_mul, Nat.cast_mul, ← hg_def, NNReal.smul_def, NNReal.coe_dconv, NNReal.coe_comp_mu] using lemma_0 p B₁ B₂ A 1 @@ -93,7 +93,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ refine ⟨_, inter_subset_left (s₂ := c p A s), _, inter_subset_left (s₂ := c p A s), ?_⟩ simp only [indicate_apply, mem_filter, mem_univ, true_and_iff, boole_mul] at hs split_ifs at hs with h; swap - · simp only [zero_mul, l2Inner_eq_sum, Function.comp_apply, RCLike.inner_apply, + · simp only [zero_mul, dL2Inner_eq_sum, Function.comp_apply, RCLike.inner_apply, RCLike.conj_to_real] at hs have : 0 ≤ 𝟭_[ℝ] (A₁ s) ○ 𝟭 (A₂ s) := dconv_nonneg indicate_nonneg indicate_nonneg -- positivity @@ -107,7 +107,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ positivity refine ⟨(lt_of_mul_lt_mul_left (hs.trans_eq' ?_) $ hg s).le, this.trans $ mul_le_of_le_one_right ?_ $ div_le_one_of_le ?_ ?_, this.trans $ mul_le_of_le_one_left ?_ $ div_le_one_of_le ?_ ?_⟩ - · simp_rw [A₁, A₂, g, ← card_smul_mu, smul_dconv, dconv_smul, l2Inner_smul_left, star_trivial, + · simp_rw [A₁, A₂, g, ← card_smul_mu, smul_dconv, dconv_smul, dL2Inner_smul_left, star_trivial, nsmul_eq_mul, mul_assoc] any_goals positivity all_goals exact Nat.cast_le.2 $ card_mono inter_subset_left @@ -187,7 +187,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 calc _ = ∑ x in (s p ε B₁ B₂ A)ᶜ, (μ A₁ ○ μ A₂) x := ?_ _ = ⟪μ_[ℝ] A₁ ○ μ A₂, (↑) ∘ 𝟭_[ℝ≥0] ((s (↑p) ε B₁ B₂ A)ᶜ)⟫_[ℝ] := by - simp [l2Inner_eq_sum, -mem_compl, -mem_s, apply_ite NNReal.toReal, indicate_apply] + simp [dL2Inner_eq_sum, -mem_compl, -mem_s, apply_ite NNReal.toReal, indicate_apply] _ ≤ _ := (le_div_iff₀ $ dLpNorm_conv_pos hp₀.ne' hB hA).2 h _ ≤ _ := ?_ · simp_rw [sub_eq_iff_eq_add', sum_add_sum_compl, sum_dconv, map_mu] diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index d2ba97bd91..2f4bc6ed5f 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/LeanAPAP/Physics/Unbalancing.lean @@ -21,7 +21,7 @@ lemma pow_inner_nonneg' {f : G → ℂ} (hf : f = g ○ g) (hν : (↑) ∘ ν = ⟪f ^ k, (↑) ∘ ν⟫_[ℂ] = ∑ z : Fin k → G, (‖∑ x, (∏ i, conj (g (x + z i))) * h x‖ : ℂ) ^ 2 by rw [this] positivity - rw [hf, hν, l2Inner_eq_sum] + rw [hf, hν, dL2Inner_eq_sum] simp only [WithLp.equiv_symm_pi_apply, Pi.pow_apply, RCLike.inner_apply, map_pow] simp_rw [dconv_apply h, mul_sum] --TODO: Please make `conv` work here :( @@ -44,7 +44,7 @@ lemma pow_inner_nonneg' {f : G → ℂ} (hf : f = g ○ g) (hν : (↑) ∘ ν = lemma pow_inner_nonneg {f : G → ℝ} (hf : (↑) ∘ f = g ○ g) (hν : (↑) ∘ ν = h ○ h) (k : ℕ) : (0 : ℝ) ≤ ⟪(↑) ∘ ν, f ^ k⟫_[ℝ] := by sorry - -- simpa [← Complex.zero_le_real, starRingEnd_apply, l2Inner_eq_sum] + -- simpa [← Complex.zero_le_real, starRingEnd_apply, dL2Inner_eq_sum] -- using pow_inner_nonneg' hf hν k private lemma log_ε_pos (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) : 0 < log (3 / ε) := @@ -92,7 +92,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 refine sum_congr rfl fun i _ ↦ ?_ rw [← abs_of_nonneg ((Nat.Odd.sub_odd hp₁ odd_one).pow_nonneg $ f _), abs_pow, pow_sub_one_mul hp₁.pos.ne', NNReal.smul_def, smul_eq_mul] - · simp [l2Inner_eq_sum, ← sum_add_distrib, ← mul_add, ← pow_sub_one_mul hp₁.pos.ne' (f _), + · simp [dL2Inner_eq_sum, ← sum_add_distrib, ← mul_add, ← pow_sub_one_mul hp₁.pos.ne' (f _), mul_sum, mul_left_comm (2 : ℝ), add_abs_eq_two_nsmul_posPart] set P := univ.filter fun i ↦ 0 ≤ f i set T := univ.filter fun i ↦ 3 / 4 * ε ≤ f i diff --git a/LeanAPAP/Prereqs/AddChar/Basic.lean b/LeanAPAP/Prereqs/AddChar/Basic.lean index 2b1c2e810a..b55a3f0d00 100644 --- a/LeanAPAP/Prereqs/AddChar/Basic.lean +++ b/LeanAPAP/Prereqs/AddChar/Basic.lean @@ -15,8 +15,8 @@ variable [AddGroup G] section RCLike variable [RCLike R] -protected lemma l2Inner_self [Fintype G] (ψ : AddChar G R) : - ⟪(ψ : G → R), ψ⟫_[R] = Fintype.card G := l2Inner_self_of_norm_eq_one ψ.norm_apply +protected lemma dL2Inner_self [Fintype G] (ψ : AddChar G R) : + ⟪(ψ : G → R), ψ⟫_[R] = Fintype.card G := dL2Inner_self_of_norm_eq_one ψ.norm_apply end RCLike @@ -45,26 +45,26 @@ variable [AddCommGroup G] section RCLike variable [RCLike R] {ψ₁ ψ₂ : AddChar G R} -lemma l2Inner_eq [Fintype G] (ψ₁ ψ₂ : AddChar G R) : +lemma dL2Inner_eq [Fintype G] (ψ₁ ψ₂ : AddChar G R) : ⟪(ψ₁ : G → R), ψ₂⟫_[R] = if ψ₁ = ψ₂ then ↑(card G) else 0 := by split_ifs with h - · rw [h, AddChar.l2Inner_self] + · rw [h, AddChar.dL2Inner_self] have : ψ₁⁻¹ * ψ₂ ≠ 1 := by rwa [Ne, inv_mul_eq_one] - simp_rw [l2Inner_eq_sum, ← inv_apply_eq_conj] + simp_rw [dL2Inner_eq_sum, ← inv_apply_eq_conj] simpa [map_neg_eq_inv] using sum_eq_zero_iff_ne_zero.2 this -lemma l2Inner_eq_zero_iff_ne [Fintype G] : ⟪(ψ₁ : G → R), ψ₂⟫_[R] = 0 ↔ ψ₁ ≠ ψ₂ := by - rw [l2Inner_eq, Ne.ite_eq_right_iff (Nat.cast_ne_zero.2 Fintype.card_ne_zero)] +lemma dL2Inner_eq_zero_iff_ne [Fintype G] : ⟪(ψ₁ : G → R), ψ₂⟫_[R] = 0 ↔ ψ₁ ≠ ψ₂ := by + rw [dL2Inner_eq, Ne.ite_eq_right_iff (Nat.cast_ne_zero.2 Fintype.card_ne_zero)] -lemma l2Inner_eq_card_iff_eq [Fintype G] : ⟪(ψ₁ : G → R), ψ₂⟫_[R] = card G ↔ ψ₁ = ψ₂ := by - rw [l2Inner_eq, Ne.ite_eq_left_iff (Nat.cast_ne_zero.2 Fintype.card_ne_zero)] +lemma dL2Inner_eq_card_iff_eq [Fintype G] : ⟪(ψ₁ : G → R), ψ₂⟫_[R] = card G ↔ ψ₁ = ψ₂ := by + rw [dL2Inner_eq, Ne.ite_eq_left_iff (Nat.cast_ne_zero.2 Fintype.card_ne_zero)] variable (G R) protected lemma linearIndependent [Finite G] : LinearIndependent R ((⇑) : AddChar G R → G → R) := by cases nonempty_fintype G - exact linearIndependent_of_ne_zero_of_l2Inner_eq_zero AddChar.coe_ne_zero fun ψ₁ ψ₂ ↦ - l2Inner_eq_zero_iff_ne.2 + exact linearIndependent_of_ne_zero_of_dL2Inner_eq_zero AddChar.coe_ne_zero fun ψ₁ ψ₂ ↦ + dL2Inner_eq_zero_iff_ne.2 noncomputable instance instFintype [Finite G] : Fintype (AddChar G R) := @Fintype.ofFinite _ (AddChar.linearIndependent G R).finite diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean index 75ac95f569..a83047eb38 100644 --- a/LeanAPAP/Prereqs/Chang.lean +++ b/LeanAPAP/Prereqs/Chang.lean @@ -48,7 +48,7 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x rotate_left · rw [← nsmul_eq_mul'] exact card_nsmul_le_sum _ _ _ fun x hx ↦ mem_largeSpec.1 $ hΔ hx - · simp_rw [mul_sum, mul_comm (f _), mul_assoc (c _), @sum_comm _ _ G, ← mul_sum, ← l2Inner_eq_sum, + · simp_rw [mul_sum, mul_comm (f _), mul_assoc (c _), @sum_comm _ _ G, ← mul_sum, ← dL2Inner_eq_sum, ← dft_apply, ← hc, ← RCLike.ofReal_sum, RCLike.norm_ofReal] exact le_abs_self _ · norm_cast @@ -88,7 +88,7 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x (norm_sum_le _ _).trans $ sum_le_sum fun _ _ ↦ norm_sum_le _ _ _ = _ := by simp [energy, norm_c, -Complex.norm_eq_abs, norm_prod] · push_cast - simp_rw [← RCLike.conj_mul, dft_apply, l2Inner_eq_sum, map_sum, map_mul, RCLike.conj_conj, + simp_rw [← RCLike.conj_mul, dft_apply, dL2Inner_eq_sum, map_sum, map_mul, RCLike.conj_conj, mul_pow, sum_pow', sum_mul, mul_sum, @sum_comm _ _ G, ← AddChar.inv_apply_eq_conj, ← AddChar.neg_apply', prod_mul_prod_comm, ← AddChar.add_apply, ← AddChar.sum_apply, mul_left_comm (Algebra.cast (ν _ : ℝ) : ℂ), ← mul_sum, ← sub_eq_add_neg, sum_sub_distrib, @@ -134,7 +134,7 @@ lemma AddDissociated.boringEnergy_le [DecidableEq G] {s : Finset G} rwa [cft_dft, support_comp_eq_preimage, support_indicate, Set.preimage_comp, Set.neg_preimage, addDissociated_neg, AddEquiv.addDissociated_preimage] _ = _ := by - simp_rw [mul_pow, pow_mul, ndL2Norm_dft_indicate] + simp_rw [mul_pow, pow_mul, cL2Norm_dft_indicate] rw [← exp_nsmul, sq_sqrt, sq_sqrt] simp_rw [← mul_pow] simp [changConst] diff --git a/LeanAPAP/Prereqs/Convolution/Norm.lean b/LeanAPAP/Prereqs/Convolution/Norm.lean index 81e5c3fd73..504bd6d527 100644 --- a/LeanAPAP/Prereqs/Convolution/Norm.lean +++ b/LeanAPAP/Prereqs/Convolution/Norm.lean @@ -1,6 +1,6 @@ import Mathlib.Data.Real.StarOrdered import LeanAPAP.Prereqs.Convolution.Order -import LeanAPAP.Prereqs.LpNorm.Compact +import LeanAPAP.Prereqs.LpNorm.Compact.Defs /-! # Norm of a convolution @@ -26,32 +26,32 @@ variable [RCLike β] · simp [nnLpNorm_exponent_zero] · simp [dLpNorm_eq_sum hp, apply_ite, hp] -lemma conv_eq_l2Inner (f g : α → β) (a : α) : (f ∗ g) a = ⟪conj f, τ a fun x ↦ g (-x)⟫_[β] := by - simp [l2Inner_eq_sum, conv_eq_sum_sub', map_sum] +lemma conv_eq_dL2Inner (f g : α → β) (a : α) : (f ∗ g) a = ⟪conj f, τ a fun x ↦ g (-x)⟫_[β] := by + simp [dL2Inner_eq_sum, conv_eq_sum_sub', map_sum] -lemma dconv_eq_l2Inner (f g : α → β) (a : α) : (f ○ g) a = conj ⟪f, τ a g⟫_[β] := by - simp [l2Inner_eq_sum, dconv_eq_sum_sub', map_sum] +lemma dconv_eq_dL2Inner (f g : α → β) (a : α) : (f ○ g) a = conj ⟪f, τ a g⟫_[β] := by + simp [dL2Inner_eq_sum, dconv_eq_sum_sub', map_sum] -lemma l2Inner_dconv (f g h : α → β) : ⟪f, g ○ h⟫_[β] = ⟪conj g, conj f ∗ conj h⟫_[β] := by +lemma dL2Inner_dconv (f g h : α → β) : ⟪f, g ○ h⟫_[β] = ⟪conj g, conj f ∗ conj h⟫_[β] := by calc _ = ∑ b, ∑ a, g a * conj (h b) * conj (f (a - b)) := by - simp_rw [l2Inner, mul_comm _ ((_ ○ _) _), sum_dconv_mul]; exact sum_comm + simp_rw [dL2Inner, mul_comm _ ((_ ○ _) _), sum_dconv_mul]; exact sum_comm _ = ∑ b, ∑ a, conj (f a) * conj (h b) * g (a + b) := by simp_rw [← Fintype.sum_prod_type'] exact Fintype.sum_equiv ((Equiv.refl _).prodShear Equiv.subRight) _ _ (by simp [mul_rotate, mul_right_comm]) _ = _ := by - simp_rw [l2Inner, mul_comm _ ((_ ∗ _) _), sum_conv_mul, Pi.conj_apply, RCLike.conj_conj] + simp_rw [dL2Inner, mul_comm _ ((_ ∗ _) _), sum_conv_mul, Pi.conj_apply, RCLike.conj_conj] exact sum_comm -lemma l2Inner_conv (f g h : α → β) : ⟪f, g ∗ h⟫_[β] = ⟪conj g, conj f ○ conj h⟫_[β] := by - simp_rw [l2Inner_dconv, RCLike.conj_conj] +lemma dL2Inner_conv (f g h : α → β) : ⟪f, g ∗ h⟫_[β] = ⟪conj g, conj f ○ conj h⟫_[β] := by + simp_rw [dL2Inner_dconv, RCLike.conj_conj] -lemma dconv_l2Inner (f g h : α → β) : ⟪f ○ g, h⟫_[β] = ⟪conj h ∗ conj g, conj f⟫_[β] := by - rw [l2Inner_anticomm, l2Inner_anticomm (_ ∗ _), conj_dconv, l2Inner_dconv]; simp +lemma dconv_dL2Inner (f g h : α → β) : ⟪f ○ g, h⟫_[β] = ⟪conj h ∗ conj g, conj f⟫_[β] := by + rw [dL2Inner_anticomm, dL2Inner_anticomm (_ ∗ _), conj_dconv, dL2Inner_dconv]; simp -lemma conv_l2Inner (f g h : α → β) : ⟪f ∗ g, h⟫_[β] = ⟪conj h ○ conj g, conj f⟫_[β] := by - rw [l2Inner_anticomm, l2Inner_anticomm (_ ○ _), conj_conv, l2Inner_conv]; simp +lemma conv_dL2Inner (f g h : α → β) : ⟪f ∗ g, h⟫_[β] = ⟪conj h ○ conj g, conj f⟫_[β] := by + rw [dL2Inner_anticomm, dL2Inner_anticomm (_ ○ _), conj_conv, dL2Inner_conv]; simp -- TODO: This proof would feel much less painful if we had `ℝ≥0`-valued Lp-norms. /-- A special case of **Young's convolution inequality**. -/ diff --git a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean index d7d29814f8..a6c9ebd369 100644 --- a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean +++ b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean @@ -10,12 +10,12 @@ open scoped Pointwise variable {G : Type*} [AddCommGroup G] [DecidableEq G] [Fintype G] {s : Finset G} -lemma ThreeAPFree.l2Inner_mu_conv_mu_mu_two_smul_mu (hG : Odd (card G)) +lemma ThreeAPFree.dL2Inner_mu_conv_mu_mu_two_smul_mu (hG : Odd (card G)) (hs : ThreeAPFree (s : Set G)) : ⟪μ s ∗ μ s, μ (s.image (2 • ·))⟫_[ℝ] = (s.card ^ 2 : ℝ)⁻¹ := by obtain rfl | hs' := s.eq_empty_or_nonempty · simp - simp only [l2Inner_eq_sum, sum_conv_mul, ← sum_product', RCLike.conj_to_real] + simp only [dL2Inner_eq_sum, sum_conv_mul, ← sum_product', RCLike.conj_to_real] rw [← diag_union_offDiag univ, sum_union (disjoint_diag_offDiag _), sum_diag, ← sum_add_sum_compl s, @sum_eq_card_nsmul _ _ _ _ _ (s.card ^ 3 : ℝ)⁻¹, nsmul_eq_mul, Finset.sum_eq_zero, Finset.sum_eq_zero, add_zero, add_zero, pow_succ', mul_inv, diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean index 97dbaca5e0..a468c085a2 100644 --- a/LeanAPAP/Prereqs/Energy.lean +++ b/LeanAPAP/Prereqs/Energy.lean @@ -51,18 +51,18 @@ lemma cLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) : refine Complex.ofReal_injective ?_ calc _ = ⟪dft (𝟭 s ∗^ n), dft (𝟭 s ∗^ n)⟫ₙ_[ℂ] := ?_ - _ = ⟪𝟭 s ∗^ n, 𝟭 s ∗^ n⟫_[ℂ] := nl2Inner_dft _ _ + _ = ⟪𝟭 s ∗^ n, 𝟭 s ∗^ n⟫_[ℂ] := ndL2Inner_dft _ _ _ = _ := ?_ · rw [cLpNorm_pow_eq_expect] simp_rw [pow_mul', ← norm_pow _ n, Complex.ofReal_expect, Complex.ofReal_pow, - ← Complex.conj_mul', nl2Inner_eq_expect, dft_iterConv_apply] + ← Complex.conj_mul', ndL2Inner_eq_expect, dft_iterConv_apply] positivity - · simp only [l2Inner_eq_sum, boringEnergy_eq, Complex.ofReal_mul, Complex.ofReal_natCast, + · simp only [dL2Inner_eq_sum, boringEnergy_eq, Complex.ofReal_mul, Complex.ofReal_natCast, Complex.ofReal_sum, Complex.ofReal_pow, mul_eq_mul_left_iff, Nat.cast_eq_zero, Fintype.card_ne_zero, or_false, sq, (((indicate_isSelfAdjoint _).iterConv _).apply _).conj_eq, Complex.coe_iterConv, Complex.ofReal_comp_indicate] -lemma ndL2Norm_dft_indicate (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[2] = sqrt s.card := by +lemma cL2Norm_dft_indicate (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[2] = sqrt s.card := by rw [eq_comm, sqrt_eq_iff_sq_eq] simpa using cLpNorm_dft_indicate_pow 1 s all_goals positivity diff --git a/LeanAPAP/Prereqs/FourierTransform/Compact.lean b/LeanAPAP/Prereqs/FourierTransform/Compact.lean index 690ed1cf36..a94a5f1fb1 100644 --- a/LeanAPAP/Prereqs/FourierTransform/Compact.lean +++ b/LeanAPAP/Prereqs/FourierTransform/Compact.lean @@ -25,28 +25,28 @@ lemma cft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : cft f ψ = ⟪ψ, f⟫ @[simp] lemma cft_zero : cft (0 : α → ℂ) = 0 := by ext; simp [cft_apply] @[simp] lemma cft_add (f g : α → ℂ) : cft (f + g) = cft f + cft g := by - ext; simp [nl2Inner_add_right, cft_apply] + ext; simp [ndL2Inner_add_right, cft_apply] @[simp] lemma cft_neg (f : α → ℂ) : cft (-f) = - cft f := by ext; simp [cft_apply] @[simp] lemma cft_sub (f g : α → ℂ) : cft (f - g) = cft f - cft g := by - ext; simp [nl2Inner_sub_right, cft_apply] + ext; simp [ndL2Inner_sub_right, cft_apply] @[simp] lemma cft_const (a : ℂ) (hψ : ψ ≠ 0) : cft (const α a) ψ = 0 := by - simp only [cft_apply, nl2Inner_eq_expect, const_apply, ← expect_mul, ← map_expect, + simp only [cft_apply, ndL2Inner_eq_expect, const_apply, ← expect_mul, ← map_expect, expect_eq_zero_iff_ne_zero.2 hψ, map_zero, zero_mul] @[simp] lemma cft_smul [DistribSMul γ ℂ] [Star γ] [StarModule γ ℂ] [IsScalarTower γ ℂ ℂ] [SMulCommClass γ ℂ ℂ] (c : γ) (f : α → ℂ) : cft (c • f) = c • cft f := by have := SMulCommClass.symm γ ℂ ℂ ext - simp [nl2Inner_smul_right, cft_apply] + simp [ndL2Inner_smul_right, cft_apply] /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/ -@[simp] lemma l2Inner_cft (f g : α → ℂ) : ⟪cft f, cft g⟫_[ℂ] = ⟪f, g⟫ₙ_[ℂ] := by +@[simp] lemma dL2Inner_cft (f g : α → ℂ) : ⟪cft f, cft g⟫_[ℂ] = ⟪f, g⟫ₙ_[ℂ] := by classical unfold cft - simp_rw [l2Inner_eq_sum, nl2Inner_eq_expect, map_expect, map_mul, starRingEnd_self_apply, + simp_rw [dL2Inner_eq_sum, ndL2Inner_eq_expect, map_expect, map_mul, starRingEnd_self_apply, expect_mul, mul_expect, ← expect_sum_comm, mul_mul_mul_comm _ (conj $ f _), ← sum_mul, ← AddChar.inv_apply_eq_conj, ← map_neg_eq_inv, ← map_add_eq_mul, AddChar.sum_apply_eq_ite] simp [add_neg_eq_zero, card_univ, Fintype.card_ne_zero, NNRat.smul_def (α := ℂ)] @@ -54,21 +54,21 @@ lemma cft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : cft f ψ = ⟪ψ, f⟫ /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/ @[simp] lemma dL2Norm_cft (f : α → ℂ) : ‖cft f‖_[2] = ‖f‖ₙ_[2] := (sq_eq_sq nnLpNorm_nonneg cLpNorm_nonneg).1 $ Complex.ofReal_injective $ by - push_cast; simpa only [nl2Inner_self, l2Inner_self] using l2Inner_cft f f + push_cast; simpa only [ndL2Inner_self, dL2Inner_self] using dL2Inner_cft f f /-- **Fourier inversion** for the discrete Fourier transform. -/ lemma cft_inversion (f : α → ℂ) (a : α) : ∑ ψ, cft f ψ * ψ a = f a := by - classical simp_rw [cft, nl2Inner_eq_expect, expect_mul, ← expect_sum_comm, mul_right_comm _ (f _), + classical simp_rw [cft, ndL2Inner_eq_expect, expect_mul, ← expect_sum_comm, mul_right_comm _ (f _), ← sum_mul, ← AddChar.inv_apply_eq_conj, inv_mul_eq_div, ← map_sub_eq_div, AddChar.sum_apply_eq_ite, sub_eq_zero, ite_mul, zero_mul, Fintype.expect_ite_eq] simp [add_neg_eq_zero, card_univ, NNRat.smul_def (α := ℂ), Fintype.card_ne_zero] lemma dft_cft_doubleDualEmb (f : α → ℂ) (a : α) : dft (cft f) (doubleDualEmb a) = f (-a) := by - simp only [← cft_inversion f (-a), mul_comm (conj _), dft_apply, l2Inner_eq_sum, map_neg_eq_inv, + simp only [← cft_inversion f (-a), mul_comm (conj _), dft_apply, dL2Inner_eq_sum, map_neg_eq_inv, AddChar.inv_apply_eq_conj, doubleDualEmb_apply] lemma cft_dft_doubleDualEmb (f : α → ℂ) (a : α) : cft (dft f) (doubleDualEmb a) = f (-a) := by - simp only [← dft_inversion f (-a), mul_comm (conj _), cft_apply, nl2Inner_eq_expect, + simp only [← dft_inversion f (-a), mul_comm (conj _), cft_apply, ndL2Inner_eq_expect, map_neg_eq_inv, AddChar.inv_apply_eq_conj, doubleDualEmb_apply] lemma dft_cft (f : α → ℂ) : dft (cft f) = f ∘ doubleDualEquiv.symm ∘ Neg.neg := @@ -83,16 +83,16 @@ lemma cft_injective : Injective (cft : (α → ℂ) → AddChar α ℂ → ℂ) funext fun a ↦ (cft_inversion _ _).symm.trans $ by rw [h, cft_inversion] lemma cft_inv (ψ : AddChar α ℂ) (hf : IsSelfAdjoint f) : cft f ψ⁻¹ = conj (cft f ψ) := by - simp_rw [cft_apply, nl2Inner_eq_expect, map_expect, AddChar.inv_apply', map_mul, + simp_rw [cft_apply, ndL2Inner_eq_expect, map_expect, AddChar.inv_apply', map_mul, AddChar.inv_apply_eq_conj, Complex.conj_conj, (hf.apply _).conj_eq] @[simp] lemma cft_conj (f : α → ℂ) (ψ : AddChar α ℂ) : cft (conj f) ψ = conj (cft f ψ⁻¹) := by - simp only [cft_apply, nl2Inner_eq_expect, map_expect, map_mul, ← inv_apply', ← inv_apply_eq_conj, + simp only [cft_apply, ndL2Inner_eq_expect, map_expect, map_mul, ← inv_apply', ← inv_apply_eq_conj, inv_inv, Pi.conj_apply] lemma cft_conjneg_apply (f : α → ℂ) (ψ : AddChar α ℂ) : cft (conjneg f) ψ = conj (cft f ψ) := by - simp only [cft_apply, nl2Inner_eq_expect, conjneg_apply, map_expect, map_mul, RCLike.conj_conj] + simp only [cft_apply, ndL2Inner_eq_expect, conjneg_apply, map_expect, map_mul, RCLike.conj_conj] refine Fintype.expect_equiv (Equiv.neg _) _ _ fun i ↦ ?_ simp only [Equiv.neg_apply, ← inv_apply_eq_conj, ← inv_apply', inv_apply] @@ -104,14 +104,14 @@ lemma cft_conjneg (f : α → ℂ) : cft (conjneg f) = conj (cft f) := funext $ lemma cft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime n) : cft (dilate f n) ψ = cft f (ψ ^ n) := by - simp_rw [cft_apply, nl2Inner_eq_expect, dilate] + simp_rw [cft_apply, ndL2Inner_eq_expect, dilate] rw [← Nat.card_eq_fintype_card] at hn refine (Fintype.expect_bijective _ hn.nsmul_right_bijective _ _ ?_).symm simp only [pow_apply, ← map_nsmul_eq_pow, zmod_val_inv_nsmul_nsmul hn, forall_const] @[simp] lemma cft_trivNChar [DecidableEq α] : cft (trivNChar : α → ℂ) = 1 := by ext - simp [trivChar_apply, cft_apply, nl2Inner_eq_expect, ← map_expect, card_univ, + simp [trivChar_apply, cft_apply, ndL2Inner_eq_expect, ← map_expect, card_univ, NNRat.smul_def (α := ℂ)] @[simp] lemma cft_one : cft (1 : α → ℂ) = trivChar := @@ -120,12 +120,12 @@ lemma cft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime variable [DecidableEq α] @[simp] lemma cft_indicate_zero (s : Finset α) : cft (𝟭 s) 0 = s.dens := by - simp only [cft_apply, nl2Inner_eq_expect, expect_indicate, AddChar.zero_apply, map_one, one_mul, + simp only [cft_apply, ndL2Inner_eq_expect, expect_indicate, AddChar.zero_apply, map_one, one_mul, dens, NNRat.smul_def (α := ℂ), div_eq_inv_mul] simp lemma cft_nconv_apply (f g : α → ℂ) (ψ : AddChar α ℂ) : cft (f ∗ₙ g) ψ = cft f ψ * cft g ψ := by - simp_rw [cft, nl2Inner_eq_expect, nconv_eq_expect_sub', mul_expect, expect_mul, ← expect_product', + simp_rw [cft, ndL2Inner_eq_expect, nconv_eq_expect_sub', mul_expect, expect_mul, ← expect_product', univ_product_univ] refine Fintype.expect_equiv ((Equiv.prodComm _ _).trans $ ((Equiv.refl _).prodShear Equiv.subRight).trans $ Equiv.prodComm _ _) _ _ fun (a, b) ↦ ?_ diff --git a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean index f7bb0387a1..3f63476493 100644 --- a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean +++ b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean @@ -1,5 +1,6 @@ import LeanAPAP.Prereqs.AddChar.PontryaginDuality -import LeanAPAP.Prereqs.LpNorm.Compact +import LeanAPAP.Prereqs.LpNorm.Compact.Inner +import LeanAPAP.Prereqs.LpNorm.Discrete.Inner import LeanAPAP.Prereqs.Convolution.Discrete.Defs /-! @@ -9,7 +10,7 @@ This file defines the discrete Fourier transform and shows the Parseval-Plancher Fourier inversion formula for it. -/ -open AddChar Finset Function +open AddChar Finset Function MeasureTheory open Fintype (card) open scoped BigOperators ComplexConjugate ComplexOrder @@ -23,37 +24,37 @@ lemma dft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : dft f ψ = ⟪ψ, f⟫_ @[simp] lemma dft_zero : dft (0 : α → ℂ) = 0 := by ext; simp [dft_apply] @[simp] lemma dft_add (f g : α → ℂ) : dft (f + g) = dft f + dft g := by - ext; simp [l2Inner_add_right, dft_apply] + ext; simp [dL2Inner_add_right, dft_apply] @[simp] lemma dft_neg (f : α → ℂ) : dft (-f) = - dft f := by ext; simp [dft_apply] @[simp] lemma dft_sub (f g : α → ℂ) : dft (f - g) = dft f - dft g := by - ext; simp [l2Inner_sub_right, dft_apply] + ext; simp [dL2Inner_sub_right, dft_apply] @[simp] lemma dft_const (a : ℂ) (hψ : ψ ≠ 0) : dft (const α a) ψ = 0 := by - simp only [dft_apply, l2Inner_eq_sum, const_apply, ← sum_mul, ← map_sum, + simp only [dft_apply, dL2Inner_eq_sum, const_apply, ← sum_mul, ← map_sum, sum_eq_zero_iff_ne_zero.2 hψ, map_zero, zero_mul] @[simp] lemma dft_smul [DistribSMul γ ℂ] [Star γ] [StarModule γ ℂ] [SMulCommClass γ ℂ ℂ] (c : γ) - (f : α → ℂ) : dft (c • f) = c • dft f := by ext; simp [l2Inner_smul_right, dft_apply] + (f : α → ℂ) : dft (c • f) = c • dft f := by ext; simp [dL2Inner_smul_right, dft_apply] /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/ -@[simp] lemma nl2Inner_dft (f g : α → ℂ) : ⟪dft f, dft g⟫ₙ_[ℂ] = ⟪f, g⟫_[ℂ] := by +@[simp] lemma ndL2Inner_dft (f g : α → ℂ) : ⟪dft f, dft g⟫ₙ_[ℂ] = ⟪f, g⟫_[ℂ] := by classical unfold dft - simp_rw [l2Inner_eq_sum, nl2Inner_eq_expect, map_sum, map_mul, starRingEnd_self_apply, sum_mul, + simp_rw [dL2Inner_eq_sum, ndL2Inner_eq_expect, map_sum, map_mul, starRingEnd_self_apply, sum_mul, mul_sum, expect_sum_comm, mul_mul_mul_comm _ (conj $ f _), ← expect_mul, ← AddChar.inv_apply_eq_conj, ← map_neg_eq_inv, ← map_add_eq_mul, AddChar.expect_apply_eq_ite, add_neg_eq_zero, boole_mul, Fintype.sum_ite_eq] /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/ -@[simp] lemma ndL2Norm_dft (f : α → ℂ) : ‖dft f‖ₙ_[2] = ‖f‖_[2] := +@[simp] lemma cL2Norm_dft (f : α → ℂ) : ‖dft f‖ₙ_[2] = ‖f‖_[2] := (sq_eq_sq cLpNorm_nonneg nnLpNorm_nonneg).1 $ Complex.ofReal_injective $ by - push_cast; simpa only [nl2Inner_self, l2Inner_self] using nl2Inner_dft f f + push_cast; simpa only [ndL2Inner_self, dL2Inner_self] using ndL2Inner_dft f f /-- **Fourier inversion** for the discrete Fourier transform. -/ lemma dft_inversion (f : α → ℂ) (a : α) : 𝔼 ψ, dft f ψ * ψ a = f a := by - classical simp_rw [dft, l2Inner_eq_sum, sum_mul, expect_sum_comm, mul_right_comm _ (f _), + classical simp_rw [dft, dL2Inner_eq_sum, sum_mul, expect_sum_comm, mul_right_comm _ (f _), ← expect_mul, ← AddChar.inv_apply_eq_conj, inv_mul_eq_div, ← map_sub_eq_div, AddChar.expect_apply_eq_ite, sub_eq_zero, boole_mul, Fintype.sum_ite_eq] @@ -65,7 +66,7 @@ lemma dft_inversion' (f : α → ℂ) (a : α) : ∑ ψ : AddChar α ℂ, dft f lemma dft_dft_doubleDualEmb (f : α → ℂ) (a : α) : dft (dft f) (doubleDualEmb a) = card α * f (-a) := by - simp only [← dft_inversion f (-a), mul_comm (conj _), dft_apply, l2Inner_eq_sum, map_neg_eq_inv, + simp only [← dft_inversion f (-a), mul_comm (conj _), dft_apply, dL2Inner_eq_sum, map_neg_eq_inv, AddChar.inv_apply_eq_conj, doubleDualEmb_apply, ← Fintype.card_mul_expect, AddChar.card_eq] lemma dft_dft (f : α → ℂ) : dft (dft f) = card α * f ∘ doubleDualEquiv.symm ∘ Neg.neg := @@ -77,16 +78,16 @@ lemma dft_injective : Injective (dft : (α → ℂ) → AddChar α ℂ → ℂ) funext fun a ↦ (dft_inversion _ _).symm.trans $ by rw [h, dft_inversion] lemma dft_inv (ψ : AddChar α ℂ) (hf : IsSelfAdjoint f) : dft f ψ⁻¹ = conj (dft f ψ) := by - simp_rw [dft_apply, l2Inner_eq_sum, map_sum, AddChar.inv_apply', map_mul, + simp_rw [dft_apply, dL2Inner_eq_sum, map_sum, AddChar.inv_apply', map_mul, AddChar.inv_apply_eq_conj, Complex.conj_conj, (hf.apply _).conj_eq] @[simp] lemma dft_conj (f : α → ℂ) (ψ : AddChar α ℂ) : dft (conj f) ψ = conj (dft f ψ⁻¹) := by - simp only [dft_apply, l2Inner_eq_sum, map_sum, map_mul, ← inv_apply', ← inv_apply_eq_conj, + simp only [dft_apply, dL2Inner_eq_sum, map_sum, map_mul, ← inv_apply', ← inv_apply_eq_conj, inv_inv, Pi.conj_apply] lemma dft_conjneg_apply (f : α → ℂ) (ψ : AddChar α ℂ) : dft (conjneg f) ψ = conj (dft f ψ) := by - simp only [dft_apply, l2Inner_eq_sum, conjneg_apply, map_sum, map_mul, RCLike.conj_conj] + simp only [dft_apply, dL2Inner_eq_sum, conjneg_apply, map_sum, map_mul, RCLike.conj_conj] refine Fintype.sum_equiv (Equiv.neg α) _ _ fun i ↦ ?_ simp only [Equiv.neg_apply, ← inv_apply_eq_conj, ← inv_apply', inv_apply] @@ -98,13 +99,13 @@ lemma dft_conjneg (f : α → ℂ) : dft (conjneg f) = conj (dft f) := funext $ lemma dft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime n) : dft (dilate f n) ψ = dft f (ψ ^ n) := by - simp_rw [dft_apply, l2Inner_eq_sum, dilate] + simp_rw [dft_apply, dL2Inner_eq_sum, dilate] rw [← Nat.card_eq_fintype_card] at hn refine (Fintype.sum_bijective _ hn.nsmul_right_bijective _ _ ?_).symm simp only [pow_apply, ← map_nsmul_eq_pow, zmod_val_inv_nsmul_nsmul hn, forall_const] @[simp] lemma dft_trivChar [DecidableEq α] : dft (trivChar : α → ℂ) = 1 := by - ext; simp [trivChar_apply, dft_apply, l2Inner_eq_sum, ← map_sum] + ext; simp [trivChar_apply, dft_apply, dL2Inner_eq_sum, ← map_sum] @[simp] lemma dft_one : dft (1 : α → ℂ) = card α • trivChar := dft_injective $ by classical rw [dft_smul, dft_trivChar, dft_dft, Pi.one_comp, nsmul_eq_mul] @@ -112,10 +113,10 @@ lemma dft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime variable [DecidableEq α] @[simp] lemma dft_indicate_zero (A : Finset α) : dft (𝟭 A) 0 = A.card := by - simp only [dft_apply, l2Inner_eq_sum, sum_indicate, AddChar.zero_apply, map_one, one_mul] + simp only [dft_apply, dL2Inner_eq_sum, sum_indicate, AddChar.zero_apply, map_one, one_mul] lemma dft_conv_apply (f g : α → ℂ) (ψ : AddChar α ℂ) : dft (f ∗ g) ψ = dft f ψ * dft g ψ := by - simp_rw [dft, l2Inner_eq_sum, conv_eq_sum_sub', mul_sum, sum_mul, ← sum_product', + simp_rw [dft, dL2Inner_eq_sum, conv_eq_sum_sub', mul_sum, sum_mul, ← sum_product', univ_product_univ] refine Fintype.sum_equiv ((Equiv.prodComm _ _).trans $ ((Equiv.refl _).prodShear Equiv.subRight).trans $ Equiv.prodComm _ _) _ _ fun (a, b) ↦ ?_ diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean deleted file mode 100644 index 703203a7a4..0000000000 --- a/LeanAPAP/Prereqs/LpNorm/Compact.lean +++ /dev/null @@ -1,543 +0,0 @@ -import Mathlib.Data.Finset.Density -import LeanAPAP.Prereqs.LpNorm.Discrete.Basic -import LeanAPAP.Prereqs.LpNorm.Discrete.Inner - -/-! -# Normalised Lp norms --/ - -open Finset hiding card -open Function Real -open Fintype (card) -open scoped BigOperators ComplexConjugate ENNReal NNReal - -variable {α 𝕜 E : Type*} [Fintype α] [MeasurableSpace α] - -/-! ### Lp norm -/ - -namespace MeasureTheory -section NormedAddCommGroup -variable [NormedAddCommGroup E] {p q : ℝ≥0∞} {f g h : α → E} - -/-- The Lp norm of a function with the compact normalisation. -/ -noncomputable def cLpNorm (p : ℝ≥0∞) (f : α → E) : ℝ := nnLpNorm f p ((card α : ℝ≥0∞)⁻¹ • .count) - -notation "‖" f "‖ₙ_[" p "]" => cLpNorm p f - -lemma cLpNorm_eq_expect' (hp : p.toReal ≠ 0) (f : α → E) : - ‖f‖ₙ_[p] = (𝔼 i, ‖f i‖ ^ p.toReal) ^ p.toReal⁻¹ := by - rw [cLpNorm, dLpNorm_eq_sum', ← div_rpow, Fintype.expect_eq_sum_div_card (α := ℝ)] <;> positivity - -lemma cLpNorm_eq_expect'' {p : ℝ} (hp : 0 < p) (f : α → E) : - ‖f‖ₙ_[p.toNNReal] = (𝔼 i, ‖f i‖ ^ p) ^ p⁻¹ := by - rw [cLpNorm_eq_expect'] <;> simp [hp.ne', hp.le] - -lemma cLpNorm_eq_expect {p : ℝ≥0} (hp : p ≠ 0) (f : α → E) : - ‖f‖ₙ_[p] = (𝔼 i, ‖f i‖ ^ (p : ℝ)) ^ (p⁻¹ : ℝ) := cLpNorm_eq_expect' (by simpa using hp) _ - -lemma cLpNorm_rpow_eq_expect {p : ℝ≥0} (hp : p ≠ 0) (f : α → E) : - ‖f‖ₙ_[p] ^ (p : ℝ) = 𝔼 i, ‖f i‖ ^ (p : ℝ) := by - rw [cLpNorm_eq_expect hp, rpow_inv_rpow] <;> positivity - -lemma cLpNorm_pow_eq_expect {p : ℕ} (hp : p ≠ 0) (f : α → E) : - ‖f‖ₙ_[p] ^ p = 𝔼 i, ‖f i‖ ^ p := by - simpa using cLpNorm_rpow_eq_expect (Nat.cast_ne_zero.2 hp) f - -lemma ndL2Norm_sq_eq_expect (f : α → E) : ‖f‖ₙ_[2] ^ 2 = 𝔼 i, ‖f i‖ ^ 2 := by - simpa using cLpNorm_pow_eq_expect two_ne_zero _ - -lemma ndL2Norm_eq_expect (f : α → E) : ‖f‖ₙ_[2] = sqrt (𝔼 i, ‖f i‖ ^ 2) := by - simpa [sqrt_eq_rpow] using cLpNorm_eq_expect two_ne_zero _ - -lemma ndL1Norm_eq_expect (f : α → E) : ‖f‖ₙ_[1] = 𝔼 i, ‖f i‖ := by simp [cLpNorm_eq_expect'] - -lemma nnLpNorm_exponent_zero (f : α → E) : ‖f‖ₙ_[0] = {i | f i ≠ 0}.toFinite.toFinset.card := by - simp [nnLpNorm_exponent_zero, cLpNorm] - -lemma nlinftyNorm_eq_iSup (f : α → E) : ‖f‖ₙ_[∞] = ⨆ i, ‖f i‖ := by - simp [cLpNorm, dLinftyNorm_eq_iSup] - -@[simp] lemma nnnLpNorm_zero : ‖(0 : α → E)‖ₙ_[p] = 0 := by simp [cLpNorm] - -@[simp] lemma cLpNorm_of_isEmpty [IsEmpty α] (p : ℝ≥0∞) (f : α → E) : ‖f‖ₙ_[p] = 0 := by - simp [cLpNorm] - -@[simp] lemma cLpNorm_norm (p : ℝ≥0∞) (f : α → E) : ‖fun i ↦ ‖f i‖‖ₙ_[p] = ‖f‖ₙ_[p] := by - simp [cLpNorm] - -@[simp] lemma cLpNorm_neg (f : α → E) : ‖-f‖ₙ_[p] = ‖f‖ₙ_[p] := by simp [← cLpNorm_norm _ (-f)] - -lemma cLpNorm_sub_comm (f g : α → E) : ‖f - g‖ₙ_[p] = ‖g - f‖ₙ_[p] := by - simp [← cLpNorm_neg (f - g)] - -@[simp] lemma cLpNorm_nonneg : 0 ≤ ‖f‖ₙ_[p] := by unfold cLpNorm; positivity - -@[simp] lemma cLpNorm_eq_zero [Nonempty α] : ‖f‖ₙ_[p] = 0 ↔ f = 0 := by - obtain p | p := p - · simp [nlinftyNorm_eq_iSup, ENNReal.none_eq_top, ← sup'_univ_eq_ciSup, le_antisymm_iff, - Function.funext_iff] - obtain rfl | hp := eq_or_ne p 0 - · simp [nnLpNorm_exponent_zero, eq_empty_iff_forall_not_mem, Function.funext_iff] - · rw [← rpow_eq_zero cLpNorm_nonneg (NNReal.coe_ne_zero.2 hp)] - simp [cLpNorm_rpow_eq_expect hp, Fintype.expect_eq_zero_iff_of_nonneg, rpow_nonneg, - Function.funext_iff, rpow_eq_zero _ (NNReal.coe_ne_zero.2 hp), Pi.le_def] - -@[simp] lemma cLpNorm_pos [Nonempty α] : 0 < ‖f‖ₙ_[p] ↔ f ≠ 0 := - cLpNorm_nonneg.gt_iff_ne.trans cLpNorm_eq_zero.not - -lemma cLpNorm_mono_right (hpq : p ≤ q) (f : α → E) : ‖f‖ₙ_[p] ≤ ‖f‖ₙ_[q] := sorry - -section one_le - -lemma cLpNorm_add_le (hp : 1 ≤ p) (f g : α → E) : ‖f + g‖ₙ_[p] ≤ ‖f‖ₙ_[p] + ‖g‖ₙ_[p] := by - simp only [cLpNorm, ← add_div] - exact div_le_div_of_nonneg_right (dLpNorm_add_le hp _ _) (by positivity) - -lemma cLpNorm_sub_le (hp : 1 ≤ p) (f g : α → E) : ‖f - g‖ₙ_[p] ≤ ‖f‖ₙ_[p] + ‖g‖ₙ_[p] := by - simp only [cLpNorm, ← add_div] - exact div_le_div_of_nonneg_right (dLpNorm_sub_le hp _ _) (by positivity) - -lemma cLpNorm_le_cLpNorm_add_cLpNorm_sub' (hp : 1 ≤ p) (f g : α → E) : - ‖f‖ₙ_[p] ≤ ‖g‖ₙ_[p] + ‖f - g‖ₙ_[p] := by - simp only [cLpNorm, ← add_div] - exact div_le_div_of_nonneg_right (dLpNorm_le_dLpNorm_add_dLpNorm_sub' hp _ _) (by positivity) - -lemma cLpNorm_le_cLpNorm_add_cLpNorm_sub (hp : 1 ≤ p) (f g : α → E) : - ‖f‖ₙ_[p] ≤ ‖g‖ₙ_[p] + ‖g - f‖ₙ_[p] := by - simp only [cLpNorm, ← add_div] - exact div_le_div_of_nonneg_right (dLpNorm_le_dLpNorm_add_dLpNorm_sub hp _ _) (by positivity) - -lemma cLpNorm_le_add_cLpNorm_add (hp : 1 ≤ p) (f g : α → E) : - ‖f‖ₙ_[p] ≤ ‖f + g‖ₙ_[p] + ‖g‖ₙ_[p] := by - simp only [cLpNorm, ← add_div] - exact div_le_div_of_nonneg_right (dLpNorm_le_add_dLpNorm_add hp _ _) (by positivity) - -lemma cLpNorm_sub_le_cLpNorm_sub_add_cLpNorm_sub (hp : 1 ≤ p) (f g : α → E) : - ‖f - h‖ₙ_[p] ≤ ‖f - g‖ₙ_[p] + ‖g - h‖ₙ_[p] := by - simp only [cLpNorm, ← add_div] - exact div_le_div_of_nonneg_right (dLpNorm_sub_le_dLpNorm_sub_add_dLpNorm_sub hp _ _) (by positivity) - -variable [NormedField 𝕜] [∀ i, NormedSpace 𝕜 E] - --- TODO: `p ≠ 0` is enough -lemma cLpNorm_smul (hp : 1 ≤ p) (c : 𝕜) (f : α → E) : ‖c • f‖ₙ_[p] = ‖c‖ * ‖f‖ₙ_[p] := by - simp only [cLpNorm, mul_div_assoc, nnLpNorm_const_smul hp] - -variable [∀ i, NormedSpace ℝ E] - -lemma cLpNorm_nsmul (hp : 1 ≤ p) (n : ℕ) (f : α → E) : ‖n • f‖ₙ_[p] = n • ‖f‖ₙ_[p] := by - simp only [cLpNorm, nsmul_eq_mul, mul_div_assoc, dLpNorm_nsmul hp] - -end one_le -end NormedAddCommGroup - -section NormedAddCommGroup -variable {α : Type*} [NormedAddCommGroup α] {p : ℝ≥0∞} - -@[simp] -lemma cLpNorm_const [Nonempty α] (hp : p ≠ 0) (a : α) : ‖const α a‖ₙ_[p] = ‖a‖ := by - obtain _ | p := p - · simp [nlinftyNorm_eq_iSup] - have : (card α : ℝ) ^ (p : ℝ)⁻¹ ≠ 0 := by positivity - simp [cLpNorm, ENNReal.coe_ne_coe.1 hp, mul_div_cancel_left₀ _ this] - -end NormedAddCommGroup - -section RCLike -variable [RCLike 𝕜] {p : ℝ≥0∞} {f g : α → 𝕜} - -@[simp] lemma cLpNorm_one [Nonempty α] (hp : p ≠ 0) : ‖(1 : α → 𝕜)‖ₙ_[p] = 1 := - (cLpNorm_const hp 1).trans $ by simp - -lemma cLpNorm_natCast_mul (hp : 1 ≤ p) (n : ℕ) (f : α → 𝕜) : - ‖(n : α → 𝕜) * f‖ₙ_[p] = n * ‖f‖ₙ_[p] := by simpa only [nsmul_eq_mul] using cLpNorm_nsmul hp n f - -lemma cLpNorm_natCast_mul' (hp : 1 ≤ p) (n : ℕ) (f : α → 𝕜) : - ‖(n * f ·)‖ₙ_[p] = n * ‖f‖ₙ_[p] := cLpNorm_natCast_mul hp _ _ - -lemma cLpNorm_mul_natCast (hp : 1 ≤ p) (f : α → 𝕜) (n : ℕ) : - ‖f * (n : α → 𝕜)‖ₙ_[p] = ‖f‖ₙ_[p] * n := by - simpa only [mul_comm] using cLpNorm_natCast_mul hp n f - -lemma cLpNorm_mul_natCast' (hp : 1 ≤ p) (f : α → 𝕜) (n : ℕ) : - ‖(f · * n)‖ₙ_[p] = ‖f‖ₙ_[p] * n := cLpNorm_mul_natCast hp _ _ - -lemma cLpNorm_div_natCast' (hp : 1 ≤ p) (f : α → 𝕜) (n : ℕ) : - ‖(f · / n)‖ₙ_[p] = ‖f‖ₙ_[p] / n := by simp [cLpNorm, dLpNorm_div_natCast' hp, div_right_comm] - -lemma cLpNorm_div_natCast (hp : 1 ≤ p) (f : α → 𝕜) (n : ℕ) : - ‖f / (n : α → 𝕜)‖ₙ_[p] = ‖f‖ₙ_[p] / n := cLpNorm_div_natCast' hp _ _ - -end RCLike - -section Real -variable {p : ℝ≥0} {f g : α → ℝ} - -lemma cLpNorm_mono (hf : 0 ≤ f) (hfg : f ≤ g) : ‖f‖ₙ_[p] ≤ ‖g‖ₙ_[p] := - div_le_div_of_nonneg_right (dLpNorm_mono hf hfg) $ by positivity - -end Real - -/-! #### Inner product -/ - -section Semifield -variable [Semifield 𝕜] [CharZero 𝕜] [StarRing 𝕜] {γ : Type*} [DistribSMul γ 𝕜] - -/-- Inner product giving rise to the L2 norm with the compact normalisation. -/ -def nl2Inner (f g : α → 𝕜) : 𝕜 := 𝔼 i, conj (f i) * g i - -notation "⟪" f ", " g "⟫ₙ_[" 𝕜 "]" => @nl2Inner _ 𝕜 _ _ _ _ f g - -lemma nl2Inner_eq_expect (f g : α → 𝕜) : ⟪f, g⟫ₙ_[𝕜] = 𝔼 i, conj (f i) * g i := rfl -lemma nl2Inner_eq_l2Inner_div_card (f g : α → 𝕜) : ⟪f, g⟫ₙ_[𝕜] = ⟪f, g⟫_[𝕜] / card α := - Fintype.expect_eq_sum_div_card _ - -@[simp] lemma conj_nl2Inner (f g : α → 𝕜) : conj ⟪f, g⟫ₙ_[𝕜] = ⟪g, f⟫ₙ_[𝕜] := by - simp [nl2Inner_eq_expect, map_expect, mul_comm] - -@[simp] lemma nl2Inner_zero_left (g : α → 𝕜) : ⟪0, g⟫ₙ_[𝕜] = 0 := by simp [nl2Inner] -@[simp] lemma nl2Inner_zero_right (f : α → 𝕜) : ⟪f, 0⟫ₙ_[𝕜] = 0 := by simp [nl2Inner] - -@[simp] lemma nl2Inner_of_isEmpty [IsEmpty α] (f g : α → 𝕜) : ⟪f, g⟫ₙ_[𝕜] = 0 := by - simp [nl2Inner_eq_l2Inner_div_card] - -@[simp] lemma nl2Inner_const_left (a : 𝕜) (f : α → 𝕜) : - ⟪const _ a, f⟫ₙ_[𝕜] = conj a * 𝔼 x, f x := by - simp only [nl2Inner, const_apply, mul_expect] - -@[simp] -lemma nl2Inner_const_right (f : α → 𝕜) (a : 𝕜) : ⟪f, const _ a⟫ₙ_[𝕜] = (𝔼 x, conj (f x)) * a := by - simp only [nl2Inner, const_apply, expect_mul] - -lemma nl2Inner_add_left (f₁ f₂ g : α → 𝕜) : ⟪f₁ + f₂, g⟫ₙ_[𝕜] = ⟪f₁, g⟫ₙ_[𝕜] + ⟪f₂, g⟫ₙ_[𝕜] := by - simp_rw [nl2Inner, Pi.add_apply, map_add, add_mul, expect_add_distrib] - -lemma nl2Inner_add_right (f g₁ g₂ : α → 𝕜) : ⟪f, g₁ + g₂⟫ₙ_[𝕜] = ⟪f, g₁⟫ₙ_[𝕜] + ⟪f, g₂⟫ₙ_[𝕜] := by - simp_rw [nl2Inner, Pi.add_apply, mul_add, expect_add_distrib] - -lemma nl2Inner_smul_left [Star γ] [StarModule γ 𝕜] [SMulCommClass γ ℚ≥0 𝕜] - [IsScalarTower γ 𝕜 𝕜] (c : γ) (f g : α → 𝕜) : - ⟪c • f, g⟫ₙ_[𝕜] = star c • ⟪f, g⟫ₙ_[𝕜] := by - simp only [nl2Inner, Pi.smul_apply, smul_mul_assoc, smul_expect, starRingEnd_apply, - star_smul] - -lemma nl2Inner_smul_right [Star γ] [StarModule γ 𝕜] [SMulCommClass γ ℚ≥0 𝕜] [IsScalarTower γ 𝕜 𝕜] - [SMulCommClass γ 𝕜 𝕜] (c : γ) (f g : α → 𝕜) : ⟪f, c • g⟫ₙ_[𝕜] = c • ⟪f, g⟫ₙ_[𝕜] := by - simp only [nl2Inner, Pi.smul_apply, mul_smul_comm, smul_expect, starRingEnd_apply, - star_smul] - -lemma smul_nl2Inner_left [InvolutiveStar γ] [StarModule γ 𝕜] [SMulCommClass γ ℚ≥0 𝕜] - [IsScalarTower γ 𝕜 𝕜] (c : γ) (f g : α → 𝕜) : c • ⟪f, g⟫ₙ_[𝕜] = ⟪star c • f, g⟫ₙ_[𝕜] := by - rw [nl2Inner_smul_left, star_star] - -end Semifield - -section Field -variable [Field 𝕜] [CharZero 𝕜] [StarRing 𝕜] - -@[simp] lemma nl2Inner_neg_left (f g : α → 𝕜) : ⟪-f, g⟫ₙ_[𝕜] = -⟪f, g⟫ₙ_[𝕜] := by simp [nl2Inner] -@[simp] lemma nl2Inner_neg_right (f g : α → 𝕜) : ⟪f, -g⟫ₙ_[𝕜] = -⟪f, g⟫ₙ_[𝕜] := by simp [nl2Inner] - -lemma nl2Inner_sub_left (f₁ f₂ g : α → 𝕜) : ⟪f₁ - f₂, g⟫ₙ_[𝕜] = ⟪f₁, g⟫ₙ_[𝕜] - ⟪f₂, g⟫ₙ_[𝕜] := by - simp_rw [sub_eq_add_neg, nl2Inner_add_left, nl2Inner_neg_left] - -lemma nl2Inner_sub_right (f g₁ g₂ : α → 𝕜) : ⟪f, g₁ - g₂⟫ₙ_[𝕜] = ⟪f, g₁⟫ₙ_[𝕜] - ⟪f, g₂⟫ₙ_[𝕜] := by - simp_rw [sub_eq_add_neg, nl2Inner_add_right, nl2Inner_neg_right] - -end Field - -section LinearOrderedSemifield -variable [LinearOrderedSemifield 𝕜] [PosSMulMono ℚ≥0 𝕜] [CharZero 𝕜] [StarRing 𝕜] - [StarOrderedRing 𝕜] {f g : α → 𝕜} - -lemma nl2Inner_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫ₙ_[𝕜] := - expect_nonneg fun _ _ ↦ mul_nonneg (star_nonneg_iff.2 $ hf _) $ hg _ - -end LinearOrderedSemifield - -section LinearOrderedField -variable [LinearOrderedField 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {f g : α → 𝕜} - ---TODO: Can we remove the `TrivialStar` assumption? -lemma abs_nl2Inner_le_nl2Inner_abs : |⟪f, g⟫ₙ_[𝕜]| ≤ ⟪|f|, |g|⟫ₙ_[𝕜] := - (abs_expect_le_expect_abs _ _).trans_eq $ - expect_congr rfl fun i _ ↦ by simp only [abs_mul, conj_trivial, Pi.abs_apply] - -end LinearOrderedField - -section RCLike -variable {κ : Type*} [RCLike 𝕜] {f : α → 𝕜} - -@[simp] lemma nl2Inner_self (f : α → 𝕜) : ⟪f, f⟫ₙ_[𝕜] = (‖f‖ₙ_[2] : 𝕜) ^ 2 := by - simp_rw [← algebraMap.coe_pow, ndL2Norm_sq_eq_expect, nl2Inner, - algebraMap.coe_expect _ (α := ℝ) (β := 𝕜), RCLike.ofReal_pow, RCLike.conj_mul] - -lemma nl2Inner_self_of_norm_eq_one [Nonempty α] (hf : ∀ x, ‖f x‖ = 1) : ⟪f, f⟫ₙ_[𝕜] = 1 := by - simp [-nl2Inner_self, nl2Inner, RCLike.conj_mul, hf] - -lemma linearIndependent_of_ne_zero_of_nl2Inner_eq_zero {v : κ → α → 𝕜} (hz : ∀ k, v k ≠ 0) - (ho : Pairwise fun k l ↦ ⟪v k, v l⟫ₙ_[𝕜] = 0) : LinearIndependent 𝕜 v := by - cases isEmpty_or_nonempty α - · have : IsEmpty κ := ⟨fun k ↦ hz k $ Subsingleton.elim _ _⟩ - exact linearIndependent_empty_type - · exact linearIndependent_of_ne_zero_of_l2Inner_eq_zero hz $ by - simpa [nl2Inner_eq_l2Inner_div_card] using ho - -end RCLike - -section cLpNorm -variable {α β : Type*} [Fintype α] {p : ℝ≥0∞} - -@[simp] lemma cLpNorm_conj [RCLike β] (f : α → β) : ‖conj f‖ₙ_[p] = ‖f‖ₙ_[p] := by simp [cLpNorm] - -variable [AddCommGroup α] - -@[simp] -lemma cLpNorm_translate [NormedAddCommGroup β] (a : α) (f : α → β) : ‖τ a f‖ₙ_[p] = ‖f‖ₙ_[p] := by - simp [cLpNorm] - -@[simp] lemma cLpNorm_conjneg [RCLike β] (f : α → β) : ‖conjneg f‖ₙ_[p] = ‖f‖ₙ_[p] := by - simp [cLpNorm] - -end cLpNorm - -section RCLike -variable {α β : Type*} [Fintype α] - -lemma ndL1Norm_mul [RCLike β] (f g : α → β) : - ‖f * g‖ₙ_[1] = ⟪fun i ↦ ‖f i‖, fun i ↦ ‖g i‖⟫ₙ_[ℝ] := by simp [nl2Inner, ndL1Norm_eq_expect] - -end RCLike - -/-- **Cauchy-Schwarz inequality** -/ -lemma nl2Inner_le_dL2Norm_mul_dL2Norm (f g : α → ℝ) : ⟪f, g⟫ₙ_[ℝ] ≤ ‖f‖ₙ_[2] * ‖g‖ₙ_[2] := by - simp only [cLpNorm, div_mul_div_comm, ← sq, ENNReal.toReal_ofNat, ← one_div, ← sqrt_eq_rpow] - rw [sq_sqrt, nl2Inner_eq_l2Inner_div_card (𝕜 := ℝ)] - refine div_le_div_of_nonneg_right (l2Inner_le_dL2Norm_mul_dL2Norm _ _) ?_ - all_goals positivity - -namespace Mathlib.Meta.Positivity -open Lean Meta Qq Function - -private alias ⟨_, cLpNorm_pos_of_ne_zero⟩ := cLpNorm_pos - -private lemma cLpNorm_pos_of_pos {α : α → Type*} [Nonempty α] [∀ i, NormedAddCommGroup E] - [∀ i, Preorder E] {p : ℝ≥0∞} {f : α → E} (hf : 0 < f) : 0 < ‖f‖ₙ_[p] := - cLpNorm_pos_of_ne_zero hf.ne' - -section LinearOrderedSemifield -variable [LinearOrderedSemifield 𝕜] [Module ℚ≥0 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] {f g : α → 𝕜} - -private lemma nl2Inner_nonneg_of_nonneg_of_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫ₙ_[𝕜] := - sorry - -private lemma nl2Inner_nonneg_of_pos_of_nonneg (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫ₙ_[𝕜] := - nl2Inner_nonneg_of_nonneg_of_nonneg hf.le hg - -private lemma nl2Inner_nonneg_of_nonneg_of_pos (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫ₙ_[𝕜] := - nl2Inner_nonneg_of_nonneg_of_nonneg hf hg.le - -private lemma nl2Inner_nonneg_of_pos_of_pos (hf : 0 < f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫ₙ_[𝕜] := - nl2Inner_nonneg_of_nonneg_of_nonneg hf.le hg.le - -end LinearOrderedSemifield - -/-- The `positivity` extension which identifies expressions of the form `‖f‖ₙ_[p]`. -/ -@[positivity ‖_‖ₙ_[_]] def evalNLpNorm : PositivityExt where eval {u} α _z _p e := do - if let 0 := u then -- lean4#3060 means we can't combine this with the match below - match α, e with - | ~q(ℝ), ~q(@cLpNorm $α $instα $α $instnorm $p $f) => - try - let _pα ← synthInstanceQ (q(∀ i, PartialOrder ($α i)) : Q(Type (max u_1 u_2))) - let _instαno ← synthInstanceQ (q(Nonempty $α) : Q(Prop)) - assumeInstancesCommute - match ← core (q(inferInstance) : Q(Zero (∀ i, $α i))) q(inferInstance) f with - | .positive pf => return .positive q(cLpNorm_pos_of_pos $pf) - | .nonzero pf => return .positive q(cLpNorm_pos_of_ne_zero $pf) - | _ => return .nonnegative q(cLpNorm_nonneg) - catch _ => - assumeInstancesCommute - if let some pf ← findLocalDeclWithType? q($f ≠ 0) then - let pf : Q($f ≠ 0) := .fvar pf - let _instαno ← synthInstanceQ q(Nonempty $α) - return .positive q(cLpNorm_pos_of_ne_zero $pf) - else - return .nonnegative q(cLpNorm_nonneg) - | _ => throwError "not cLpNorm" - else - throwError "not cLpNorm" - -/-- The `positivity` extension which identifies expressions of the form `⟪f, g⟫_[𝕜]`. -/ -@[positivity ⟪_, _⟫ₙ_[_]] def evalNL2Inner : PositivityExt where eval {u 𝕜} _ _ e := do - match e with - | ~q(@nl2Inner $α _ $instα $instfield $instmod $inststar $f $g) => - let _p𝕜 ← synthInstanceQ q(LinearOrderedSemifield $𝕜) - let _p𝕜 ← synthInstanceQ q(StarRing $𝕜) - let _p𝕜 ← synthInstanceQ q(StarOrderedRing $𝕜) - assumeInstancesCommute - match ← core q(inferInstance) q(inferInstance) f, - ← core q(inferInstance) q(inferInstance) g with - | .positive pf, .positive pg => return .nonnegative q(nl2Inner_nonneg_of_pos_of_pos $pf $pg) - | .positive pf, .nonnegative pg => - return .nonnegative q(nl2Inner_nonneg_of_pos_of_nonneg $pf $pg) - | .nonnegative pf, .positive pg => - return .nonnegative q(nl2Inner_nonneg_of_nonneg_of_pos $pf $pg) - | .nonnegative pf, .nonnegative pg => - return .nonnegative q(nl2Inner_nonneg_of_nonneg_of_nonneg $pf $pg) - | _, _ => return .none - | _ => throwError "not nl2Inner" - -section Examples -section NormedAddCommGroup -variable {α : α → Type*} [∀ i, NormedAddCommGroup E] {w : α → ℝ≥0} {f : α → E} - -example {p : ℝ≥0∞} : 0 ≤ ‖f‖ₙ_[p] := by positivity -example {p : ℝ≥0∞} [Nonempty α] (hf : f ≠ 0) : 0 < ‖f‖ₙ_[p] := by positivity -example {p : ℝ≥0∞} [Nonempty α] {f : α → ℝ} (hf : 0 < f) : 0 < ‖f‖ₙ_[p] := by positivity - -end NormedAddCommGroup - -section Complex -variable {w : α → ℝ≥0} {f : α → ℂ} - -example {p : ℝ≥0∞} : 0 ≤ ‖f‖ₙ_[p] := by positivity -example {p : ℝ≥0∞} [Nonempty α] (hf : f ≠ 0) : 0 < ‖f‖ₙ_[p] := by positivity -example {p : ℝ≥0∞} [Nonempty α] {f : α → ℝ} (hf : 0 < f) : 0 < ‖f‖ₙ_[p] := by positivity - -end Complex - -section LinearOrderedSemifield -variable [LinearOrderedSemifield 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] {f g : α → 𝕜} - -example (hf : 0 < f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫ₙ_[𝕜] := by positivity -example (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫ₙ_[𝕜] := by positivity -example (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫ₙ_[𝕜] := by positivity -example (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫ₙ_[𝕜] := by positivity - -end LinearOrderedSemifield -end Examples -end Mathlib.Meta.Positivity - -/-! ### Hölder inequality -/ - -section cLpNorm -variable {α : Type*} [Fintype α] {p q : ℝ≥0} {f g : α → ℝ} - -@[simp] -lemma cLpNorm_abs (p : ℝ≥0∞) (f : α → ℝ) : ‖|f|‖ₙ_[p] = ‖f‖ₙ_[p] := by simpa using cLpNorm_norm p f - -lemma ndL1Norm_mul_of_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : ‖f * g‖ₙ_[1] = ⟪f, g⟫ₙ_[ℝ] := by - convert ndL1Norm_mul f g using 2 <;> ext a <;> refine (norm_of_nonneg ?_).symm; exacts [hf _, hg _] - -lemma cLpNorm_rpow (hp : p ≠ 0) (hq : q ≠ 0) (hf : 0 ≤ f) : - ‖f ^ (q : ℝ)‖ₙ_[p] = ‖f‖ₙ_[p * q] ^ (q : ℝ) := by - refine rpow_left_injOn (NNReal.coe_ne_zero.2 hp) cLpNorm_nonneg (by dsimp; positivity) ?_ - dsimp - rw [← rpow_mul cLpNorm_nonneg, ← mul_comm, ← ENNReal.coe_mul, ← NNReal.coe_mul, - cLpNorm_rpow_eq_expect hp, cLpNorm_rpow_eq_expect (mul_ne_zero hq hp)] - simp [abs_rpow_of_nonneg (hf _), ← rpow_mul] - -lemma ndL1Norm_rpow (hq : q ≠ 0) (hf : 0 ≤ f) : ‖f ^ (q : ℝ)‖ₙ_[1] = ‖f‖ₙ_[q] ^ (q : ℝ) := by - simpa only [ENNReal.coe_one, one_mul] using cLpNorm_rpow one_ne_zero hq hf - -lemma cLpNorm_eq_dL1Norm_rpow (hp : p ≠ 0) (f : α → ℝ) : - ‖f‖ₙ_[p] = ‖|f| ^ (p : ℝ)‖ₙ_[1] ^ (p⁻¹ : ℝ) := by - simp [cLpNorm_eq_expect hp, ndL1Norm_eq_expect, abs_rpow_of_nonneg] - -lemma cLpNorm_rpow' (hp : p ≠ 0) (hq : q ≠ 0) (f : α → ℝ) : - ‖f‖ₙ_[p] ^ (q : ℝ) = ‖|f| ^ (q : ℝ)‖ₙ_[p / q] := by - rw [← ENNReal.coe_div hq, cLpNorm_rpow (div_ne_zero hp hq) hq (abs_nonneg f), cLpNorm_abs, - ← ENNReal.coe_mul, div_mul_cancel₀ _ hq] - ---TODO: Generalise the following four to include `f g : α → ℂ` -/-- **Hölder's inequality**, binary case. -/ -lemma nl2Inner_le_cLpNorm_mul_cLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) : - ⟪f, g⟫ₙ_[ℝ] ≤ ‖f‖ₙ_[p] * ‖g‖ₙ_[q] := by - cases isEmpty_or_nonempty α - · simp - have : 0 < (card α : ℝ) := by positivity - simpa [nl2Inner_eq_l2Inner_div_card, cLpNorm, div_mul_div_comm, ← rpow_add this, - hpq.coe.inv_add_inv_conj, div_le_div_right this] using l2Inner_le_dLpNorm_mul_dLpNorm hpq _ _ - -/-- **Hölder's inequality**, binary case. -/ -lemma abs_nl2Inner_le_cLpNorm_mul_cLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) : - |⟪f, g⟫ₙ_[ℝ]| ≤ ‖f‖ₙ_[p] * ‖g‖ₙ_[q] := - abs_nl2Inner_le_nl2Inner_abs.trans $ - (nl2Inner_le_cLpNorm_mul_cLpNorm hpq _ _).trans_eq $ by simp_rw [cLpNorm_abs] - -/-- **Hölder's inequality**, binary case. -/ -lemma cLpNorm_mul_le (hp : p ≠ 0) (hq : q ≠ 0) (r : ℝ≥0) (hpqr : p⁻¹ + q⁻¹ = r⁻¹) (f g : α → ℝ) : - ‖f * g‖ₙ_[r] ≤ ‖f‖ₙ_[p] * ‖g‖ₙ_[q] := by - cases isEmpty_or_nonempty α - · simp - have : 0 < (card α : ℝ) := by positivity - simp only [nl2Inner_eq_l2Inner_div_card, cLpNorm, div_mul_div_comm, ← rpow_add this, - hpqr, div_le_div_right this, ← NNReal.coe_add, ← NNReal.coe_inv, ENNReal.coe_toReal] - exact div_le_div_of_nonneg_right (dLpNorm_mul_le hp hq _ hpqr _ _) $ by positivity - -/-- **Hölder's inequality**, finitary case. -/ -lemma cLpNorm_prod_le {α : Type*} {s : Finset α} (hs : s.Nonempty) {p : α → ℝ≥0} (hp : ∀ i, p i ≠ 0) - (q : ℝ≥0) (hpq : ∑ i ∈ s, (p i)⁻¹ = q⁻¹) (f : α → α → ℝ) : - ‖∏ i ∈ s, f i‖ₙ_[q] ≤ ∏ i ∈ s, ‖f i‖ₙ_[p i] := by - cases isEmpty_or_nonempty α - · simp - have : 0 < (card α : ℝ) := by positivity - simp only [nl2Inner_eq_l2Inner_div_card, cLpNorm, prod_div_distrib, ← rpow_sum_of_pos this, - hpq, div_le_div_right this, ← NNReal.coe_sum, ← NNReal.coe_inv, ENNReal.coe_toReal] - exact div_le_div_of_nonneg_right (dLpNorm_prod_le hs hp _ hpq _) $ by positivity - -end cLpNorm - -/-! ### Indicator -/ - -section indicate -variable {α β : Type*} [RCLike β] [Fintype α] [DecidableEq α] {s : Finset α} {p : ℝ≥0} - -lemma cLpNorm_rpow_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖ₙ_[p] ^ (p : ℝ) = s.dens := by - rw [cLpNorm, div_rpow] - simp [dLpNorm_rpow_indicate hp, dLpNorm_indicate, hp, dens] - all_goals positivity - -lemma cLpNorm_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖ₙ_[p] = s.dens ^ (p⁻¹ : ℝ) := by - refine (eq_rpow_inv ?_ ?_ ?_).2 (cLpNorm_rpow_indicate ?_ _) <;> positivity - -lemma cLpNorm_pow_indicate {p : ℕ} (hp : p ≠ 0) (s : Finset α) : - ‖𝟭_[β] s‖ₙ_[p] ^ (p : ℝ) = s.dens := by - simpa using cLpNorm_rpow_indicate (Nat.cast_ne_zero.2 hp) s - -lemma ndL2Norm_sq_indicate (s : Finset α) : ‖𝟭_[β] s‖ₙ_[2] ^ 2 = s.dens := by - simpa using cLpNorm_pow_indicate two_ne_zero s - -lemma ndL2Norm_indicate (s : Finset α) : ‖𝟭_[β] s‖ₙ_[2] = Real.sqrt s.dens := by - rw [eq_comm, sqrt_eq_iff_sq_eq, ndL2Norm_sq_indicate] <;> positivity - -@[simp] lemma ndL1Norm_indicate (s : Finset α) : ‖𝟭_[β] s‖ₙ_[1] = s.dens := by - simpa using cLpNorm_pow_indicate one_ne_zero s - -end indicate - -section mu -variable {α β : Type*} [RCLike β] [Fintype α] [DecidableEq α] {s : Finset α} {p : ℝ≥0} - -lemma cLpNorm_mu (hp : 1 ≤ p) (s : Finset α) : ‖μ_[β] s‖ₙ_[p] = s.dens ^ (p⁻¹ : ℝ) / s.card := by - rw [mu, cLpNorm_smul (ENNReal.one_le_coe_iff.2 hp) (s.card⁻¹ : β) (𝟭_[β] s), cLpNorm_indicate, - norm_inv, RCLike.norm_natCast, inv_mul_eq_div]; positivity - -lemma ndL1Norm_mu (s : Finset α) : ‖μ_[β] s‖ₙ_[1] = s.dens / s.card := by - simpa using cLpNorm_mu le_rfl s - -end mu - -section -variable {α : Type*} [Fintype α] - -@[simp] -lemma RCLike.cLpNorm_coe_comp {𝕜 : Type*} [RCLike 𝕜] (p) (f : α → ℝ) : - ‖((↑) : ℝ → 𝕜) ∘ f‖ₙ_[p] = ‖f‖ₙ_[p] := by - simp only [← cLpNorm_norm _ (((↑) : ℝ → 𝕜) ∘ f), ← cLpNorm_norm _ f, Function.comp_apply, - RCLike.norm_ofReal, Real.norm_eq_abs] - -@[simp] lemma Complex.cLpNorm_coe_comp (p) (f : α → ℝ) : ‖((↑) : ℝ → ℂ) ∘ f‖ₙ_[p] = ‖f‖ₙ_[p] := - RCLike.cLpNorm_coe_comp _ _ - -end diff --git a/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean new file mode 100644 index 0000000000..4c410c237e --- /dev/null +++ b/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean @@ -0,0 +1,175 @@ +import Mathlib.Data.Finset.Density +import LeanAPAP.Mathlib.Probability.ConditionalProbability +import LeanAPAP.Prereqs.LpNorm.Discrete.Basic +import LeanAPAP.Prereqs.LpNorm.Discrete.Inner + +/-! +# Normalised Lp norms +-/ + +open Finset hiding card +open Function ProbabilityTheory Real +open Fintype (card) +open scoped BigOperators ComplexConjugate ENNReal NNReal + +variable {α 𝕜 R E : Type*} [MeasurableSpace α] + +/-! ### Lp norm -/ + +namespace MeasureTheory +section NormedAddCommGroup +variable [NormedAddCommGroup E] {p q : ℝ≥0∞} {f g h : α → E} + +/-- The Lp norm of a function with the compact normalisation. -/ +noncomputable def cLpNorm (p : ℝ≥0∞) (f : α → E) : ℝ≥0 := nnLpNorm f p .count[|Set.univ] + +notation "‖" f "‖ₙ_[" p "]" => cLpNorm p f + +@[simp] lemma cLpNorm_exponent_zero (f : α → E) : ‖f‖ₙ_[0] = 0 := by simp [cLpNorm] + +@[simp] lemma cLpNorm_zero (p : ℝ≥0∞) : ‖(0 : α → E)‖ₙ_[p] = 0 := by simp [cLpNorm] +@[simp] lemma cLpNorm_zero' (p : ℝ≥0∞) : ‖(fun _ ↦ 0 : α → E)‖ₙ_[p] = 0 := by simp [cLpNorm] + +@[simp] lemma cLpNorm_of_isEmpty [IsEmpty α] (f : α → E) (p : ℝ≥0∞) : ‖f‖ₙ_[p] = 0 := by + simp [cLpNorm] + +@[simp] lemma cLpNorm_neg (f : α → E) (p : ℝ≥0∞) : ‖-f‖ₙ_[p] = ‖f‖ₙ_[p] := by simp [cLpNorm] +@[simp] lemma cLpNorm_neg' (f : α → E) (p : ℝ≥0∞) : ‖fun x ↦ -f x‖ₙ_[p] = ‖f‖ₙ_[p] := by + simp [cLpNorm] + +lemma cLpNorm_sub_comm (f g : α → E) (p : ℝ≥0∞) : ‖f - g‖ₙ_[p] = ‖g - f‖ₙ_[p] := by + simp [cLpNorm, nnLpNorm_sub_comm] + +@[simp] lemma cLpNorm_norm (p : ℝ≥0∞) (f : α → E) : ‖fun i ↦ ‖f i‖‖ₙ_[p] = ‖f‖ₙ_[p] := + nnLpNorm_norm .. + +section NormedField +variable [NormedField 𝕜] {p : ℝ≥0∞} {f g : α → 𝕜} + +lemma cLpNorm_const_smul [Module 𝕜 E] [BoundedSMul 𝕜 E] (c : 𝕜) (f : α → E) : + ‖c • f‖ₙ_[p] = ‖c‖₊ * ‖f‖ₙ_[p] := by simp [cLpNorm, nnLpNorm_const_smul] + +lemma cLpNorm_nsmul [NormedSpace ℝ E] (n : ℕ) (f : α → E) : ‖n • f‖ₙ_[p] = n • ‖f‖ₙ_[p] := by + simp [cLpNorm, nnLpNorm_nsmul] + +variable [NormedSpace ℝ 𝕜] + +lemma cLpNorm_natCast_mul (n : ℕ) (f : α → 𝕜) (p : ℝ≥0∞) : ‖(n : α → 𝕜) * f‖ₙ_[p] = n * ‖f‖ₙ_[p] := + nnLpNorm_natCast_mul .. + +lemma cLpNorm_natCast_mul' (n : ℕ) (f : α → 𝕜) (p : ℝ≥0∞) : ‖(n * f ·)‖ₙ_[p] = n * ‖f‖ₙ_[p] := + nnLpNorm_natCast_mul' .. + +lemma cLpNorm_mul_natCast (f : α → 𝕜) (n : ℕ) (p : ℝ≥0∞) : ‖f * (n : α → 𝕜)‖ₙ_[p] = ‖f‖ₙ_[p] * n := + nnLpNorm_mul_natCast .. + +lemma cLpNorm_mul_natCast' (f : α → 𝕜) (n : ℕ) (p : ℝ≥0∞) : ‖(f · * n)‖ₙ_[p] = ‖f‖ₙ_[p] * n := + nnLpNorm_mul_natCast' .. + +lemma cLpNorm_div_natCast [CharZero 𝕜] {n : ℕ} (hn : n ≠ 0) (f : α → 𝕜) (p : ℝ≥0∞) : + ‖f / (n : α → 𝕜)‖ₙ_[p] = ‖f‖ₙ_[p] / n := nnLpNorm_div_natCast hn .. + +lemma cLpNorm_div_natCast' [CharZero 𝕜] {n : ℕ} (hn : n ≠ 0) (f : α → 𝕜) (p : ℝ≥0∞) : + ‖(f · / n)‖ₙ_[p] = ‖f‖ₙ_[p] / n := nnLpNorm_div_natCast' hn .. + +end NormedField + +section RCLike +variable {p : ℝ≥0∞} + +@[simp] lemma cLpNorm_conj [RCLike R] (f : α → R) : ‖conj f‖ₙ_[p] = ‖f‖ₙ_[p] := nnLpNorm_conj .. + +end RCLike + +section DiscreteMeasurableSpace +variable [DiscreteMeasurableSpace α] [Finite α] + +lemma cLpNorm_add_le (hp : 1 ≤ p) : ‖f + g‖ₙ_[p] ≤ ‖f‖ₙ_[p] + ‖g‖ₙ_[p] := + nnLpNorm_add_le .of_discrete .of_discrete hp + +lemma cLpNorm_sub_le (hp : 1 ≤ p) : ‖f - g‖ₙ_[p] ≤ ‖f‖ₙ_[p] + ‖g‖ₙ_[p] := + nnLpNorm_sub_le .of_discrete .of_discrete hp + +lemma cLpNorm_sum_le {ι : Type*} {s : Finset ι} {f : ι → α → E} (hp : 1 ≤ p) : + ‖∑ i ∈ s, f i‖ₙ_[p] ≤ ∑ i ∈ s, ‖f i‖ₙ_[p] := nnLpNorm_sum_le (fun _ _ ↦ .of_discrete) hp + +lemma cLpNorm_expect_le [Module ℚ≥0 E] [NormedSpace ℝ E] {ι : Type*} {s : Finset ι} {f : ι → α → E} + (hp : 1 ≤ p) : ‖𝔼 i ∈ s, f i‖ₙ_[p] ≤ 𝔼 i ∈ s, ‖f i‖ₙ_[p] := + nnLpNorm_expect_le (fun _ _ ↦ .of_discrete) hp + +lemma cLpNorm_le_cLpNorm_add_cLpNorm_sub' (hp : 1 ≤ p) : ‖f‖ₙ_[p] ≤ ‖g‖ₙ_[p] + ‖f - g‖ₙ_[p] := + nnLpNorm_le_nnLpNorm_add_nnLpNorm_sub' .of_discrete .of_discrete hp + +lemma cLpNorm_le_cLpNorm_add_cLpNorm_sub (hp : 1 ≤ p) : ‖f‖ₙ_[p] ≤ ‖g‖ₙ_[p] + ‖g - f‖ₙ_[p] := + nnLpNorm_le_nnLpNorm_add_nnLpNorm_sub .of_discrete .of_discrete hp + +lemma cLpNorm_le_add_cLpNorm_add (hp : 1 ≤ p) : ‖f‖ₙ_[p] ≤ ‖f + g‖ₙ_[p] + ‖g‖ₙ_[p] := + nnLpNorm_le_add_nnLpNorm_add .of_discrete .of_discrete hp + +lemma cLpNorm_sub_le_cLpNorm_sub_add_cLpNorm_sub (hp : 1 ≤ p) : + ‖f - h‖ₙ_[p] ≤ ‖f - g‖ₙ_[p] + ‖g - h‖ₙ_[p] := + nnLpNorm_sub_le_nnLpNorm_sub_add_nnLpNorm_sub .of_discrete .of_discrete .of_discrete hp + +end DiscreteMeasurableSpace + +variable [Fintype α] + +@[simp] lemma cLpNorm_const [Nonempty α] {p : ℝ≥0∞} (hp : p ≠ 0) (a : E) : + ‖fun _i : α ↦ a‖ₙ_[p] = ‖a‖₊ := by simp [cLpNorm, *] + + +section NormedField +variable [NormedField 𝕜] {p : ℝ≥0∞} {f g : α → 𝕜} + +@[simp] lemma cLpNorm_one [Nonempty α] (hp : p ≠ 0) : + ‖(1 : α → 𝕜)‖ₙ_[p] = 1 := by simp [cLpNorm, *] + +end NormedField + +variable [DiscreteMeasurableSpace α] + +lemma cLpNorm_eq_expect' (hp₀ : p ≠ 0) (hp : p ≠ ∞) (f : α → E) : + ‖f‖ₙ_[p] = (𝔼 i, ‖f i‖ ^ p.toReal) ^ p.toReal⁻¹ := by + simp [cLpNorm, coe_nnLpNorm_eq_integral_norm_rpow_toReal hp₀ hp .of_discrete, one_div, ← mul_sum, + integral_fintype, tsum_eq_sum' (s := univ) (by simp), ENNReal.coe_rpow_of_nonneg, cond_apply, expect_eq_sum_div_card, div_eq_inv_mul] + +lemma cLpNorm_eq_expect'' {p : ℝ} (hp : 0 < p) (f : α → E) : + ‖f‖ₙ_[p.toNNReal] = (𝔼 i, ‖f i‖ ^ p) ^ p⁻¹ := by + rw [cLpNorm_eq_expect'] <;> simp [hp.le, hp] + +lemma cLpNorm_eq_expect {p : ℝ≥0} (hp : p ≠ 0) (f : α → E) : + ‖f‖ₙ_[p] = (𝔼 i, ‖f i‖ ^ (p : ℝ)) ^ (p⁻¹ : ℝ) := + cLpNorm_eq_expect' (by simpa using hp) (by simp) _ + +lemma cLpNorm_rpow_eq_expect {p : ℝ≥0} (hp : p ≠ 0) (f : α → E) : + ‖f‖ₙ_[p] ^ (p : ℝ) = 𝔼 i, ‖f i‖ ^ (p : ℝ) := by + rw [cLpNorm_eq_expect hp, rpow_inv_rpow] <;> positivity + +lemma cLpNorm_pow_eq_expect {p : ℕ} (hp : p ≠ 0) (f : α → E) : + ‖f‖ₙ_[p] ^ p = 𝔼 i, ‖f i‖ ^ p := by + simpa using cLpNorm_rpow_eq_expect (Nat.cast_ne_zero.2 hp) f + +lemma cL2Norm_sq_eq_expect (f : α → E) : ‖f‖ₙ_[2] ^ 2 = 𝔼 i, ‖f i‖ ^ 2 := by + simpa using cLpNorm_pow_eq_expect two_ne_zero _ + +lemma cL2Norm_eq_expect (f : α → E) : ‖f‖ₙ_[2] = sqrt (𝔼 i, ‖f i‖ ^ 2) := by + simpa [sqrt_eq_rpow] using cLpNorm_eq_expect two_ne_zero _ + +lemma cL1Norm_eq_expect (f : α → E) : ‖f‖ₙ_[1] = 𝔼 i, ‖f i‖ := by simp [cLpNorm_eq_expect'] + +lemma nLinftyNorm_eq_iSup (f : α → E) : ‖f‖ₙ_[∞] = ⨆ i, ‖f i‖ := by + cases isEmpty_or_nonempty α + · simp + · simp [cLpNorm, nnLinftyNorm_eq_essSup] + sorry + +@[simp] lemma cLpNorm_eq_zero (hp : p ≠ 0) : ‖f‖ₙ_[p] = 0 ↔ f = 0 := by + simp [cLpNorm, nnLpNorm_eq_zero .of_discrete hp, ae_eq_top.2]; sorry + +@[simp] lemma cLpNorm_pos (hp : p ≠ 0) : 0 < ‖f‖ₙ_[p] ↔ f ≠ 0 := + pos_iff_ne_zero.trans (cLpNorm_eq_zero hp).not + +@[gcongr] lemma cLpNorm_mono_right (hpq : p ≤ q) : ‖f‖ₙ_[p] ≤ ‖f‖ₙ_[q] := sorry + +lemma cLpNorm_mono_real {g : α → ℝ} (h : ∀ x, ‖f x‖ ≤ g x) : ‖f‖ₙ_[p] ≤ ‖g‖ₙ_[p] := + nnLpNorm_mono_real .of_discrete h diff --git a/LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean b/LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean new file mode 100644 index 0000000000..460eabadf2 --- /dev/null +++ b/LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean @@ -0,0 +1,276 @@ +import Mathlib.Analysis.InnerProductSpace.PiL2 +import LeanAPAP.Mathlib.Algebra.Algebra.Rat +import LeanAPAP.Mathlib.Algebra.Star.Rat +import LeanAPAP.Prereqs.LpNorm.Compact.Defs + +/-! # Inner product -/ + +open Finset hiding card +open Function Real +open Fintype (card) +open scoped BigOperators ComplexConjugate ENNReal NNReal NNRat + +variable {ι R S : Type*} [Fintype ι] + +namespace MeasureTheory +section CommSemiring +variable [CommSemiring R] [StarRing R] [Module ℚ≥0 R] [DistribSMul S R] + +/-- Inner product giving rise to the L2 norm. -/ +def cL2Inner (f g : ι → R) : R := 𝔼 i, conj (f i) * g i + +notation "⟪" f ", " g "⟫ₙ_[" S "]" => cL2Inner (R := S) f g + +lemma cL2Inner_eq_smul_dL2Inner (f g : ι → R) : ⟪f, g⟫ₙ_[R] = (card ι : ℚ≥0)⁻¹ • ⟪f, g⟫_[R] := rfl + +lemma cL2Inner_eq_expect (f g : ι → R) : ⟪f, g⟫ₙ_[R] = 𝔼 i, conj (f i) * g i := rfl + +@[simp] lemma conj_cL2Inner (f g : ι → R) : conj ⟪f, g⟫ₙ_[R] = ⟪conj f, conj g⟫ₙ_[R] := by + simp [cL2Inner_eq_expect, map_expect] + exact Eq.trans (map_expect (starLinearEquiv ℚ≥0) _ _) (by simp [starRingEnd, starLinearEquiv]) + +lemma cL2Inner_anticomm (f g : ι → R) : ⟪f, g⟫ₙ_[R] = ⟪conj g, conj f⟫ₙ_[R] := by + simp [cL2Inner_eq_expect, map_sum, mul_comm] + +@[simp] lemma cL2Inner_zero_left (g : ι → R) : ⟪0, g⟫ₙ_[R] = 0 := by simp [cL2Inner_eq_expect] +@[simp] lemma cL2Inner_zero_right (f : ι → R) : ⟪f, 0⟫ₙ_[R] = 0 := by simp [cL2Inner_eq_expect] + +@[simp] lemma cL2Inner_of_isEmpty [IsEmpty ι] (f g : ι → R) : ⟪f, g⟫ₙ_[R] = 0 := by + simp [Subsingleton.elim f 0] + +@[simp] lemma cL2Inner_const_left (a : R) (f : ι → R) : + ⟪const _ a, f⟫ₙ_[R] = conj a * 𝔼 x, f x := by + simp only [cL2Inner_eq_expect, const_apply, mul_expect] + +@[simp] +lemma cL2Inner_const_right (f : ι → R) (a : R) : ⟪f, const _ a⟫ₙ_[R] = (𝔼 x, conj (f x)) * a := by + simp only [cL2Inner_eq_expect, const_apply, expect_mul] + +lemma cL2Inner_add_left (f₁ f₂ g : ι → R) : ⟪f₁ + f₂, g⟫ₙ_[R] = ⟪f₁, g⟫ₙ_[R] + ⟪f₂, g⟫ₙ_[R] := by + simp_rw [cL2Inner_eq_expect, Pi.add_apply, map_add, add_mul, expect_add_distrib] + +lemma cL2Inner_add_right (f g₁ g₂ : ι → R) : ⟪f, g₁ + g₂⟫ₙ_[R] = ⟪f, g₁⟫ₙ_[R] + ⟪f, g₂⟫ₙ_[R] := by + simp_rw [cL2Inner_eq_expect, Pi.add_apply, mul_add, expect_add_distrib] + +lemma cL2Inner_smul_left [Star S] [StarModule S R] [IsScalarTower S R R] (c : S) (f g : ι → R) : + ⟪c • f, g⟫ₙ_[R] = star c • ⟪f, g⟫ₙ_[R] := by + simp only [cL2Inner_eq_expect, Pi.smul_apply, smul_mul_assoc, smul_expect, starRingEnd_apply, + star_smul]; sorry + +lemma cL2Inner_smul_right [Star S] [StarModule S R] [SMulCommClass S R R] (c : S) (f g : ι → R) : + ⟪f, c • g⟫ₙ_[R] = c • ⟪f, g⟫ₙ_[R] := by + simp only [cL2Inner_eq_expect, Pi.smul_apply, mul_smul_comm, smul_expect, starRingEnd_apply, + star_smul]; sorry + +lemma smul_cL2Inner_left [InvolutiveStar S] [StarModule S R] [IsScalarTower S R R] (c : S) + (f g : ι → R) : c • ⟪f, g⟫ₙ_[R] = ⟪star c • f, g⟫ₙ_[R] := by rw [cL2Inner_smul_left, star_star] + +end CommSemiring + +section CommRing +variable [CommRing R] [StarRing R] [Module ℚ≥0 R] + +@[simp] +lemma cL2Inner_neg_left (f g : ι → R) : ⟪-f, g⟫ₙ_[R] = -⟪f, g⟫ₙ_[R] := by simp [cL2Inner_eq_expect] + +@[simp] +lemma cL2Inner_neg_right (f g : ι → R) : ⟪f, -g⟫ₙ_[R] = -⟪f, g⟫ₙ_[R] := by simp [cL2Inner_eq_expect] + +lemma cL2Inner_sub_left (f₁ f₂ g : ι → R) : ⟪f₁ - f₂, g⟫ₙ_[R] = ⟪f₁, g⟫ₙ_[R] - ⟪f₂, g⟫ₙ_[R] := by + simp_rw [sub_eq_add_neg, cL2Inner_add_left, cL2Inner_neg_left] + +lemma cL2Inner_sub_right (f g₁ g₂ : ι → R) : ⟪f, g₁ - g₂⟫ₙ_[R] = ⟪f, g₁⟫ₙ_[R] - ⟪f, g₂⟫ₙ_[R] := by + simp_rw [sub_eq_add_neg, cL2Inner_add_right, cL2Inner_neg_right] + +end CommRing + +section OrderedCommSemiring +variable [OrderedCommSemiring R] [StarRing R] [StarOrderedRing R] [Module ℚ≥0 R] + [PosSMulMono ℚ≥0 R] {f g : ι → R} + +lemma cL2Inner_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫ₙ_[R] := + expect_nonneg fun _ _ ↦ mul_nonneg (star_nonneg_iff.2 $ hf _) $ hg _ + +end OrderedCommSemiring + +section LinearOrderedCommRing +variable [LinearOrderedCommRing R] [StarRing R] [TrivialStar R] [Module ℚ≥0 R] + [PosSMulMono ℚ≥0 R] {f g : ι → R} + +--TODO: Can we remove the `TrivialStar` assumption? +lemma abs_cL2Inner_le_cL2Inner_abs : |⟪f, g⟫ₙ_[R]| ≤ ⟪|f|, |g|⟫ₙ_[R] := + (abs_expect_le_expect_abs _ _).trans_eq $ + expect_congr rfl fun i _ ↦ by simp only [abs_mul, conj_trivial, Pi.abs_apply] + +end LinearOrderedCommRing + +section RCLike +variable {κ : Type*} [RCLike R] {f : ι → R} + +@[simp] lemma cL2Inner_self {_ : MeasurableSpace ι} [DiscreteMeasurableSpace ι] (f : ι → R) : + ⟪f, f⟫ₙ_[R] = ((‖f‖ₙ_[2] : ℝ) : R) ^ 2 := by + simp_rw [← algebraMap.coe_pow, ← NNReal.coe_pow] + simp [cL2Norm_sq_eq_expect, cL2Inner_eq_expect, RCLike.conj_mul] + +lemma cL2Inner_self_of_norm_eq_one [Nonempty ι] (hf : ∀ x, ‖f x‖ = 1) : ⟪f, f⟫ₙ_[R] = 1 := by + simp [-cL2Inner_self, cL2Inner_eq_expect, RCLike.conj_mul, hf, card_univ] + +lemma linearIndependent_of_ne_zero_of_cL2Inner_eq_zero {v : κ → ι → R} (hz : ∀ k, v k ≠ 0) + (ho : Pairwise fun k l ↦ ⟪v k, v l⟫ₙ_[R] = 0) : LinearIndependent R v := by + cases isEmpty_or_nonempty ι + · have : IsEmpty κ := ⟨fun k ↦ hz k $ Subsingleton.elim _ _⟩ + exact linearIndependent_empty_type + · exact linearIndependent_of_ne_zero_of_dL2Inner_eq_zero hz $ by + simpa [cL2Inner_eq_smul_dL2Inner, ← NNRat.cast_smul_eq_nnqsmul R] using ho + +variable {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] + +lemma cL1Norm_mul (f g : ι → R) : ‖f * g‖ₙ_[1] = ⟪fun i ↦ ‖f i‖, fun i ↦ ‖g i‖⟫ₙ_[ℝ] := by + simp [cL2Inner_eq_expect, cL1Norm_eq_expect] + +end RCLike + +variable {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] + +/-- **Cauchy-Schwarz inequality** -/ +lemma cL2Inner_le_cL2Norm_mul_cL2Norm (f g : ι → ℝ) : ⟪f, g⟫ₙ_[ℝ] ≤ ‖f‖ₙ_[2] * ‖g‖ₙ_[2] := by + simp only [cL2Norm_eq_expect, div_mul_div_comm, ← sq, ENNReal.toReal_ofNat] + rw [← sqrt_mul, le_sqrt, cL2Inner_eq_smul_dL2Inner, expect, card_univ] + gcongr + refine div_le_div_of_nonneg_right (dL2Inner_le_dL2Norm_mul_dL2Norm _ _) ?_ + all_goals positivity + +end MeasureTheory + +namespace Mathlib.Meta.Positivity +open Lean Meta Qq Function MeasureTheory + +section OrderedCommSemiring +variable [OrderedCommSemiring R] [StarRing R] [StarOrderedRing R] {f g : ι → R} + +private lemma cL2Inner_nonneg_of_pos_of_nonneg (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫ₙ_[R] := + cL2Inner_nonneg hf.le hg + +private lemma cL2Inner_nonneg_of_nonneg_of_pos (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫ₙ_[R] := + cL2Inner_nonneg hf hg.le + +private lemma cL2Inner_nonneg_of_pos_of_pos (hf : 0 < f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫ₙ_[R] := + cL2Inner_nonneg hf.le hg.le + +end OrderedCommSemiring + +/-- The `positivity` extension which identifies expressions of the form `⟪f, g⟫ₙ_[R]`. -/ +@[positivity ⟪_, _⟫ₙ_[_]] def evalL2Inner : PositivityExt where eval {u R} _ _ e := do + match e with + | ~q(@cL2Inner $ι _ $instι $instring $inststar $f $g) => + let _p𝕜 ← synthInstanceQ q(OrderedCommSemiring $R) + let _p𝕜 ← synthInstanceQ q(StarOrderedRing $R) + assumeInstancesCommute + match ← core q(inferInstance) q(inferInstance) f, + ← core q(inferInstance) q(inferInstance) g with + | .positive pf, .positive pg => return .nonnegative q(cL2Inner_nonneg_of_pos_of_pos $pf $pg) + | .positive pf, .nonnegative pg => + return .nonnegative q(cL2Inner_nonneg_of_pos_of_nonneg $pf $pg) + | .nonnegative pf, .positive pg => + return .nonnegative q(cL2Inner_nonneg_of_nonneg_of_pos $pf $pg) + | .nonnegative pf, .nonnegative pg => return .nonnegative q(cL2Inner_nonneg $pf $pg) + | _, _ => return .none + | _ => throwError "not cL2Inner" + +section OrderedCommSemiring +variable [OrderedCommSemiring R] [StarRing R] [StarOrderedRing R] {f g : ι → R} + +example (hf : 0 < f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫ₙ_[R] := by positivity +example (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫ₙ_[R] := by positivity +example (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫ₙ_[R] := by positivity +example (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫ₙ_[R] := by positivity + +end OrderedCommSemiring +end Mathlib.Meta.Positivity + +/-! ### Hölder inequality -/ + +namespace MeasureTheory +section Real +variable {α : Type*} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] {p q : ℝ≥0} + {f g : α → ℝ} + +lemma dL1Norm_mul_of_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : ‖f * g‖_[1] = ⟪f, g⟫ₙ_[ℝ] := by + convert dL1Norm_mul f g using 2 <;> ext a <;> refine (norm_of_nonneg ?_).symm; exacts [hf _, hg _] + +/-- **Hölder's inequality**, binary case. -/ +lemma cL2Inner_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) : + ⟪f, g⟫ₙ_[ℝ] ≤ ‖f‖_[p] * ‖g‖_[q] := by + have hp := hpq.ne_zero + have hq := hpq.symm.ne_zero + norm_cast at hp hq + simpa [cL2Inner_eq_expect, dLpNorm_eq_sum, *] using inner_le_Lp_mul_Lq _ f g hpq.coe + +/-- **Hölder's inequality**, binary case. -/ +lemma abs_cL2Inner_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) : + |⟪f, g⟫ₙ_[ℝ]| ≤ ‖f‖_[p] * ‖g‖_[q] := + abs_cL2Inner_le_cL2Inner_abs.trans $ + (cL2Inner_le_dLpNorm_mul_dLpNorm hpq _ _).trans_eq $ by simp_rw [dLpNorm_abs] + +end Real + +section Hoelder +variable {α : Type*} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] [RCLike R] + {p q : ℝ≥0} {f g : α → R} + +lemma norm_cL2Inner_le (f g : α → R) : ‖⟪f, g⟫ₙ_[R]‖₊ ≤ ⟪fun a ↦ ‖f a‖, fun a ↦ ‖g a‖⟫ₙ_[ℝ] := + (norm_sum_le _ _).trans $ by simp [cL2Inner] + +/-- **Hölder's inequality**, binary case. -/ +lemma norm_cL2Inner_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → R) : + ‖⟪f, g⟫ₙ_[R]‖₊ ≤ ‖f‖_[p] * ‖g‖_[q] := + calc + _ ≤ ⟪fun a ↦ ‖f a‖, fun a ↦ ‖g a‖⟫ₙ_[ℝ] := norm_cL2Inner_le _ _ + _ ≤ ‖fun a ↦ ‖f a‖‖_[p] * ‖fun a ↦ ‖g a‖‖_[q] := cL2Inner_le_dLpNorm_mul_dLpNorm hpq _ _ + _ = ‖f‖_[p] * ‖g‖_[q] := by simp_rw [dLpNorm_norm] + +/-- **Hölder's inequality**, binary case. -/ +lemma dLpNorm_mul_le (hp : p ≠ 0) (hq : q ≠ 0) (r : ℝ≥0) (hpqr : p⁻¹ + q⁻¹ = r⁻¹) (f g : α → R) : + ‖f * g‖_[r] ≤ ‖f‖_[p] * ‖g‖_[q] := by + have hr : r ≠ 0 := by + rintro rfl + simp [hp] at hpqr + have : (‖(f * g) ·‖ ^ (r : ℝ)) = (‖f ·‖ ^ (r : ℝ)) * (‖g ·‖ ^ (r : ℝ)) := by + ext; simp [mul_rpow, abs_mul] + rw [dLpNorm_eq_dL1Norm_rpow, NNReal.rpow_inv_le_iff_of_pos, this, ← NNReal.coe_le_coe] + push_cast + rw [dL1Norm_mul_of_nonneg, mul_rpow, ← NNReal.coe_rpow, ← NNReal.coe_rpow, dLpNorm_rpow', + dLpNorm_rpow', ← ENNReal.coe_div, ← ENNReal.coe_div] + refine cL2Inner_le_dLpNorm_mul_dLpNorm ⟨?_, ?_⟩ _ _ + · norm_cast + rw [div_eq_mul_inv, ← hpqr, mul_add, mul_inv_cancel₀ hp] + exact lt_add_of_pos_right _ (by positivity) + · norm_cast + simp [div_eq_mul_inv, hpqr, ← mul_add, hr] + any_goals intro a; dsimp + all_goals positivity + +/-- **Hölder's inequality**, binary case. -/ +lemma dL1Norm_mul_le (hpq : p.IsConjExponent q) (f g : α → R) : + ‖f * g‖_[1] ≤ ‖f‖_[p] * ‖g‖_[q] := + dLpNorm_mul_le (mod_cast hpq.ne_zero) (mod_cast hpq.symm.ne_zero) _ + (by simpa using hpq.inv_add_inv_conj) _ _ + +/-- **Hölder's inequality**, finitary case. -/ +lemma dLpNorm_prod_le {ι : Type*} {s : Finset ι} (hs : s.Nonempty) {p : ι → ℝ≥0} + (hp : ∀ i, p i ≠ 0) (q : ℝ≥0) + (hpq : 𝔼 i in s, (p i)⁻¹ = q⁻¹) (f : ι → α → R) : + ‖∏ i in s, f i‖_[q] ≤ ∏ i in s, ‖f i‖_[p i] := by + induction' s using Finset.cons_induction with i s hi ih generalizing q + · cases not_nonempty_empty hs + obtain rfl | hs := s.eq_empty_or_nonempty + · simp only [sum_cons, sum_empty, add_zero, inv_inj] at hpq + simp [← hpq] + simp_rw [prod_cons] + rw [sum_cons, ← inv_inv (𝔼 _ ∈ _, _ : ℝ≥0)] at hpq + refine (dLpNorm_mul_le (hp _) (inv_ne_zero (sum_pos (fun _ _ ↦ ?_) hs).ne') _ hpq _ _).trans + (mul_le_mul_left' (ih hs _ (inv_inv _).symm) _) + exact pos_iff_ne_zero.2 (inv_ne_zero $ hp _) + +end Hoelder +end MeasureTheory diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean index 5fe3bf738d..4b48881152 100644 --- a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean +++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean @@ -13,25 +13,6 @@ open scoped BigOperators ComplexConjugate ENNReal NNReal namespace MeasureTheory variable {ι G 𝕜 E R : Type*} [Fintype ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] -/-! ### Lp norm -/ - -section NormedAddCommGroup -variable [NormedAddCommGroup E] {p q : ℝ≥0∞} {f g h : ι → E} - -section one_le -variable [NormedField 𝕜] [NormedSpace ℝ E] - -lemma dLpNorm_expect_le [Module ℚ≥0 E] (hp : 1 ≤ p) {κ : Type*} (s : Finset κ) (f : κ → ι → E) : - ‖𝔼 i ∈ s, f i‖_[p] ≤ 𝔼 i ∈ s, ‖f i‖_[p] := by - obtain rfl | hs := s.eq_empty_or_nonempty - · simp - refine (le_inv_smul_iff_of_pos $ by positivity).2 ?_ - rw [Nat.cast_smul_eq_nsmul, ← nnLpNorm_nsmul, card_smul_expect] - exact dLpNorm_sum_le hp _ _ - -end one_le -end NormedAddCommGroup - /-! ### Indicator -/ section Indicator @@ -60,7 +41,7 @@ lemma dL2Norm_indicate (s : Finset ι) : ‖𝟭_[R] s‖_[2] = NNReal.sqrt s.ca simpa using dLpNorm_pow_indicate one_ne_zero s lemma dLpNorm_mu (hp : 1 ≤ p) (hs : s.Nonempty) : ‖μ_[R] s‖_[p] = s.card ^ ((p : ℝ)⁻¹ - 1) := by - rw [mu, nnLpNorm_const_smul (s.card⁻¹ : R) (𝟭_[R] s), dLpNorm_indicate, nnnorm_inv, + rw [mu, dLpNorm_const_smul (s.card⁻¹ : R) (𝟭_[R] s), dLpNorm_indicate, nnnorm_inv, RCLike.nnnorm_natCast, inv_mul_eq_div, ← NNReal.rpow_sub_one] <;> positivity lemma dLpNorm_mu_le (hp : 1 ≤ p) : ‖μ_[R] s‖_[p] ≤ s.card ^ (p⁻¹ - 1 : ℝ) := by @@ -86,7 +67,7 @@ lemma dLpNorm_translate [NormedAddCommGroup E] (a : G) (f : G → E) : ‖τ a f · simp only [dLinftyNorm_eq_iSup, ENNReal.none_eq_top, translate_apply] exact (Equiv.subRight _).iSup_congr fun _ ↦ rfl obtain rfl | hp := eq_or_ne p 0 - · simp only [nnLpNorm_exponent_zero, translate_apply, Ne, ENNReal.some_eq_coe, ENNReal.coe_zero, + · simp only [dLpNorm_exponent_zero, translate_apply, Ne, ENNReal.some_eq_coe, ENNReal.coe_zero, Nat.cast_inj] · simp only [dLpNorm_eq_sum hp, ENNReal.some_eq_coe, translate_apply] congr 1 @@ -98,7 +79,7 @@ lemma dLpNorm_translate [NormedAddCommGroup E] (a : G) (f : G → E) : ‖τ a f · simp only [dLinftyNorm_eq_iSup, ENNReal.none_eq_top, conjneg, RCLike.norm_conj] exact (Equiv.neg _).iSup_congr fun _ ↦ rfl obtain rfl | hp := eq_or_ne p 0 - · simp only [nnLpNorm_exponent_zero, Ne, ENNReal.some_eq_coe, ENNReal.coe_zero, Nat.cast_inj] + · simp only [dLpNorm_exponent_zero, Ne, ENNReal.some_eq_coe, ENNReal.coe_zero, Nat.cast_inj] · simp only [dLpNorm_eq_sum hp, ENNReal.some_eq_coe] congr 1 exact Fintype.sum_equiv (Equiv.neg _) _ _ fun _ ↦ rfl @@ -110,8 +91,7 @@ lemma dLpNorm_translate_sum_sub_le [NormedAddCommGroup E] (hp : 1 ≤ p) {ι : T calc _ = ‖τ (∑ j ∈ s, a j) (τ (a i) f - f) + (τ (∑ j ∈ s, a j) f - f)‖_[p] := by rw [sum_cons, translate_add', translate_sub_right, sub_add_sub_cancel] - _ ≤ ‖τ (∑ j ∈ s, a j) (τ (a i) f - f)‖_[p] + ‖(τ (∑ j ∈ s, a j) f - f)‖_[p] := - dLpNorm_add_le hp _ _ + _ ≤ ‖τ (∑ j ∈ s, a j) (τ (a i) f - f)‖_[p] + ‖(τ (∑ j ∈ s, a j) f - f)‖_[p] := dLpNorm_add_le hp _ ≤ ‖τ (∑ j ∈ s, a j) (τ (a i) f - f)‖_[p] + ∑ j ∈ s, ‖(τ (a j) f - f)‖_[p] := add_le_add_left hs _ _ = _ := by rw [dLpNorm_translate, sum_cons] diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean index 8937b36142..1bd2e98203 100644 --- a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean +++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean @@ -11,7 +11,7 @@ import LeanAPAP.Prereqs.NNLpNorm -/ open Finset Function Real -open scoped ComplexConjugate ENNReal NNReal NNRat +open scoped BigOperators ComplexConjugate ENNReal NNReal NNRat variable {α 𝕜 R E : Type*} [MeasurableSpace α] @@ -38,6 +38,13 @@ notation "‖" f "‖_[" p "]" => dLpNorm p f lemma dLpNorm_sub_comm (f g : α → E) (p : ℝ≥0∞) : ‖f - g‖_[p] = ‖g - f‖_[p] := by simp [dLpNorm, nnLpNorm_sub_comm] +@[simp] lemma dLpNorm_norm (f : α → E) (p : ℝ≥0∞) : ‖fun i ↦ ‖f i‖‖_[p] = ‖f‖_[p] := + nnLpNorm_norm .. + +@[simp] lemma dLpNorm_abs (f : α → ℝ) (p : ℝ≥0∞) : ‖|f|‖_[p] = ‖f‖_[p] := nnLpNorm_abs .. +@[simp] lemma dLpNorm_abs' (f : α → ℝ) (p : ℝ≥0∞) : ‖fun i ↦ |f i|‖_[p] = ‖f‖_[p] := + nnLpNorm_abs' .. + section NormedField variable [NormedField 𝕜] {p : ℝ≥0∞} {f g : α → 𝕜} @@ -88,6 +95,10 @@ lemma dLpNorm_sub_le (hp : 1 ≤ p) : ‖f - g‖_[p] ≤ ‖f‖_[p] + ‖g‖_ lemma dLpNorm_sum_le {ι : Type*} {s : Finset ι} {f : ι → α → E} (hp : 1 ≤ p) : ‖∑ i ∈ s, f i‖_[p] ≤ ∑ i ∈ s, ‖f i‖_[p] := nnLpNorm_sum_le (fun _ _ ↦ .of_discrete) hp +lemma dLpNorm_expect_le [Module ℚ≥0 E] [NormedSpace ℝ E] {ι : Type*} {s : Finset ι} {f : ι → α → E} + (hp : 1 ≤ p) : ‖𝔼 i ∈ s, f i‖_[p] ≤ 𝔼 i ∈ s, ‖f i‖_[p] := + nnLpNorm_expect_le (fun _ _ ↦ .of_discrete) hp + lemma dLpNorm_le_dLpNorm_add_dLpNorm_sub' (hp : 1 ≤ p) : ‖f‖_[p] ≤ ‖g‖_[p] + ‖f - g‖_[p] := nnLpNorm_le_nnLpNorm_add_nnLpNorm_sub' .of_discrete .of_discrete hp @@ -159,26 +170,17 @@ lemma dL1Norm_eq_sum (f : α → E) : ‖f‖_[1] = ∑ i, ‖f i‖₊ := by si · simp · simp [dLpNorm, nnLinftyNorm_eq_essSup] -@[simp] lemma dLpNorm_norm (p : ℝ≥0∞) (f : α → E) : ‖fun i ↦ ‖f i‖‖_[p] = ‖f‖_[p] := by - obtain p | p := p; swap - obtain rfl | hp := @eq_zero_or_pos _ _ p - all_goals simp [dLinftyNorm_eq_iSup, nnLpNorm_exponent_zero, dLpNorm_eq_sum, *, ne_of_gt] - @[simp] lemma dLpNorm_eq_zero (hp : p ≠ 0) : ‖f‖_[p] = 0 ↔ f = 0 := by simp [dLpNorm, nnLpNorm_eq_zero .of_discrete hp, ae_eq_top.2] @[simp] lemma dLpNorm_pos (hp : p ≠ 0) : 0 < ‖f‖_[p] ↔ f ≠ 0 := pos_iff_ne_zero.trans (dLpNorm_eq_zero hp).not -lemma dLpNorm_mono_right (hpq : p ≤ q) (f : α → E) : ‖f‖_[p] ≤ ‖f‖_[q] := sorry +@[gcongr] lemma dLpNorm_mono_right (hpq : p ≤ q) : ‖f‖_[p] ≤ ‖f‖_[q] := sorry -section Real -variable {p : ℝ≥0} {f g : α → ℝ} +lemma dLpNorm_mono_real {g : α → ℝ} (h : ∀ x, ‖f x‖ ≤ g x) : ‖f‖_[p] ≤ ‖g‖_[p] := + nnLpNorm_mono_real .of_discrete h -lemma dLpNorm_mono (hf : 0 ≤ f) (hfg : f ≤ g) : ‖f‖_[p] ≤ ‖g‖_[p] := - nnLpNorm_mono_real .of_discrete fun i ↦ by simpa [norm_of_nonneg (hf i)] using hfg i - -end Real end MeasureTheory namespace Mathlib.Meta.Positivity @@ -246,9 +248,6 @@ section Real variable {α : Type*} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] {p q : ℝ≥0} {f g : α → ℝ} -@[simp] -lemma dLpNorm_abs (p : ℝ≥0∞) (f : α → ℝ) : ‖|f|‖_[p] = ‖f‖_[p] := by simpa using dLpNorm_norm p f - lemma dLpNorm_rpow (hp : p ≠ 0) (hq : q ≠ 0) (hf : 0 ≤ f) : ‖f ^ (q : ℝ)‖_[p] = ‖f‖_[p * q] ^ (q : ℝ) := by refine NNReal.rpow_left_injective (NNReal.coe_ne_zero.2 hp) ?_ @@ -291,12 +290,12 @@ lemma dLpNorm_rpow' (hp : p ≠ 0) (hq : q ≠ 0) (f : α → 𝕜) : end Hoelder section -variable {α : Type*} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] +variable {α : Type*} {mα : MeasurableSpace α} @[simp] -lemma RCLike.dLpNorm_coe_comp {𝕜 : Type*} [RCLike 𝕜] (p) (f : α → ℝ) : +lemma RCLike.dLpNorm_coe_comp [RCLike 𝕜] (p) (f : α → ℝ) : ‖((↑) : ℝ → 𝕜) ∘ f‖_[p] = ‖f‖_[p] := by - simp only [← dLpNorm_norm _ (((↑) : ℝ → 𝕜) ∘ f), ← dLpNorm_norm _ f, Function.comp_apply, + simp only [← dLpNorm_norm (((↑) : ℝ → 𝕜) ∘ f), ← dLpNorm_norm f, Function.comp_apply, RCLike.norm_ofReal, Real.norm_eq_abs] @[simp] lemma Complex.dLpNorm_coe_comp (p) (f : α → ℝ) : ‖((↑) : ℝ → ℂ) ∘ f‖_[p] = ‖f‖_[p] := diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Inner.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Inner.lean index 55dceec203..8cf59357fb 100644 --- a/LeanAPAP/Prereqs/LpNorm/Discrete/Inner.lean +++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Inner.lean @@ -6,128 +6,126 @@ import LeanAPAP.Prereqs.LpNorm.Discrete.Defs open Finset Function Real open scoped ComplexConjugate ENNReal NNReal NNRat -variable {ι 𝕜 R : Type*} [Fintype ι] - -/-! ### Lp norm -/ +variable {ι R S : Type*} [Fintype ι] namespace MeasureTheory section CommSemiring -variable [CommSemiring 𝕜] [StarRing 𝕜] {γ : Type*} [DistribSMul γ 𝕜] +variable [CommSemiring R] [StarRing R] [DistribSMul S R] /-- Inner product giving rise to the L2 norm. -/ -def l2Inner (f g : ι → 𝕜) : 𝕜 := ∑ i, conj (f i) * g i +def dL2Inner (f g : ι → R) : R := ∑ i, conj (f i) * g i -notation "⟪" f ", " g "⟫_[" 𝕜 "]" => @l2Inner _ 𝕜 _ _ _ f g +notation "⟪" f ", " g "⟫_[" S "]" => dL2Inner (R := S) f g -lemma l2Inner_eq_sum (f g : ι → 𝕜) : ⟪f, g⟫_[𝕜] = ∑ i, conj (f i) * g i := rfl +lemma dL2Inner_eq_sum (f g : ι → R) : ⟪f, g⟫_[R] = ∑ i, conj (f i) * g i := rfl -@[simp] lemma conj_l2Inner (f g : ι → 𝕜) : conj ⟪f, g⟫_[𝕜] = ⟪conj f, conj g⟫_[𝕜] := by - simp [l2Inner_eq_sum, map_sum] +@[simp] lemma conj_dL2Inner (f g : ι → R) : conj ⟪f, g⟫_[R] = ⟪conj f, conj g⟫_[R] := by + simp [dL2Inner_eq_sum, map_sum] -lemma l2Inner_anticomm (f g : ι → 𝕜) : ⟪f, g⟫_[𝕜] = ⟪conj g, conj f⟫_[𝕜] := by - simp [l2Inner_eq_sum, map_sum, mul_comm] +lemma dL2Inner_anticomm (f g : ι → R) : ⟪f, g⟫_[R] = ⟪conj g, conj f⟫_[R] := by + simp [dL2Inner_eq_sum, map_sum, mul_comm] -@[simp] lemma l2Inner_zero_left (g : ι → 𝕜) : ⟪0, g⟫_[𝕜] = 0 := by simp [l2Inner_eq_sum] -@[simp] lemma l2Inner_zero_right (f : ι → 𝕜) : ⟪f, 0⟫_[𝕜] = 0 := by simp [l2Inner_eq_sum] +@[simp] lemma dL2Inner_zero_left (g : ι → R) : ⟪0, g⟫_[R] = 0 := by simp [dL2Inner_eq_sum] +@[simp] lemma dL2Inner_zero_right (f : ι → R) : ⟪f, 0⟫_[R] = 0 := by simp [dL2Inner_eq_sum] -@[simp] lemma l2Inner_of_isEmpty [IsEmpty ι] (f g : ι → 𝕜) : ⟪f, g⟫_[𝕜] = 0 := by +@[simp] lemma dL2Inner_of_isEmpty [IsEmpty ι] (f g : ι → R) : ⟪f, g⟫_[R] = 0 := by simp [Subsingleton.elim f 0] -@[simp] lemma l2Inner_const_left (a : 𝕜) (f : ι → 𝕜) : ⟪const _ a, f⟫_[𝕜] = conj a * ∑ x, f x := by - simp only [l2Inner_eq_sum, const_apply, mul_sum] +@[simp] lemma dL2Inner_const_left (a : R) (f : ι → R) : ⟪const _ a, f⟫_[R] = conj a * ∑ x, f x := by + simp only [dL2Inner_eq_sum, const_apply, mul_sum] @[simp] -lemma l2Inner_const_right (f : ι → 𝕜) (a : 𝕜) : ⟪f, const _ a⟫_[𝕜] = (∑ x, conj (f x)) * a := by - simp only [l2Inner_eq_sum, const_apply, sum_mul] +lemma dL2Inner_const_right (f : ι → R) (a : R) : ⟪f, const _ a⟫_[R] = (∑ x, conj (f x)) * a := by + simp only [dL2Inner_eq_sum, const_apply, sum_mul] -lemma l2Inner_add_left (f₁ f₂ g : ι → 𝕜) : ⟪f₁ + f₂, g⟫_[𝕜] = ⟪f₁, g⟫_[𝕜] + ⟪f₂, g⟫_[𝕜] := by - simp_rw [l2Inner_eq_sum, Pi.add_apply, map_add, add_mul, sum_add_distrib] +lemma dL2Inner_add_left (f₁ f₂ g : ι → R) : ⟪f₁ + f₂, g⟫_[R] = ⟪f₁, g⟫_[R] + ⟪f₂, g⟫_[R] := by + simp_rw [dL2Inner_eq_sum, Pi.add_apply, map_add, add_mul, sum_add_distrib] -lemma l2Inner_add_right (f g₁ g₂ : ι → 𝕜) : ⟪f, g₁ + g₂⟫_[𝕜] = ⟪f, g₁⟫_[𝕜] + ⟪f, g₂⟫_[𝕜] := by - simp_rw [l2Inner_eq_sum, Pi.add_apply, mul_add, sum_add_distrib] +lemma dL2Inner_add_right (f g₁ g₂ : ι → R) : ⟪f, g₁ + g₂⟫_[R] = ⟪f, g₁⟫_[R] + ⟪f, g₂⟫_[R] := by + simp_rw [dL2Inner_eq_sum, Pi.add_apply, mul_add, sum_add_distrib] -lemma l2Inner_smul_left [Star γ] [StarModule γ 𝕜] [IsScalarTower γ 𝕜 𝕜] (c : γ) (f g : ι → 𝕜) : - ⟪c • f, g⟫_[𝕜] = star c • ⟪f, g⟫_[𝕜] := by - simp only [l2Inner_eq_sum, Pi.smul_apply, smul_mul_assoc, smul_sum, starRingEnd_apply, star_smul] +lemma dL2Inner_smul_left [Star S] [StarModule S R] [IsScalarTower S R R] (c : S) (f g : ι → R) : + ⟪c • f, g⟫_[R] = star c • ⟪f, g⟫_[R] := by + simp only [dL2Inner_eq_sum, Pi.smul_apply, smul_mul_assoc, smul_sum, starRingEnd_apply, star_smul] -lemma l2Inner_smul_right [Star γ] [StarModule γ 𝕜] [SMulCommClass γ 𝕜 𝕜] (c : γ) (f g : ι → 𝕜) : - ⟪f, c • g⟫_[𝕜] = c • ⟪f, g⟫_[𝕜] := by - simp only [l2Inner_eq_sum, Pi.smul_apply, mul_smul_comm, smul_sum, starRingEnd_apply, star_smul] +lemma dL2Inner_smul_right [Star S] [StarModule S R] [SMulCommClass S R R] (c : S) (f g : ι → R) : + ⟪f, c • g⟫_[R] = c • ⟪f, g⟫_[R] := by + simp only [dL2Inner_eq_sum, Pi.smul_apply, mul_smul_comm, smul_sum, starRingEnd_apply, star_smul] -lemma smul_l2Inner_left [InvolutiveStar γ] [StarModule γ 𝕜] [IsScalarTower γ 𝕜 𝕜] (c : γ) - (f g : ι → 𝕜) : c • ⟪f, g⟫_[𝕜] = ⟪star c • f, g⟫_[𝕜] := by rw [l2Inner_smul_left, star_star] +lemma smul_dL2Inner_left [InvolutiveStar S] [StarModule S R] [IsScalarTower S R R] (c : S) + (f g : ι → R) : c • ⟪f, g⟫_[R] = ⟪star c • f, g⟫_[R] := by rw [dL2Inner_smul_left, star_star] end CommSemiring section CommRing -variable [CommRing 𝕜] [StarRing 𝕜] +variable [CommRing R] [StarRing R] @[simp] -lemma l2Inner_neg_left (f g : ι → 𝕜) : ⟪-f, g⟫_[𝕜] = -⟪f, g⟫_[𝕜] := by simp [l2Inner_eq_sum] +lemma dL2Inner_neg_left (f g : ι → R) : ⟪-f, g⟫_[R] = -⟪f, g⟫_[R] := by simp [dL2Inner_eq_sum] @[simp] -lemma l2Inner_neg_right (f g : ι → 𝕜) : ⟪f, -g⟫_[𝕜] = -⟪f, g⟫_[𝕜] := by simp [l2Inner_eq_sum] +lemma dL2Inner_neg_right (f g : ι → R) : ⟪f, -g⟫_[R] = -⟪f, g⟫_[R] := by simp [dL2Inner_eq_sum] -lemma l2Inner_sub_left (f₁ f₂ g : ι → 𝕜) : ⟪f₁ - f₂, g⟫_[𝕜] = ⟪f₁, g⟫_[𝕜] - ⟪f₂, g⟫_[𝕜] := by - simp_rw [sub_eq_add_neg, l2Inner_add_left, l2Inner_neg_left] +lemma dL2Inner_sub_left (f₁ f₂ g : ι → R) : ⟪f₁ - f₂, g⟫_[R] = ⟪f₁, g⟫_[R] - ⟪f₂, g⟫_[R] := by + simp_rw [sub_eq_add_neg, dL2Inner_add_left, dL2Inner_neg_left] -lemma l2Inner_sub_right (f g₁ g₂ : ι → 𝕜) : ⟪f, g₁ - g₂⟫_[𝕜] = ⟪f, g₁⟫_[𝕜] - ⟪f, g₂⟫_[𝕜] := by - simp_rw [sub_eq_add_neg, l2Inner_add_right, l2Inner_neg_right] +lemma dL2Inner_sub_right (f g₁ g₂ : ι → R) : ⟪f, g₁ - g₂⟫_[R] = ⟪f, g₁⟫_[R] - ⟪f, g₂⟫_[R] := by + simp_rw [sub_eq_add_neg, dL2Inner_add_right, dL2Inner_neg_right] end CommRing section OrderedCommSemiring -variable [OrderedCommSemiring 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] {f g : ι → 𝕜} +variable [OrderedCommSemiring R] [StarRing R] [StarOrderedRing R] {f g : ι → R} -lemma l2Inner_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[𝕜] := +lemma dL2Inner_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[R] := sum_nonneg fun _ _ ↦ mul_nonneg (star_nonneg_iff.2 $ hf _) $ hg _ end OrderedCommSemiring section LinearOrderedCommRing -variable [LinearOrderedCommRing 𝕜] [StarRing 𝕜] [TrivialStar 𝕜] {f g : ι → 𝕜} +variable [LinearOrderedCommRing R] [StarRing R] [TrivialStar R] {f g : ι → R} --TODO: Can we remove the `TrivialStar` assumption? -lemma abs_l2Inner_le_l2Inner_abs : |⟪f, g⟫_[𝕜]| ≤ ⟪|f|, |g|⟫_[𝕜] := +lemma abs_dL2Inner_le_dL2Inner_abs : |⟪f, g⟫_[R]| ≤ ⟪|f|, |g|⟫_[R] := (abs_sum_le_sum_abs _ _).trans_eq $ sum_congr rfl fun i _ ↦ by simp only [abs_mul, conj_trivial, Pi.abs_apply] end LinearOrderedCommRing section RCLike -variable {κ : Type*} [RCLike 𝕜] {f : ι → 𝕜} +variable {κ : Type*} [RCLike R] {f : ι → R} -lemma l2Inner_eq_inner (f g : ι → 𝕜) : - ⟪f, g⟫_[𝕜] = inner ((WithLp.equiv 2 _).symm f) ((WithLp.equiv 2 _).symm g) := rfl +lemma dL2Inner_eq_inner (f g : ι → R) : + ⟪f, g⟫_[R] = inner ((WithLp.equiv 2 _).symm f) ((WithLp.equiv 2 _).symm g) := rfl -lemma inner_eq_l2Inner (f g : PiLp 2 fun _i : ι ↦ 𝕜) : - inner f g = ⟪WithLp.equiv 2 _ f, WithLp.equiv 2 _ g⟫_[𝕜] := rfl +lemma inner_eq_dL2Inner (f g : PiLp 2 fun _i : ι ↦ R) : + inner f g = ⟪WithLp.equiv 2 _ f, WithLp.equiv 2 _ g⟫_[R] := rfl -@[simp] lemma l2Inner_self {_ : MeasurableSpace ι} [DiscreteMeasurableSpace ι] (f : ι → 𝕜) : - ⟪f, f⟫_[𝕜] = ((‖f‖_[2] : ℝ) : 𝕜) ^ 2 := by +@[simp] lemma dL2Inner_self {_ : MeasurableSpace ι} [DiscreteMeasurableSpace ι] (f : ι → R) : + ⟪f, f⟫_[R] = ((‖f‖_[2] : ℝ) : R) ^ 2 := by simp_rw [← algebraMap.coe_pow, ← NNReal.coe_pow] - simp [dL2Norm_sq_eq_sum, l2Inner_eq_sum, RCLike.conj_mul] + simp [dL2Norm_sq_eq_sum, dL2Inner_eq_sum, RCLike.conj_mul] -lemma l2Inner_self_of_norm_eq_one (hf : ∀ x, ‖f x‖ = 1) : ⟪f, f⟫_[𝕜] = Fintype.card ι := by - simp [-l2Inner_self, l2Inner_eq_sum, RCLike.conj_mul, hf, card_univ] +lemma dL2Inner_self_of_norm_eq_one (hf : ∀ x, ‖f x‖ = 1) : ⟪f, f⟫_[R] = Fintype.card ι := by + simp [-dL2Inner_self, dL2Inner_eq_sum, RCLike.conj_mul, hf, card_univ] -lemma linearIndependent_of_ne_zero_of_l2Inner_eq_zero {v : κ → ι → 𝕜} (hz : ∀ k, v k ≠ 0) - (ho : Pairwise fun k l ↦ ⟪v k, v l⟫_[𝕜] = 0) : LinearIndependent 𝕜 v := by - simp_rw [l2Inner_eq_inner] at ho +lemma linearIndependent_of_ne_zero_of_dL2Inner_eq_zero {v : κ → ι → R} (hz : ∀ k, v k ≠ 0) + (ho : Pairwise fun k l ↦ ⟪v k, v l⟫_[R] = 0) : LinearIndependent R v := by + simp_rw [dL2Inner_eq_inner] at ho have := linearIndependent_of_ne_zero_of_inner_eq_zero ?_ ho exacts [this, hz] variable {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] -lemma dL1Norm_mul (f g : ι → 𝕜) : ‖f * g‖_[1] = ⟪fun i ↦ ‖f i‖, fun i ↦ ‖g i‖⟫_[ℝ] := by - simp [l2Inner_eq_sum, dL1Norm_eq_sum] +lemma dL1Norm_mul (f g : ι → R) : ‖f * g‖_[1] = ⟪fun i ↦ ‖f i‖, fun i ↦ ‖g i‖⟫_[ℝ] := by + simp [dL2Inner_eq_sum, dL1Norm_eq_sum] end RCLike variable {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] /-- **Cauchy-Schwarz inequality** -/ -lemma l2Inner_le_dL2Norm_mul_dL2Norm (f g : ι → ℝ) : ⟪f, g⟫_[ℝ] ≤ ‖f‖_[2] * ‖g‖_[2] := by +lemma dL2Inner_le_dL2Norm_mul_dL2Norm (f g : ι → ℝ) : ⟪f, g⟫_[ℝ] ≤ ‖f‖_[2] * ‖g‖_[2] := by simpa [dL2Norm_eq_sum, PiLp.norm_eq_of_L2, sqrt_eq_rpow] using real_inner_le_norm ((WithLp.equiv 2 _).symm f) _ @@ -137,44 +135,44 @@ namespace Mathlib.Meta.Positivity open Lean Meta Qq Function MeasureTheory section OrderedCommSemiring -variable [OrderedCommSemiring 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] {f g : ι → 𝕜} +variable [OrderedCommSemiring R] [StarRing R] [StarOrderedRing R] {f g : ι → R} -private lemma l2Inner_nonneg_of_pos_of_nonneg (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[𝕜] := - l2Inner_nonneg hf.le hg +private lemma dL2Inner_nonneg_of_pos_of_nonneg (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[R] := + dL2Inner_nonneg hf.le hg -private lemma l2Inner_nonneg_of_nonneg_of_pos (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫_[𝕜] := - l2Inner_nonneg hf hg.le +private lemma dL2Inner_nonneg_of_nonneg_of_pos (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫_[R] := + dL2Inner_nonneg hf hg.le -private lemma l2Inner_nonneg_of_pos_of_pos (hf : 0 < f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫_[𝕜] := - l2Inner_nonneg hf.le hg.le +private lemma dL2Inner_nonneg_of_pos_of_pos (hf : 0 < f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫_[R] := + dL2Inner_nonneg hf.le hg.le end OrderedCommSemiring -/-- The `positivity` extension which identifies expressions of the form `⟪f, g⟫_[𝕜]`. -/ -@[positivity ⟪_, _⟫_[_]] def evalL2Inner : PositivityExt where eval {u 𝕜} _ _ e := do +/-- The `positivity` extension which identifies expressions of the form `⟪f, g⟫_[R]`. -/ +@[positivity ⟪_, _⟫_[_]] def evalL2Inner : PositivityExt where eval {u R} _ _ e := do match e with - | ~q(@l2Inner $ι _ $instι $instring $inststar $f $g) => - let _p𝕜 ← synthInstanceQ q(OrderedCommSemiring $𝕜) - let _p𝕜 ← synthInstanceQ q(StarOrderedRing $𝕜) + | ~q(@dL2Inner $ι _ $instι $instring $inststar $f $g) => + let _p𝕜 ← synthInstanceQ q(OrderedCommSemiring $R) + let _p𝕜 ← synthInstanceQ q(StarOrderedRing $R) assumeInstancesCommute match ← core q(inferInstance) q(inferInstance) f, ← core q(inferInstance) q(inferInstance) g with - | .positive pf, .positive pg => return .nonnegative q(l2Inner_nonneg_of_pos_of_pos $pf $pg) + | .positive pf, .positive pg => return .nonnegative q(dL2Inner_nonneg_of_pos_of_pos $pf $pg) | .positive pf, .nonnegative pg => - return .nonnegative q(l2Inner_nonneg_of_pos_of_nonneg $pf $pg) + return .nonnegative q(dL2Inner_nonneg_of_pos_of_nonneg $pf $pg) | .nonnegative pf, .positive pg => - return .nonnegative q(l2Inner_nonneg_of_nonneg_of_pos $pf $pg) - | .nonnegative pf, .nonnegative pg => return .nonnegative q(l2Inner_nonneg $pf $pg) + return .nonnegative q(dL2Inner_nonneg_of_nonneg_of_pos $pf $pg) + | .nonnegative pf, .nonnegative pg => return .nonnegative q(dL2Inner_nonneg $pf $pg) | _, _ => return .none - | _ => throwError "not l2Inner" + | _ => throwError "not dL2Inner" section OrderedCommSemiring -variable [OrderedCommSemiring 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] {f g : ι → 𝕜} +variable [OrderedCommSemiring R] [StarRing R] [StarOrderedRing R] {f g : ι → R} -example (hf : 0 < f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫_[𝕜] := by positivity -example (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[𝕜] := by positivity -example (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫_[𝕜] := by positivity -example (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[𝕜] := by positivity +example (hf : 0 < f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫_[R] := by positivity +example (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[R] := by positivity +example (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫_[R] := by positivity +example (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[R] := by positivity end OrderedCommSemiring end Mathlib.Meta.Positivity @@ -190,38 +188,38 @@ lemma dL1Norm_mul_of_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : ‖f * g‖_[1] = convert dL1Norm_mul f g using 2 <;> ext a <;> refine (norm_of_nonneg ?_).symm; exacts [hf _, hg _] /-- **Hölder's inequality**, binary case. -/ -lemma l2Inner_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) : +lemma dL2Inner_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) : ⟪f, g⟫_[ℝ] ≤ ‖f‖_[p] * ‖g‖_[q] := by have hp := hpq.ne_zero have hq := hpq.symm.ne_zero norm_cast at hp hq - simpa [l2Inner_eq_sum, dLpNorm_eq_sum, *] using inner_le_Lp_mul_Lq _ f g hpq.coe + simpa [dL2Inner_eq_sum, dLpNorm_eq_sum, *] using inner_le_Lp_mul_Lq _ f g hpq.coe /-- **Hölder's inequality**, binary case. -/ -lemma abs_l2Inner_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) : +lemma abs_dL2Inner_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) : |⟪f, g⟫_[ℝ]| ≤ ‖f‖_[p] * ‖g‖_[q] := - abs_l2Inner_le_l2Inner_abs.trans $ - (l2Inner_le_dLpNorm_mul_dLpNorm hpq _ _).trans_eq $ by simp_rw [dLpNorm_abs] + abs_dL2Inner_le_dL2Inner_abs.trans $ + (dL2Inner_le_dLpNorm_mul_dLpNorm hpq _ _).trans_eq $ by simp_rw [dLpNorm_abs] end Real section Hoelder -variable {α : Type*} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] [RCLike 𝕜] - {p q : ℝ≥0} {f g : α → 𝕜} +variable {α : Type*} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] [RCLike R] + {p q : ℝ≥0} {f g : α → R} -lemma norm_l2Inner_le (f g : α → 𝕜) : ‖⟪f, g⟫_[𝕜]‖₊ ≤ ⟪fun a ↦ ‖f a‖, fun a ↦ ‖g a‖⟫_[ℝ] := - (norm_sum_le _ _).trans $ by simp [l2Inner] +lemma norm_dL2Inner_le (f g : α → R) : ‖⟪f, g⟫_[R]‖₊ ≤ ⟪fun a ↦ ‖f a‖, fun a ↦ ‖g a‖⟫_[ℝ] := + (norm_sum_le _ _).trans $ by simp [dL2Inner] /-- **Hölder's inequality**, binary case. -/ -lemma norm_l2Inner_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → 𝕜) : - ‖⟪f, g⟫_[𝕜]‖₊ ≤ ‖f‖_[p] * ‖g‖_[q] := +lemma norm_dL2Inner_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → R) : + ‖⟪f, g⟫_[R]‖₊ ≤ ‖f‖_[p] * ‖g‖_[q] := calc - _ ≤ ⟪fun a ↦ ‖f a‖, fun a ↦ ‖g a‖⟫_[ℝ] := norm_l2Inner_le _ _ - _ ≤ ‖fun a ↦ ‖f a‖‖_[p] * ‖fun a ↦ ‖g a‖‖_[q] := l2Inner_le_dLpNorm_mul_dLpNorm hpq _ _ + _ ≤ ⟪fun a ↦ ‖f a‖, fun a ↦ ‖g a‖⟫_[ℝ] := norm_dL2Inner_le _ _ + _ ≤ ‖fun a ↦ ‖f a‖‖_[p] * ‖fun a ↦ ‖g a‖‖_[q] := dL2Inner_le_dLpNorm_mul_dLpNorm hpq _ _ _ = ‖f‖_[p] * ‖g‖_[q] := by simp_rw [dLpNorm_norm] /-- **Hölder's inequality**, binary case. -/ -lemma dLpNorm_mul_le (hp : p ≠ 0) (hq : q ≠ 0) (r : ℝ≥0) (hpqr : p⁻¹ + q⁻¹ = r⁻¹) (f g : α → 𝕜) : +lemma dLpNorm_mul_le (hp : p ≠ 0) (hq : q ≠ 0) (r : ℝ≥0) (hpqr : p⁻¹ + q⁻¹ = r⁻¹) (f g : α → R) : ‖f * g‖_[r] ≤ ‖f‖_[p] * ‖g‖_[q] := by have hr : r ≠ 0 := by rintro rfl @@ -232,7 +230,7 @@ lemma dLpNorm_mul_le (hp : p ≠ 0) (hq : q ≠ 0) (r : ℝ≥0) (hpqr : p⁻¹ push_cast rw [dL1Norm_mul_of_nonneg, mul_rpow, ← NNReal.coe_rpow, ← NNReal.coe_rpow, dLpNorm_rpow', dLpNorm_rpow', ← ENNReal.coe_div, ← ENNReal.coe_div] - refine l2Inner_le_dLpNorm_mul_dLpNorm ⟨?_, ?_⟩ _ _ + refine dL2Inner_le_dLpNorm_mul_dLpNorm ⟨?_, ?_⟩ _ _ · norm_cast rw [div_eq_mul_inv, ← hpqr, mul_add, mul_inv_cancel₀ hp] exact lt_add_of_pos_right _ (by positivity) @@ -242,7 +240,7 @@ lemma dLpNorm_mul_le (hp : p ≠ 0) (hq : q ≠ 0) (r : ℝ≥0) (hpqr : p⁻¹ all_goals positivity /-- **Hölder's inequality**, binary case. -/ -lemma dL1Norm_mul_le (hpq : p.IsConjExponent q) (f g : α → 𝕜) : +lemma dL1Norm_mul_le (hpq : p.IsConjExponent q) (f g : α → R) : ‖f * g‖_[1] ≤ ‖f‖_[p] * ‖g‖_[q] := dLpNorm_mul_le (mod_cast hpq.ne_zero) (mod_cast hpq.symm.ne_zero) _ (by simpa using hpq.inv_add_inv_conj) _ _ @@ -250,7 +248,7 @@ lemma dL1Norm_mul_le (hpq : p.IsConjExponent q) (f g : α → 𝕜) : /-- **Hölder's inequality**, finitary case. -/ lemma dLpNorm_prod_le {ι : Type*} {s : Finset ι} (hs : s.Nonempty) {p : ι → ℝ≥0} (hp : ∀ i, p i ≠ 0) (q : ℝ≥0) - (hpq : ∑ i in s, (p i)⁻¹ = q⁻¹) (f : ι → α → 𝕜) : + (hpq : ∑ i in s, (p i)⁻¹ = q⁻¹) (f : ι → α → R) : ‖∏ i in s, f i‖_[q] ≤ ∏ i in s, ‖f i‖_[p i] := by induction' s using Finset.cons_induction with i s hi ih generalizing q · cases not_nonempty_empty hs diff --git a/LeanAPAP/Prereqs/LpNorm/Weighted.lean b/LeanAPAP/Prereqs/LpNorm/Weighted.lean index f12f7af549..f1c1306131 100644 --- a/LeanAPAP/Prereqs/LpNorm/Weighted.lean +++ b/LeanAPAP/Prereqs/LpNorm/Weighted.lean @@ -30,7 +30,7 @@ lemma wLpNorm_sub_comm (w : α → ℝ≥0) (f g : α → E) : ‖f - g‖_[p, w simp [wLpNorm, nnLpNorm_sub_comm] @[simp] lemma wLpNorm_one_eq_dLpNorm (p : ℝ≥0) (f : α → E) : ‖f‖_[p, 1] = ‖f‖_[p] := by - simp [wLpNorm, nnLpNorm, Measure.count] + simp [wLpNorm, dLpNorm, nnLpNorm, Measure.count] @[simp] lemma wLpNorm_exponent_zero (w : α → ℝ≥0) (f : α → E) : ‖f‖_[0, w] = 0 := by simp [wLpNorm] @@ -38,10 +38,10 @@ lemma wLpNorm_sub_comm (w : α → ℝ≥0) (f g : α → E) : ‖f - g‖_[p, w simp [wLpNorm] lemma wLpNorm_smul [NormedField 𝕜] [NormedSpace 𝕜 E] (c : 𝕜) (f : α → E) (p : ℝ≥0∞) (w : α → ℝ≥0) : - ‖c • f‖_[p, w] = ‖c‖₊ * ‖f‖_[p, w] := nnLpNorm_const_smul _ _ _ + ‖c • f‖_[p, w] = ‖c‖₊ * ‖f‖_[p, w] := nnLpNorm_const_smul .. lemma wLpNorm_nsmul [NormedSpace ℝ E] (n : ℕ) (f : α → E) (p : ℝ≥0∞) (w : α → ℝ≥0) : - ‖n • f‖_[p, w] = n • ‖f‖_[p, w] := nnLpNorm_nsmul _ _ _ + ‖n • f‖_[p, w] = n • ‖f‖_[p, w] := nnLpNorm_nsmul .. section RCLike variable {K : Type*} [RCLike K] @@ -60,7 +60,7 @@ variable [Fintype α] @[simp] lemma wLpNorm_const_right (hp : p ≠ ∞) (w : ℝ≥0) (f : α → E) : ‖f‖_[p, const _ w] = w ^ p.toReal⁻¹ * ‖f‖_[p] := by - simp [wLpNorm, ← Finset.smul_sum, nnLpNorm_smul_measure_of_ne_top hp, Measure.count] + simp [wLpNorm, dLpNorm, ← Finset.smul_sum, nnLpNorm_smul_measure_of_ne_top hp, Measure.count] @[simp] lemma wLpNorm_smul_right (hp : p ≠ ⊤) (c : ℝ≥0) (f : α → E) : ‖f‖_[p, c • w] = c ^ p.toReal⁻¹ * ‖f‖_[p, w] := by @@ -106,7 +106,7 @@ lemma wLpNorm_le_wLpNorm_add_wLpNorm_sub' (hp : 1 ≤ p) (w : α → ℝ≥0) (f lemma wLpNorm_le_wLpNorm_add_wLpNorm_sub (hp : 1 ≤ p) (w : α → ℝ≥0) (f g : α → E) : ‖f‖_[p, w] ≤ ‖g‖_[p, w] + ‖g - f‖_[p, w] := by - rw [wLpNorm_sub_comm]; exact wLpNorm_le_wLpNorm_add_wLpNorm_sub' hp _ _ _ + rw [wLpNorm_sub_comm]; exact wLpNorm_le_wLpNorm_add_wLpNorm_sub' hp .. lemma wLpNorm_le_add_wLpNorm_add (hp : 1 ≤ p) (w : α → ℝ≥0) (f g : α → E) : ‖f‖_[p, w] ≤ ‖f + g‖_[p, w] + ‖g‖_[p, w] := by simpa using wLpNorm_add_le hp w (f + g) (-g) diff --git a/LeanAPAP/Prereqs/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean index dc5931b23e..ef78924492 100644 --- a/LeanAPAP/Prereqs/NNLpNorm.lean +++ b/LeanAPAP/Prereqs/NNLpNorm.lean @@ -1,11 +1,13 @@ +import Mathlib.Analysis.Normed.Group.Constructions import Mathlib.MeasureTheory.Integral.Bochner import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal import LeanAPAP.Mathlib.Data.ENNReal.Basic import LeanAPAP.Mathlib.Data.ENNReal.Operations import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic +import LeanAPAP.Prereqs.Expect.Basic open Filter -open scoped ENNReal NNReal ComplexConjugate +open scoped BigOperators ComplexConjugate ENNReal NNReal namespace MeasureTheory variable {α E : Type*} {m : MeasurableSpace α} {p : ℝ≥0∞} {q : ℝ} {μ ν : Measure α} @@ -72,42 +74,14 @@ lemma nnLpNorm_eq_zero (hf : Memℒp f p μ) (hp : p ≠ 0) : nnLpNorm f p μ = lemma nnLpNorm_sub_comm (f g : α → E) (p : ℝ≥0∞) (μ : Measure α) : nnLpNorm (f - g) p μ = nnLpNorm (g - f) p μ := by simp [nnLpNorm, eLpNorm_sub_comm] -lemma nnLpNorm_add_le (hf : Memℒp f p μ) (hg : Memℒp g p μ) (hp : 1 ≤ p) : - nnLpNorm (f + g) p μ ≤ nnLpNorm f p μ + nnLpNorm g p μ := by - unfold nnLpNorm - rw [← ENNReal.toNNReal_add hf.eLpNorm_ne_top hg.eLpNorm_ne_top] - gcongr - exacts [ENNReal.add_ne_top.2 ⟨hf.eLpNorm_ne_top, hg.eLpNorm_ne_top⟩, - eLpNorm_add_le hf.aestronglyMeasurable hg.aestronglyMeasurable hp] - -lemma nnLpNorm_sub_le (hf : Memℒp f p μ) (hg : Memℒp g p μ) (hp : 1 ≤ p) : - nnLpNorm (f - g) p μ ≤ nnLpNorm f p μ + nnLpNorm g p μ := by - simpa [sub_eq_add_neg] using nnLpNorm_add_le hf hg.neg hp - -lemma nnLpNorm_le_nnLpNorm_add_nnLpNorm_sub' (hf : Memℒp f p μ) (hg : Memℒp g p μ) (hp : 1 ≤ p) : - nnLpNorm f p μ ≤ nnLpNorm g p μ + nnLpNorm (f - g) p μ := by - simpa using nnLpNorm_add_le hg (hf.sub hg) hp - -lemma nnLpNorm_le_nnLpNorm_add_nnLpNorm_sub (hf : Memℒp f p μ) (hg : Memℒp g p μ) (hp : 1 ≤ p) : - nnLpNorm f p μ ≤ nnLpNorm g p μ + nnLpNorm (g - f) p μ := by - simpa [neg_add_eq_sub] using nnLpNorm_add_le hg.neg (hg.sub hf) hp - -lemma nnLpNorm_le_add_nnLpNorm_add (hf : Memℒp f p μ) (hg : Memℒp g p μ) (hp : 1 ≤ p) : - nnLpNorm f p μ ≤ nnLpNorm (f + g) p μ + nnLpNorm g p μ := by - simpa using nnLpNorm_add_le (hf.add hg) hg.neg hp +@[simp] lemma nnLpNorm_norm (f : α → E) (p : ℝ≥0∞) : + nnLpNorm (fun x ↦ ‖f x‖) p μ = nnLpNorm f p μ := by simp [nnLpNorm] -lemma nnLpNorm_sub_le_nnLpNorm_sub_add_nnLpNorm_sub (hf : Memℒp f p μ) (hg : Memℒp g p μ) - (hh : Memℒp h p μ) (hp : 1 ≤ p) : - nnLpNorm (f - h) p μ ≤ nnLpNorm (f - g) p μ + nnLpNorm (g - h) p μ := by - simpa using nnLpNorm_add_le (hf.sub hg) (hg.sub hh) hp +@[simp] lemma nnLpNorm_abs (f : α → ℝ) (p : ℝ≥0∞) : nnLpNorm (|f|) p μ = nnLpNorm f p μ := + nnLpNorm_norm f p -lemma nnLpNorm_sum_le {ι : Type*} {s : Finset ι} {f : ι → α → E} (hf : ∀ i ∈ s, Memℒp (f i) p μ) - (hp : 1 ≤ p) : nnLpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, nnLpNorm (f i) p μ := by - unfold nnLpNorm - rw [← ENNReal.toNNReal_sum fun i hi ↦ (hf _ hi).eLpNorm_ne_top] - gcongr - exacts [ENNReal.sum_ne_top.2 fun i hi ↦ (hf _ hi).eLpNorm_ne_top, - eLpNorm_sum_le (fun i hi ↦ (hf _ hi).aestronglyMeasurable) hp] +@[simp] lemma nnLpNorm_abs' (f : α → ℝ) (p : ℝ≥0∞) : + nnLpNorm (fun x ↦ |f x|) p μ = nnLpNorm f p μ := nnLpNorm_abs .. @[simp] lemma nnLpNorm_const (hp : p ≠ 0) (hμ : μ ≠ 0) (c : E) : nnLpNorm (fun _x ↦ c) p μ = ‖c‖₊ * (μ Set.univ).toNNReal ^ p.toReal⁻¹ := by @@ -150,7 +124,7 @@ lemma nnLpNorm_mul_natCast (f : α → 𝕜) (n : ℕ) (p : ℝ≥0∞) (μ : Me lemma nnLpNorm_mul_natCast' (f : α → 𝕜) (n : ℕ) (p : ℝ≥0∞) (μ : Measure α) : nnLpNorm (f · * n) p μ = nnLpNorm f p μ * n := nnLpNorm_mul_natCast .. -lemma nnLpNorm_div_natCast [CharZero 𝕜] {n : ℕ} (hn : n ≠ 0) (f : α → 𝕜) (p : ℝ≥0∞) +lemma nnLpNorm_div_natCast [CharZero 𝕜] {n : ℕ} (hn : n ≠ 0) (f : α → 𝕜) (p : ℝ≥0∞) (μ : Measure α) : nnLpNorm (f / (n : α → 𝕜)) p μ = nnLpNorm f p μ / n := by rw [eq_div_iff (by positivity), ← nnLpNorm_mul_natCast]; simp [Pi.mul_def, hn] @@ -159,6 +133,52 @@ lemma nnLpNorm_div_natCast' [CharZero 𝕜] {n : ℕ} (hn : n ≠ 0) (f : α → end NormedField +lemma nnLpNorm_add_le (hf : Memℒp f p μ) (hg : Memℒp g p μ) (hp : 1 ≤ p) : + nnLpNorm (f + g) p μ ≤ nnLpNorm f p μ + nnLpNorm g p μ := by + unfold nnLpNorm + rw [← ENNReal.toNNReal_add hf.eLpNorm_ne_top hg.eLpNorm_ne_top] + gcongr + exacts [ENNReal.add_ne_top.2 ⟨hf.eLpNorm_ne_top, hg.eLpNorm_ne_top⟩, + eLpNorm_add_le hf.aestronglyMeasurable hg.aestronglyMeasurable hp] + +lemma nnLpNorm_sub_le (hf : Memℒp f p μ) (hg : Memℒp g p μ) (hp : 1 ≤ p) : + nnLpNorm (f - g) p μ ≤ nnLpNorm f p μ + nnLpNorm g p μ := by + simpa [sub_eq_add_neg] using nnLpNorm_add_le hf hg.neg hp + +lemma nnLpNorm_le_nnLpNorm_add_nnLpNorm_sub' (hf : Memℒp f p μ) (hg : Memℒp g p μ) (hp : 1 ≤ p) : + nnLpNorm f p μ ≤ nnLpNorm g p μ + nnLpNorm (f - g) p μ := by + simpa using nnLpNorm_add_le hg (hf.sub hg) hp + +lemma nnLpNorm_le_nnLpNorm_add_nnLpNorm_sub (hf : Memℒp f p μ) (hg : Memℒp g p μ) (hp : 1 ≤ p) : + nnLpNorm f p μ ≤ nnLpNorm g p μ + nnLpNorm (g - f) p μ := by + simpa [neg_add_eq_sub] using nnLpNorm_add_le hg.neg (hg.sub hf) hp + +lemma nnLpNorm_le_add_nnLpNorm_add (hf : Memℒp f p μ) (hg : Memℒp g p μ) (hp : 1 ≤ p) : + nnLpNorm f p μ ≤ nnLpNorm (f + g) p μ + nnLpNorm g p μ := by + simpa using nnLpNorm_add_le (hf.add hg) hg.neg hp + +lemma nnLpNorm_sub_le_nnLpNorm_sub_add_nnLpNorm_sub (hf : Memℒp f p μ) (hg : Memℒp g p μ) + (hh : Memℒp h p μ) (hp : 1 ≤ p) : + nnLpNorm (f - h) p μ ≤ nnLpNorm (f - g) p μ + nnLpNorm (g - h) p μ := by + simpa using nnLpNorm_add_le (hf.sub hg) (hg.sub hh) hp + +lemma nnLpNorm_sum_le {ι : Type*} {s : Finset ι} {f : ι → α → E} (hf : ∀ i ∈ s, Memℒp (f i) p μ) + (hp : 1 ≤ p) : nnLpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, nnLpNorm (f i) p μ := by + unfold nnLpNorm + rw [← ENNReal.toNNReal_sum fun i hi ↦ (hf _ hi).eLpNorm_ne_top] + gcongr + exacts [ENNReal.sum_ne_top.2 fun i hi ↦ (hf _ hi).eLpNorm_ne_top, + eLpNorm_sum_le (fun i hi ↦ (hf _ hi).aestronglyMeasurable) hp] + +lemma nnLpNorm_expect_le [Module ℚ≥0 E] [NormedSpace ℝ E] {ι : Type*} {s : Finset ι} + {f : ι → α → E} (hf : ∀ i ∈ s, Memℒp (f i) p μ) (hp : 1 ≤ p) : + nnLpNorm (𝔼 i ∈ s, f i) p μ ≤ 𝔼 i ∈ s, nnLpNorm (f i) p μ := by + obtain rfl | hs := s.eq_empty_or_nonempty + · simp + refine (le_inv_smul_iff_of_pos $ by positivity).2 ?_ + rw [Nat.cast_smul_eq_nsmul, ← nnLpNorm_nsmul, Finset.card_smul_expect] + exact nnLpNorm_sum_le hf hp + lemma nnLpNorm_mono_real {g : α → ℝ} (hg : Memℒp g p μ) (h : ∀ x, ‖f x‖ ≤ g x) : nnLpNorm f p μ ≤ nnLpNorm g p μ := ENNReal.toNNReal_mono (hg.eLpNorm_ne_top) (eLpNorm_mono_real h) @@ -171,9 +191,6 @@ lemma nnLpNorm_smul_measure_of_ne_top (hp : p ≠ ∞) {f : α → E} (c : ℝ nnLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • nnLpNorm f p μ := by simp [nnLpNorm, eLpNorm_smul_measure_of_ne_top'' hp] -@[simp] lemma nnLpNorm_norm (f : α → E) (p : ℝ≥0∞) : - nnLpNorm (fun x ↦ ‖f x‖) p μ = nnLpNorm f p μ := by simp [nnLpNorm] - @[simp] lemma nnLpNorm_conj {K : Type*} [RCLike K] (f : α → K) (p : ℝ≥0∞) (μ : Measure α) : nnLpNorm (conj f) p μ = nnLpNorm f p μ := by simp [← nnLpNorm_norm] diff --git a/blueprint/src/chapter/ff.tex b/blueprint/src/chapter/ff.tex index 272719c18b..33dd7629ac 100644 --- a/blueprint/src/chapter/ff.tex +++ b/blueprint/src/chapter/ff.tex @@ -172,7 +172,7 @@ \chapter{Finite field model} \begin{lemma} \label{no3aps_inner_prod} -\lean{AddSalemSpencer.l2Inner_mu_conv_mu_mu_two_smul_mu} +\lean{AddSalemSpencer.dL2Inner_mu_conv_mu_mu_two_smul_mu} \leanok If $A\subseteq G$ has no non-trivial three-term arithmetic progressions and $G$ has odd order then \[\langle \mu_A\ast \mu_A,\mu_{2\cdot A}\rangle = 1/\abs{A}^2.\]