Skip to content

refactor: use the compact normalisation in physical space #9

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
YaelDillies wants to merge 1 commit into
base: master
Choose a base branch
from
Open

refactor: use the compact normalisation in physical space #9

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
141 changes: 113 additions & 28 deletions LeanAPAP/FiniteField.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ attribute [-simp] Real.log_inv

open Fintype Function MeasureTheory Module RCLike Real
open Finset hiding card
open scoped ENNReal NNReal BigOperators Combinatorics.Additive Pointwise mu
open scoped ENNReal NNReal BigOperators Combinatorics.Additive Pointwise ComplexConjugate

universe u
variable {G : Type u} [AddCommGroup G] [DecidableEq G] [Fintype G] {A C : Finset G} {x y γ ε : ℝ}
Expand Down Expand Up @@ -136,11 +136,12 @@ variable {q n : ℕ} [Module (ZMod q) G] {A₁ A₂ : Finset G} (S : Finset G) {
lemma ap_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε)
(hε₁ : ε ≤ 1) (hαA₁ : α ≤ A₁.dens) (hαA₂ : α ≤ A₂.dens) :
∃ (V : Submodule (ZMod q) G) (_ : DecidablePred (· ∈ V)),
↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤ 2 ^ 32 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 ∧
↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤ 2 ^ 36 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 ∧
|∑ x ∈ S, (μ (Set.toFinset V) ∗ μ A₁ ∗ μ A₂) x - ∑ x ∈ S, (μ A₁ ∗ μ A₂) x| ≤ ε := by
classical
let _ : MeasurableSpace G := ⊤
have : Fact (1 < q) := sorry
have : Fact (1 < q) := ⟨hq.one_lt⟩
have : Fact q.Prime := ⟨hq⟩
have : DiscreteMeasurableSpace G := ⟨fun _ ↦ trivial⟩
have hA₁ : A₁.Nonempty := by simpa using hα₀.trans_le hαA₁
have hA₂ : A₂.Nonempty := by simpa using hα₀.trans_le hαA₂
Expand All @@ -158,50 +159,68 @@ lemma ap_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hα₀ : 0 < α) (hα₂ : α
calc
ε * α / 4 ≤ ε * 1 / 4 := by gcongr
_ ≤ 1 := by linarith
obtain ⟨T, hTcard, hTε⟩ := AlmostPeriodicity.linfty_almost_periodicity_boosted ε hε₀ hε₁ k
(by positivity) (le_inv_of_le_inv₀ (by positivity) hα₂) hA₁ univ_nonempty S A₂ hS hA₂
obtain ⟨T, hTcard, hTε⟩ := AlmostPeriodicity.linfty_almost_periodicity_boosted (ε / 4)
(by positivity) (by linarith) k (by positivity) ((le_inv (by positivity) (by positivity)).2 hα₂)
hA₁ univ_nonempty (-S) A₂ hS.neg hA₂
have hT : 0 < (#T : ℝ) := hTcard.trans_lt' (by positivity)
replace hT : T.Nonempty := by simpa using hT
let Δ := largeSpec (μ T) 2⁻¹
let Δ := largeSpec (𝟭 T) 2⁻¹
let V : Submodule (ZMod q) G := AddSubgroup.toZModSubmodule _ <| ⨅ γ ∈ Δ, γ.toAddMonoidHom.ker
let V' : Finset G := Set.toFinset V
have hV' : V'.Nonempty := by simpa [V'] using V.nonempty
refine ⟨V, inferInstance, ?_, ?_⟩
· obtain ⟨Δ', hΔ'Δ, hΔ'card, hfΔ'⟩ : ∃ Δ' ⊆ Δ, _ := chang (mu_ne_zero.2 hT) (by norm_num)
· obtain ⟨Δ', hΔ'Δ, hΔΔ', hΔ'card⟩ : ∃ Δ' ⊆ Δ, Δ ⊆ Δ'.addSpan ∧ _ :=
chang (indicate_ne_zero.2 hT) (by norm_num)
let W : Submodule (ZMod q) G := AddSubgroup.toZModSubmodule _ <| ⨅ γ ∈ Δ', γ.toAddMonoidHom.ker
have mem_V {x} : x ∈ V ↔ ∀ γ ∈ Δ, γ x = 1 := by simp [V]
have mem_W {x} : x ∈ W ↔ ∀ γ ∈ Δ', γ x = 1 := by simp [W]
have hWV : W ≤ V := by sorry
have hWV : W ≤ V := by
rintro x
simp only [mem_V, mem_W]
rintro hx γ hγ
obtain ⟨ℰ, hℰ, rfl⟩ := mem_addSpan.1 $ hΔΔ' hγ
rw [AddChar.sum_apply, Finset.prod_eq_one]
rintro γ hγ
simp [hx _ hγ]
have :=
calc
log T.dens⁻¹ ≤ log (α⁻¹ ^ (-4096 * ⌈𝓛 (min 1 (#A₂ / #S))⌉ * k ^ 2 / ε ^ 2))⁻¹ := by
gcongr; rwa [nnratCast_dens, le_div_iff₀]; positivity
rw [card_neg] at hTcard
gcongr
rwa [nnratCast_dens, le_div_iff₀, ← card_univ]
positivity
_ = 2 ^ 12 * log α⁻¹ * ⌈𝓛 (min 1 (#A₂ / #S))⌉ * k ^ 2 / ε ^ 2 := by
rw [log_inv, log_rpow (by positivity)]; ring_nf
_ ≤ 2 ^ 12 * log α⁻¹ * ⌈𝓛 (min 1 A₂.dens)⌉ * k ^ 2 / ε ^ 2 := by
_ ≤ 2 ^ 16 * log α⁻¹ * ⌈𝓛 (min 1 A₂.dens)⌉ * k ^ 2 / ε ^ 2 := by
rw [nnratCast_dens, ← card_univ]; gcongr; exact S.subset_univ
_ ≤ 2 ^ 12 * log α⁻¹ * ⌈𝓛 (min 1 α)⌉ * (k) ^ 2 / ε ^ 2 := by gcongr
_ = 2 ^ 12 * log α⁻¹ * ⌈𝓛 α⌉ * k ^ 2 / ε ^ 2 := by rw [min_eq_right hα₁]
_ ≤ 2 ^ 12 * 𝓛 α * (2 * 𝓛 α) * (2 ^ 3 * 𝓛 (ε * α)) ^ 2 / ε ^ 2 := by
_ ≤ 2 ^ 16 * log α⁻¹ * ⌈𝓛 (min 1 α)⌉ * (k) ^ 2 / ε ^ 2 := by gcongr
_ = 2 ^ 16 * log α⁻¹ * ⌈𝓛 α⌉ * k ^ 2 / ε ^ 2 := by rw [min_eq_right hα₁]
_ ≤ 2 ^ 16 * 𝓛 α * (2 * 𝓛 α) * (2 ^ 3 * 𝓛 (ε * α)) ^ 2 / ε ^ 2 := by
gcongr
· exact le_add_of_nonneg_left zero_le_one
· exact Int.ceil_le_two_mul <| two_inv_lt_one.le.trans <| one_le_curlog hα₀.le hα₁
· calc
k ≤ 2 * 𝓛 (ε * α / 4) :=
Nat.ceil_le_two_mul <| two_inv_lt_one.le.trans <| one_le_curlog (by positivity)
sorry
k ≤ 2 * 𝓛 (ε * α / 4) := (Nat.ceil_lt_two_mul $ one_le_curlog (by positivity)
?_).le
_ ≤ 2 * (4 * 𝓛 (ε * α)) := by
gcongr
exact curlog_div_le (by positivity) (mul_le_one₀ hε₁ hα₀.le hα₁) (by norm_num)
_ = 2 ^ 3 * 𝓛 (ε * α) := by ring
_ = 2 ^ 19 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 := by ring_nf
calc
ε * α / 4 ≤ 1 * α / 4 := by gcongr
_ ≤ 1 := by linarith
_ = 2 ^ 23 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 := by ring_nf
calc
(↑(finrank (ZMod q) G - finrank (ZMod q) V) : ℝ)
≤ ↑(finrank (ZMod q) G - finrank (ZMod q) W) := by
gcongr; exact Submodule.finrank_mono hWV
_ = Cardinal.toNat (Module.rank (ZMod q) (G ⧸ W)) := by
simp [← finrank_eq_rank, ← eq_tsub_of_add_eq W.finrank_quotient_add_finrank]
_ ≤ #Δ' := sorry
_ ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖μ T‖_[1] ^ 2 / ‖μ T‖_[2] ^ 2 / card G)⌉₊ / 2⁻¹ ^ 2⌉₊ := by
_ ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖𝟭_[ℂ] T‖ₙ_[1] ^ 2 / ‖𝟭_[ℂ] T‖ₙ_[2] ^ 2)⌉₊ / 2⁻¹ ^ 2⌉₊ := by
gcongr
_ = ⌈2 ^ 7 * exp 1 ^ 2 * ⌈𝓛 T.dens⌉₊⌉₊ := by
simp [hT, ← rpow_mul_natCast, dens, changConst, -exp_one_pow, rpow_neg_one]; ring_nf
simp [hT, ← rpow_mul_natCast, dens, changConst, -exp_one_pow, rpow_neg_one, sq]; ring_nf
_ ≤ ⌈2 ^ 7 * 2 ^ 3 * (2 * 𝓛 T.dens)⌉₊ := by
gcongr
· calc
Expand All @@ -216,20 +235,86 @@ lemma ap_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hα₀ : 0 < α) (hα₂ : α
_ ≤ 2 ^ 11 * 𝓛 T.dens := by
gcongr; exact one_le_curlog (by positivity) <| mod_cast T.dens_le_one
_ = 2 ^ 12 * 𝓛 T.dens := by ring
_ ≤ 2 ^ 12 * (1 + 2 ^ 19 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2) := by gcongr
_ ≤ 2 ^ 12 * (2 ^ 19 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 +
2 ^ 19 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2) := by
_ ≤ 2 ^ 12 * (1 + 2 ^ 23 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2) := by gcongr
_ ≤ 2 ^ 12 * (2 ^ 23 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 +
2 ^ 23 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2) := by
gcongr
sorry
_ = 2 ^ 32 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 := by ring
exact one_le_mul_of_one_le_of_one_le (one_le_mul_of_one_le_of_one_le
(one_le_mul_of_one_le_of_one_le (by norm_num) $ one_le_pow₀ (one_le_curlog hα₀.le hα₁) _)
$ one_le_pow₀ (one_le_curlog (by positivity) $ mul_le_one hε₁ hα₀.le hα₁) _) $
one_le_pow₀ (one_le_inv hε₀ hε₁) _
_ = 2 ^ 36 * 𝓛 α ^ 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_wInner_one, ← indicate_wInner_one, conv_rotate,
← dconv_wInner_one_eq_wInner_one_conv, wInner_one_dconv_eq_conv_wInner_one, ← conv_conjneg,
rw [← mu_dL2Inner, ← indicate_dL2Inner, conv_rotate,
← dconv_dL2Inner_eq_dL2Inner_conv, dL2Inner_dconv_eq_conv_dL2Inner, ← conv_conjneg,
conjneg_mu, this, conv_comm]
have : ∑ x ∈ S, (μ_[ℝ] A₁ ∗ μ A₂) x = (μ_[ℝ] A₁ ∗ μ A₂ ○ 𝟭 S) 0 := by simp [dconv_indicate]
sorry
have : ∑ x ∈ S, (μ_[ℝ] A₁ ∗ μ A₂) x = (μ A₁ ∗ μ A₂ ○ 𝟭 S) 0 := by simp [dconv_indicate]
calc
|∑ x ∈ S, (μ_[ℝ] V' ∗ μ A₁ ∗ μ A₂) x - ∑ x ∈ S, (μ A₁ ∗ μ A₂) x|
= |𝔼 x ∈ V', ((μ A₁ ∗ μ A₂ ○ 𝟭 S) x - (μ A₁ ∗ μ A₂ ○ 𝟭 S) 0)| := by
rw [expect_sub_distrib, Finset.expect_const hV']; congr
_ ≤ 𝔼 x ∈ V', |((μ A₁ ∗ μ A₂ ○ 𝟭 S) x - (μ A₁ ∗ μ A₂ ○ 𝟭 S) 0)| :=
abs_expect_le_expect_abs ..
_ ≤ ε := expect_le hV' _ _ fun v hv ↦ ?_
suffices h : |(μ T ∗^ k ∗ μ A₁ ∗ μ A₂ ○ 𝟭 S) v - (μ T ∗^ k ∗ μ A₁ ∗ μ A₂ ○ 𝟭 S) 0| ≤ ε / 2 by
calc
|(μ_[ℝ] A₁ ∗ μ A₂ ○ 𝟭 S) v - (μ A₁ ∗ μ A₂ ○ 𝟭 S) 0|
≤ |(μ T ∗^ k ∗ μ A₁ ∗ μ A₂ ○ 𝟭 S) v - (μ T ∗^ k ∗ μ A₁ ∗ μ A₂ ○ 𝟭 S) 0|
+ |(μ T ∗^ k ∗ μ A₁ ∗ μ A₂ ○ 𝟭 S) v - (μ A₁ ∗ μ A₂ ○ 𝟭 S) v|
+ |(μ T ∗^ k ∗ μ A₁ ∗ μ A₂ ○ 𝟭 S) 0 - (μ A₁ ∗ μ A₂ ○ 𝟭 S) 0| := sorry
_ ≤ ε / 2 + ε / 4 + ε / 4 := by
rw [← conjneg_indicate, conv_right_comm, conv_conjneg, ← conv_dconv_assoc, ← conv_assoc]
at hTε
gcongr <;> rw [← Real.norm_eq_abs, ← Pi.sub_apply] <;> exact norm_le_dLinftyNorm.trans hTε
_ = ε := by ring
have (x) :
(μ_[ℝ] T ∗^ k ∗ μ A₁ ∗ μ A₂ ○ 𝟭 S) x =
𝔼 γ, cft (μ T) γ ^ k * cft (μ A₁) γ * cft (μ A₂) γ * cft (𝟭 (-S)) γ * γ x := by
sorry
calc
|(μ T ∗^ k ∗ μ A₁ ∗ μ A₂ ○ 𝟭 S) v - (μ T ∗^ k ∗ μ A₁ ∗ μ A₂ ○ 𝟭 S) 0|
= ‖𝔼 γ, cft (μ T) γ ^ k * cft (μ A₁) γ * cft (μ A₂) γ * cft (𝟭 (-S)) γ * (γ v - 1)‖ := sorry
_ ≤ 𝔼 γ, ‖cft (μ T) γ ^ k * cft (μ A₁) γ * cft (μ A₂) γ * cft (𝟭 (-S)) γ * (γ v - 1)‖ :=
norm_expect_le (K := ℂ)
_ = (card G : ℝ)⁻¹ * ∑ γ ∈ Δᶜ,
‖cft (μ T) γ‖ ^ k * ‖cft (μ A₁) γ * cft (μ A₂) γ‖ * ‖cft (𝟭 (-S)) γ‖ * ‖γ v - 1‖ := by
simp_rw [norm_mul, Fintype.expect_eq_sum_div_card, AddChar.card_eq, inv_mul_eq_div,
norm_pow, mul_assoc]
rw [← Fintype.sum_subset]
simp_rw [mem_compl]
simp [V', V] at hv
refine fun γ ↦ mt fun hγ ↦ ?_
simp [hv _ hγ]
_ ≤ (card G : ℝ)⁻¹ * ∑ γ ∈ Δᶜ,
(2⁻¹ / card T) ^ k * ‖cft (μ A₁) γ * cft (μ A₂) γ‖ * 1 * 2 := by
gcongr with γ hγ
· have : (0 : ℝ) < card G := by positivity
refine le_of_lt ?_
simpa [Δ, hT, -nsmul_eq_mul, nnratCast_dens, ← mul_div_assoc, lt_div_iff this,
← card_smul_mu, -Complex.norm_eq_abs, norm_smul] using hγ
· calc
‖cft (𝟭 (-S)) γ‖ ≤ ∑ x, ‖conj (γ x) * 𝟭 (-S) x‖ := norm_expect_le
_ = S.dens := by simp? [indicate_apply, apply_ite, -mem_neg']
· calc
‖γ v - 1‖ ≤ ‖γ v‖ + ‖(1 : ℂ)‖ := norm_sub_le ..
_ = 2 := by simp; norm_num
_ = 2 * 2⁻¹ ^ k * S.dens * ∑ γ ∈ Δᶜ, ‖cft (μ A₁) γ‖ * ‖cft (μ A₂) γ‖ := by
simp [nnratCast_dens, mul_sum]; congr 1 with x; ring
_ ≤ 2 * 2⁻¹ ^ k * S.dens * ∑ γ, ‖cft (μ A₁) γ‖ * ‖cft (μ A₂) γ‖ := by
gcongr
· intros
positivity
· exact Δᶜ.subset_univ
_ ≤ 2 * 2⁻¹ ^ k * S.dens * (√(∑ γ, ‖cft (μ A₁) γ‖ ^ 2) * √(∑ γ, ‖cft (μ A₂) γ‖ ^ 2)) := by
gcongr; exact sum_mul_le_sqrt_mul_sqrt ..
_ = 2 * 2⁻¹ ^ k * S.dens * (√A₁.dens * √A₂.dens) := by
rw [← dL2Norm_sq_eq_sum_norm, ← dL2Norm_sq_eq_sum_norm]



sorry
#exit
lemma ap_in_ff' (hq₃ : 3 ≤ q) (hq : q.Prime) (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε)
(hε₁ : ε ≤ 1) (hαA₁ : α ≤ A₁.dens) (hαA₂ : α ≤ A₂.dens) :
∃ (V : Submodule (ZMod q) G) (_ : DecidablePred (· ∈ V)),
Expand Down
27 changes: 18 additions & 9 deletions LeanAPAP/Physics/AlmostPeriodicity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ import Mathlib.Data.Finset.CastCard
import Mathlib.Tactic.Bound
import LeanAPAP.Prereqs.Convolution.Discrete.Basic
import LeanAPAP.Prereqs.Convolution.Norm
import LeanAPAP.Prereqs.Function.Indicator.Complex
import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
import LeanAPAP.Prereqs.MarcinkiewiczZygmund

Expand Down Expand Up @@ -406,16 +407,24 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (
have := just_the_triangle_inequality ha ht hk.bot_lt hm
rwa [neg_neg, mul_div_cancel₀ _ (two_ne_zero' ℝ)] at this

lemma almost_periodicity' (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (f : G → ℝ)
(hK₂ : 2 ≤ K) (hK : σ[A, S] ≤ K) :
∃ T : Finset G,
K ^ (-512 * m / ε ^ 2 : ℝ) * S.card ≤ T.card ∧
∀ t ∈ T, ‖τ t (mu A ∗ f) - mu A ∗ f‖_[2 * m] ≤ ε * ‖f‖_[2 * m] := by
simpa [← Complex.ofReal_comp_mu, ← Complex.ofReal_comp_conv, ← comp_translate,
← Complex.ofReal_comp_sub] using almost_periodicity ε hε hε' m ((↑) ∘ f) hK₂ hK

theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hK₂ : 2 ≤ K)
(hK : σ[A, S] ≤ K) (B C : Finset G) (hB : B.Nonempty) (hC : C.Nonempty) :
∃ T : Finset G,
K ^ (-4096 * ⌈𝓛 (#C / #B)⌉ / ε ^ 2) * #S ≤ #T ∧
∀ t ∈ T, ‖τ t (μ_[ℂ] A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C‖_[∞] ≤ ε := by
∀ t ∈ T, ‖τ t (μ_[ℝ] A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C‖_[∞] ≤ ε := by
let r : ℝ := min 1 (#C / #B)
set m : ℝ := 𝓛 (#C / #B)
have hm₀ : 0 < m := curlog_pos (by positivity)
have hm₁ : 1 ≤ ⌈m⌉₊ := Nat.one_le_iff_ne_zero.2 <| by positivity
obtain ⟨T, hKT, hT⟩ := almost_periodicity (ε / exp 1) (by positivity)
obtain ⟨T, hKT, hT⟩ := almost_periodicity' (ε / exp 1) (by positivity)
(div_le_one_of_le₀ (hε₁.trans <| one_le_exp zero_le_one) <| by positivity) ⌈m⌉₊ (𝟭 B) hK₂ hK
norm_cast at hT
set M : ℕ := 2 * ⌈m⌉₊
Expand All @@ -435,22 +444,22 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
_ ≤ _ := by norm_num
_ = _ := by simp [div_div_eq_mul_div, ← mul_div_right_comm, mul_right_comm, div_pow]
_ ≤ _ := hKT
set F : G → ℂ := τ t (μ A ∗ 𝟭 B) - μ A ∗ 𝟭 B
set F : G → ℝ := τ t (μ A ∗ 𝟭 B) - μ A ∗ 𝟭 B
have (x) :=
calc
(τ t (μ A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C : G → ℂ) x
(τ t (μ A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C : G → ℝ) x
= (F ∗ μ C) x := by simp [sub_conv, F]
_ = ∑ y, F y * μ C (x - y) := conv_eq_sum_sub' ..
_ = ∑ y, F y * μ (x +ᵥ -C) y := by simp [neg_add_eq_sub]
rw [dLinftyNorm_eq_iSup_norm]
refine ciSup_le fun x ↦ ?_
calc
‖(τ t (μ A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C : G → ℂ) x‖
‖(τ t (μ A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C : G → ℝ) x‖
= ‖∑ y, F y * μ (x +ᵥ -C) y‖ := by rw [this]
_ ≤ ∑ y, ‖F y * μ (x +ᵥ -C) y‖ := norm_sum_le _ _
_ = ‖F * μ (x +ᵥ -C)‖_[1] := by rw [dL1Norm_eq_sum_norm]; rfl
_ ≤ ‖F‖_[M] * ‖μ_[ℂ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := dL1Norm_mul_le _ _
_ ≤ ε / exp 1 * #B ^ (M : ℝ)⁻¹ * ‖μ_[ℂ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := by
_ ≤ ‖F‖_[M] * ‖μ_[ℝ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := dL1Norm_mul_le _ _
_ ≤ ε / exp 1 * #B ^ (M : ℝ)⁻¹ * ‖μ_[ℝ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := by
gcongr
simpa only [← ENNReal.coe_natCast, dLpNorm_indicate hM₀] using hT _ ht
_ = ε * ((#C / #B) ^ (-(M : ℝ)⁻¹) / exp 1) := by
Expand Down Expand Up @@ -482,12 +491,12 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ :
(B C : Finset G) (hB : B.Nonempty) (hC : C.Nonempty) :
∃ T : Finset G,
K ^ (-4096 * ⌈𝓛 (#C / #B)⌉ * k ^ 2/ ε ^ 2) * #S ≤ #T ∧
‖μ T ∗^ k ∗ (μ_[ℂ] A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C‖_[∞] ≤ ε := by
‖μ 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
set F := μ_[ℝ] A ∗ 𝟭 B ∗ μ C
have hT' : T.Nonempty := by
have : (0 : ℝ) < #T := hKT.trans_lt' <| by positivity
simpa [card_pos] using this
Expand Down
Loading