Source indexedtheorem · leanprover/lean4:v4.32.0

Real.marcinkiewicz_zygmund

APAP.Prereqs.MarcinkiewiczZygmund · APAP/Prereqs/MarcinkiewiczZygmund.lean:228 to 245

Source documentation

The Marcinkiewicz-Zygmund inequality for real-valued functions, with a slightly easier to bound constant than Real.marcinkiewicz_zygmund'.

Note that RCLike.marcinkiewicz_zygmund is another version that works for both ℝ and ℂ at the expense of a slightly worse constant.

Exact Lean statement

theorem marcinkiewicz_zygmund (hm : m ≠ 0) (f : ι → ℝ) (hf : ∀ i, ∑ a ∈ A ^^ n, f (a i) = 0) :
    ∑ a ∈ A ^^ n, (∑ i, f (a i)) ^ (2 * m) ≤
      (4 * m) ^ m * n ^ (m - 1) * ∑ a ∈ A ^^ n, ∑ i, f (a i) ^ (2 * m)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem marcinkiewicz_zygmund (hm : m ≠ 0) (f : ι → ℝ) (hf : ∀ i, ∑ a ∈ A ^^ n, f (a i) = 0) :    ∑ a ∈ A ^^ n, (∑ i, f (a i)) ^ (2 * m) ≤      (4 * m) ^ m * n ^ (m - 1) * ∑ a ∈ A ^^ n, ∑ i, f (a i) ^ (2 * m) := by  obtain _ | m := m  · simp at hm  obtain rfl | hn := n.eq_zero_or_pos  · simp  calc    ∑ a ∈ A ^^ n, (∑ i, f (a i)) ^ (2 * (m + 1))      ≤ (4 * ↑(m + 1)) ^ (m + 1) * ∑ a ∈ A ^^ n, (∑ i, f (a i) ^ 2) ^ (m + 1) :=      marcinkiewicz_zygmund' _ f hf    _ ≤ (4 * ↑(m + 1)) ^ (m + 1) * (∑ a ∈ A ^^ n, n ^ m * ∑ i, f (a i) ^ (2 * (m + 1))) := ?_    _ ≤ (4 * ↑(m + 1)) ^ (m + 1) * n ^ m * ∑ a ∈ A ^^ n, ∑ i, f (a i) ^ (2 * (m + 1)) := by      simp_rw [mul_assoc, mul_sum]; rfl  gcongr with a  rw [← div_le_iff₀' (by positivity)]  simpa only [Finset.card_fin, pow_mul] using    pow_sum_div_card_le_sum_pow (f := fun i ↦ f (a i) ^ 2) (s := univ) (fun i _ ↦ by positivity) m