Source indexedlemma · leanprover/lean4:v4.32.0

integrableOn_K_Icc

Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:472 to 480

Mathematical statement

Exact Lean statement

lemma integrableOn_K_Icc [IsOpenPosMeasure (volume : Measure X)]
    [IsFiniteMeasureOnCompacts (volume : Measure X)] [ProperSpace X]
    [IsOneSidedKernel a K] {x : X} {r R : ℝ} (hr : r > 0) :
    IntegrableOn (K x) {y | dist x y ∈ Icc r R} volume

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integrableOn_K_Icc [IsOpenPosMeasure (volume : Measure X)]    [IsFiniteMeasureOnCompacts (volume : Measure X)] [ProperSpace X]    [IsOneSidedKernel a K] {x : X} {r R : ℝ} (hr : r > 0) :    IntegrableOn (K x) {y | dist x y ∈ Icc r R} volume := by  rw [← mul_one (K x)]  refine integrableOn_K_mul ?_ x hr ?_  · have : {y | dist x y ∈ Icc r R} ⊆ closedBall x R := Annulus.cc_subset_closedBall    exact integrableOn_const ((measure_mono this).trans_lt measure_closedBall_lt_top).ne  · intro y hy; simp [hy.1, dist_comm y x]