Source indexedlemma · leanprover/lean4:v4.32.0

eLpNorm_czOperator

Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:955 to 975

Mathematical statement

Exact Lean statement

lemma eLpNorm_czOperator {g : ℝ → ℂ} {r : ℝ} (hr : 0 < r) (hg : MemLp g ∞ volume) :
    eLpNorm (czOperator K r g) 2 ≤ 2 ^ 9 * eLpNorm g 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eLpNorm_czOperator {g : ℝ → ℂ} {r : ℝ} (hr : 0 < r) (hg : MemLp g ∞ volume) :    eLpNorm (czOperator K r g) 2 ≤ 2 ^ 9 * eLpNorm g 2 := by  rcases le_or_gt 1 r with h'r | h'r  · have : czOperator K r g = 0 := by      ext x      simp only [czOperator, K, Pi.zero_apply]      apply setIntegral_eq_zero_of_forall_eq_zero      intro y hy      have : k (x - y) = 0 := by        apply k_of_one_le_abs        simp only [mem_compl_iff, Metric.mem_ball, dist_eq_norm', Real.norm_eq_abs, not_lt] at hy        linarith      simp [this]    simp [this]  · have := ENNReal.rpow_le_rpow (z := 2⁻¹) (eLpNorm_czOperator_sq ⟨hr, h'r⟩ hg) (by norm_num)    rw [ENNReal.mul_rpow_of_nonneg _ _ (by norm_num), ← ENNReal.rpow_ofNat, ← ENNReal.rpow_mul,      ← ENNReal.rpow_ofNat, ← ENNReal.rpow_mul, ← ENNReal.rpow_ofNat, ← ENNReal.rpow_mul] at this    simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, mul_inv_cancel₀,      ENNReal.rpow_one] at this    convert this    norm_num