Source indexedlemma · leanprover/lean4:v4.32.0

measurable_carlesonOperatorIntegrand

Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:88 to 97

Mathematical statement

Exact Lean statement

@[fun_prop]
lemma measurable_carlesonOperatorIntegrand (mf : Measurable f) :
    Measurable (fun x ↦ carlesonOperatorIntegrand K (Q x) R₁ R₂ f x)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[fun_prop]lemma measurable_carlesonOperatorIntegrand (mf : Measurable f) :    Measurable (fun x ↦ carlesonOperatorIntegrand K (Q x) R₁ R₂ f x) := by  unfold carlesonOperatorIntegrand  rw [← stronglyMeasurable_iff_measurable]  conv => enter [1, x]; rw [← integral_indicator Annulus.measurableSet_oo]  apply StronglyMeasurable.integral_prod_right  rw [stronglyMeasurable_iff_measurable]  have hK : Measurable (fun (x, y) ↦ K x y) := measurable_K  exact Measurable.indicator (by fun_prop) (measurable_dist.comp measurable_id measurableSet_Ioo)