Source indexedlemma · leanprover/lean4:v4.33.0-rc1

MeasureTheory.Measure.ae_of_compProd_eq_zero

PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:534 to 546

Mathematical statement

Exact Lean statement

lemma _root_.MeasureTheory.Measure.ae_of_compProd_eq_zero {α β : Type*}
    {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
    {μ : Measure α} [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ]
    {s : Set (α × β)} (hs : (μ ⊗ₘ κ) s = 0) :
    ∀ᵐ a ∂μ, κ a (Prod.mk a ⁻¹' s) = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma _root_.MeasureTheory.Measure.ae_of_compProd_eq_zero {α β : Type*}    {mα : MeasurableSpace α} {mβ : MeasurableSpace β}    {μ : Measure α} [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ]    {s : Set (α × β)} (hs : (μ ⊗ₘ κ) s = 0) :    ∀ᵐ a ∂μ, κ a (Prod.mk a ⁻¹' s) = 0 := by  let t := toMeasurable (μ ⊗ₘ κ) s  have ht : (μ ⊗ₘ κ) t = 0 := by    unfold t    rwa [measure_toMeasurable]  rw [Measure.compProd_apply (measurableSet_toMeasurable _ _), lintegral_eq_zero_iff] at ht  swap; · exact measurable_kernel_prodMk_left (measurableSet_toMeasurable _ _)  filter_upwards [ht] with a ha  exact measure_mono_null (fun y hy ↦ subset_toMeasurable (μ ⊗ₘ κ) s hy) ha