Source indexedlemma · leanprover/lean4:v4.32.0

step_one'

APAP.Prereqs.MarcinkiewiczZygmund · APAP/Prereqs/MarcinkiewiczZygmund.lean:53 to 62

Mathematical statement

Exact Lean statement

lemma step_one' (hA : A.Nonempty) (f : ι → ℝ) (hf : ∀ i, ∑ a ∈ A ^^ n, f (a i) = 0) (m : ℕ)
    (a : Fin n → ι) :
    |∑ i, f (a i)| ^ m ≤ (∑ b ∈ A ^^ n, |∑ i, (f (a i) - f (b i))| ^ m) / #A ^ n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma step_one' (hA : A.Nonempty) (f : ι → ℝ) (hf : ∀ i, ∑ a ∈ A ^^ n, f (a i) = 0) (m : ℕ)    (a : Fin n → ι) :    |∑ i, f (a i)| ^ m ≤ (∑ b ∈ A ^^ n, |∑ i, (f (a i) - f (b i))| ^ m) / #A ^ n := by  cases m  · simp only [_root_.pow_zero, sum_const, prod_const, Nat.smul_one_eq_cast, Finset.card_fin,      card_piFinset, ← Nat.cast_pow]    rw [div_self]    rw [Nat.cast_ne_zero, ← pos_iff_ne_zero]    exact pow_pos (Finset.card_pos.2 hA) _  exact step_one hA f a hf