Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.lintegral_congr_support

Carleson.ToMathlib.RealInterpolation.Minkowski · Carleson/ToMathlib/RealInterpolation/Minkowski.lean:549 to 561

Mathematical statement

Exact Lean statement

lemma lintegral_congr_support {f : α → E₁} {g h : α → ENNReal}
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]
    (hf : AEStronglyMeasurable f μ) (hgh : ∀ x ∈ (fun x ↦ ‖f x‖ₑ).support, g x = h x) :
    ∫⁻ x : α in (fun x ↦ ‖f x‖ₑ).support, g x ∂μ =
    ∫⁻ x : α in (fun x ↦ ‖f x‖ₑ).support, h x ∂μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma lintegral_congr_support {f : α → E₁} {g h : α → ENNReal}    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]    (hf : AEStronglyMeasurable f μ) (hgh : ∀ x ∈ (fun x ↦ ‖f x‖ₑ).support, g x = h x) :    ∫⁻ x : α in (fun x ↦ ‖f x‖ₑ).support, g x ∂μ =    ∫⁻ x : α in (fun x ↦ ‖f x‖ₑ).support, h x ∂μ := by  refine lintegral_congr_ae (ae_iff.mpr ?_)  rw [Measure.restrict_apply₀']  · refine measure_mono_null (fun x h₀ ↦ ?_) measure_empty    have : g x = h x := hgh _ (mem_of_mem_inter_right h₀)    have : x ∈ {a | ¬g a = h a} := mem_of_mem_sdiff h₀    change ¬ (g x = h x) at this    contradiction  · exact (aestronglyMeasurable_iff_aemeasurable.mpr hf.enorm).nullMeasurableSet_support