Source indexedlemma · leanprover/lean4:v4.32.0

enorm_Ks_sub_Ks_le

Carleson.Psi · Carleson/Psi.lean:820 to 830

Source documentation

Lemma 2.1.3 part 3, equation (2.1.4)

Exact Lean statement

lemma enorm_Ks_sub_Ks_le {s : ℤ} {x y y' : X} :
    ‖Ks s x y - Ks s x y'‖ₑ ≤
      D2_1_3 a / volume (ball x (D ^ s)) * (edist y y' / D ^ s) ^ (a : ℝ)⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma enorm_Ks_sub_Ks_le {s : ℤ} {x y y' : X} :    ‖Ks s x y - Ks s x y'‖ₑ ≤      D2_1_3 a / volume (ball x (D ^ s)) * (edist y y' / D ^ s) ^ (a : ℝ)⁻¹ := by  by_cases h : Ks s x y ≠ 0 ∨ Ks s x y' ≠ 0  · rcases h with hy | hy'    · exact enorm_Ks_sub_Ks_le_of_nonzero hy    · rw [← neg_sub, enorm_neg, edist_comm]      exact enorm_Ks_sub_Ks_le_of_nonzero hy'  · simp only [ne_eq, not_or, Decidable.not_not] at h    rw [h.1, h.2, sub_zero, enorm_zero]    positivity