Source indexedlemma · leanprover/lean4:v4.32.0

czOperator_aestronglyMeasurable'

Carleson.TwoSidedCarleson.Basic · Carleson/TwoSidedCarleson/Basic.lean:55 to 69

Mathematical statement

Exact Lean statement

@[fun_prop]
lemma czOperator_aestronglyMeasurable' (hK : Measurable (uncurry K))
    {g : X → ℂ} (hg : AEStronglyMeasurable g) :
    AEStronglyMeasurable (fun x ↦ czOperator K r g x)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[fun_prop]lemma czOperator_aestronglyMeasurable' (hK : Measurable (uncurry K))    {g : X → ℂ} (hg : AEStronglyMeasurable g) :    AEStronglyMeasurable (fun x ↦ czOperator K r g x) := by  unfold czOperator  conv => arg 1; intro x; rw [← integral_indicator (by measurability)]  let f := fun (x,z) ↦ (ball x r)ᶜ.indicator (fun y ↦ K x y * g y) z  apply AEStronglyMeasurable.integral_prod_right' (f := f)  unfold f  apply AEStronglyMeasurable.indicator  · apply Continuous.comp_aestronglyMeasurable₂ (by fun_prop) hK.aestronglyMeasurable    exact hg.comp_snd  · conv => arg 1; change {x : (X × X) | x.2 ∈ (ball x.1 r)ᶜ}    simp_rw [mem_compl_iff, mem_ball, not_lt]    apply measurableSet_le <;> fun_prop