Source indexedlemma · leanprover/lean4:v4.32.0

M14_bound

Carleson.Antichain.AntichainOperator · Carleson/Antichain/AntichainOperator.lean:232 to 244

Mathematical statement

Exact Lean statement

lemma M14_bound (hg : MemLp g 2 volume) :
    eLpNorm (M14 𝔄 (q₆ a) g) 2 ≤ 2 ^ (a + 2) * eLpNorm g 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma M14_bound (hg : MemLp g 2 volume) :    eLpNorm (M14 𝔄 (q₆ a) g) 2 ≤ 2 ^ (a + 2) * eLpNorm g 2 := by  have a4 := four_le_a X  have ha22 : HasStrongType (M14 𝔄 (q₆ a).toNNReal) 2 2 volume volume      (C2_0_6 (defaultA a) (q₆ a).toNNReal 2) := by    apply hasStrongType_maximalFunction      (Real.toNNReal_pos.mpr <| zero_lt_one.trans (one_lt_q₆ a4))    simp only [Nat.cast_ofNat, Real.toNNReal_lt_ofNat]    exact (q₆_le_superparticular a4).trans_lt (by norm_num)  rw [Real.coe_toNNReal _ (q₆_pos (four_le_a X)).le] at ha22  apply (ha22 g hg).2.trans; gcongr  rw [show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl, ← ENNReal.coe_pow, ENNReal.coe_le_coe]  exact C2_0_6_q₆_le a4