Replace dL2Inner and cL2Inner by wInner

LeanAPAP.lean

@@ -43,10 +43,10 @@ import LeanAPAP.Prereqs.Function.Indicator.Basic
 import LeanAPAP.Prereqs.Function.Indicator.Complex
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.Function.Translate
-import LeanAPAP.Prereqs.Inner.Compact
-import LeanAPAP.Prereqs.Inner.Discrete.Basic
-import LeanAPAP.Prereqs.Inner.Discrete.Defs
 import LeanAPAP.Prereqs.Inner.Function
+import LeanAPAP.Prereqs.Inner.Hoelder.Compact
+import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
+import LeanAPAP.Prereqs.Inner.Weighted
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Prereqs.LpNorm.Compact
 import LeanAPAP.Prereqs.LpNorm.Discrete.Basic

LeanAPAP/FiniteField.lean

@@ -17,7 +17,7 @@ set_option linter.haveLet 0
 
 attribute [-simp] Real.log_inv
 
-open FiniteDimensional Fintype Function Real MeasureTheory
+open FiniteDimensional Fintype Function MeasureTheory RCLike Real
 open Finset hiding card
 open scoped ENNReal NNReal BigOperators Combinatorics.Additive Pointwise
 
@@ -85,7 +85,7 @@ private lemma curlog_pow_le {n : ℕ} (hx₀ : 0 < x) (hn : n ≠ 0) : 𝓛 (x ^
   rw [← rpow_natCast]; exact curlog_rpow_le hx₀ $ mod_cast Nat.one_le_iff_ne_zero.2 hn
 
 lemma global_dichotomy [MeasurableSpace G] [DiscreteMeasurableSpace G] (hA : A.Nonempty)
-    (hγC : γ ≤ C.dens) (hγ : 0 < γ) (hAC : ε ≤ |card G * ⟪μ A ∗ μ A, μ C⟫_[ℝ] - 1|) :
+    (hγC : γ ≤ C.dens) (hγ : 0 < γ) (hAC : ε ≤ |card G * ⟪μ_[ℝ] A ∗ μ A, μ C⟫_[ℝ] - 1|) :
     ε / (2 * card G) ≤ ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[↑(2 * ⌈𝓛 γ⌉₊), μ univ] := by
   have hC : C.Nonempty := by simpa using hγ.trans_le hγC
   have hγ₁ : γ ≤ 1 := hγC.trans (by norm_cast; exact dens_le_one)
@@ -99,13 +99,13 @@ lemma global_dichotomy [MeasurableSpace G] [DiscreteMeasurableSpace G] (hA : A.N
     _ ≤ _ := 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_dL2Inner_le_dLpNorm_mul_dLpNorm hp''.coe_ennreal _ _
+        abs_wInner_one_le_dLpNorm_mul_dLpNorm hp''.coe_ennreal _ _
     _ ≤ ‖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 * ⌈𝓛 γ⌉₊), μ univ] * γ ^ (-(p : ℝ)⁻¹) := ?_
     _ ≤ _ := mul_le_mul_of_nonneg_left ?_ $ by positivity
-  · rw [← balance_conv, balance, dL2Inner_sub_left, dL2Inner_const_left, expect_conv, sum_mu ℝ hA,
+  · rw [← balance_conv, balance, wInner_sub_left, wInner_one_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]
@@ -221,8 +221,8 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
       _ = 2 ^ 32 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 := by ring
   · have : ∑ x ∈ S, (μ_[ℝ] V' ∗ μ A₁ ∗ μ A₂) x = 𝔼 x ∈ V', (μ A₁ ∗ μ A₂ ○ 𝟭 S) x := by
       have : -V' = V' := by ext; simp [V']
-      rw [← mu_dL2Inner, ← indicate_dL2Inner, conv_rotate, ← dconv_dL2Inner_eq_dL2Inner_conv,
-        dL2Inner_dconv_eq_conv_dL2Inner, ← conv_conjneg, conjneg_mu, this, conv_comm]
+      rw [← mu_wInner_one, ← indicate_wInner_one, conv_rotate, ← dconv_wInner_one_eq_wInner_one_conv,
+        wInner_one_dconv_eq_conv_wInner_one, ← conv_conjneg, conjneg_mu, this, conv_comm]
     have : ∑ x ∈ S, (μ_[ℝ] A₁ ∗ μ A₂) x = (μ_[ℝ] A₁ ∗ μ A₂ ○ 𝟭 S) 0 := by simp [dconv_indicate]
     sorry
 
@@ -236,7 +236,7 @@ lemma ap_in_ff' (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (h
 set_option maxHeartbeats 300000 in
 lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q) (hq : q.Prime)
     (hε₀ : 0 < ε) (hε₁ : ε < 1) (hγC : γ ≤ C.dens) (hγ : 0 < γ)
-    (hAC : ε ≤ |card G * ⟪μ A ∗ μ A, μ C⟫_[ℝ] - 1|) :
+    (hAC : ε ≤ |card G * ⟪μ_[ℝ] A ∗ μ A, μ C⟫_[ℝ] - 1|) :
     ∃ (V : Submodule (ZMod q) G) (_ : DecidablePred (· ∈ V)),
         ↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤
             2 ^ 132 * 𝓛 A.dens ^ 4 * 𝓛 γ ^ 4 / ε ^ 16 ∧
@@ -407,11 +407,12 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
           positivity
         · exact subset_univ _
       _ = card G • ⟪μ_[ℝ] (Set.toFinset V) ∗ μ A, μ A ∗ μ A₂ ○ μ A₁⟫_[ℝ] := by
-        rw [← dL2Inner_dconv_eq_conv_dL2Inner, dconv_right_comm, conv_dconv_right_comm (μ A),
-          dL2Inner_dconv_eq_conv_dL2Inner, ← dconv_dL2Inner_eq_dL2Inner_conv, dL2Inner_anticomm]
-        simp [dL2Inner, smul_sum, mul_assoc]
+        rw [← wInner_one_dconv_eq_conv_wInner_one, dconv_right_comm, conv_dconv_right_comm (μ A),
+          wInner_one_dconv_eq_conv_wInner_one, ← dconv_wInner_one_eq_wInner_one_conv,
+          ← conj_wInner_symm]
+        simp [wInner_one_eq_sum, inner_apply, smul_sum, mul_assoc]
       _ ≤ card G • (‖μ_[ℝ] (Set.toFinset V) ∗ μ A‖_[∞] * ‖μ A ∗ μ A₂ ○ μ A₁‖_[1]) := by
-        gcongr; exact dL2Inner_le_dLpNorm_mul_dLpNorm .top_one _ _
+        gcongr; exact wInner_one_le_dLpNorm_mul_dLpNorm .top_one _ _
       _ = _ := by
         have : 0 < (4 : ℝ)⁻¹ * A.dens ^ (2 * q') := by positivity
         replace hA₁ : A₁.Nonempty := by simpa using this.trans_le hA₁
@@ -463,18 +464,18 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
       (B : Finset V), n ≤ finrank (ZMod q) V + 2 ^ 148 * i * 𝓛 α ^ 8 ∧ ThreeAPFree (B : Set V)
         ∧ α ≤ B.dens ∧
       (B.dens < (65 / 64 : ℝ) ^ i * α →
-        2⁻¹ ≤ card V * ⟪μ B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ]) := by
+        2⁻¹ ≤ card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ]) := by
     induction' i with i ih hi
     · exact ⟨G, inferInstance, inferInstance, inferInstance, inferInstance, A, by simp, hA,
         by simp, by simp [α, nnratCast_dens, Fintype.card_subtype, subset_iff]⟩
     obtain ⟨V, _, _, _, _, B, hV, hB, hαβ, hBV⟩ := ih
-    obtain hB' | hB' := le_or_lt 2⁻¹ (card V * ⟪μ B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ])
+    obtain hB' | hB' := le_or_lt 2⁻¹ (card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ])
     · exact ⟨V, inferInstance, inferInstance, inferInstance, inferInstance, B,
         hV.trans (by gcongr; exact i.le_succ), hB, hαβ, fun _ ↦ hB'⟩
     let _ : MeasurableSpace V := ⊤
     have : DiscreteMeasurableSpace V := ⟨fun _ ↦ trivial⟩
     have : 0 < 𝓛 B.dens := curlog_pos (by positivity) (by simp)
-    have : 2⁻¹ ≤ |card V * ⟪μ B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ] - 1| := by
+    have : 2⁻¹ ≤ |card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ] - 1| := by
       rw [abs_sub_comm, le_abs, le_sub_comm]
       norm_num at hB' ⊢
       exact .inl hB'.le
@@ -538,7 +539,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
           log (65 / 64) ≤ 65/64 - 1 := log_le_sub_one_of_pos $ by norm_num
           _ ≤ 1 := by norm_num
     all_goals positivity
-  rw [hB.dL2Inner_mu_conv_mu_mu_two_smul_mu] at hBV
+  rw [hB.wInner_one_mu_conv_mu_mu_two_smul_mu] at hBV
   suffices h : (q ^ (n - 2 ^ 155 * 𝓛 α ^ 9) : ℝ) ≤ q ^ (n / 2) by
     rwa [rpow_le_rpow_left_iff ‹_›, sub_le_comm, sub_half, div_le_iff₀' zero_lt_two, ← mul_assoc,
       ← pow_succ'] at h

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -4,7 +4,7 @@ import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Expect.Complex
-import LeanAPAP.Prereqs.Inner.Discrete.Basic
+import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 
 /-!

LeanAPAP/Physics/DRC.lean

@@ -8,7 +8,7 @@ import LeanAPAP.Prereqs.LpNorm.Weighted
 # Dependent Random Choice
 -/
 
-open Real Finset Fintype Function MeasureTheory
+open Finset Fintype Function MeasureTheory RCLike Real
 open scoped ENNReal NNReal Pointwise
 
 variable {G : Type*} [DecidableEq G] [Fintype G] [AddCommGroup G] {p : ℕ} {B₁ B₂ A : Finset G}
@@ -22,7 +22,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 [dL2Inner_eq_sum, RCLike.conj_to_real, mul_sum, sum_mul, smul_sum,
+  simp only [wInner_one_eq_sum, inner_apply, 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₂
@@ -102,7 +102,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_norm hp₀, dL2Inner_eq_sum, sum_dconv, sum_indicate, Pi.one_apply,
+    simpa only [wLpNorm_pow_eq_sum_norm hp₀, wInner_one_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
@@ -113,7 +113,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, boole_mul] at hs
     split_ifs at hs with h; swap
-    · simp only [zero_mul, dL2Inner_eq_sum, Function.comp_apply, RCLike.inner_apply,
+    · simp only [zero_mul, wInner_one_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
@@ -127,8 +127,8 @@ 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, dL2Inner_smul_left, star_trivial,
-        nsmul_eq_mul, mul_assoc]
+    · simp_rw [A₁, A₂, g, ← card_smul_mu, smul_dconv, dconv_smul, ← Nat.cast_smul_eq_nsmul ℝ,
+        wInner_smul_left, star_trivial, mul_assoc]
     any_goals positivity
     all_goals exact Nat.cast_le.2 $ card_mono inter_subset_left
   rw [← sum_mul, lemma_0, nsmul_eq_mul, Nat.cast_mul, ← sum_mul, mul_right_comm, ← hgB,
@@ -200,7 +200,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 [dL2Inner_eq_sum, -mem_compl, -mem_s, apply_ite NNReal.toReal, indicate_apply]
+      simp [wInner_one_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

@@ -3,7 +3,7 @@ import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Complex
-import LeanAPAP.Prereqs.Inner.Discrete.Defs
+import LeanAPAP.Prereqs.Inner.Weighted
 import LeanAPAP.Prereqs.LpNorm.Weighted
 
 /-!
@@ -12,20 +12,20 @@ import LeanAPAP.Prereqs.LpNorm.Weighted
 
 open Finset hiding card
 open Fintype (card)
-open Function Real MeasureTheory
+open Function MeasureTheory RCLike Real
 open scoped ComplexConjugate ComplexOrder NNReal ENNReal
 
 variable {G : Type*} [Fintype 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 : g ○ g = f) (hν : h ○ h = (↑) ∘ ν) (k : ℕ) :
-    (0 : ℂ) ≤ ⟪f ^ k, (↑) ∘ ν⟫_[ℂ] := by
+    0 ≤ ⟪f ^ k, (↑) ∘ ν⟫_[ℂ] := by
   suffices
     ⟪f ^ k, (↑) ∘ ν⟫_[ℂ] = ∑ z : Fin k → G, (‖∑ x, (∏ i, conj (g (x + z i))) * h x‖ : ℂ) ^ 2 by
     rw [this]
     positivity
-  rw [← hf, ← hν, dL2Inner_eq_sum]
+  rw [← hf, ← hν, wInner_one_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 :(
@@ -50,7 +50,7 @@ lemma pow_inner_nonneg' {f : G → ℂ} (hf : g ○ g = f) (hν : h ○ h = (↑
 /-- Note that we do the physical proof in order to avoid the Fourier transform. -/
 lemma pow_inner_nonneg {f : G → ℝ} (hf : g ○ g = (↑) ∘ f) (hν : h ○ h = (↑) ∘ ν) (k : ℕ) :
     (0 : ℝ) ≤ ⟪(↑) ∘ ν, f ^ k⟫_[ℝ] := by
-  simpa [← Complex.zero_le_real, dL2Inner_eq_sum, mul_comm] using pow_inner_nonneg' hf hν k
+  simpa [← Complex.zero_le_real, wInner_one_eq_sum, mul_comm] using pow_inner_nonneg' hf hν k
 
 private lemma log_ε_pos (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) : 0 < log (3 / ε) :=
   log_pos $ (one_lt_div hε₀).2 $ hε₁.trans_lt $ by norm_num
@@ -99,7 +99,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 [dL2Inner_eq_sum, ← sum_add_distrib, ← mul_add, ← pow_sub_one_mul hp₁.pos.ne' (f _),
+    · simp [wInner_one_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

@@ -1,24 +1,17 @@
 import Mathlib.Algebra.BigOperators.Expect
 import Mathlib.Algebra.Group.AddChar
-import LeanAPAP.Prereqs.Inner.Discrete.Defs
+import LeanAPAP.Prereqs.Inner.Weighted
 
 open Finset hiding card
 open Fintype (card)
-open Function MeasureTheory
+open Function RCLike
 open scoped BigOperators ComplexConjugate DirectSum
 
 variable {G H R : Type*}
 
 namespace AddChar
 section AddGroup
 variable [AddGroup G]
-section RCLike
-variable [RCLike R]
-
-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
 
 section Semifield
 variable [Fintype G] [Semifield R] [IsDomain R] [CharZero R] {ψ : AddChar G R}
@@ -37,6 +30,14 @@ lemma expect_eq_zero_iff_ne_zero : 𝔼 x, ψ x = 0 ↔ ψ ≠ 0 := by
 lemma expect_ne_zero_iff_eq_zero : 𝔼 x, ψ x ≠ 0 ↔ ψ = 0 := expect_eq_zero_iff_ne_zero.not_left
 
 end Semifield
+
+section RCLike
+variable [RCLike R] [Fintype G]
+
+lemma wInner_compact_self (ψ : AddChar G R) : ⟪(ψ : G → R), ψ⟫ₙ_[R] = 1 := by
+  simp [wInner_compact_eq_expect, ψ.norm_apply, RCLike.conj_mul]
+
+end RCLike
 end AddGroup
 
 section AddCommGroup
@@ -45,26 +46,26 @@ variable [AddCommGroup G]
 section RCLike
 variable [RCLike R] {ψ₁ ψ₂ : AddChar G R}
 
-lemma dL2Inner_eq [Fintype G] (ψ₁ ψ₂ : AddChar G R) :
-    ⟪(ψ₁ : G → R), ψ₂⟫_[R] = if ψ₁ = ψ₂ then ↑(card G) else 0 := by
+lemma wInner_compact_eq_boole [Fintype G] (ψ₁ ψ₂ : AddChar G R) :
+    ⟪(ψ₁ : G → R), ψ₂⟫ₙ_[R] = if ψ₁ = ψ₂ then 1 else 0 := by
   split_ifs with h
-  · rw [h, AddChar.dL2Inner_self]
+  · rw [h, wInner_compact_self]
   have : ψ₁⁻¹ * ψ₂ ≠ 1 := by rwa [Ne, inv_mul_eq_one]
-  simp_rw [dL2Inner_eq_sum, ← inv_apply_eq_conj]
-  simpa [map_neg_eq_inv] using sum_eq_zero_iff_ne_zero.2 this
+  simp_rw [wInner_compact_eq_expect, RCLike.inner_apply, ← inv_apply_eq_conj]
+  simpa [map_neg_eq_inv] using expect_eq_zero_iff_ne_zero.2 this
 
-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 wInner_compact_eq_zero_iff_ne [Fintype G] : ⟪(ψ₁ : G → R), ψ₂⟫ₙ_[R] = 0 ↔ ψ₁ ≠ ψ₂ := by
+  rw [wInner_compact_eq_boole, one_ne_zero.ite_eq_right_iff]
 
-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)]
+lemma wInner_compact_eq_one_iff_eq [Fintype G] : ⟪(ψ₁ : G → R), ψ₂⟫ₙ_[R] = 1 ↔ ψ₁ = ψ₂ := by
+  rw [wInner_compact_eq_boole, one_ne_zero.ite_eq_left_iff]
 
 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_dL2Inner_eq_zero AddChar.coe_ne_zero fun ψ₁ ψ₂ ↦
-    dL2Inner_eq_zero_iff_ne.2
+  exact linearIndependent_of_ne_zero_of_wInner_compact_eq_zero AddChar.coe_ne_zero fun ψ₁ ψ₂ ↦
+    wInner_compact_eq_zero_iff_ne.2
 
 noncomputable instance instFintype [Finite G] : Fintype (AddChar G R) :=
   @Fintype.ofFinite _ (AddChar.linearIndependent G R).finite