From 9e777f71460033f910375be92d66eb1ba14f0b71 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 22 Aug 2024 21:29:12 +0000 Subject: [PATCH] Progress yet again --- LeanAPAP.lean | 1 + LeanAPAP/FiniteField/Basic.lean | 4 +- LeanAPAP/Mathlib/Data/ENNReal/Operations.lean | 5 +- .../MeasureTheory/Function/EssSup.lean | 18 +- .../Function/LpSeminorm/Basic.lean | 19 ++ .../MeasureTheory/Measure/MeasureSpace.lean | 12 + .../MeasureTheory/Measure/Typeclasses.lean | 10 + LeanAPAP/Physics/DRC.lean | 8 +- LeanAPAP/Physics/Unbalancing.lean | 20 +- LeanAPAP/Prereqs/Chang.lean | 2 +- LeanAPAP/Prereqs/Energy.lean | 6 +- .../Prereqs/FourierTransform/Compact.lean | 14 +- .../Prereqs/FourierTransform/Discrete.lean | 2 +- LeanAPAP/Prereqs/LpNorm/Compact.lean | 259 +++++++++--------- LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean | 2 +- LeanAPAP/Prereqs/LpNorm/Weighted.lean | 151 +++++----- LeanAPAP/Prereqs/NNLpNorm.lean | 8 + LeanAPAP/Prereqs/Rudin.lean | 12 +- 18 files changed, 308 insertions(+), 245 deletions(-) create mode 100644 LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean diff --git a/LeanAPAP.lean b/LeanAPAP.lean index b86835ac58..798e133cb6 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -23,6 +23,7 @@ import LeanAPAP.Mathlib.MeasureTheory.Measure.Count import LeanAPAP.Mathlib.MeasureTheory.Measure.Dirac import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpace import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef +import LeanAPAP.Mathlib.MeasureTheory.Measure.Typeclasses import LeanAPAP.Mathlib.Order.LiminfLimsup import LeanAPAP.Mathlib.Tactic.Positivity import LeanAPAP.Physics.AlmostPeriodicity diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean index 57ece896e2..7c861502fb 100644 --- a/LeanAPAP/FiniteField/Basic.lean +++ b/LeanAPAP/FiniteField/Basic.lean @@ -52,7 +52,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ) refine rpow_le_rpow_of_nonpos ?_ hγC (neg_nonpos.2 ?_) all_goals positivity · simp_rw [Nat.cast_mul, Nat.cast_two, p] - rw [wdLpNorm_const_right, mul_assoc, mul_left_comm, NNReal.coe_inv, inv_rpow, rpow_neg] + rw [wLpNorm_const_right, mul_assoc, mul_left_comm, NNReal.coe_inv, inv_rpow, rpow_neg] push_cast any_goals norm_cast; rw [Nat.succ_le_iff] rfl @@ -130,7 +130,7 @@ lemma di_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hε₀ : 0 < ε) (hε₁ : ε < -- mul_inv_cancel₀ (show (card G : ℝ) ≠ 0 by positivity)] · have hγ' : (1 : ℝ≥0) ≤ 2 * ⌈γ.curlog⌉₊ := sorry sorry - -- simpa [wdLpNorm_nsmul hγ', ← nsmul_eq_mul, div_le_iff' (show (0 : ℝ) < card G by positivity), + -- simpa [wLpNorm_nsmul hγ', ← nsmul_eq_mul, div_le_iff' (show (0 : ℝ) < card G by positivity), -- ← div_div, *] using global_dichotomy hA hγC hγ hAC sorry diff --git a/LeanAPAP/Mathlib/Data/ENNReal/Operations.lean b/LeanAPAP/Mathlib/Data/ENNReal/Operations.lean index 1f8913fc51..ca6849d839 100644 --- a/LeanAPAP/Mathlib/Data/ENNReal/Operations.lean +++ b/LeanAPAP/Mathlib/Data/ENNReal/Operations.lean @@ -3,7 +3,10 @@ import Mathlib.Data.ENNReal.Operations namespace ENNReal variable {α : Type*} {s : Finset α} {f : α → ℝ≥0∞} -lemma sum_ne_top : ∑ a ∈ s, f a ≠ ∞ ↔ ∀ a ∈ s, f a ≠ ⊤ := by +-- TODO: Unify `sum_lt_top` and `sum_lt_top_iff` +attribute [simp] sum_lt_top_iff + +@[simp] lemma sum_ne_top : ∑ a ∈ s, f a ≠ ∞ ↔ ∀ a ∈ s, f a ≠ ⊤ := by simpa [lt_top_iff_ne_top] using sum_lt_top_iff end ENNReal diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean index 233997b14a..41aa553bf1 100644 --- a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean +++ b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean @@ -1,11 +1,25 @@ -import LeanAPAP.Mathlib.Order.LiminfLimsup import Mathlib.MeasureTheory.Function.EssSup +import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpace +import LeanAPAP.Mathlib.Order.LiminfLimsup open Filter MeasureTheory +open scoped ENNReal -variable {α β : Type*} [Nonempty α] {m : MeasurableSpace α} [ConditionallyCompleteLattice β] +variable {α β : Type*} {m : MeasurableSpace α} [ConditionallyCompleteLattice β] {μ : Measure α} {f : α → β} +section SMul +variable {R : Type*} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] + [NoZeroSMulDivisors R ℝ≥0∞] {c : ℝ≥0∞} + +-- TODO: Replace in mathlib +@[simp] lemma essSup_smul_measure' {f : α → β} {c : ℝ≥0∞} (hc : c ≠ 0) : + essSup f (c • μ) = essSup f μ := by simp_rw [essSup, Measure.ae_smul_measure_eq hc] + +end SMul + +variable [Nonempty α] + lemma essSup_eq_ciSup (hμ : ∀ a, μ {a} ≠ 0) (hf : BddAbove (Set.range f)) : essSup f μ = ⨆ a, f a := by rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_ciSup hf] diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean index e7fabf7179..02d1aa70c2 100644 --- a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean +++ b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean @@ -44,4 +44,23 @@ lemma eLpNorm_nsmul [NormedSpace ℝ F] (n : ℕ) (f : α → F) : eLpNorm (n • f) p μ = n * eLpNorm f p μ := by simpa [Nat.cast_smul_eq_nsmul] using eLpNorm_const_smul (n : ℝ) f +-- TODO: Replace `eLpNorm_smul_measure_of_ne_zero` +lemma eLpNorm_smul_measure_of_ne_zero' {c : ℝ≥0∞} (hc : c ≠ 0) (f : α → F) (p : ℝ≥0∞) + (μ : Measure α) : eLpNorm f p (c • μ) = c ^ p⁻¹.toReal * eLpNorm f p μ := by + simpa using eLpNorm_smul_measure_of_ne_zero hc + +lemma eLpNorm_smul_measure_of_ne_zero'' {c : ℝ≥0} (hc : c ≠ 0) (f : α → F) (p : ℝ≥0∞) + (μ : Measure α) : eLpNorm f p (c • μ) = c ^ p⁻¹.toReal • eLpNorm f p μ := + (eLpNorm_smul_measure_of_ne_zero (ENNReal.coe_ne_zero.2 hc)).trans (by simp; norm_cast) + +lemma eLpNorm_smul_measure_of_ne_top' (hp : p ≠ ∞) (c : ℝ≥0∞) (f : α → F) : + eLpNorm f p (c • μ) = c ^ p⁻¹.toReal * eLpNorm f p μ := by + simpa using eLpNorm_smul_measure_of_ne_top hp _ + +lemma eLpNorm_smul_measure_of_ne_top'' (hp : p ≠ ∞) (c : ℝ≥0) (f : α → F) : + eLpNorm f p (c • μ) = c ^ p⁻¹.toReal • eLpNorm f p μ := by + have : 0 ≤ p⁻¹.toReal := by positivity + refine (eLpNorm_smul_measure_of_ne_top' hp _ _).trans ?_ + simp [ENNReal.smul_def, ENNReal.coe_rpow_of_nonneg, this] + end MeasureTheory diff --git a/LeanAPAP/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/LeanAPAP/Mathlib/MeasureTheory/Measure/MeasureSpace.lean index c14dc51cb8..136e4cc91c 100644 --- a/LeanAPAP/Mathlib/MeasureTheory/Measure/MeasureSpace.lean +++ b/LeanAPAP/Mathlib/MeasureTheory/Measure/MeasureSpace.lean @@ -1,9 +1,21 @@ import Mathlib.MeasureTheory.Measure.MeasureSpace +open scoped ENNReal + namespace MeasureTheory.Measure variable {ι α : Type*} {mα : MeasurableSpace α} {f : ι → Measure α} @[simp] lemma sum_eq_zero : sum f = 0 ↔ ∀ i, f i = 0 := by simp (config := { contextual := true }) [Measure.ext_iff, forall_swap (α := ι)] +variable {R : Type*} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] + [NoZeroSMulDivisors R ℝ≥0∞] {c : ℝ≥0∞} + +-- TODO: Replace in mathlib +lemma ae_smul_measure_iff' {p : α → Prop} {c : R} (hc : c ≠ 0) {μ : Measure α} : + (∀ᵐ x ∂c • μ, p x) ↔ ∀ᵐ x ∂μ, p x := by simp [ae_iff, hc] + +@[simp] lemma ae_smul_measure_eq' (hc : c ≠ 0) (μ : Measure α) : ae (c • μ) = ae μ := by + ext; exact ae_smul_measure_iff hc + end MeasureTheory.Measure diff --git a/LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean new file mode 100644 index 0000000000..ef1f54efc4 --- /dev/null +++ b/LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean @@ -0,0 +1,10 @@ +import Mathlib.MeasureTheory.Measure.Typeclasses +import LeanAPAP.Mathlib.Data.ENNReal.Operations + +namespace MeasureTheory +variable {ι α : Type*} {mα : MeasurableSpace α} {s : Finset ι} {μ : ι → Measure α} + [∀ i, IsFiniteMeasure (μ i)] + +instance : IsFiniteMeasure (∑ i ∈ s, μ i) where measure_univ_lt_top := by simp [measure_lt_top] + +end MeasureTheory diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean index c3691cc932..7ae7508a54 100644 --- a/LeanAPAP/Physics/DRC.lean +++ b/LeanAPAP/Physics/DRC.lean @@ -42,7 +42,7 @@ private lemma sum_cast_c (p : ℕ) (B A : Finset G) : `𝟭 A ○ 𝟭 A` is positive. -/ private lemma dLpNorm_conv_pos (hp : p ≠ 0) (hB : (B₁ ∩ B₂).Nonempty) (hA : A.Nonempty) : 0 < ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p := by - rw [wdLpNorm_pow_eq_sum] + rw [wLpNorm_pow_eq_sum] refine sum_pos' (fun x _ ↦ by positivity) ⟨0, mem_univ _, smul_pos ?_ $ pow_pos ?_ _⟩ · rwa [pos_iff_ne_zero, ← Function.mem_support, support_dconv, support_mu, support_mu, ← coe_sub, mem_coe, zero_mem_sub_iff, not_disjoint_iff_nonempty_inter] <;> exact mu_nonneg @@ -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 [wdLpNorm_pow_eq_sum hp₀, l2Inner_eq_sum, sum_dconv, sum_indicate, Pi.one_apply, + simpa only [wLpNorm_pow_eq_sum hp₀, l2Inner_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 @@ -239,8 +239,8 @@ lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p rw [nnratCast_dens, le_div_iff, ← mul_div_right_comm] calc _ = ‖𝟭_[ℝ] A ○ 𝟭 A‖_[1, μ univ] := by - simp [mu, wdLpNorm_smul_right, hp₀, dL1Norm_dconv, card_univ, inv_mul_eq_div] - _ ≤ _ := wdLpNorm_mono_right (one_le_two.trans $ by norm_cast) _ _ + simp [mu, wLpNorm_smul_right, hp₀, dL1Norm_dconv, card_univ, inv_mul_eq_div] + _ ≤ _ := wLpNorm_mono_right (one_le_two.trans $ by norm_cast) _ _ · exact Nat.cast_pos.2 hA.card_pos obtain ⟨A₁, -, A₂, -, h, hcard₁, hcard₂⟩ := sifting univ univ hε hε₁ hδ hp hp₂ hpε (by simp [univ_nonempty]) hA (by simpa) diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index 481e64b951..cf29e147dd 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/LeanAPAP/Physics/Unbalancing.lean @@ -63,7 +63,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 1 + ε / 2 ≤ 1 + 1 / 2 := add_le_add_left (div_le_div_of_nonneg_right hε₁ zero_le_two) _ _ ≤ 2 := by norm_num _ ≤ ‖f + 1‖_[2 * p, ν] := hf₁ - _ ≤ _ := wdLpNorm_mono_right (NNReal.coe_le_coe.1 ?_) _ _ + _ ≤ _ := wLpNorm_mono_right (NNReal.coe_le_coe.1 ?_) _ _ push_cast refine mul_le_mul_of_nonneg_right ?_ ?_ calc @@ -82,7 +82,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 _ ≤ ⟪((↑) ∘ ν : G → ℝ), f ^ p⟫_[ℝ] + ∑ i, ↑(ν i) * ((f ^ (p - 1)) i * |f| i) := (le_add_of_nonneg_left $ pow_inner_nonneg hf hν _) _ = _ := ?_ - rw [wdLpNorm_pow_eq_sum hp₁.pos.ne'] + rw [wLpNorm_pow_eq_sum hp₁.pos.ne'] dsimp refine sum_congr rfl fun i _ ↦ ?_ rw [← abs_of_nonneg ((Nat.Odd.sub_odd hp₁ odd_one).pow_nonneg $ f _), abs_pow, @@ -116,8 +116,8 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 | norm_num replace hf₁ : ‖f‖_[2 * p, ν] ≤ 3 := by calc - _ ≤ ‖f + 1‖_[2 * p, ν] + ‖(1 : G → ℝ)‖_[2 * p, ν] := wdLpNorm_le_add_wdLpNorm_add hp' _ _ _ - _ ≤ (2 + 1 : ℝ) := (add_le_add hf₁ (by rw [wdLpNorm_one, hν₁, one_rpow]; positivity)) + _ ≤ ‖f + 1‖_[2 * p, ν] + ‖(1 : G → ℝ)‖_[2 * p, ν] := wLpNorm_le_add_wLpNorm_add hp' _ _ _ + _ ≤ (2 + 1 : ℝ) := (add_le_add hf₁ (by rw [wLpNorm_one, hν₁, one_rpow]; positivity)) _ = 3 := by norm_num replace hp' := zero_lt_one.trans_le hp' have : 4⁻¹ * ε ^ p ≤ sqrt (∑ i in T, ν i) * 3 ^ p := by @@ -133,11 +133,11 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 _ ≤ sqrt (∑ i in T, ν i) * sqrt (∑ i, ν i * |(f ^ (2 * p)) i|) := (mul_le_mul_of_nonneg_left (sqrt_le_sqrt $ sum_le_univ_sum_of_nonneg fun i ↦ ?_) ?_) _ = sqrt (∑ i in T, ν i) * ‖f‖_[2 * ↑p, ν] ^ p := ?_ - _ ≤ _ := mul_le_mul_of_nonneg_left (pow_le_pow_left wdLpNorm_nonneg hf₁ _) ?_ + _ ≤ _ := mul_le_mul_of_nonneg_left (pow_le_pow_left wLpNorm_nonneg hf₁ _) ?_ any_goals positivity - rw [wdLpNorm_eq_sum hp'.ne', NNReal.coe_mul, mul_inv, rpow_mul, NNReal.coe_natCast, + rw [wLpNorm_eq_sum hp'.ne', NNReal.coe_mul, mul_inv, rpow_mul, NNReal.coe_natCast, rpow_inv_natCast_pow] - simp only [wdLpNorm_eq_sum hp'.ne', sqrt_eq_rpow, Nonneg.coe_one, rpow_two, + simp only [wLpNorm_eq_sum hp'.ne', sqrt_eq_rpow, Nonneg.coe_one, rpow_two, abs_nonneg, NNReal.smul_def, rpow_mul, Pi.pow_apply, abs_pow, norm_eq_abs, mul_pow, rpow_natCast, smul_eq_mul, pow_mul, one_div, NNReal.coe_two] all_goals positivity @@ -177,7 +177,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 _ ≤ (∑ i, ↑(ν i) * |f i + 1| ^ p') ^ p'⁻¹ := rpow_le_rpow ?_ (sum_le_sum_of_subset_of_nonneg (subset_univ _) fun i _ _ ↦ ?_) ?_ _ = _ := by - rw [wdLpNorm_eq_sum (NNReal.coe_ne_zero.1 _)] + rw [wLpNorm_eq_sum (NNReal.coe_ne_zero.1 _)] simp [NNReal.smul_def, hp'.ne', p'] dsimp positivity @@ -200,9 +200,9 @@ lemma unbalancing (p : ℕ) (hp : p ≠ 0) (ε : ℝ) (hε₀ : 0 < ε) (hε₁ _ ≤ ‖f + 1‖_[(⟨_, (p'_pos this hε₀ hε₁).le⟩ : ℝ≥0), ν] := unbalancing' (2 * p + 3) this ((even_two_mul _).add_odd $ by decide) hε₀ hε₁ hf hν hν₁ $ hε.trans $ - wdLpNorm_mono_right + wLpNorm_mono_right (Nat.cast_le.2 $ le_add_of_le_left $ le_mul_of_one_le_left' one_le_two) _ _ - _ ≤ _ := wdLpNorm_mono_right ?_ _ _ + _ ≤ _ := wLpNorm_mono_right ?_ _ _ calc _ ≤ 24 / ε * log (3 / ε) * ↑(2 * p + 3 * p) := mul_le_mul_of_nonneg_left (Nat.cast_le.2 $ add_le_add_left diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean index e59fe8d49a..4ecb819b1f 100644 --- a/LeanAPAP/Prereqs/Chang.lean +++ b/LeanAPAP/Prereqs/Chang.lean @@ -126,7 +126,7 @@ lemma AddDissociated.boringEnergy_le [DecidableEq G] {s : Finset G} obtain rfl | hn := eq_or_ne n 0 · simp calc - _ = ‖dft (𝟭 s)‖ₙ_[↑(2 * n)] ^ (2 * n) := by rw [ndLpNorm_dft_indicate_pow] + _ = ‖dft (𝟭 s)‖ₙ_[↑(2 * n)] ^ (2 * n) := by rw [cLpNorm_dft_indicate_pow] _ ≤ (4 * rexp 2⁻¹ * sqrt ↑(2 * n) * ‖dft (𝟭 s)‖ₙ_[2]) ^ (2 * n) := by gcongr refine rudin_ineq (le_mul_of_one_le_right zero_le_two $ Nat.one_le_iff_ne_zero.2 hn) diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean index 4fb1f55552..97dbaca5e0 100644 --- a/LeanAPAP/Prereqs/Energy.lean +++ b/LeanAPAP/Prereqs/Energy.lean @@ -44,7 +44,7 @@ lemma boringEnergy_eq (n : ℕ) (s : Finset G) : boringEnergy n s = ∑ x, (𝟭 @[simp] lemma boringEnergy_one (s : Finset G) : boringEnergy 1 s = s.card := by simp [boringEnergy_eq, indicate_apply] -lemma ndLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) : +lemma cLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[↑(2 * n)] ^ (2 * n) = boringEnergy n s := by obtain rfl | hn := n.eq_zero_or_pos · simp @@ -53,7 +53,7 @@ lemma ndLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) : _ = ⟪dft (𝟭 s ∗^ n), dft (𝟭 s ∗^ n)⟫ₙ_[ℂ] := ?_ _ = ⟪𝟭 s ∗^ n, 𝟭 s ∗^ n⟫_[ℂ] := nl2Inner_dft _ _ _ = _ := ?_ - · rw [ndLpNorm_pow_eq_expect] + · 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] positivity @@ -64,5 +64,5 @@ lemma ndLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) : lemma ndL2Norm_dft_indicate (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[2] = sqrt s.card := by rw [eq_comm, sqrt_eq_iff_sq_eq] - simpa using ndLpNorm_dft_indicate_pow 1 s + 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 3008c27017..690ed1cf36 100644 --- a/LeanAPAP/Prereqs/FourierTransform/Compact.lean +++ b/LeanAPAP/Prereqs/FourierTransform/Compact.lean @@ -53,7 +53,7 @@ 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 ndLpNorm_nonneg).1 $ Complex.ofReal_injective $ by + (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 /-- **Fourier inversion** for the discrete Fourier transform. -/ @@ -159,13 +159,13 @@ lemma cft_ndconv (f g : α → ℂ) : cft (f ○ₙ g) = cft f * conj (cft g) := -- push_cast -- simp_rw [pow_mul, ← Complex.mul_conj', conj_iterConv_apply, mul_pow] -lemma ndLpNorm_nconv_le_ndLpNorm_ndconv (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℂ) : +lemma cLpNorm_nconv_le_cLpNorm_ndconv (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℂ) : ‖f ∗ₙ f‖ₙ_[n] ≤ ‖f ○ₙ f‖ₙ_[n] := by cases isEmpty_or_nonempty α · rw [Subsingleton.elim (f ∗ₙ f) (f ○ₙ f)] refine le_of_pow_le_pow_left hn₀ (by positivity) ?_ obtain ⟨n, rfl⟩ := hn.two_dvd - simp_rw [ndLpNorm_pow_eq_expect hn₀, ← cft_inversion (f ∗ₙ f), ← cft_inversion (f ○ₙ f), + simp_rw [cLpNorm_pow_eq_expect hn₀, ← cft_inversion (f ∗ₙ f), ← cft_inversion (f ○ₙ f), cft_nconv, cft_ndconv, Pi.mul_apply] rw [← Real.norm_of_nonneg (expect_nonneg fun i _ ↦ ?_), ← Complex.norm_real] rw [Complex.ofReal_expect (univ : Finset α)] @@ -194,8 +194,8 @@ lemma ndLpNorm_nconv_le_ndLpNorm_ndconv (hn₀ : n ≠ 0) (hn : Even n) (f : α -- refine expect_congr rfl fun x _ ↦ expect_congr rfl fun a _ ↦ prod_congr rfl fun i _ ↦ _ -- ring ---TODO: Can we unify with `ndLpNorm_nconv_le_ndLpNorm_ndconv`? -lemma ndLpNorm_nconv_le_ndLpNorm_ndconv' (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℝ) : +--TODO: Can we unify with `cLpNorm_nconv_le_cLpNorm_ndconv`? +lemma cLpNorm_nconv_le_cLpNorm_ndconv' (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℝ) : ‖f ∗ₙ f‖ₙ_[n] ≤ ‖f ○ₙ f‖ₙ_[n] := by - simpa only [← Complex.coe_comp_nconv, ← Complex.coe_comp_ndconv, Complex.ndLpNorm_coe_comp] using - ndLpNorm_nconv_le_ndLpNorm_ndconv hn₀ hn ((↑) ∘ f) + simpa only [← Complex.coe_comp_nconv, ← Complex.coe_comp_ndconv, Complex.cLpNorm_coe_comp] using + cLpNorm_nconv_le_cLpNorm_ndconv hn₀ hn ((↑) ∘ f) diff --git a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean index 461f4f8395..f7bb0387a1 100644 --- a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean +++ b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean @@ -48,7 +48,7 @@ lemma dft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : dft f ψ = ⟪ψ, f⟫_ /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/ @[simp] lemma ndL2Norm_dft (f : α → ℂ) : ‖dft f‖ₙ_[2] = ‖f‖_[2] := - (sq_eq_sq ndLpNorm_nonneg nnLpNorm_nonneg).1 $ Complex.ofReal_injective $ by + (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 /-- **Fourier inversion** for the discrete Fourier transform. -/ diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean index fd6d0ae376..1c813fb588 100644 --- a/LeanAPAP/Prereqs/LpNorm/Compact.lean +++ b/LeanAPAP/Prereqs/LpNorm/Compact.lean @@ -10,121 +10,122 @@ open Function Real open Fintype (card) open scoped BigOperators ComplexConjugate ENNReal NNReal -variable {ι 𝕜 : Type*} [Fintype ι] +variable {ι 𝕜 E : Type*} [Fintype ι] [MeasurableSpace ι] /-! ### Lp norm -/ +namespace MeasureTheory section NormedAddCommGroup -variable {α : ι → Type*} [∀ i, NormedAddCommGroup (α i)] {p q : ℝ≥0∞} {f g h : ∀ i, α i} +variable {α : ι → Type*} [NormedAddCommGroup E] {p q : ℝ≥0∞} {f g h : ι → E} /-- The Lp norm of a function with the compact normalisation. -/ -noncomputable def ndLpNorm (p : ℝ≥0∞) (f : ∀ i, α i) : ℝ := ‖f‖_[p] / card ι ^ p.toReal⁻¹ +noncomputable def cLpNorm (p : ℝ≥0∞) (f : ι → E) : ℝ := nnLpNorm f p ((card ι : ℝ≥0∞)⁻¹ • .count) -notation "‖" f "‖ₙ_[" p "]" => ndLpNorm p f +notation "‖" f "‖ₙ_[" p "]" => cLpNorm p f -lemma ndLpNorm_eq_expect' (hp : p.toReal ≠ 0) (f : ∀ i, α i) : +lemma cLpNorm_eq_expect' (hp : p.toReal ≠ 0) (f : ι → E) : ‖f‖ₙ_[p] = (𝔼 i, ‖f i‖ ^ p.toReal) ^ p.toReal⁻¹ := by - rw [ndLpNorm, dLpNorm_eq_sum', ← div_rpow, Fintype.expect_eq_sum_div_card (α := ℝ)] <;> positivity + rw [cLpNorm, dLpNorm_eq_sum', ← div_rpow, Fintype.expect_eq_sum_div_card (α := ℝ)] <;> positivity -lemma ndLpNorm_eq_expect'' {p : ℝ} (hp : 0 < p) (f : ∀ i, α i) : +lemma cLpNorm_eq_expect'' {p : ℝ} (hp : 0 < p) (f : ι → E) : ‖f‖ₙ_[p.toNNReal] = (𝔼 i, ‖f i‖ ^ p) ^ p⁻¹ := by - rw [ndLpNorm_eq_expect'] <;> simp [hp.ne', hp.le] + rw [cLpNorm_eq_expect'] <;> simp [hp.ne', hp.le] -lemma ndLpNorm_eq_expect {p : ℝ≥0} (hp : p ≠ 0) (f : ∀ i, α i) : - ‖f‖ₙ_[p] = (𝔼 i, ‖f i‖ ^ (p : ℝ)) ^ (p⁻¹ : ℝ) := ndLpNorm_eq_expect' (by simpa using 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) _ -lemma ndLpNorm_rpow_eq_expect {p : ℝ≥0} (hp : p ≠ 0) (f : ∀ i, α i) : +lemma cLpNorm_rpow_eq_expect {p : ℝ≥0} (hp : p ≠ 0) (f : ι → E) : ‖f‖ₙ_[p] ^ (p : ℝ) = 𝔼 i, ‖f i‖ ^ (p : ℝ) := by - rw [ndLpNorm_eq_expect hp, rpow_inv_rpow] <;> positivity + rw [cLpNorm_eq_expect hp, rpow_inv_rpow] <;> positivity -lemma ndLpNorm_pow_eq_expect {p : ℕ} (hp : p ≠ 0) (f : ∀ i, α i) : +lemma cLpNorm_pow_eq_expect {p : ℕ} (hp : p ≠ 0) (f : ι → E) : ‖f‖ₙ_[p] ^ p = 𝔼 i, ‖f i‖ ^ p := by - simpa using ndLpNorm_rpow_eq_expect (Nat.cast_ne_zero.2 hp) f + simpa using cLpNorm_rpow_eq_expect (Nat.cast_ne_zero.2 hp) f -lemma ndL2Norm_sq_eq_expect (f : ∀ i, α i) : ‖f‖ₙ_[2] ^ 2 = 𝔼 i, ‖f i‖ ^ 2 := by - simpa using ndLpNorm_pow_eq_expect two_ne_zero _ +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 : ∀ i, α i) : ‖f‖ₙ_[2] = sqrt (𝔼 i, ‖f i‖ ^ 2) := by - simpa [sqrt_eq_rpow] using ndLpNorm_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 : ∀ i, α i) : ‖f‖ₙ_[1] = 𝔼 i, ‖f i‖ := by simp [ndLpNorm_eq_expect'] +lemma ndL1Norm_eq_expect (f : ι → E) : ‖f‖ₙ_[1] = 𝔼 i, ‖f i‖ := by simp [cLpNorm_eq_expect'] -lemma nnLpNorm_exponent_zero (f : ∀ i, α i) : ‖f‖ₙ_[0] = {i | f i ≠ 0}.toFinite.toFinset.card := by - simp [nnLpNorm_exponent_zero, ndLpNorm] +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 : ∀ i, α i) : ‖f‖ₙ_[∞] = ⨆ i, ‖f i‖ := by - simp [ndLpNorm, dLinftyNorm_eq_iSup] +lemma nlinftyNorm_eq_iSup (f : ι → E) : ‖f‖ₙ_[∞] = ⨆ i, ‖f i‖ := by + simp [cLpNorm, dLinftyNorm_eq_iSup] -@[simp] lemma nnnLpNorm_zero : ‖(0 : ∀ i, α i)‖ₙ_[p] = 0 := by simp [ndLpNorm] +@[simp] lemma nnnLpNorm_zero : ‖(0 : ι → E)‖ₙ_[p] = 0 := by simp [cLpNorm] -@[simp] lemma ndLpNorm_of_isEmpty [IsEmpty ι] (p : ℝ≥0∞) (f : ∀ i, α i) : ‖f‖ₙ_[p] = 0 := by - simp [ndLpNorm] +@[simp] lemma cLpNorm_of_isEmpty [IsEmpty ι] (p : ℝ≥0∞) (f : ι → E) : ‖f‖ₙ_[p] = 0 := by + simp [cLpNorm] -@[simp] lemma ndLpNorm_norm (p : ℝ≥0∞) (f : ∀ i, α i) : ‖fun i ↦ ‖f i‖‖ₙ_[p] = ‖f‖ₙ_[p] := by - simp [ndLpNorm] +@[simp] lemma cLpNorm_norm (p : ℝ≥0∞) (f : ι → E) : ‖fun i ↦ ‖f i‖‖ₙ_[p] = ‖f‖ₙ_[p] := by + simp [cLpNorm] -@[simp] lemma ndLpNorm_neg (f : ∀ i, α i) : ‖-f‖ₙ_[p] = ‖f‖ₙ_[p] := by simp [← ndLpNorm_norm _ (-f)] +@[simp] lemma cLpNorm_neg (f : ι → E) : ‖-f‖ₙ_[p] = ‖f‖ₙ_[p] := by simp [← cLpNorm_norm _ (-f)] -lemma ndLpNorm_sub_comm (f g : ∀ i, α i) : ‖f - g‖ₙ_[p] = ‖g - f‖ₙ_[p] := by - simp [← ndLpNorm_neg (f - g)] +lemma cLpNorm_sub_comm (f g : ι → E) : ‖f - g‖ₙ_[p] = ‖g - f‖ₙ_[p] := by + simp [← cLpNorm_neg (f - g)] -@[simp] lemma ndLpNorm_nonneg : 0 ≤ ‖f‖ₙ_[p] := by unfold ndLpNorm; positivity +@[simp] lemma cLpNorm_nonneg : 0 ≤ ‖f‖ₙ_[p] := by unfold cLpNorm; positivity -@[simp] lemma ndLpNorm_eq_zero [Nonempty ι] : ‖f‖ₙ_[p] = 0 ↔ f = 0 := by +@[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 ndLpNorm_nonneg (NNReal.coe_ne_zero.2 hp)] - simp [ndLpNorm_rpow_eq_expect hp, Fintype.expect_eq_zero_iff_of_nonneg, rpow_nonneg, + · 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 ndLpNorm_pos [Nonempty ι] : 0 < ‖f‖ₙ_[p] ↔ f ≠ 0 := - ndLpNorm_nonneg.gt_iff_ne.trans ndLpNorm_eq_zero.not +@[simp] lemma cLpNorm_pos [Nonempty ι] : 0 < ‖f‖ₙ_[p] ↔ f ≠ 0 := + cLpNorm_nonneg.gt_iff_ne.trans cLpNorm_eq_zero.not -lemma ndLpNorm_mono_right (hpq : p ≤ q) (f : ∀ i, α i) : ‖f‖ₙ_[p] ≤ ‖f‖ₙ_[q] := sorry +lemma cLpNorm_mono_right (hpq : p ≤ q) (f : ι → E) : ‖f‖ₙ_[p] ≤ ‖f‖ₙ_[q] := sorry section one_le -lemma ndLpNorm_add_le (hp : 1 ≤ p) (f g : ∀ i, α i) : ‖f + g‖ₙ_[p] ≤ ‖f‖ₙ_[p] + ‖g‖ₙ_[p] := by - simp only [ndLpNorm, ← add_div] +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 ndLpNorm_sub_le (hp : 1 ≤ p) (f g : ∀ i, α i) : ‖f - g‖ₙ_[p] ≤ ‖f‖ₙ_[p] + ‖g‖ₙ_[p] := by - simp only [ndLpNorm, ← add_div] +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 ndLpNorm_le_ndLpNorm_add_ndLpNorm_sub' (hp : 1 ≤ p) (f g : ∀ i, α i) : +lemma cLpNorm_le_cLpNorm_add_cLpNorm_sub' (hp : 1 ≤ p) (f g : ι → E) : ‖f‖ₙ_[p] ≤ ‖g‖ₙ_[p] + ‖f - g‖ₙ_[p] := by - simp only [ndLpNorm, ← add_div] + simp only [cLpNorm, ← add_div] exact div_le_div_of_nonneg_right (dLpNorm_le_dLpNorm_add_dLpNorm_sub' hp _ _) (by positivity) -lemma ndLpNorm_le_ndLpNorm_add_ndLpNorm_sub (hp : 1 ≤ p) (f g : ∀ i, α i) : +lemma cLpNorm_le_cLpNorm_add_cLpNorm_sub (hp : 1 ≤ p) (f g : ι → E) : ‖f‖ₙ_[p] ≤ ‖g‖ₙ_[p] + ‖g - f‖ₙ_[p] := by - simp only [ndLpNorm, ← add_div] + simp only [cLpNorm, ← add_div] exact div_le_div_of_nonneg_right (dLpNorm_le_dLpNorm_add_dLpNorm_sub hp _ _) (by positivity) -lemma ndLpNorm_le_add_ndLpNorm_add (hp : 1 ≤ p) (f g : ∀ i, α i) : +lemma cLpNorm_le_add_cLpNorm_add (hp : 1 ≤ p) (f g : ι → E) : ‖f‖ₙ_[p] ≤ ‖f + g‖ₙ_[p] + ‖g‖ₙ_[p] := by - simp only [ndLpNorm, ← add_div] + simp only [cLpNorm, ← add_div] exact div_le_div_of_nonneg_right (dLpNorm_le_add_dLpNorm_add hp _ _) (by positivity) -lemma ndLpNorm_sub_le_ndLpNorm_sub_add_ndLpNorm_sub (hp : 1 ≤ p) (f g : ∀ i, α i) : +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 [ndLpNorm, ← add_div] + 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 𝕜 (α i)] +variable [NormedField 𝕜] [∀ i, NormedSpace 𝕜 E] -- TODO: `p ≠ 0` is enough -lemma ndLpNorm_smul (hp : 1 ≤ p) (c : 𝕜) (f : ∀ i, α i) : ‖c • f‖ₙ_[p] = ‖c‖ * ‖f‖ₙ_[p] := by - simp only [ndLpNorm, mul_div_assoc, dLpNorm_smul hp] +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 ℝ (α i)] +variable [∀ i, NormedSpace ℝ E] -lemma ndLpNorm_nsmul (hp : 1 ≤ p) (n : ℕ) (f : ∀ i, α i) : ‖n • f‖ₙ_[p] = n • ‖f‖ₙ_[p] := by - simp only [ndLpNorm, nsmul_eq_mul, mul_div_assoc, dLpNorm_nsmul hp] +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 @@ -133,45 +134,45 @@ section NormedAddCommGroup variable {α : Type*} [NormedAddCommGroup α] {p : ℝ≥0∞} @[simp] -lemma ndLpNorm_const [Nonempty ι] (hp : p ≠ 0) (a : α) : ‖const ι a‖ₙ_[p] = ‖a‖ := by +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 [ndLpNorm, ENNReal.coe_ne_coe.1 hp, mul_div_cancel_left₀ _ this] + 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 ndLpNorm_one [Nonempty ι] (hp : p ≠ 0) : ‖(1 : ι → 𝕜)‖ₙ_[p] = 1 := - (ndLpNorm_const hp 1).trans $ by simp +@[simp] lemma cLpNorm_one [Nonempty ι] (hp : p ≠ 0) : ‖(1 : ι → 𝕜)‖ₙ_[p] = 1 := + (cLpNorm_const hp 1).trans $ by simp -lemma ndLpNorm_natCast_mul (hp : 1 ≤ p) (n : ℕ) (f : ι → 𝕜) : - ‖(n : ι → 𝕜) * f‖ₙ_[p] = n * ‖f‖ₙ_[p] := by simpa only [nsmul_eq_mul] using ndLpNorm_nsmul hp n f +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 ndLpNorm_natCast_mul' (hp : 1 ≤ p) (n : ℕ) (f : ι → 𝕜) : - ‖(n * f ·)‖ₙ_[p] = n * ‖f‖ₙ_[p] := ndLpNorm_natCast_mul hp _ _ +lemma cLpNorm_natCast_mul' (hp : 1 ≤ p) (n : ℕ) (f : ι → 𝕜) : + ‖(n * f ·)‖ₙ_[p] = n * ‖f‖ₙ_[p] := cLpNorm_natCast_mul hp _ _ -lemma ndLpNorm_mul_natCast (hp : 1 ≤ p) (f : ι → 𝕜) (n : ℕ) : +lemma cLpNorm_mul_natCast (hp : 1 ≤ p) (f : ι → 𝕜) (n : ℕ) : ‖f * (n : ι → 𝕜)‖ₙ_[p] = ‖f‖ₙ_[p] * n := by - simpa only [mul_comm] using ndLpNorm_natCast_mul hp n f + simpa only [mul_comm] using cLpNorm_natCast_mul hp n f -lemma ndLpNorm_mul_natCast' (hp : 1 ≤ p) (f : ι → 𝕜) (n : ℕ) : - ‖(f · * n)‖ₙ_[p] = ‖f‖ₙ_[p] * n := ndLpNorm_mul_natCast hp _ _ +lemma cLpNorm_mul_natCast' (hp : 1 ≤ p) (f : ι → 𝕜) (n : ℕ) : + ‖(f · * n)‖ₙ_[p] = ‖f‖ₙ_[p] * n := cLpNorm_mul_natCast hp _ _ -lemma ndLpNorm_div_natCast' (hp : 1 ≤ p) (f : ι → 𝕜) (n : ℕ) : - ‖(f · / n)‖ₙ_[p] = ‖f‖ₙ_[p] / n := by simp [ndLpNorm, dLpNorm_div_natCast' hp, div_right_comm] +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 ndLpNorm_div_natCast (hp : 1 ≤ p) (f : ι → 𝕜) (n : ℕ) : - ‖f / (n : ι → 𝕜)‖ₙ_[p] = ‖f‖ₙ_[p] / n := ndLpNorm_div_natCast' hp _ _ +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 ndLpNorm_mono (hf : 0 ≤ f) (hfg : f ≤ g) : ‖f‖ₙ_[p] ≤ ‖g‖ₙ_[p] := +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 @@ -283,21 +284,21 @@ lemma linearIndependent_of_ne_zero_of_nl2Inner_eq_zero {v : κ → ι → 𝕜} end RCLike -section ndLpNorm +section cLpNorm variable {α β : Type*} [Fintype α] {p : ℝ≥0∞} -@[simp] lemma ndLpNorm_conj [RCLike β] (f : α → β) : ‖conj f‖ₙ_[p] = ‖f‖ₙ_[p] := by simp [ndLpNorm] +@[simp] lemma cLpNorm_conj [RCLike β] (f : α → β) : ‖conj f‖ₙ_[p] = ‖f‖ₙ_[p] := by simp [cLpNorm] variable [AddCommGroup α] @[simp] -lemma ndLpNorm_translate [NormedAddCommGroup β] (a : α) (f : α → β) : ‖τ a f‖ₙ_[p] = ‖f‖ₙ_[p] := by - simp [ndLpNorm] +lemma cLpNorm_translate [NormedAddCommGroup β] (a : α) (f : α → β) : ‖τ a f‖ₙ_[p] = ‖f‖ₙ_[p] := by + simp [cLpNorm] -@[simp] lemma ndLpNorm_conjneg [RCLike β] (f : α → β) : ‖conjneg f‖ₙ_[p] = ‖f‖ₙ_[p] := by - simp [ndLpNorm] +@[simp] lemma cLpNorm_conjneg [RCLike β] (f : α → β) : ‖conjneg f‖ₙ_[p] = ‖f‖ₙ_[p] := by + simp [cLpNorm] -end ndLpNorm +end cLpNorm section RCLike variable {α β : Type*} [Fintype α] @@ -309,7 +310,7 @@ end RCLike /-- **Cauchy-Schwarz inequality** -/ lemma nl2Inner_le_dL2Norm_mul_dL2Norm (f g : ι → ℝ) : ⟪f, g⟫ₙ_[ℝ] ≤ ‖f‖ₙ_[2] * ‖g‖ₙ_[2] := by - simp only [ndLpNorm, div_mul_div_comm, ← sq, ENNReal.toReal_ofNat, ← one_div, ← sqrt_eq_rpow] + 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 @@ -317,11 +318,11 @@ lemma nl2Inner_le_dL2Norm_mul_dL2Norm (f g : ι → ℝ) : ⟪f, g⟫ₙ_[ℝ] namespace Mathlib.Meta.Positivity open Lean Meta Qq Function -private alias ⟨_, ndLpNorm_pos_of_ne_zero⟩ := ndLpNorm_pos +private alias ⟨_, cLpNorm_pos_of_ne_zero⟩ := cLpNorm_pos -private lemma ndLpNorm_pos_of_pos {α : ι → Type*} [Nonempty ι] [∀ i, NormedAddCommGroup (α i)] - [∀ i, Preorder (α i)] {p : ℝ≥0∞} {f : ∀ i, α i} (hf : 0 < f) : 0 < ‖f‖ₙ_[p] := - ndLpNorm_pos_of_ne_zero hf.ne' +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 : ι → 𝕜} @@ -344,26 +345,26 @@ end LinearOrderedSemifield @[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(@ndLpNorm $ι $instι $α $instnorm $p $f) => + | ~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(ndLpNorm_pos_of_pos $pf) - | .nonzero pf => return .positive q(ndLpNorm_pos_of_ne_zero $pf) - | _ => return .nonnegative q(ndLpNorm_nonneg) + | .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(ndLpNorm_pos_of_ne_zero $pf) + return .positive q(cLpNorm_pos_of_ne_zero $pf) else - return .nonnegative q(ndLpNorm_nonneg) - | _ => throwError "not ndLpNorm" + return .nonnegative q(cLpNorm_nonneg) + | _ => throwError "not cLpNorm" else - throwError "not ndLpNorm" + throwError "not cLpNorm" /-- The `positivity` extension which identifies expressions of the form `⟪f, g⟫_[𝕜]`. -/ @[positivity ⟪_, _⟫ₙ_[_]] def evalNL2Inner : PositivityExt where eval {u 𝕜} _ _ e := do @@ -387,7 +388,7 @@ end LinearOrderedSemifield section Examples section NormedAddCommGroup -variable {α : ι → Type*} [∀ i, NormedAddCommGroup (α i)] {w : ι → ℝ≥0} {f : ∀ i, α i} +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 @@ -418,111 +419,111 @@ end Mathlib.Meta.Positivity /-! ### Hölder inequality -/ -section ndLpNorm +section cLpNorm variable {α : Type*} [Fintype α] {p q : ℝ≥0} {f g : α → ℝ} @[simp] -lemma ndLpNorm_abs (p : ℝ≥0∞) (f : α → ℝ) : ‖|f|‖ₙ_[p] = ‖f‖ₙ_[p] := by simpa using ndLpNorm_norm p f +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 ndLpNorm_rpow (hp : p ≠ 0) (hq : q ≠ 0) (hf : 0 ≤ f) : +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) ndLpNorm_nonneg (by dsimp; positivity) ?_ + refine rpow_left_injOn (NNReal.coe_ne_zero.2 hp) cLpNorm_nonneg (by dsimp; positivity) ?_ dsimp - rw [← rpow_mul ndLpNorm_nonneg, ← mul_comm, ← ENNReal.coe_mul, ← NNReal.coe_mul, - ndLpNorm_rpow_eq_expect hp, ndLpNorm_rpow_eq_expect (mul_ne_zero hq hp)] + 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 ndLpNorm_rpow one_ne_zero hq hf + simpa only [ENNReal.coe_one, one_mul] using cLpNorm_rpow one_ne_zero hq hf -lemma ndLpNorm_eq_dL1Norm_rpow (hp : p ≠ 0) (f : α → ℝ) : +lemma cLpNorm_eq_dL1Norm_rpow (hp : p ≠ 0) (f : α → ℝ) : ‖f‖ₙ_[p] = ‖|f| ^ (p : ℝ)‖ₙ_[1] ^ (p⁻¹ : ℝ) := by - simp [ndLpNorm_eq_expect hp, ndL1Norm_eq_expect, abs_rpow_of_nonneg] + simp [cLpNorm_eq_expect hp, ndL1Norm_eq_expect, abs_rpow_of_nonneg] -lemma ndLpNorm_rpow' (hp : p ≠ 0) (hq : q ≠ 0) (f : α → ℝ) : +lemma cLpNorm_rpow' (hp : p ≠ 0) (hq : q ≠ 0) (f : α → ℝ) : ‖f‖ₙ_[p] ^ (q : ℝ) = ‖|f| ^ (q : ℝ)‖ₙ_[p / q] := by - rw [← ENNReal.coe_div hq, ndLpNorm_rpow (div_ne_zero hp hq) hq (abs_nonneg f), ndLpNorm_abs, + 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_ndLpNorm_mul_ndLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) : +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, ndLpNorm, div_mul_div_comm, ← rpow_add this, + 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_ndLpNorm_mul_ndLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) : +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_ndLpNorm_mul_ndLpNorm hpq _ _).trans_eq $ by simp_rw [ndLpNorm_abs] + (nl2Inner_le_cLpNorm_mul_cLpNorm hpq _ _).trans_eq $ by simp_rw [cLpNorm_abs] /-- **Hölder's inequality**, binary case. -/ -lemma ndLpNorm_mul_le (hp : p ≠ 0) (hq : q ≠ 0) (r : ℝ≥0) (hpqr : p⁻¹ + q⁻¹ = r⁻¹) (f g : α → ℝ) : +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, ndLpNorm, div_mul_div_comm, ← rpow_add this, + 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 ndLpNorm_prod_le {ι : Type*} {s : Finset ι} (hs : s.Nonempty) {p : ι → ℝ≥0} (hp : ∀ i, p i ≠ 0) +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, ndLpNorm, prod_div_distrib, ← rpow_sum_of_pos this, + 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 ndLpNorm +end cLpNorm /-! ### Indicator -/ section indicate variable {α β : Type*} [RCLike β] [Fintype α] [DecidableEq α] {s : Finset α} {p : ℝ≥0} -lemma ndLpNorm_rpow_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖ₙ_[p] ^ (p : ℝ) = s.dens := by - rw [ndLpNorm, div_rpow] +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 ndLpNorm_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖ₙ_[p] = s.dens ^ (p⁻¹ : ℝ) := by - refine (eq_rpow_inv ?_ ?_ ?_).2 (ndLpNorm_rpow_indicate ?_ _) <;> 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 ndLpNorm_pow_indicate {p : ℕ} (hp : p ≠ 0) (s : Finset α) : +lemma cLpNorm_pow_indicate {p : ℕ} (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖ₙ_[p] ^ (p : ℝ) = s.dens := by - simpa using ndLpNorm_rpow_indicate (Nat.cast_ne_zero.2 hp) s + 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 ndLpNorm_pow_indicate two_ne_zero s + 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 ndLpNorm_pow_indicate one_ne_zero s + simpa using cLpNorm_pow_indicate one_ne_zero s end indicate section mu variable {α β : Type*} [RCLike β] [Fintype α] [DecidableEq α] {s : Finset α} {p : ℝ≥0} -lemma ndLpNorm_mu (hp : 1 ≤ p) (s : Finset α) : ‖μ_[β] s‖ₙ_[p] = s.dens ^ (p⁻¹ : ℝ) / s.card := by - rw [mu, ndLpNorm_smul (ENNReal.one_le_coe_iff.2 hp) (s.card⁻¹ : β) (𝟭_[β] s), ndLpNorm_indicate, +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 ndLpNorm_mu le_rfl s + simpa using cLpNorm_mu le_rfl s end mu @@ -530,12 +531,12 @@ section variable {α : Type*} [Fintype α] @[simp] -lemma RCLike.ndLpNorm_coe_comp {𝕜 : Type*} [RCLike 𝕜] (p) (f : α → ℝ) : +lemma RCLike.cLpNorm_coe_comp {𝕜 : Type*} [RCLike 𝕜] (p) (f : α → ℝ) : ‖((↑) : ℝ → 𝕜) ∘ f‖ₙ_[p] = ‖f‖ₙ_[p] := by - simp only [← ndLpNorm_norm _ (((↑) : ℝ → 𝕜) ∘ f), ← ndLpNorm_norm _ f, Function.comp_apply, + simp only [← cLpNorm_norm _ (((↑) : ℝ → 𝕜) ∘ f), ← cLpNorm_norm _ f, Function.comp_apply, RCLike.norm_ofReal, Real.norm_eq_abs] -@[simp] lemma Complex.ndLpNorm_coe_comp (p) (f : α → ℝ) : ‖((↑) : ℝ → ℂ) ∘ f‖ₙ_[p] = ‖f‖ₙ_[p] := - RCLike.ndLpNorm_coe_comp _ _ +@[simp] lemma Complex.cLpNorm_coe_comp (p) (f : α → ℝ) : ‖((↑) : ℝ → ℂ) ∘ f‖ₙ_[p] = ‖f‖ₙ_[p] := + RCLike.cLpNorm_coe_comp _ _ end diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean index ea4efb4c62..f49d047db9 100644 --- a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean +++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean @@ -13,7 +13,7 @@ import LeanAPAP.Prereqs.NNLpNorm open Finset Function Real open scoped ComplexConjugate ENNReal NNReal NNRat -variable {ι 𝕜 : Type*} [Fintype ι] [MeasurableSpace ι] +variable {ι 𝕜 : Type*} [Fintype ι] {mι : MeasurableSpace ι} namespace MeasureTheory variable {E : Type*} [NormedAddCommGroup E] {p q : ℝ≥0∞} {f g h : ι → E} diff --git a/LeanAPAP/Prereqs/LpNorm/Weighted.lean b/LeanAPAP/Prereqs/LpNorm/Weighted.lean index ee11aad715..267ce5ce11 100644 --- a/LeanAPAP/Prereqs/LpNorm/Weighted.lean +++ b/LeanAPAP/Prereqs/LpNorm/Weighted.lean @@ -1,133 +1,128 @@ +import LeanAPAP.Mathlib.MeasureTheory.Measure.Typeclasses import LeanAPAP.Prereqs.LpNorm.Discrete.Basic /-! # Lp norms -/ -open Finset Function Real +open Finset Function Real MeasureTheory open scoped ComplexConjugate ENNReal NNReal -variable {ι 𝕜 : Type*} [Fintype ι] +variable {ι 𝕜 E : Type*} [Fintype ι] [MeasurableSpace ι] /-! #### Weighted Lp norm -/ section NormedAddCommGroup -variable {α : ι → Type*} [∀ i, NormedAddCommGroup (α i)] {p q : ℝ≥0} {w : ι → ℝ≥0} - {f g h : ∀ i, α i} +variable {α : ι → Type*} [NormedAddCommGroup E] {p q : ℝ≥0∞} {w : ι → ℝ≥0} {f g h : ι → E} /-- The weighted Lp norm of a function. -/ -noncomputable def wdLpNorm (p : ℝ≥0) (w : ι → ℝ≥0) (f : ∀ i, α i) : ℝ := - ‖fun i ↦ w i ^ (p⁻¹ : ℝ) • ‖f i‖‖_[p] +noncomputable def wLpNorm (p : ℝ≥0∞) (w : ι → ℝ≥0) (f : ι → E) : ℝ≥0 := + nnLpNorm f p $ .sum fun i ↦ w i • .dirac i -notation "‖" f "‖_[" p ", " w "]" => wdLpNorm p w f +notation "‖" f "‖_[" p ", " w "]" => wLpNorm p w f -@[simp] -lemma wdLpNorm_one_eq_dLpNorm (p : ℝ≥0) (f : ∀ i, α i) : ‖f‖_[p, 1] = ‖f‖_[p] := by - simp [wdLpNorm, nnLpNorm_exponent_zero, dLpNorm_eq_sum, *] +@[simp] lemma wLpNorm_one_eq_dLpNorm (p : ℝ≥0) (f : ι → E) : ‖f‖_[p, 1] = ‖f‖_[p] := by + simp [wLpNorm, nnLpNorm, Measure.count] @[simp] -lemma wdLpNorm_const_right (hp : 1 ≤ p) (w : ℝ≥0) (f : ∀ i, α i) : - ‖f‖_[p, const _ w] = w ^ (p⁻¹ : ℝ) * ‖f‖_[p] := by - simpa [wdLpNorm, -norm_eq_abs, norm_of_nonneg, Pi.smul_def, NNReal.smul_def, rpow_nonneg] using - dLpNorm_smul (ENNReal.one_le_coe_iff.2 hp) (w ^ (p⁻¹ : ℝ) : ℝ) fun i ↦ ‖f i‖ - -lemma wdLpNorm_eq_sum (hp : p ≠ 0) (w : ι → ℝ≥0) (f : ∀ i, α i) : - ‖f‖_[p, w] = (∑ i, w i • ‖f i‖ ^ (p : ℝ)) ^ (p⁻¹ : ℝ) := by - have : (p : ℝ) ≠ 0 := by positivity - simp_rw [wdLpNorm, dLpNorm_eq_sum hp, NNReal.smul_def, norm_smul] - simp only [NNReal.coe_rpow, norm_norm, Algebra.id.smul_eq_mul, mul_rpow, norm_nonneg, - rpow_nonneg, hp, NNReal.coe_nonneg, norm_of_nonneg, rpow_inv_rpow _ this] - -lemma wdLpNorm_eq_sum' {p : ℝ} (hp : 0 < p) (w : ι → ℝ≥0) (f : ∀ i, α i) : +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] + +variable [DiscreteMeasurableSpace ι] + +lemma wLpNorm_eq_sum (hp₀ : p ≠ 0) (hp : p ≠ ∞) (w : ι → ℝ≥0) (f : ι → E) : + ‖f‖_[p, w] = (∑ i, w i • ‖f i‖₊ ^ p.toReal) ^ p⁻¹.toReal := by + ext + simp [wLpNorm, coe_nnLpNorm_eq_integral_norm_rpow_toReal hp₀ hp .of_discrete, one_div, + integral_finset_sum_measure, tsum_eq_sum' (s := univ) (by simp), ENNReal.coe_rpow_of_nonneg, + ENNReal.toReal_inv, NNReal.smul_def] + +lemma wLpNorm_eq_sum' {p : ℝ} (hp : 0 < p) (w : ι → ℝ≥0) (f : ι → E) : ‖f‖_[p.toNNReal, w] = (∑ i, w i • ‖f i‖ ^ p) ^ p⁻¹ := by - rw [wdLpNorm_eq_sum] <;> simp [hp, hp.ne', hp.le] + rw [wLpNorm_eq_sum] <;> simp [hp, hp.ne', hp.le] -lemma wdLpNorm_rpow_eq_sum {p : ℝ≥0} (hp : p ≠ 0) (w : ι → ℝ≥0) (f : ∀ i, α i) : +lemma wLpNorm_rpow_eq_sum {p : ℝ≥0} (hp : p ≠ 0) (w : ι → ℝ≥0) (f : ι → E) : ‖f‖_[p, w] ^ (p : ℝ) = ∑ i, w i • ‖f i‖ ^ (p : ℝ) := by - rw [wdLpNorm_eq_sum hp, rpow_inv_rpow] -- positivity + rw [wLpNorm_eq_sum hp, rpow_inv_rpow] -- positivity · exact sum_nonneg fun _ _ ↦ by positivity · positivity -lemma wdLpNorm_pow_eq_sum {p : ℕ} (hp : p ≠ 0) (w : ι → ℝ≥0) (f : ∀ i, α i) : +lemma wLpNorm_pow_eq_sum {p : ℕ} (hp : p ≠ 0) (w : ι → ℝ≥0) (f : ι → E) : ‖f‖_[p, w] ^ p = ∑ i, w i • ‖f i‖ ^ p := by - simpa using wdLpNorm_rpow_eq_sum (Nat.cast_ne_zero.2 hp) w f + simpa using wLpNorm_rpow_eq_sum (Nat.cast_ne_zero.2 hp) w f -lemma wdL1Norm_eq_sum (w : ι → ℝ≥0) (f : ∀ i, α i) : ‖f‖_[1, w] = ∑ i, w i • ‖f i‖ := by - simp [wdLpNorm_eq_sum] - -lemma wnnLpNorm_exponent_zero (w : ι → ℝ≥0) (f : ∀ i, α i) : - ‖f‖_[0, w] = {i | f i ≠ 0}.toFinite.toFinset.card := by simp [wdLpNorm, nnLpNorm_exponent_zero] - -@[simp] -lemma wnnLpNorm_zero (w : ι → ℝ≥0) : ‖(0 : ∀ i, α i)‖_[p, w] = 0 := by simp [wdLpNorm, ← Pi.zero_def] +lemma wdL1Norm_eq_sum (w : ι → ℝ≥0) (f : ι → E) : ‖f‖_[1, w] = ∑ i, w i • ‖f i‖ := by + simp [wLpNorm_eq_sum] -@[simp] lemma wdLpNorm_norm (w : ι → ℝ≥0) (f : ∀ i, α i) : ‖fun i ↦ ‖f i‖‖_[p, w] = ‖f‖_[p, w] := by - obtain rfl | hp := @eq_zero_or_pos _ _ p <;> simp [wnnLpNorm_exponent_zero, wdLpNorm_eq_sum, *, ne_of_gt] +lemma wnnLpNorm_exponent_zero (w : ι → ℝ≥0) (f : ι → E) : + ‖f‖_[0, w] = {i | f i ≠ 0}.toFinite.toFinset.card := by simp [wLpNorm, nnLpNorm_exponent_zero] -@[simp]lemma wdLpNorm_neg (w : ι → ℝ≥0) (f : ∀ i, α i) : ‖-f‖_[p, w] = ‖f‖_[p, w] := by - simp [← wdLpNorm_norm _ (-f)] +@[simp] lemma wLpNorm_norm (w : ι → ℝ≥0) (f : ι → E) : ‖fun i ↦ ‖f i‖‖_[p, w] = ‖f‖_[p, w] := by + obtain rfl | hp := @eq_zero_or_pos _ _ p <;> simp [wnnLpNorm_exponent_zero, wLpNorm_eq_sum, *, ne_of_gt] -lemma wdLpNorm_sub_comm (w : ι → ℝ≥0) (f g : ∀ i, α i) : ‖f - g‖_[p, w] = ‖g - f‖_[p, w] := by - simp [← wdLpNorm_neg _ (f - g)] +@[simp]lemma wLpNorm_neg (w : ι → ℝ≥0) (f : ι → E) : ‖-f‖_[p, w] = ‖f‖_[p, w] := by + simp [← wLpNorm_norm _ (-f)] -@[simp] lemma wdLpNorm_nonneg : 0 ≤ ‖f‖_[p, w] := nnLpNorm_nonneg +lemma wLpNorm_sub_comm (w : ι → ℝ≥0) (f g : ι → E) : ‖f - g‖_[p, w] = ‖g - f‖_[p, w] := by + simp [← wLpNorm_neg _ (f - g)] -lemma wdLpNorm_mono_right (hpq : p ≤ q) (w : ι → ℝ≥0) (f : ∀ i, α i) : ‖f‖_[p, w] ≤ ‖f‖_[q, w] := +lemma wLpNorm_mono_right (hpq : p ≤ q) (w : ι → ℝ≥0) (f : ι → E) : ‖f‖_[p, w] ≤ ‖f‖_[q, w] := sorry section one_le -lemma wdLpNorm_add_le (hp : 1 ≤ p) (w : ι → ℝ≥0) (f g : ∀ i, α i) : +lemma wLpNorm_add_le (hp : 1 ≤ p) (w : ι → ℝ≥0) (f g : ι → E) : ‖f + g‖_[p, w] ≤ ‖f‖_[p, w] + ‖g‖_[p, w] := by - unfold wdLpNorm + unfold wLpNorm refine (dLpNorm_add_le (by exact_mod_cast hp) _ _).trans' (dLpNorm_mono (fun i ↦ by dsimp; positivity) fun i ↦ ?_) dsimp rw [← smul_add] exact smul_le_smul_of_nonneg_left (norm_add_le _ _) (zero_le _) -lemma wdLpNorm_sub_le (hp : 1 ≤ p) (w : ι → ℝ≥0) (f g : ∀ i, α i) : +lemma wLpNorm_sub_le (hp : 1 ≤ p) (w : ι → ℝ≥0) (f g : ι → E) : ‖f - g‖_[p, w] ≤ ‖f‖_[p, w] + ‖g‖_[p, w] := by - simpa [sub_eq_add_neg] using wdLpNorm_add_le hp w f (-g) + simpa [sub_eq_add_neg] using wLpNorm_add_le hp w f (-g) -lemma wdLpNorm_le_wdLpNorm_add_wdLpNorm_sub' (hp : 1 ≤ p) (w : ι → ℝ≥0) (f g : ∀ i, α i) : - ‖f‖_[p, w] ≤ ‖g‖_[p, w] + ‖f - g‖_[p, w] := by simpa using wdLpNorm_add_le hp w g (f - g) +lemma wLpNorm_le_wLpNorm_add_wLpNorm_sub' (hp : 1 ≤ p) (w : ι → ℝ≥0) (f g : ι → E) : + ‖f‖_[p, w] ≤ ‖g‖_[p, w] + ‖f - g‖_[p, w] := by simpa using wLpNorm_add_le hp w g (f - g) -lemma wdLpNorm_le_wdLpNorm_add_wdLpNorm_sub (hp : 1 ≤ p) (w : ι → ℝ≥0) (f g : ∀ i, α i) : +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 [wdLpNorm_sub_comm]; exact wdLpNorm_le_wdLpNorm_add_wdLpNorm_sub' hp _ _ _ + rw [wLpNorm_sub_comm]; exact wLpNorm_le_wLpNorm_add_wLpNorm_sub' hp _ _ _ -lemma wdLpNorm_le_add_wdLpNorm_add (hp : 1 ≤ p) (w : ι → ℝ≥0) (f g : ∀ i, α i) : - ‖f‖_[p, w] ≤ ‖f + g‖_[p, w] + ‖g‖_[p, w] := by simpa using wdLpNorm_add_le hp w (f + g) (-g) +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) -lemma wdLpNorm_sub_le_wdLpNorm_sub_add_wdLpNorm_sub (hp : 1 ≤ p) (f g : ∀ i, α i) : +lemma wLpNorm_sub_le_wLpNorm_sub_add_wLpNorm_sub (hp : 1 ≤ p) (f g : ι → E) : ‖f - h‖_[p, w] ≤ ‖f - g‖_[p, w] + ‖g - h‖_[p, w] := by - simpa using wdLpNorm_add_le hp w (f - g) (g - h) + simpa using wLpNorm_add_le hp w (f - g) (g - h) -variable [NormedField 𝕜] [∀ i, NormedSpace 𝕜 (α i)] +variable [NormedField 𝕜] [∀ i, NormedSpace 𝕜 E] -- TODO: `p ≠ 0` is enough -lemma wdLpNorm_smul (hp : 1 ≤ p) (c : 𝕜) (f : ∀ i, α i) : ‖c • f‖_[p, w] = ‖c‖ * ‖f‖_[p, w] := by - rw [wdLpNorm, wdLpNorm] +lemma wLpNorm_smul (hp : 1 ≤ p) (c : 𝕜) (f : ι → E) : ‖c • f‖_[p, w] = ‖c‖ * ‖f‖_[p, w] := by + rw [wLpNorm, wLpNorm] have : (1 : ℝ≥0∞) ≤ p := by exact_mod_cast hp - have := dLpNorm_smul this ‖c‖ fun i ↦ w i ^ (p⁻¹ : ℝ) • ‖f i‖ + have := nnLpNorm_const_smul this ‖c‖ fun i ↦ w i ^ (p⁻¹ : ℝ) • ‖f i‖ rw [norm_norm] at this rw [← this] congr with i : 1 simp only [Pi.smul_apply, Algebra.id.smul_eq_mul, Algebra.mul_smul_comm, norm_smul] @[simp] -lemma wdLpNorm_smul_right (hp : p ≠ 0) (c : ℝ≥0) (f : ∀ i, α i) : +lemma wLpNorm_smul_right (hp : p ≠ 0) (c : ℝ≥0) (f : ι → E) : ‖f‖_[p, c • w] = c ^ (p⁻¹ : ℝ) * ‖f‖_[p, w] := by - simp only [wdLpNorm_eq_sum hp, NNReal.smul_def, Pi.smul_apply, Algebra.id.smul_eq_mul, + simp only [wLpNorm_eq_sum hp, NNReal.smul_def, Pi.smul_apply, Algebra.id.smul_eq_mul, NNReal.coe_mul, mul_assoc, ← mul_sum] exact mul_rpow (by positivity) (sum_nonneg fun _ _ ↦ by positivity) -- positivity -variable [∀ i, NormedSpace ℝ (α i)] +variable [∀ i, NormedSpace ℝ E] -lemma wdLpNorm_nsmul (hp : 1 ≤ p) (n : ℕ) (w : ι → ℝ≥0) (f : ∀ i, α i) : +lemma wLpNorm_nsmul (hp : 1 ≤ p) (n : ℕ) (w : ι → ℝ≥0) (f : ι → E) : ‖n • f‖_[p, w] = n • ‖f‖_[p, w] := by - rw [← Nat.cast_smul_eq_nsmul ℝ, wdLpNorm_smul hp, RCLike.norm_natCast, nsmul_eq_mul] + rw [← Nat.cast_smul_eq_nsmul ℝ, wLpNorm_smul hp, RCLike.norm_natCast, nsmul_eq_mul] end one_le @@ -137,32 +132,32 @@ section Real variable {p : ℝ≥0} {w : ι → ℝ≥0} {f g : ι → ℝ} @[simp] -lemma wdLpNorm_one (hp : p ≠ 0) (w : ι → ℝ≥0) : +lemma wLpNorm_one (hp : p ≠ 0) (w : ι → ℝ≥0) : ‖(1 : ι → ℝ)‖_[p, w] = (∑ i, w i : ℝ) ^ (p⁻¹ : ℝ) := by - simp [wdLpNorm_eq_sum hp, NNReal.smul_def] + simp [wLpNorm_eq_sum hp, NNReal.smul_def] -lemma wdLpNorm_mono (hf : 0 ≤ f) (hfg : f ≤ g) : ‖f‖_[p, w] ≤ ‖g‖_[p, w] := +lemma wLpNorm_mono (hf : 0 ≤ f) (hfg : f ≤ g) : ‖f‖_[p, w] ≤ ‖g‖_[p, w] := dLpNorm_mono (fun i ↦ by dsimp; positivity) fun i ↦ smul_le_smul_of_nonneg_left (by rw [norm_of_nonneg (hf _), norm_of_nonneg (hf.trans hfg _)]; exact hfg _) $ by positivity end Real -section wdLpNorm +section wLpNorm variable {α β : Type*} [Fintype α] {p : ℝ≥0} {w : α → ℝ≥0} @[simp] -lemma wdLpNorm_conj [RCLike β] (f : α → β) : ‖conj f‖_[p, w] = ‖f‖_[p, w] := by simp [wdLpNorm] +lemma wLpNorm_conj [RCLike β] (f : α → β) : ‖conj f‖_[p, w] = ‖f‖_[p, w] := by simp [wLpNorm] variable [AddCommGroup α] -@[simp] lemma wdLpNorm_translate [NormedAddCommGroup β] (a : α) (f : α → β) : +@[simp] lemma wLpNorm_translate [NormedAddCommGroup β] (a : α) (f : α → β) : ‖τ a f‖_[p, τ a w] = ‖f‖_[p, w] := (dLpNorm_translate a fun i ↦ w i ^ (p⁻¹ : ℝ) • ‖f i‖ : _) @[simp] -lemma wdLpNorm_conjneg [RCLike β] (f : α → β) : ‖conjneg f‖_[p] = ‖f‖_[p] := by simp [wdLpNorm] +lemma wLpNorm_conjneg [RCLike β] (f : α → β) : ‖conjneg f‖_[p] = ‖f‖_[p] := by simp [wLpNorm] -end wdLpNorm +end wLpNorm namespace Mathlib.Meta.Positivity open Lean Meta Qq Function @@ -171,16 +166,16 @@ open Lean Meta Qq Function @[positivity ‖_‖_[_, _]] def evalWLpNorm : PositivityExt where eval {u α} _ _ e := do if let 0 := u then -- lean4#3060 means we can't combine this with the match below match α, e with - | ~q(ℝ), ~q(@wdLpNorm $ι $instι $α $instnorm $p $w $f) => + | ~q(ℝ), ~q(@wLpNorm $ι $instι $α $instnorm $p $w $f) => assumeInstancesCommute - return .nonnegative q(wdLpNorm_nonneg) - | _ => throwError "not wdLpNorm" + return .nonnegative q(wLpNorm_nonneg) + | _ => throwError "not wLpNorm" else - throwError "not wdLpNorm" + throwError "not wLpNorm" section Examples section NormedAddCommGroup -variable {α : ι → Type*} [∀ i, NormedAddCommGroup (α i)] {w : ι → ℝ≥0} {f : ∀ i, α i} +variable {α : ι → Type*} [∀ i, NormedAddCommGroup E] {w : ι → ℝ≥0} {f : ι → E} example {p : ℝ≥0} : 0 ≤ ‖f‖_[p, w] := by positivity diff --git a/LeanAPAP/Prereqs/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean index cfe900706f..23f7c64759 100644 --- a/LeanAPAP/Prereqs/NNLpNorm.lean +++ b/LeanAPAP/Prereqs/NNLpNorm.lean @@ -136,4 +136,12 @@ lemma nnLpNorm_mono_real {g : α → ℝ} (hg : Memℒp g p μ) (h : ∀ x, ‖f nnLpNorm f p μ ≤ nnLpNorm g p μ := ENNReal.toNNReal_mono (hg.eLpNorm_ne_top) (eLpNorm_mono_real h) +lemma nnLpNorm_smul_measure_of_ne_zero {p : ℝ≥0∞} {f : α → F} {c : ℝ≥0} (hc : c ≠ 0) : + nnLpNorm f p (c • μ) = c ^ p⁻¹.toReal • nnLpNorm f p μ := by + simp [nnLpNorm, eLpNorm_smul_measure_of_ne_zero'' hc f p μ] + +lemma nnLpNorm_smul_measure_of_ne_top {p : ℝ≥0∞} (hp : p ≠ ∞) {f : α → F} (c : ℝ≥0) : + nnLpNorm f p (c • μ) = c ^ p⁻¹.toReal • nnLpNorm f p μ := by + simp [nnLpNorm, eLpNorm_smul_measure_of_ne_top'' hp] + end MeasureTheory diff --git a/LeanAPAP/Prereqs/Rudin.lean b/LeanAPAP/Prereqs/Rudin.lean index efe33afb2f..384097ec57 100644 --- a/LeanAPAP/Prereqs/Rudin.lean +++ b/LeanAPAP/Prereqs/Rudin.lean @@ -94,7 +94,7 @@ private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociate · rwa [cft_smul, support_const_smul_of_ne_zero] positivity simp_rw [Function.comp_def, Pi.smul_apply, Complex.smul_re, ← Pi.smul_def] at H - rw [ndLpNorm_smul, ndLpNorm_smul, norm_div, norm_of_nonneg, norm_of_nonneg, mul_left_comm, + rw [cLpNorm_smul, cLpNorm_smul, norm_div, norm_of_nonneg, norm_of_nonneg, mul_left_comm, mul_le_mul_left] at H refine H ?_ rw [div_mul_cancel₀] @@ -106,7 +106,7 @@ private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociate have : (‖re ∘ f‖ₙ_[↑p] / p) ^ p ≤ (2 * exp 2⁻¹) ^ p := by calc _ = 𝔼 a, |(f a).re| ^ p / p ^ p := by - simp [div_pow, ndLpNorm_pow_eq_expect hp₀]; rw [expect_div] + simp [div_pow, cLpNorm_pow_eq_expect hp₀]; rw [expect_div] _ ≤ 𝔼 a, |(f a).re| ^ p / p ! := by gcongr; norm_cast; exact p.factorial_le_pow _ ≤ 𝔼 a, exp |(f a).re| := by gcongr; exact pow_div_factorial_le_exp _ (abs_nonneg _) _ _ ≤ _ := rudin_exp_abs_ineq f hf @@ -125,10 +125,10 @@ lemma rudin_ineq (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociated $ support ‖f‖ₙ_[p] = ‖(fun a ↦ ((f a).re : ℂ)) + I • (fun a ↦ ((f a).im : ℂ))‖ₙ_[p] := by congr with a; simp [mul_comm I] _ ≤ ‖fun a ↦ ((f a).re : ℂ)‖ₙ_[p] + ‖I • (fun a ↦ ((f a).im : ℂ))‖ₙ_[p] - := ndLpNorm_add_le hp₁ _ _ + := cLpNorm_add_le hp₁ _ _ _ = ‖re ∘ f‖ₙ_[p] + ‖re ∘ ((-I) • f)‖ₙ_[p] := by - rw [ndLpNorm_smul hp₁, Complex.norm_I, one_mul, ← Complex.ndLpNorm_coe_comp, - ← Complex.ndLpNorm_coe_comp] + rw [cLpNorm_smul hp₁, Complex.norm_I, one_mul, ← Complex.cLpNorm_coe_comp, + ← Complex.cLpNorm_coe_comp] congr ext a : 1 simp @@ -136,4 +136,4 @@ lemma rudin_ineq (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociated $ support := add_le_add (rudin_ineq_aux hp _ hf) $ rudin_ineq_aux hp _ $ by rwa [cft_smul, support_const_smul_of_ne_zero]; simp _ = 4 * exp 2⁻¹ * sqrt p * ‖f‖ₙ_[2] := by - rw [ndLpNorm_smul one_le_two, norm_neg, Complex.norm_I, one_mul]; ring + rw [cLpNorm_smul one_le_two, norm_neg, Complex.norm_I, one_mul]; ring