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

MeasureTheory.Measure.compProd_apply_singleton

PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:513 to 532

Mathematical statement

Exact Lean statement

lemma _root_.MeasureTheory.Measure.compProd_apply_singleton
    [MeasurableSingletonClass S] [MeasurableSingletonClass T]
    (μ : Measure T) [SFinite μ]
    (κ : Kernel T S) [IsSFiniteKernel κ] (t : T) (s : S) :
    (μ ⊗ₘ κ) {(t, s)} = κ t {s} * μ {t}

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma _root_.MeasureTheory.Measure.compProd_apply_singleton    [MeasurableSingletonClass S] [MeasurableSingletonClass T]    (μ : Measure T) [SFinite μ]    (κ : Kernel T S) [IsSFiniteKernel κ] (t : T) (s : S) :    (μ ⊗ₘ κ) {(t, s)} = κ t {s} * μ {t} := by  rw [Measure.compProd_apply (.singleton _)]  have : ∀ a, κ a (Prod.mk a ⁻¹' {(t, s)}) = ({t} : Set T).indicator (fun _ ↦ κ t {s}) a := by    intro a    by_cases ha : a = t    · simp only [ha, Set.mem_singleton_iff, Set.indicator_of_mem]      congr      ext y      simp    · simp only [Set.mem_singleton_iff, ha, not_false_eq_true, Set.indicator_of_notMem]      suffices Prod.mk a ⁻¹' {(t, s)} = ∅ by simp [this]      ext y      simp [ha]  simp_rw [this]  rw [lintegral_indicator (.singleton _)]  simp