Almost-periodicity

theorem Finset.big_shifts_step1 {α : Type u_1} [DecidableEq α] {s : Finset α} {k : ℕ} [Add α] (L : Finset (Fin k → α)) (hk : k ≠ 0) : (∑ x ∈ L + s.piDiag (Fin k), ∑ l ∈ L, ∑ s ∈ s.piDiag (Fin k), if l + s = x then 1 else 0) = L.card * s.card

theorem Finset.reindex_count {α : Type u_1} [DecidableEq α] {k : ℕ} [AddCommGroup α] [Fintype α] (L : Finset (Fin k → α)) (hk : k ≠ 0) (hL' : L.Nonempty) (l₁ : Fin k → α) : (∑ l₂ ∈ L, if l₁ - l₂ ∈ univ.piDiag (Fin k) then 1 else 0) = {t : α | (l₁ - fun (x : Fin k) => t) ∈ L}.card

theorem my_markov {α : Type u_1} {g : α → ℝ} {c ε : ℝ} {A : Finset α} (hc : 0 < c) (hg : ∀ a ∈ A, 0 ≤ g a) (h : ∑ a ∈ A, g a ≤ ε * c * ↑A.card) : (1 - ε) * ↑A.card ≤ ↑{a ∈ A | g a ≤ c}.card

theorem my_other_markov {α : Type u_1} {g : α → ℝ} {c ε : ℝ} {A : Finset α} (hc : 0 ≤ c) (hε : 0 ≤ ε) (hg : ∀ a ∈ A, 0 ≤ g a) (h : ∑ a ∈ A, g a ≤ ε * c * ↑A.card) : (1 - ε) * ↑A.card ≤ ↑{a ∈ A | g a ≤ c}.card

theorem lemma28_end {G : Type u_1} [Fintype G] {A : Finset G} {f : G → ℂ} {ε : ℝ} {k m : ℕ} [MeasurableSpace G] [DiscreteMeasurableSpace G] (hε : 0 < ε) (hm : 1 ≤ m) (hk : 64 * ↑m / ε ^ 2 ≤ ↑k) : (8 * ↑m) ^ m * ↑k ^ (m - 1) * ↑A.card ^ k * ↑k * (2 * ‖f‖_[2 * ↑m]) ^ (2 * m) ≤ 1 / 2 * ((↑k * ε) ^ (2 * m) * ∑ i : G, ‖f i‖ ^ (2 * m)) * ↑A.card ^ k

theorem lemma28_part_one {G : Type u_1} [Fintype G] {A : Finset G} {f : G → ℂ} {k m : ℕ} [DecidableEq G] [AddCommGroup G] (hm : 1 ≤ m) (x : G) : ∑ a ∈ Fintype.piFinset fun (x : Fin k) => A, ‖∑ i : Fin k, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤ (8 * ↑m) ^ m * ↑k ^ (m - 1) * ∑ a ∈ Fintype.piFinset fun (x : Fin k) => A, ∑ i : Fin k, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m)

theorem big_shifts_step2 {G : Type u_1} [Fintype G] {S : Finset G} {k : ℕ} [DecidableEq G] [AddCommGroup G] (L : Finset (Fin k → G)) (hk : k ≠ 0) : (∑ x ∈ L + S.piDiag (Fin k), ∑ l ∈ L, ∑ s ∈ S.piDiag (Fin k), if l + s = x then 1 else 0) ^ 2 ≤ ↑(L + S.piDiag (Fin k)).card * ↑S.card * ∑ l₁ ∈ L, ∑ l₂ ∈ L, if l₁ - l₂ ∈ Finset.univ.piDiag (Fin k) then 1 else 0

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

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

Equations

• AlmostPeriodicity.LProp k m ε f A a = (‖fun (x : G) => ∑ i : Fin k, f (x - a i) - (k • (mu A ∗ f)) x‖_[2 * ↑m] ≤ ↑k * ε * ‖f‖_[2 * ↑m])

noncomputable instance AlmostPeriodicity.instDecidablePredForallFinLProp {G : Type u_1} [Fintype G] {A : Finset G} {f : G → ℂ} {ε : ℝ} {k m : ℕ} [DecidableEq G] [AddCommGroup G] [MeasurableSpace G] : DecidablePred (LProp k m ε f A)

Equations

• AlmostPeriodicity.instDecidablePredForallFinLProp = Classical.decPred (AlmostPeriodicity.LProp k m ε f A)

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_markov {G : Type u_1} [Fintype G] {A : Finset G} {f : G → ℂ} {ε : ℝ} {k m : ℕ} [DecidableEq G] [AddCommGroup G] [MeasurableSpace G] (hε : 0 < ε) (hm : 1 ≤ m) (h : ∑ a ∈ Fintype.piFinset fun (x : Fin k) => A, ‖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

theorem AlmostPeriodicity.lemma28_part_two {G : Type u_1} [Fintype G] {A : Finset G} {f : G → ℂ} {k m : ℕ} [DecidableEq G] [AddCommGroup G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (hm : 1 ≤ m) (hA : A.Nonempty) : (8 * ↑m) ^ m * ↑k ^ (m - 1) * ∑ a ∈ Fintype.piFinset fun (x : Fin k) => A, ∑ i : Fin k, ‖translate (a i) f - mu A ∗ f‖_[2 * ↑m] ^ (2 * m) ≤ (8 * ↑m) ^ m * ↑k ^ (m - 1) * ∑ _a ∈ Fintype.piFinset fun (x : Fin k) => A, ∑ _i : Fin k, (2 * ‖f‖_[2 * ↑m]) ^ (2 * m)

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.T_bound {ε K : ℝ} {k m : ℕ} (hK₂ : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈64 * ↑m / (ε / 2) ^ 2⌉₊) (h₁ : Lc * Sc ≤ ASc ^ k * Tc) (h₂ : ↑Ac ^ k / 2 ≤ ↑Lc) (h₃ : ↑ASc ≤ K * ↑Ac) (hAc : 0 < Ac) (hε : 0 < ε) (hε' : ε ≤ 1) (hm : 1 ≤ m) : K ^ (-512 * ↑m / ε ^ 2) * ↑Sc ≤ ↑Tc

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 ∗ mu C) - mu A ∗ 𝟭 B ∗ 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 ∗ mu C) - mu A ∗ 𝟭 B ∗ mu C‖_[⊤] ≤ ε