Source indexedlemma · leanprover/lean4:v4.32.0

enorm_Ks_le

Carleson.Psi · Carleson/Psi.lean:530 to 540

Source documentation

Lemma 2.1.3 part 2, equation (2.1.3)

Exact Lean statement

lemma enorm_Ks_le {s : ℤ} {x y : X} :
    ‖Ks s x y‖ₑ ≤ C2_1_3 a / volume (ball x (D ^ s))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma enorm_Ks_le {s : ℤ} {x y : X} :    ‖Ks s x y‖ₑ ≤ C2_1_3 a / volume (ball x (D ^ s)) := by  calc    _ ≤ ‖C2_1_3 a / volume.real (ball x (D ^ s))‖ₑ := by      rw [← enorm_norm]; exact Real.enorm_le_enorm (norm_nonneg _) norm_Ks_le    _ = _ := by      rw [div_eq_mul_inv, enorm_mul, enorm_inv]; swap      · exact ENNReal.toReal_ne_zero.mpr          ⟨(measure_ball_pos volume _ (defaultD_pow_pos a s)).ne', by finiteness⟩      rw [enorm_eq, ← div_eq_mul_inv, Real.enorm_eq_ofReal measureReal_nonneg]; congr 1      exact ENNReal.ofReal_toReal (by finiteness)