Source indexedlemma · leanprover/lean4:v4.32.0

AlmostPeriodicity.lemma28_markov

APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:243 to 255

Mathematical statement

Exact Lean statement

lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m)
    (h : ∑ a ∈ 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 ^ k) :
    (#A ^ k : ℝ) / 2 ≤ #(l k m ε f A)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m)    (h : ∑ a ∈ 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 ^ k) :    (#A ^ k : ℝ) / 2 ≤ #(l k m ε f A) := by  rw [← Nat.cast_pow, ← Fintype.card_piFinset_const] at h  have := my_other_markov (by positivity) (by norm_num) (fun _ _ ↦ by positivity) h  norm_num1 at this  rw [Fintype.card_piFinset_const, mul_comm, mul_one_div, Nat.cast_pow] at this  refine this.trans_eq ?_  rw [l]  congr with a : 3  refine pow_le_pow_iff_left₀ ?_ ?_ ?_ <;> positivity