linfty_ap_boosted

LeanAPAP.lean

@@ -45,6 +45,7 @@ import LeanAPAP.Mathlib.Data.Finset.Basic
 import LeanAPAP.Mathlib.Data.Finset.Card
 import LeanAPAP.Mathlib.Data.Finset.Image
 import LeanAPAP.Mathlib.Data.Finset.NatAntidiagonal
+import LeanAPAP.Mathlib.Data.Finset.Pi
 import LeanAPAP.Mathlib.Data.Finset.Pointwise
 import LeanAPAP.Mathlib.Data.Finset.Powerset
 import LeanAPAP.Mathlib.Data.Fintype.Basic

LeanAPAP/Mathlib/Data/Finset/Pi.lean

@@ -0,0 +1,11 @@
+import Mathlib.Data.Finset.Pi
+
+namespace Finset
+variable {α : Type*} {β : α → Type*} [DecidableEq α] {s : Finset α} {t : ∀ a, Finset (β a)}
+
+lemma pi_nonempty (ht : ∀ a ∈ s, (t a).Nonempty) : (s.pi t).Nonempty := by
+  choose x hx using ht
+  simp_rw [Finset.Nonempty, mem_pi]
+  exact ⟨x, hx⟩
+
+end Finset

LeanAPAP/Mathlib/Data/Fintype/Pi.lean

@@ -1,12 +1,16 @@
 import Mathlib.Data.Finset.NAry
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.Fintype.Pi
+import LeanAPAP.Mathlib.Data.Finset.Pi
 
 open Finset
 
 namespace Fintype
 variable {α : Type*} {β γ : α → Type*} [Fintype α] [DecidableEq α] [∀ a, DecidableEq (γ a)]
 
+lemma piFinset_nonempty {s : ∀ a, Finset (β a)} (hs : ∀ a, (s a).Nonempty) :
+    (piFinset s).Nonempty := (pi_nonempty fun _ _ ↦ hs _).map
+
 @[simp]
 lemma piFinset_of_isEmpty [IsEmpty α] (s : ∀ a, Finset (β a)) : piFinset s = univ :=
   eq_univ_of_forall fun _ ↦ by simp
@@ -29,13 +33,16 @@ lemma piFinset_image₂ (f : ∀ a, β a → γ a → δ a) (s : ∀ a, Finset (
 end Fintype
 
 namespace Fintype
-variable {α β : Type*} {δ : α → Type*}
+variable {α β : Type*} {δ : α → Type*} {s : Finset α} {n : ℕ}
 
 @[reducible]
 def piFinsetConst (s : Finset α) (n : ℕ) := piFinset fun _ : Fin n ↦ s
 
 infixl:70 "^^" => piFinsetConst
 
+protected lemma _root_.Finset.Nonempty.piFinsetConst (hs : s.Nonempty) : (s ^^ n).Nonempty :=
+  piFinset_nonempty fun _ ↦ hs
+
 @[simp] lemma card_piFinsetConst (s : Finset α) (n : ℕ) : (s ^^ n).card = s.card ^ n := by
   simp [piFinsetConst, card_piFinset]
 

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -50,7 +50,7 @@ variable {G : Type*} [DecidableEq G] [Fintype G] [AddCommGroup G] {A S : Finset
   {ε K : ℝ} {k m : ℕ}
 
 open Finset Real
-open scoped BigOperators Pointwise NNReal ENNReal
+open scoped BigOps Pointwise NNReal ENNReal
 
 namespace AlmostPeriodicity
 
@@ -60,10 +60,10 @@ def LProp (k m : ℕ) (ε : ℝ) (f : G → ℂ) (A : Finset G) (a : Fin k → G
 noncomputable instance : DecidablePred (LProp k m ε f A) := Classical.decPred _
 
 noncomputable def l (k m : ℕ) (ε : ℝ) (f : G → ℂ) (A : Finset G) : Finset (Fin k → G) :=
-  (Fintype.piFinset fun _ ↦ A).filter (LProp k m ε f A)
+  (A ^^ k).filter (LProp k m ε f A)
 
 lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m)
-    (h : ∑ a in Fintype.piFinset fun _ ↦ A,
+    (h : ∑ a in A ^^ k,
         ‖fun x : G ↦ ∑ i : Fin k, f (x - a i) - (k • (mu A ∗ f)) x‖_[2 * m] ^ (2 * m) ≤
       1 / 2 * (k * ε * ‖f‖_[2 * m]) ^ (2 * m) * A.card ^ k) :
     (A.card ^ k : ℝ) / 2 ≤ (l k m ε f A).card := by
@@ -77,9 +77,9 @@ lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m)
   refine pow_le_pow_iff_left ?_ ?_ ?_ <;> positivity
 
 lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :
-    ∑ a in Fintype.piFinset fun _ : Fin k ↦ A, ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤
+    ∑ a in A ^^ k, ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤
       (8 * m) ^ m * k ^ (m - 1) *
-        ∑ a in Fintype.piFinset fun _ : Fin k ↦ A, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) := by
+        ∑ a in A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) := by
   let f' : G → ℂ := fun a ↦ f (x - a) - (mu A ∗ f) x
   refine' (complex_marcinkiewicz_zygmund f' (by linarith only [hm]) _).trans_eq' _
   · intro i
@@ -93,10 +93,10 @@ lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :
 
 lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) :
     (8 * m : ℝ) ^ m * k ^ (m - 1) *
-        ∑ a in Fintype.piFinset fun _ : Fin k ↦ A,
+        ∑ a in A ^^ k,
           ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤
       (8 * m : ℝ) ^ m * k ^ (m - 1) *
-        ∑ a in Fintype.piFinset fun _ : Fin k ↦ A, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) := by
+        ∑ a in A ^^ k, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) := by
   -- lots of the equalities about m can be automated but it's *way* slower
   have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two]
   have hm' : 1 < 2 * m := (Nat.mul_le_mul_left 2 hm).trans_lt' $ by norm_num1
@@ -160,10 +160,10 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k)
   rw [←hmeq, mul_pow]
   simp only [lpNorm_pow_eq_sum hm']
   rw [sum_comm]
-  have : ∀ x : G, ∑ a in Fintype.piFinset fun _ : Fin k ↦ A,
+  have : ∀ x : G, ∑ a in A ^^ k,
       ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤
     (8 * m) ^ m * k ^ (m - 1) *
-      ∑ a in Fintype.piFinset fun _ : Fin k ↦ A, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) :=
+      ∑ a in A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) :=
     lemma28_part_one hm
   refine' (sum_le_sum fun x _ ↦ this x).trans _
   rw [←mul_sum]
@@ -175,9 +175,9 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k)
   simp only [this]
   have :
     (8 * m : ℝ) ^ m * k ^ (m - 1) *
-        ∑ a in Fintype.piFinset fun _ : Fin k ↦ A, ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤
+        ∑ a in A ^^ k, ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤
       (8 * m : ℝ) ^ m * k ^ (m - 1) *
-        ∑ a in Fintype.piFinset fun _ : Fin k ↦ A, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) :=
+        ∑ a in A ^^ k, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) :=
     lemma28_part_two hm hA
   refine' this.trans _
   simp only [sum_const, Fintype.card_piFinsetConst, nsmul_eq_mul, Nat.cast_pow]
@@ -263,7 +263,7 @@ lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) :
 -- might be true for dumb reason when k = 0, since L would be singleton and rhs is |G|,
 -- so its just |S| ≤ |G|
 lemma big_shifts (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0)
-    (hL' : L.Nonempty) (hL : L ⊆ Fintype.piFinset fun _ ↦ A) :
+    (hL' : L.Nonempty) (hL : L ⊆ A ^^ k) :
     ∃ a : Fin k → G, a ∈ L ∧
       L.card * S.card ≤ (A + S).card ^ k * (univ.filter fun t : G ↦ (a - fun _ ↦ t) ∈ L).card := by
   rcases S.eq_empty_or_nonempty with (rfl | hS)
@@ -431,4 +431,32 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
           (by positivity) $ (Nat.le_ceil _).trans $ mod_cast Nat.le_mul_of_pos_left (by positivity)
     _ ≤ exp 1 := rpow_neg_inv_curlog_le (by positivity) inf_le_left
 
+theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (k : ℕ) (hk : k ≠ 0)
+    (hK₂ : 2 ≤ K) (hK : (A + S).card ≤ K * A.card) (hS : S.Nonempty)
+    (B C : Finset G) (hB : B.Nonempty) (hC : C.Nonempty) :
+    ∃ T : Finset G,
+      K ^ (-4096 * ⌈curlog (min 1 (C.card / B.card))⌉ * k ^ 2/ ε ^ 2) * S.card ≤ T.card ∧
+      ‖μ T ∗^ k ∗ (μ_[ℂ] A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C‖_[∞] ≤ ε := by
+  obtain ⟨T, hKT, hT⟩ := linfty_almost_periodicity (ε / k) (by positivity)
+    (div_le_one_of_le (hε₁.trans $ mod_cast Nat.one_le_iff_ne_zero.2 hk) $ by positivity) hK₂ hK
+    _ _ hB hC
+  refine ⟨T, by simpa only [div_pow, div_div_eq_mul_div] using hKT, ?_⟩
+  set F := μ_[ℂ] A ∗ 𝟭 B ∗ μ C
+  have hT' : T.Nonempty
+  · have := hS.card_pos -- TODO: positivity
+    have : 0 < _ := hKT.trans_lt' $ by positivity
+    simpa [card_pos] using this
+  calc
+    ‖μ T ∗^ k ∗ F - F‖_[∞]
+      = ‖𝔼 a ∈ T ^^ k, (τ (∑ i, a i) F - F)‖_[∞] := by
+        rw [mu_iterConv_conv, expect_sub_distrib, expect_const hT'.piFinsetConst]
+    _ ≤ 𝔼 a ∈ T ^^ k, ‖τ (∑ i, a i) F - F‖_[∞] := lpNorm_expect_le le_top _ _
+    _ ≤ 𝔼 _a ∈ T ^^ k, ε := expect_le_expect fun x hx ↦ ?_
+    _ = ε := by rw [expect_const hT'.piFinsetConst]
+  calc
+    ‖τ (∑ i, x i) F - F‖_[⊤]
+    _ ≤ ∑ i, ‖τ (x i) F - F‖_[⊤] := lpNorm_translate_sum_sub_le le_top _ _ _
+    _ ≤ ∑ _i, ε / k := sum_le_sum fun i _ ↦ hT _ $ Fintype.mem_piFinset.1 hx _
+    _ = ε := by simp only [sum_const, card_fin, nsmul_eq_mul]; rw [mul_div_cancel']; positivity
+
 end AlmostPeriodicity

LeanAPAP/Prereqs/Discrete/Convolution/Basic.lean

@@ -519,7 +519,7 @@ lemma support_iterConv_subset (f : α → β) : ∀ n, support (f ∗^ n) ⊆ n
   | n + 1 => (support_conv_subset _ _).trans $ Set.add_subset_add_left $ support_iterConv_subset _ _
 
 lemma indicate_iterConv_apply (s : Finset α) (n : ℕ) (a : α) :
-    (𝟭_[β] s ∗^ n) a = ((piFinset fun _i ↦ s).filter fun x : Fin n → α ↦ ∑ i, x i = a).card := by
+    (𝟭_[β] s ∗^ n) a = ((s ^^ n).filter fun x : Fin n → α ↦ ∑ i, x i = a).card := by
   induction' n with n ih generalizing a
   · simp [apply_ite card, eq_comm]
   simp_rw [iterConv_succ, conv_eq_sum_sub', ih, indicate_apply, boole_mul, sum_ite, filter_mem_univ,
@@ -539,23 +539,23 @@ lemma indicate_iterConv_apply (s : Finset α) (n : ℕ) (a : α) :
         Fin.cons_self_tail _⟩
 
 lemma indicate_iterConv_conv (s : Finset α) (n : ℕ) (f : α → β) :
-    𝟭 s ∗^ n ∗ f = ∑ a ∈ piFinset (fun _ : Fin n ↦ s), τ (∑ i, a i) f := by
+    𝟭 s ∗^ n ∗ f = ∑ a ∈ s ^^ n, τ (∑ i, a i) f := by
   ext b
   simp only [conv_eq_sum_sub', indicate_iterConv_apply, mem_piFinset, Finset.sum_apply,
     translate_apply, ← nsmul_eq_mul, ← sum_const, sum_fiberwise']
 
 lemma conv_indicate_iterConv (f : α → β) (s : Finset α) (n : ℕ) :
-    f ∗ 𝟭 s ∗^ n = ∑ a ∈ piFinset (fun _ : Fin n ↦ s), τ (∑ i, a i) f := by
+    f ∗ 𝟭 s ∗^ n = ∑ a ∈ s ^^ n, τ (∑ i, a i) f := by
   ext b
   simp only [conv_eq_sum_sub, indicate_iterConv_apply, mem_piFinset, Finset.sum_apply,
     translate_apply, ← nsmul_eq_mul', ← sum_const, sum_fiberwise']
 
 lemma indicate_iterConv_dconv (s : Finset α) (n : ℕ) (f : α → β) :
-    𝟭 s ∗^ n ○ f = ∑ a ∈ piFinset (fun _ : Fin n ↦ s), τ (∑ i, a i) (conjneg f) := by
+    𝟭 s ∗^ n ○ f = ∑ a ∈ s ^^ n, τ (∑ i, a i) (conjneg f) := by
   rw [← conv_conjneg, indicate_iterConv_conv]
 
 lemma dconv_indicate_iterConv (f : α → β) (s : Finset α) (n : ℕ) :
-    f ○ 𝟭 s ∗^ n = ∑ a ∈ piFinset (fun _ : Fin n ↦ s), τ (-∑ i, a i) f := by
+    f ○ 𝟭 s ∗^ n = ∑ a ∈ s ^^ n, τ (-∑ i, a i) f := by
   simp [← conv_conjneg, conjneg_iterConv, conv_indicate_iterConv, piFinset_neg']
 
 end CommSemiring

LeanAPAP/Prereqs/Discrete/DFT/Basic.lean

@@ -60,7 +60,8 @@ lemma dft_inversion (f : α → ℂ) (a : α) : 𝔼 ψ, dft f ψ * ψ a = f a :
 
 /-- **Fourier inversion** for the discrete Fourier transform. -/
 lemma dft_inversion' (f : α → ℂ) (a : α) : ∑ ψ : AddChar α ℂ, dft f ψ * ψ a = card α * f a := by
-  rw [mul_comm, ← div_eq_iff, ← dft_inversion f, ← AddChar.card_eq, Fintype.sum_div_card (α := ℂ)]
+  rw [mul_comm, ← div_eq_iff, ← dft_inversion f, ← AddChar.card_eq,
+    Fintype.expect_eq_sum_div_card (α := ℂ)]
   simp
 
 lemma dft_dft_doubleDualEmb (f : α → ℂ) (a : α) :

LeanAPAP/Prereqs/Discrete/LpNorm/Basic.lean

@@ -18,7 +18,7 @@ import LeanAPAP.Prereqs.Indicator
 -/
 
 open Finset Function Real
-open scoped BigOps ComplexConjugate ENNReal NNReal
+open scoped BigOps ComplexConjugate ENNReal NNReal NNRat
 
 variable {ι 𝕜 : Type*} [Fintype ι]
 
@@ -111,6 +111,11 @@ lemma lpNorm_add_le (hp : 1 ≤ p) (f g : ∀ i, α i) : ‖f + g‖_[p] ≤ ‖
   haveI := Fact.mk hp
   norm_add_le _ _
 
+lemma lpNorm_sum_le (hp : 1 ≤ p) {κ : Type*} (s : Finset κ) (f : κ → ∀ i, α i) :
+    ‖∑ i ∈ s, f i‖_[p] ≤ ∑ i ∈ s, ‖f i‖_[p] :=
+  haveI := Fact.mk hp
+  norm_sum_le _ _
+
 lemma lpNorm_sub_le (hp : 1 ≤ p) (f g : ∀ i, α i) : ‖f - g‖_[p] ≤ ‖f‖_[p] + ‖g‖_[p] :=
   haveI := Fact.mk hp
   norm_sub_le _ _
@@ -147,6 +152,14 @@ lemma lpNorm_nsmul (hp : 1 ≤ p) (n : ℕ) (f : ∀ i, α i) : ‖n • f‖_[p
   haveI := Fact.mk hp
   norm_nsmul _ _
 
+lemma lpNorm_expect_le [∀ i, Module ℚ≥0 (α i)] (hp : 1 ≤ p) {κ : Type*} (s : Finset κ) (f : κ → ∀ i, α i) :
+    ‖𝔼 i ∈ s, f i‖_[p] ≤ 𝔼 i ∈ s, ‖f i‖_[p] := by
+  obtain rfl | hs := s.eq_empty_or_nonempty
+  · simp
+  refine (le_inv_smul_iff_of_pos $ by positivity).2 ?_
+  rw [← nsmul_eq_smul_cast, ← lpNorm_nsmul hp, card_smul_expect]
+  exact lpNorm_sum_le hp _ _
+
 end one_le
 end NormedAddCommGroup
 
@@ -354,6 +367,19 @@ lemma lpNorm_translate [NormedAddCommGroup β] (a : α) (f : α → β) : ‖τ
     congr 1
     exact Fintype.sum_equiv (Equiv.neg _) _ _ fun _ ↦ rfl
 
+lemma lpNorm_translate_sum_sub_le [NormedAddCommGroup β] (hp : 1 ≤ p) {ι : Type*} (s : Finset ι)
+    (a : ι → α) (f : α → β) : ‖τ (∑ i ∈ s, a i) f - f‖_[p] ≤ ∑ i ∈ s, ‖τ (a i) f - f‖_[p] := by
+  induction' s using Finset.cons_induction with i s ih hs
+  · simp
+  calc
+    _ = ‖τ (∑ j ∈ s, a j) (τ (a i) f - f) + (τ (∑ j ∈ s, a j) f - f)‖_[p] := by
+        rw [sum_cons, translate_add', translate_sub_right, sub_add_sub_cancel]
+    _ ≤ ‖τ (∑ j ∈ s, a j) (τ (a i) f - f)‖_[p] + ‖(τ (∑ j ∈ s, a j) f - f)‖_[p] :=
+        lpNorm_add_le hp _ _
+    _ ≤ ‖τ (∑ j ∈ s, a j) (τ (a i) f - f)‖_[p] + ∑ j ∈ s, ‖(τ (a j) f - f)‖_[p] :=
+        add_le_add_left hs _
+    _ = _ := by rw [lpNorm_translate, sum_cons]
+
 end lpNorm
 
 section IsROrC

LeanAPAP/Prereqs/Discrete/LpNorm/Compact.lean

@@ -27,7 +27,7 @@ notation "‖" f "‖ₙ_[" p "]" => nlpNorm p f
 
 lemma nlpNorm_eq_expect' (hp : p.toReal ≠ 0) (f : ∀ i, α i) :
     ‖f‖ₙ_[p] = (𝔼 i, ‖f i‖ ^ p.toReal) ^ p.toReal⁻¹ := by
-  rw [nlpNorm, lpNorm_eq_sum', ← div_rpow, Fintype.sum_div_card (α := ℝ)] <;> positivity
+  rw [nlpNorm, lpNorm_eq_sum', ← div_rpow, Fintype.expect_eq_sum_div_card (α := ℝ)] <;> positivity
 
 lemma nlpNorm_eq_expect'' {p : ℝ} (hp : 0 < p) (f : ∀ i, α i) :
     ‖f‖ₙ_[p.toNNReal] = (𝔼 i, ‖f i‖ ^ p) ^ p⁻¹ := by
@@ -190,7 +190,7 @@ notation "⟪" f ", " g "⟫ₙ_[" 𝕜 "]" => @nl2Inner _ 𝕜 _ _ _ _ f g
 
 lemma nl2Inner_eq_expect (f g : ι → 𝕜) : ⟪f, g⟫ₙ_[𝕜] = 𝔼 i, conj (f i) * g i := rfl
 lemma nl2Inner_eq_l2Inner_div_card (f g : ι → 𝕜) : ⟪f, g⟫ₙ_[𝕜] = ⟪f, g⟫_[𝕜] / card ι :=
-  (Fintype.sum_div_card _).symm
+  Fintype.expect_eq_sum_div_card _
 
 @[simp] lemma conj_nl2Inner (f g : ι → 𝕜) : conj ⟪f, g⟫ₙ_[𝕜] = ⟪g, f⟫ₙ_[𝕜] := by
   simp [nl2Inner_eq_expect, map_expect, mul_comm]

LeanAPAP/Prereqs/Expect/Basic.lean

@@ -317,9 +317,12 @@ lemma expect_indicate_eq' [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι 
     𝔼 i, ite (i = x) (Fintype.card ι : α) 0 * f i = f x := by
   simp_rw [@eq_comm _ _ x, expect_indicate_eq]
 
-@[simp] nonrec lemma _root_.Fintype.sum_div_card [Fintype ι] (f : ι → α) :
-    (∑ i, f i) / Fintype.card ι = 𝔼 i, f i := by
-  rw [expect, NNRat.smul_def, card_univ, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]
+lemma expect_eq_sum_div_card (s : Finset ι) (f : ι → α) :
+    𝔼 i ∈ s, f i = (∑ i ∈ s, f i) / s.card := by
+  rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]
+
+nonrec lemma _root_.Fintype.expect_eq_sum_div_card [Fintype ι] (f : ι → α) :
+    𝔼 i, f i = (∑ i, f i) / Fintype.card ι := Finset.expect_eq_sum_div_card _ _
 
 lemma expect_div (s : Finset ι) (f : ι → α) (a : α) : (𝔼 i ∈ s, f i) / a = 𝔼 i ∈ s, f i / a := by
   simp_rw [div_eq_mul_inv, expect_mul]

LeanAPAP/Prereqs/Translate.lean

@@ -21,11 +21,19 @@ def translate (a : α) (f : α → β) : α → β := fun x ↦ f (x - a)
 notation "τ " => translate
 
 @[simp] lemma translate_apply (a : α) (f : α → β) (x : α) : τ a f x = f (x - a) := rfl
-@[simp] lemma translate_zero (f : α → β) : translate 0 f = f := by ext; simp
+@[simp] lemma translate_zero (f : α → β) : τ 0 f = f := by ext; simp
 
-@[simp] lemma translate_translate (a b : α) (f : α → β) : τ a (τ b f) = τ (a + b) f := by
+lemma translate_translate (a b : α) (f : α → β) : τ a (τ b f) = τ (a + b) f := by
   ext; simp [sub_sub]
 
+lemma translate_add (a b : α) (f : α → β) : τ (a + b) f = τ a (τ b f) := by ext; simp [sub_sub]
+
+lemma translate_add' (a b : α) (f : α → β) : τ (a + b) f = τ b (τ a f) := by
+  rw [add_comm, translate_add]
+
+lemma translate_comm (a b : α) (f : α → β) : τ a (τ b f) = τ b (τ a f) := by
+  rw [← translate_add, translate_add']
+
 @[simp] lemma comp_translate (a : α) (f : α → β) (g : β → γ) : g ∘ τ a f = τ a (g ∘ f) := rfl
 
 @[simp]

blueprint/src/ap.tex

@@ -159,7 +159,8 @@ \chapter{Almost-Periodicity}
 
 \begin{theorem}
 \label{linfty_ap_boosted}
-
+\lean{AlmostPeriodicity.linfty_almost_periodicity_boosted}
+\leanok
 Let $\epsilon\in (0,1]$ and $k\geq 1$. Let $K\geq 2$ and $A,S\subseteq G$ with $\lvert A+S\rvert\leq K\lvert A\rvert$.
 Let $B,C\subseteq G$. Let $\eta=\min(1,\lvert C\rvert/\lvert B\rvert)$. There exists $T\subseteq G$ such that
 \[\lvert T\rvert \geq K^{-4096\lceil \lo{\eta}\rceil k^2\epsilon^{-2}}\lvert S\rvert\]
@@ -169,6 +170,7 @@ \chapter{Almost-Periodicity}
 
 \begin{proof}
 \uses{linfty_ap}
+\leanok
 Let $T$ be as in Theorem~\ref{linfty_ap} with $\epsilon$ replaced by $\epsilon/k$. Note that, for any $x\in G$,
 \[\mu_T^{(k)}\ast \mu_A\ast 1_B\ast \mu_C(x)=\frac{1}{\lvert T\rvert^k}\sum_{t_1,\ldots,t_k\in T}\tau_{t_1+\cdots+t_k}\mu_A\ast 1_B\ast \mu_C(x).\]
 It therefore suffices (by the triangle inequality) to show, for any fixed $x\in G$ and $t_1,\ldots,t_k\in T$, that with $F=\mu_A\ast 1_B\ast \mu_C$, we have