progress

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

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

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

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 _ _

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

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

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]

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

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

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]

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**. -/

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,

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