Source indexedlemma · leanprover/lean4:v4.32.0

enorm_K_sub_le

Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:443 to 457

Mathematical statement

Exact Lean statement

lemma enorm_K_sub_le [ProperSpace X] [IsFiniteMeasureOnCompacts (volume : Measure X)]
    [IsOneSidedKernel a K] {x y y' : X} (h : 2 * dist y y' ≤ dist x y) :
    ‖K x y - K x y'‖ₑ ≤ (edist y y' / edist x y) ^ (a : ℝ)⁻¹ * (C_K a / vol x y)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma enorm_K_sub_le [ProperSpace X] [IsFiniteMeasureOnCompacts (volume : Measure X)]    [IsOneSidedKernel a K] {x y y' : X} (h : 2 * dist y y' ≤ dist x y) :    ‖K x y - K x y'‖ₑ ≤ (edist y y' / edist x y) ^ (a : ℝ)⁻¹ * (C_K a / vol x y) := by  simp_rw [← ofReal_norm, ← ofReal_vol, ← ofReal_coe_nnreal, edist_dist]  calc    _ ≤ ENNReal.ofReal ((dist y y' / dist x y) ^ (a : ℝ)⁻¹ * (C_K a / Real.vol x y)) := by      gcongr; apply norm_K_sub_le h    _ ≤ _ := by      rw [ENNReal.ofReal_mul']; swap      · exact div_nonneg NNReal.zero_le_coe measureReal_nonneg      gcongr      · rw [← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)]        gcongr        apply ofReal_div_le (by positivity)      · exact ofReal_div_le measureReal_nonneg