wLpNorm done

LeanAPAP.lean

@@ -10,6 +10,7 @@ import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Operations
+import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Mathlib.Data.Finset.Density
 import LeanAPAP.Mathlib.Data.Fintype.Order
 import LeanAPAP.Mathlib.Data.NNReal.Basic

LeanAPAP/Mathlib/Data/ENNReal/Real.lean

@@ -0,0 +1,3 @@
+import Mathlib.Data.ENNReal.Real
+
+attribute [simp] ENNReal.toReal_inv

LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -1,9 +1,10 @@
 import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+import LeanAPAP.Mathlib.Data.ENNReal.Real
 
 noncomputable section
 
 open TopologicalSpace MeasureTheory Filter
-open scoped NNReal ENNReal Topology
+open scoped NNReal ENNReal Topology ComplexConjugate
 
 variable {α E F G : Type*} {m m0 : MeasurableSpace α} {p : ℝ≥0∞} {q : ℝ} {μ ν : Measure α}
   [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] {f : α → F}
@@ -38,29 +39,38 @@ lemma eLpNorm_lt_top_of_finite [Finite α] [IsFiniteMeasure μ] : eLpNorm f p μ
 @[simp] lemma eLpNorm_of_isEmpty [IsEmpty α] (f : α → E) (p : ℝ≥0∞) : eLpNorm f p μ = 0 := by
   simp [Subsingleton.elim f 0]
 
--- TODO: Make `p` and `μ` explicit in `eLpNorm_const_smul`
+-- TODO: Make `p` and `μ` explicit in `eLpNorm_const_smul`, `eLpNorm_neg`
+
+@[simp] lemma eLpNorm_neg' (f : α → F) (p : ℝ≥0∞) (μ : Measure α) :
+    eLpNorm (fun x ↦ -f x) p μ = eLpNorm f p μ := eLpNorm_neg
+
+lemma eLpNorm_sub_comm (f g : α → E) (p : ℝ≥0∞) (μ : Measure α) :
+    eLpNorm (f - g) p μ = eLpNorm (g - f) p μ := by simp [← eLpNorm_neg (f := f - g)]
 
 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
+    (μ : 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 μ :=
+    (μ : 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
+    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
+    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]
 
+@[simp] lemma eLpNorm_conj {K : Type*} [RCLike K] (f : α → K) (p : ℝ≥0∞) (μ : Measure α) :
+    eLpNorm (conj f) p μ = eLpNorm f p μ := by simp [← eLpNorm_norm]
+
 end MeasureTheory

LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean

@@ -7,4 +7,7 @@ variable {ι α : Type*} {mα : MeasurableSpace α} {s : Finset ι} {μ : ι →
 
 instance : IsFiniteMeasure (∑ i ∈ s, μ i) where measure_univ_lt_top := by simp [measure_lt_top]
 
+instance [Fintype ι] : IsFiniteMeasure (.sum μ) where
+  measure_univ_lt_top := by simp [measure_lt_top]
+
 end MeasureTheory

LeanAPAP/Physics/Unbalancing.lean

@@ -1,17 +1,18 @@
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
+import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 import LeanAPAP.Prereqs.LpNorm.Weighted
 
 /-!
 # Unbalancing
 -/
 
-open Finset Real
-open scoped ComplexConjugate ComplexOrder NNReal
+open Finset Real MeasureTheory
+open scoped ComplexConjugate ComplexOrder NNReal ENNReal
 
-variable {G : Type*} [Fintype G] [DecidableEq G] [AddCommGroup G] {ν : G → ℝ≥0} {f : G → ℝ}
-  {g h : G → ℂ} {ε : ℝ} {p : ℕ}
+variable {G : Type*} [Fintype G] [MeasurableSpace G] [DiscreteMeasurableSpace G] [DecidableEq G]
+  [AddCommGroup G] {ν : G → ℝ≥0} {f : G → ℝ} {g h : G → ℂ} {ε : ℝ} {p : ℕ}
 
 /-- Note that we do the physical proof in order to avoid the Fourier transform. -/
 lemma pow_inner_nonneg' {f : G → ℂ} (hf : f = g ○ g) (hν : (↑) ∘ ν = h ○ h) (k : ℕ) :
@@ -56,16 +57,18 @@ private lemma p'_pos (hp : 5 ≤ p) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) : 0 <
 private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1)
     (hf : (↑) ∘ f = g ○ g) (hν : (↑) ∘ ν = h ○ h) (hν₁ : ‖((↑) ∘ ν : G → ℝ)‖_[1] = 1)
     (hε : ε ≤ ‖f‖_[p, ν]) :
-    1 + ε / 2 ≤ ‖f + 1‖_[(⟨24 / ε * log (3 / ε) * p, (p'_pos hp hε₀ hε₁).le⟩ : ℝ≥0), ν] := by
-  simp only [dL1Norm_eq_sum, NNReal.norm_eq, Function.comp_apply] at hν₁
+    1 + ε / 2 ≤ ‖f + 1‖_[.ofReal (24 / ε * log (3 / ε) * p), ν] := by
+  simp only [dL1Norm_eq_sum, NNReal.nnnorm_eq, Function.comp_apply] at hν₁
   obtain hf₁ | hf₁ := le_total 2 ‖f + 1‖_[2 * p, ν]
   · calc
       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₁
-      _ ≤ _ := wLpNorm_mono_right (NNReal.coe_le_coe.1 ?_) _ _
+      _ ≤ _ := wLpNorm_mono_right ?_ _ _
+    norm_cast
+    rw [ENNReal.natCast_le_ofReal (by positivity)]
     push_cast
-    refine mul_le_mul_of_nonneg_right ?_ ?_
+    gcongr
     calc
       2 ≤ 24 / 1 * 0.6931471803 := by norm_num
       _ ≤ 24 / ε * log (3 / ε) :=
@@ -82,13 +85,15 @@ 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 [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,
-      pow_sub_one_mul hp₁.pos.ne']
-    simp [l2Inner_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]
+    · norm_cast
+      rw [wLpNorm_pow_eq_sum hp₁.pos.ne']
+      push_cast
+      dsimp
+      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 _),
+        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
   have hTP : T ⊆ P := monotone_filter_right _ fun i ↦ le_trans $ by positivity
@@ -106,7 +111,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       _ ≤ ∑ i in P \ T, ↑(ν i) * (3 / 4 * ε) ^ p := sum_le_sum fun i hi ↦ ?_
       _ = (3 / 4) ^ p * ε ^ p * ∑ i in P \ T, (ν i : ℝ) := by rw [← sum_mul, mul_comm, mul_pow]
       _ ≤ 4⁻¹ * ε ^ p * ∑ i, (ν i : ℝ) := ?_
-      _ = 4⁻¹ * ε ^ p := by rw [hν₁, mul_one]
+      _ = 4⁻¹ * ε ^ p := by norm_cast; simp [hν₁]
     · simp only [mem_sdiff, mem_filter, mem_univ, true_and_iff, not_le, P, T] at hi
       exact mul_le_mul_of_nonneg_left (pow_le_pow_left hi.1 hi.2.le _) (by positivity)
     · refine mul_le_mul (mul_le_mul_of_nonneg_right (le_trans (pow_le_pow_of_le_one ?_ ?_ hp) ?_)
@@ -116,8 +121,12 @@ 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, ν] := wLpNorm_le_add_wLpNorm_add hp' _ _ _
-      _ ≤ (2 + 1 : ℝ) := (add_le_add hf₁ (by rw [wLpNorm_one, hν₁, one_rpow]; positivity))
+      _ ≤ ‖f + 1‖_[2 * p, ν] + ‖(1 : G → ℝ)‖_[2 * p, ν] :=
+        wLpNorm_le_add_wLpNorm_add (mod_cast hp') _ _ _
+      _ ≤ 2 + 1 := by
+        gcongr
+        have : 2 * (p : ℝ≥0∞) ≠ 0 := mul_ne_zero two_ne_zero (by positivity)
+        simp [wLpNorm_one, ENNReal.mul_ne_top, *]
       _ = 3 := by norm_num
   replace hp' := zero_lt_one.trans_le hp'
   have : 4⁻¹ * ε ^ p ≤ sqrt (∑ i in T, ν i) * 3 ^ p := by

LeanAPAP/Prereqs/Function/Translate.lean

@@ -38,21 +38,27 @@ lemma translate_comm (a b : α) (f : α → β) : τ a (τ b f) = τ b (τ a f)
 @[simp]
 lemma translate_smul_right [SMul γ β] (a : α) (f : α → β) (c : γ) : τ a (c • f) = c • τ a f := rfl
 
-section AddCommGroup
-variable [AddCommGroup β]
+section AddCommMonoid
+variable [AddCommMonoid β]
 
 @[simp] lemma translate_zero_right (a : α) : τ a (0 : α → β) = 0 := rfl
 
 lemma translate_add_right (a : α) (f g : α → β) : τ a (f + g) = τ a f + τ a g := rfl
-lemma translate_sub_right (a : α) (f g : α → β) : τ a (f - g) = τ a f - τ a g := rfl
-lemma translate_neg_right (a : α) (f : α → β) : τ a (-f) = -τ a f := rfl
 
 lemma translate_sum_right (a : α) (f : ι → α → β) (s : Finset ι) :
     τ a (∑ i in s, f i) = ∑ i in s, τ a (f i) := by ext; simp
 
 lemma sum_translate [Fintype α] (a : α) (f : α → β) : ∑ b, τ a f b = ∑ b, f b :=
   Fintype.sum_equiv (Equiv.subRight _) _ _ fun _ ↦ rfl
 
+end AddCommMonoid
+
+section AddCommGroup
+variable [AddCommGroup β]
+
+lemma translate_sub_right (a : α) (f g : α → β) : τ a (f - g) = τ a f - τ a g := rfl
+lemma translate_neg_right (a : α) (f : α → β) : τ a (-f) = -τ a f := rfl
+
 @[simp] lemma support_translate (a : α) (f : α → β) : support (τ a f) = a +ᵥ support f := by
   ext; simp [mem_vadd_set_iff_neg_vadd_mem, sub_eq_neg_add]