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

ProbabilityTheory.Kernel.AEFiniteKernelSupport.prod

PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:861 to 868

Mathematical statement

Exact Lean statement

lemma AEFiniteKernelSupport.prod {κ : Kernel T S} {η : Kernel T U}
    [IsMarkovKernel κ] [IsMarkovKernel η] {μ : Measure T}
    (hκ : AEFiniteKernelSupport κ μ) (hη : AEFiniteKernelSupport η μ) :
    AEFiniteKernelSupport (κ ×ₖ η) μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma AEFiniteKernelSupport.prod {κ : Kernel T S} {η : Kernel T U}    [IsMarkovKernel κ] [IsMarkovKernel η] {μ : Measure T}    (hκ : AEFiniteKernelSupport κ μ) (hη : AEFiniteKernelSupport η μ) :    AEFiniteKernelSupport (κ ×ₖ η) μ := by  filter_upwards [hκ, hη] with x ⟨A, hκA⟩ ⟨B, hηB⟩  use A ×ˢ B  rw [Finset.coe_product, Set.compl_prod_eq_union, prod_apply, measure_union_null_iff,    Measure.prod_prod, Measure.prod_prod, hκA, hηB, zero_mul, mul_zero, and_self]