Source indexedlemma · leanprover/lean4:v4.32.0

cut_out_ball

Carleson.TwoSidedCarleson.NontangentialOperator · Carleson/TwoSidedCarleson/NontangentialOperator.lean:448 to 465

Mathematical statement

Exact Lean statement

lemma cut_out_ball {g : X → ℂ} (hr : r ∈ Ioc 0 R) (hx : dist x x' ≤ R / 4) :
    czOperator K R g x' = czOperator K R ((ball x (R / 2))ᶜ.indicator g) x'

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma cut_out_ball {g : X → ℂ} (hr : r ∈ Ioc 0 R) (hx : dist x x' ≤ R / 4) :    czOperator K R g x' = czOperator K R ((ball x (R / 2))ᶜ.indicator g) x' := by  have R_pos : 0 < R := by    rw [mem_Ioc] at hr    linarith  unfold czOperator  rw [← integral_indicator, ← integral_indicator]  · congr    apply indicator_eq_indicator'    intro y hy    rw [indicator_apply_eq_self.mpr]    intro hy'    exfalso    simp at hy hy'    have : dist y x' ≤ dist y x + dist x x' := dist_triangle ..    linarith  · measurability  · measurability