Source indexedlemma · leanprover/lean4:v4.32.0

lemma28_part_one

APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:139 to 152

Mathematical statement

Exact Lean statement

lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :
    ∑ a ∈ A ^^ k, ‖∑ i, f (x - a i) - (k • (mu A ∗ᵈ f)) x‖ ^ (2 * m) ≤
      (8 * m) ^ m * k ^ (m - 1) *
        ∑ a ∈ A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ᵈ f) x‖ ^ (2 * m)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :    ∑ a ∈ A ^^ k, ‖∑ i, f (x - a i) - (k • (mu A ∗ᵈ f)) x‖ ^ (2 * m) ≤      (8 * m) ^ m * k ^ (m - 1) *        ∑ a ∈ 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 (RCLike.marcinkiewicz_zygmund (by linarith only [hm]) f' ?_).trans_eq' ?_  · intro i    rw [Fintype.sum_piFinset_apply, sum_sub_distrib]    simp only [sum_const]    rw [← Pi.smul_apply (card A), ← smul_ddconv, card_smul_mu, ddconv_eq_sum_sub']    simp only [boole_mul, Set.indicator_apply, mem_coe]    rw [← sum_filter, filter_mem_eq_inter, univ_inter, sub_self, smul_zero]  congr with a : 1  simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin, f']