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

ProbabilityTheory.Kernel.FiniteKernelSupport.prod

PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:846 to 859

Source documentation

Products preserve finite kernel support.

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma FiniteKernelSupport.prod {κ : Kernel T S} {η : Kernel T U}    [MeasurableSingletonClass S] [MeasurableSingletonClass U]    [IsMarkovKernel κ] [IsMarkovKernel η]    (hκ : FiniteKernelSupport κ) (hη : FiniteKernelSupport η) :    FiniteKernelSupport (κ ×ₖ η) := by  intro t  rcases hκ t with ⟨A, hA⟩  rcases hη t with ⟨B, hB⟩  use A ×ˢ B  rw [Kernel.prod_apply' _ _ _ (by measurability)]  apply lintegral_eq_zero_of_ae_zero hA _ (by measurability)  intro s hs  refine measure_mono_null ?_ hB  intro u; simp; tauto