Almost-periodicity

theorem big_shifts {G : Type u_1} [Fintype G] {A : Finset G} {k : ℕ} [DecidableEq G] [AddCommGroup G] (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0) (hL' : L.Nonempty) (hL : L ⊆ Fintype.piFinset fun (x : Fin k) => A) : ∃ a ∈ L, L.card * S.card ≤ (A + S).card ^ k * {t : G | (a - fun (x : Fin k) => t) ∈ L}.card

noncomputable def AlmostPeriodicity.l {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] [MeasurableSpace G] (k m : ℕ) (ε : ℝ) (f : G → ℂ) (A : Finset G) : Finset (Fin k → G)

Equations

• AlmostPeriodicity.l k m ε f A = {x ∈ Fintype.piFinset fun (x : Fin k) => A | AlmostPeriodicity.LProp✝ k m ε f A x}

theorem AlmostPeriodicity.lemma28 {G : Type u_1} [Fintype G] {A : Finset G} {f : G → ℂ} {ε : ℝ} {k m : ℕ} [DecidableEq G] [AddCommGroup G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (hε : 0 < ε) (hm : 1 ≤ m) (hk : 64 * ↑m / ε ^ 2 ≤ ↑k) : ↑A.card ^ k / 2 ≤ ↑(l k m ε f A).card

theorem AlmostPeriodicity.just_the_triangle_inequality {G : Type u_1} [Fintype G] {A : Finset G} {f : G → ℂ} {ε : ℝ} {k m : ℕ} [DecidableEq G] [AddCommGroup G] [MeasurableSpace G] [DiscreteMeasurableSpace G] {t : G} {a : Fin k → G} (ha : a ∈ l k m ε f A) (ha' : (a + fun (x : Fin k) => t) ∈ l k m ε f A) (hk : 0 < k) (hm : 1 ≤ m) : ‖translate (-t) (mu A ∗ᵈ f) - mu A ∗ᵈ f‖_[2 * ↑m] ≤ 2 * ε * ‖f‖_[2 * ↑m]

theorem AlmostPeriodicity.almost_periodicity {G : Type u_1} [Fintype G] {A S : Finset G} {K : ℝ} [DecidableEq G] [AddCommGroup G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (f : G → ℂ) (hK₂ : 2 ≤ K) (hK : ↑(A.addConst S) ≤ K) : ∃ (T : Finset G), K ^ (-512 * ↑m / ε ^ 2) * ↑S.card ≤ ↑T.card ∧ ∀ t ∈ T, ‖translate t (mu A ∗ᵈ f) - mu A ∗ᵈ f‖_[2 * ↑m] ≤ ε * ‖f‖_[2 * ↑m]

theorem AlmostPeriodicity.linfty_almost_periodicity {G : Type u_1} [Fintype G] {A S : Finset G} {K : ℝ} [DecidableEq G] [AddCommGroup G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hK₂ : 2 ≤ K) (hK : ↑(A.addConst S) ≤ K) (B C : Finset G) (hB : B.Nonempty) (hC : C.Nonempty) : ∃ (T : Finset G), K ^ (-4096 * ↑⌈1 + Real.log (min 1 (↑C.card / ↑B.card))⁻¹⌉ / ε ^ 2) * ↑S.card ≤ ↑T.card ∧ ∀ t ∈ T, ‖translate t ((mu A ∗ᵈ (↑B).indicator fun (x : G) => 1) ∗ᵈ mu C) - (mu A ∗ᵈ (↑B).indicator fun (x : G) => 1) ∗ᵈ mu C‖_[⊤] ≤ ε

theorem AlmostPeriodicity.linfty_almost_periodicity_boosted {G : Type u_1} [Fintype G] {A S : Finset G} {K : ℝ} [DecidableEq G] [AddCommGroup G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (k : ℕ) (hk : k ≠ 0) (hK₂ : 2 ≤ K) (hK : ↑(A.addConst S) ≤ K) (hS : S.Nonempty) (B C : Finset G) (hB : B.Nonempty) (hC : C.Nonempty) : ∃ (T : Finset G), K ^ (-4096 * ↑⌈1 + Real.log (min 1 (↑C.card / ↑B.card))⁻¹⌉ * ↑k ^ 2 / ε ^ 2) * ↑S.card ≤ ↑T.card ∧ ‖mu T ∗ᵈ^ k ∗ᵈ ((mu A ∗ᵈ (↑B).indicator fun (x : G) => 1) ∗ᵈ mu C) - (mu A ∗ᵈ (↑B).indicator fun (x : G) => 1) ∗ᵈ mu C‖_[⊤] ≤ ε