Disintegration of kernels in finite spaces

We can write κ : kernel S (T × U) as a composition-product (fst κ) ⊗ₖ (condKernel κ) where fst κ : kernel S T and condKernel : kernel (S × T) U is defined in this file.

theorem MeasureTheory.lintegral_piecewise {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (f : α → ENNReal) (g : α → ENNReal) [(j : α) → Decidable (j ∈ s)] : ∫⁻ (a : α), s.piecewise f g a ∂μ = ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in sᶜ, g a ∂μ

instance instStandardBorelSpace_discreteMeasurableSpace {α : Type u_1} [MeasurableSpace α] [DiscreteMeasurableSpace α] [Countable α] : StandardBorelSpace α

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.kernel.condKernel_apply {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [Countable U] [Nonempty U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (κ : ↥(ProbabilityTheory.kernel T (S × U))) [ProbabilityTheory.IsFiniteKernel κ] (x : T × S) (hx : (κ x.1) (Prod.fst ⁻¹' {x.2}) ≠ 0) : (ProbabilityTheory.kernel.condKernel κ) x = (κ x.1).condKernel x.2

theorem ProbabilityTheory.kernel.condKernel_apply' {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [Countable U] [Nonempty U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (κ : ↥(ProbabilityTheory.kernel T (S × U))) [ProbabilityTheory.IsFiniteKernel κ] (x : T × S) (hx : (κ x.1) (Prod.fst ⁻¹' {x.2}) ≠ 0) {s : Set U} (hs : MeasurableSet s) : ((ProbabilityTheory.kernel.condKernel κ) x) s = ((κ x.1) (Prod.fst ⁻¹' {x.2}))⁻¹ * (κ x.1) ({x.2} ×ˢ s)

theorem ProbabilityTheory.kernel.condKernel_compProd_apply' {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [Countable U] [Nonempty U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (κ : ↥(ProbabilityTheory.kernel T S)) [ProbabilityTheory.IsFiniteKernel κ] (η : ↥(ProbabilityTheory.kernel (T × S) U)) [ProbabilityTheory.IsMarkovKernel η] (x : T × S) (hx : (κ x.1) {x.2} ≠ 0) {s : Set U} (hs : MeasurableSet s) : ((ProbabilityTheory.kernel.condKernel (ProbabilityTheory.kernel.compProd κ η)) x) s = (η x) s

theorem ProbabilityTheory.kernel.condKernel_compProd_apply {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [Countable U] [Nonempty U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (κ : ↥(ProbabilityTheory.kernel T S)) [ProbabilityTheory.IsFiniteKernel κ] (η : ↥(ProbabilityTheory.kernel (T × S) U)) [ProbabilityTheory.IsMarkovKernel η] (x : T × S) (hx : (κ x.1) {x.2} ≠ 0) : (ProbabilityTheory.kernel.condKernel (ProbabilityTheory.kernel.compProd κ η)) x = η x

theorem ProbabilityTheory.kernel.condKernel_compProd_ae_eq {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Countable U] [Nonempty U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (κ : ↥(ProbabilityTheory.kernel T S)) [ProbabilityTheory.IsFiniteKernel κ] (η : ↥(ProbabilityTheory.kernel (T × S) U)) [ProbabilityTheory.IsMarkovKernel η] (μ : MeasureTheory.Measure T) [MeasureTheory.IsFiniteMeasure μ] : (μ.compProd κ).ae.EventuallyEq ⇑(ProbabilityTheory.kernel.condKernel (ProbabilityTheory.kernel.compProd κ η)) ⇑η

theorem ProbabilityTheory.kernel.condKernel_prod_ae_eq {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Countable U] [Nonempty U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {μ : MeasureTheory.Measure T} (κ : ↥(ProbabilityTheory.kernel T S)) [ProbabilityTheory.IsFiniteKernel κ] (η : ↥(ProbabilityTheory.kernel T U)) [ProbabilityTheory.IsMarkovKernel η] [MeasureTheory.IsFiniteMeasure μ] : (μ.compProd κ).ae.EventuallyEq ⇑(ProbabilityTheory.kernel.condKernel (ProbabilityTheory.kernel.prod κ η)) ⇑(ProbabilityTheory.kernel.prodMkRight S η)

theorem ProbabilityTheory.kernel.disintegration {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [Countable U] [Nonempty U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (κ : ↥(ProbabilityTheory.kernel T (S × U))) [ProbabilityTheory.IsFiniteKernel κ] : κ = ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.fst κ) (ProbabilityTheory.kernel.condKernel κ)

theorem ProbabilityTheory.kernel.ae_eq_condKernel_of_compProd_eq {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Countable U] [Nonempty U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {μ : MeasureTheory.Measure T} (κ : ↥(ProbabilityTheory.kernel T (S × U))) [ProbabilityTheory.IsFiniteKernel κ] (η : ↥(ProbabilityTheory.kernel (T × S) U)) [ProbabilityTheory.IsMarkovKernel η] [MeasureTheory.IsFiniteMeasure μ] (h : ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.fst κ) η = κ) : (μ.compProd (ProbabilityTheory.kernel.fst κ)).ae.EventuallyEq ⇑η ⇑(ProbabilityTheory.kernel.condKernel κ)

theorem ProbabilityTheory.kernel.condKernel_map_prod_mk_left {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Countable U] [Nonempty U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {V : Type u_5} [Nonempty V] [MeasurableSpace V] [DiscreteMeasurableSpace V] [Countable V] (κ : ↥(ProbabilityTheory.kernel T (S × U))) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsFiniteMeasure μ] (f : S × U → V) : (μ.compProd (ProbabilityTheory.kernel.fst κ)).ae.EventuallyEq ⇑(ProbabilityTheory.kernel.condKernel (ProbabilityTheory.kernel.map κ (fun (p : S × U) => (p.1, f p)) ⋯)) ⇑(ProbabilityTheory.kernel.snd (ProbabilityTheory.kernel.compProd (ProbabilityTheory.kernel.condKernel κ) (ProbabilityTheory.kernel.deterministic (fun (x : (T × S) × U) => f (x.1.2, x.2)) ⋯)))

theorem ProbabilityTheory.condDistrib_apply' {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [Countable S] [Nonempty S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [MeasurableSpace T] [DiscreteMeasurableSpace T] {X : Ω → S} {Y : Ω → T} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (x : T) (hYx : μ (Y ⁻¹' {x}) ≠ 0) {s : Set S} (hs : MeasurableSet s) : ((ProbabilityTheory.condDistrib X Y μ) x) s = (μ (Y ⁻¹' {x}))⁻¹ * μ (Y ⁻¹' {x} ∩ X ⁻¹' s)

theorem ProbabilityTheory.condDistrib_apply {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [Countable S] [Nonempty S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [MeasurableSpace T] [DiscreteMeasurableSpace T] {X : Ω → S} {Y : Ω → T} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (x : T) (hYx : μ (Y ⁻¹' {x}) ≠ 0) : (ProbabilityTheory.condDistrib X Y μ) x = MeasureTheory.Measure.map X (ProbabilityTheory.cond μ (Y ⁻¹' {x}))

theorem ProbabilityTheory.condDistrib_ae_eq {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [Countable S] [Nonempty S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [MeasurableSpace T] [DiscreteMeasurableSpace T] {X : Ω → S} {Y : Ω → T} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : (MeasureTheory.Measure.map Y μ).ae.EventuallyEq ⇑(ProbabilityTheory.condDistrib X Y μ) fun (x : T) => MeasureTheory.Measure.map X (ProbabilityTheory.cond μ (Y ⁻¹' {x}))

theorem ProbabilityTheory.condDistrib_comp {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [Countable S] [Nonempty S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Countable U] [Nonempty U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (f : S → U) : (MeasureTheory.Measure.map Y μ).ae.EventuallyEq ⇑(ProbabilityTheory.condDistrib (f ∘ X) Y μ) ⇑(ProbabilityTheory.kernel.map (ProbabilityTheory.condDistrib X Y μ) f ⋯)

theorem ProbabilityTheory.condDistrib_fst_of_ne_zero {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [Countable S] [Nonempty S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [Nonempty T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Countable U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (u : U) (hu : μ (Z ⁻¹' {u}) ≠ 0) : (ProbabilityTheory.kernel.fst (ProbabilityTheory.condDistrib (fun (a : Ω) => (X a, Y a)) Z μ)) u = (ProbabilityTheory.condDistrib X Z μ) u

theorem ProbabilityTheory.condDistrib_fst_ae_eq {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [Countable S] [Nonempty S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [Nonempty T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Countable U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : (MeasureTheory.Measure.map Z μ).ae.EventuallyEq ⇑(ProbabilityTheory.kernel.fst (ProbabilityTheory.condDistrib (fun (a : Ω) => (X a, Y a)) Z μ)) ⇑(ProbabilityTheory.condDistrib X Z μ)

theorem ProbabilityTheory.condDistrib_snd_of_ne_zero {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [Countable S] [Nonempty S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [Nonempty T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Countable U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (u : U) (hu : μ (Z ⁻¹' {u}) ≠ 0) : (ProbabilityTheory.kernel.snd (ProbabilityTheory.condDistrib (fun (a : Ω) => (X a, Y a)) Z μ)) u = (ProbabilityTheory.condDistrib Y Z μ) u

theorem ProbabilityTheory.condDistrib_snd_ae_eq {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [Countable S] [Nonempty S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [Nonempty T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Countable U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : (MeasureTheory.Measure.map Z μ).ae.EventuallyEq ⇑(ProbabilityTheory.kernel.snd (ProbabilityTheory.condDistrib (fun (a : Ω) => (X a, Y a)) Z μ)) ⇑(ProbabilityTheory.condDistrib Y Z μ)

theorem ProbabilityTheory.condKernel_condDistrib_ae_eq {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [Countable S] [Nonempty S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [Nonempty T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Countable U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : (MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, X ω)) μ).ae.EventuallyEq ⇑(ProbabilityTheory.kernel.condKernel (ProbabilityTheory.condDistrib (fun (a : Ω) => (X a, Y a)) Z μ)) ⇑(ProbabilityTheory.condDistrib Y (fun (ω : Ω) => (Z ω, X ω)) μ)

theorem ProbabilityTheory.swap_condDistrib_ae_eq {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [Nonempty T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Countable U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : (MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, X ω)) μ).ae.EventuallyEq ⇑(ProbabilityTheory.kernel.comap (ProbabilityTheory.condDistrib Y (fun (a : Ω) => (X a, Z a)) μ) Prod.swap ⋯) ⇑(ProbabilityTheory.condDistrib Y (fun (ω : Ω) => (Z ω, X ω)) μ)

theorem ProbabilityTheory.condDistrib_const_unit {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [Nonempty T] [MeasurableSpace T] [DiscreteMeasurableSpace T] {X : Ω → S} {Y : Ω → T} (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : (MeasureTheory.Measure.map (fun (ω : Ω) => ((), X ω)) μ).ae.EventuallyEq ⇑(ProbabilityTheory.kernel.condKernel (ProbabilityTheory.kernel.const Unit (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, Y ω)) μ))) ⇑(ProbabilityTheory.kernel.prodMkLeft Unit (ProbabilityTheory.condDistrib Y X μ))

theorem ProbabilityTheory.condDistrib_unit_right {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [Countable S] [Nonempty S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {X : Ω → S} (hX : Measurable X) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : ProbabilityTheory.condDistrib X (fun (x : Ω) => ()) μ = ProbabilityTheory.kernel.const Unit (MeasureTheory.Measure.map X μ)

theorem ProbabilityTheory.map_compProd_condDistrib {Ω : Type u_1} {S : Type u_2} {U : Type u_4} [mΩ : MeasurableSpace Ω] [Countable S] [Nonempty S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {X : Ω → S} {Z : Ω → U} (hX : Measurable X) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : (MeasureTheory.Measure.map Z μ).compProd (ProbabilityTheory.condDistrib X Z μ) = MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, X ω)) μ

theorem ProbabilityTheory.condDistrib_eq_prod_of_indepFun {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [mΩ : MeasurableSpace Ω] [Countable S] [Nonempty S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable T] [Nonempty T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Countable U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} {V : Type u_5} [Countable V] [MeasurableSpace V] [MeasurableSingletonClass V] {W : Ω → V} (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (h : ProbabilityTheory.IndepFun (fun (ω : Ω) => (X ω, Z ω)) (fun (ω : Ω) => (Y ω, W ω)) μ) : (MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, W ω)) μ).ae.EventuallyEq ⇑(ProbabilityTheory.condDistrib (fun (ω : Ω) => (X ω, Y ω)) (fun (ω : Ω) => (Z ω, W ω)) μ) ⇑(ProbabilityTheory.kernel.prod (ProbabilityTheory.kernel.prodMkRight V (ProbabilityTheory.condDistrib X Z μ)) (ProbabilityTheory.kernel.prodMkLeft U (ProbabilityTheory.condDistrib Y W μ)))

theorem MeasureTheory.Measure.compProd_apply_singleton {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSingletonClass S] [MeasurableSpace T] [MeasurableSingletonClass T] (μ : MeasureTheory.Measure T) [MeasureTheory.SFinite μ] (κ : ↥(ProbabilityTheory.kernel T S)) [ProbabilityTheory.IsSFiniteKernel κ] (t : T) (s : S) : (μ.compProd κ) {(t, s)} = (κ t) {s} * μ {t}

theorem MeasureTheory.Measure.ae_of_compProd_eq_zero {α : Type u_5} {β : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {κ : ↥(ProbabilityTheory.kernel α β)} [ProbabilityTheory.IsSFiniteKernel κ] {s : Set (α × β)} (hs : (μ.compProd κ) s = 0) : ∀ᵐ (a : α) ∂μ, (κ a) (Prod.mk a ⁻¹' s) = 0

theorem MeasureTheory.Measure.ae_of_ae_compProd {α : Type u_5} {β : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {κ : ↥(ProbabilityTheory.kernel α β)} [ProbabilityTheory.IsSFiniteKernel κ] {p : α × β → Prop} (hp : ∀ᵐ (x : α × β) ∂μ.compProd κ, p x) : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)

theorem ProbabilityTheory.kernel.compProd_congr {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] {μ : MeasureTheory.Measure T} [MeasureTheory.SFinite μ] {κ : ↥(ProbabilityTheory.kernel T S)} {κ' : ↥(ProbabilityTheory.kernel T S)} [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel κ'] {η : ↥(ProbabilityTheory.kernel (T × S) U)} {η' : ↥(ProbabilityTheory.kernel (T × S) U)} [ProbabilityTheory.IsMarkovKernel η] [ProbabilityTheory.IsMarkovKernel η'] (hκ : μ.ae.EventuallyEq ⇑κ ⇑κ') (hη : (μ.compProd κ).ae.EventuallyEq ⇑η ⇑η') : μ.ae.EventuallyEq ⇑(ProbabilityTheory.kernel.compProd κ η) ⇑(ProbabilityTheory.kernel.compProd κ' η')

noncomputable def ProbabilityTheory.kernel.FiniteKernelSupport {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (κ : ↥(ProbabilityTheory.kernel T S)) : Prop

The analogue of FiniteSupport for probability kernels.

Equations

• ProbabilityTheory.kernel.FiniteKernelSupport κ = ∀ (t : T), ∃ (A : Finset S), (κ t) (↑A)ᶜ = 0

noncomputable def ProbabilityTheory.kernel.AEFiniteKernelSupport {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] (κ : ↥(ProbabilityTheory.kernel T S)) (μ : MeasureTheory.Measure T) : Prop

Equations

• ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ = ∀ᵐ (t : T) ∂μ, ∃ (A : Finset S), (κ t) (↑A)ᶜ = 0

theorem ProbabilityTheory.kernel.FiniteKernelSupport.aefiniteKernelSupport {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] {κ : ↥(ProbabilityTheory.kernel T S)} (hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ) (μ : MeasureTheory.Measure T) : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ

noncomputable def ProbabilityTheory.kernel.AEFiniteKernelSupport.mk {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} [hS : Nonempty S] {κ : ↥(ProbabilityTheory.kernel T S)} (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : ↥(ProbabilityTheory.kernel T S)

Equations

• hκ.mk = ProbabilityTheory.kernel.piecewise ⋯ κ (ProbabilityTheory.kernel.const T (MeasureTheory.Measure.dirac hS.some))

theorem ProbabilityTheory.kernel.AEFiniteKernelSupport.finiteKernelSupport_mk {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} [hS : Nonempty S] {κ : ↥(ProbabilityTheory.kernel T S)} (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : ProbabilityTheory.kernel.FiniteKernelSupport hκ.mk

theorem ProbabilityTheory.kernel.AEFiniteKernelSupport.ae_eq_mk {S : Type u_2} {T : Type u_3} [Nonempty S] [MeasurableSpace S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} {κ : ↥(ProbabilityTheory.kernel T S)} (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : μ.ae.EventuallyEq ⇑κ ⇑hκ.mk

instance ProbabilityTheory.kernel.AEFiniteKernelSupport.isMarkovKernel_mk {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} [hS : Nonempty S] {κ : ↥(ProbabilityTheory.kernel T S)} [ProbabilityTheory.IsMarkovKernel κ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : ProbabilityTheory.IsMarkovKernel hκ.mk

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.kernel.aefiniteKernelSupport_iff {S : Type u_2} {T : Type u_3} [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] {κ : ↥(ProbabilityTheory.kernel T S)} {μ : MeasureTheory.Measure T} : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ ↔ ∃ (κ' : ↥(ProbabilityTheory.kernel T S)), ProbabilityTheory.kernel.FiniteKernelSupport κ' ∧ μ.ae.EventuallyEq ⇑κ' ⇑κ

theorem ProbabilityTheory.kernel.local_support_of_finiteKernelSupport {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] {κ : ↥(ProbabilityTheory.kernel T S)} (h : ProbabilityTheory.kernel.FiniteKernelSupport κ) (A : Finset T) : ∃ (B : Finset S), ∀ t ∈ A, (κ t) (↑B)ᶜ = 0

Finite kernel support locally implies uniform finite kernel support.

theorem ProbabilityTheory.kernel.finiteKernelSupport_of_finite_range {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [Fintype S] (κ : ↥(ProbabilityTheory.kernel T S)) : ProbabilityTheory.kernel.FiniteKernelSupport κ

Finite range implies finite kernel support.

theorem ProbabilityTheory.kernel.finiteKernelSupport_of_deterministic {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace U] [MeasurableSingletonClass U] (f : T × S → U) : ProbabilityTheory.kernel.FiniteKernelSupport (ProbabilityTheory.kernel.deterministic f ⋯)

Deterministic kernels have finite kernel support.

theorem ProbabilityTheory.kernel.finiteKernelSupport_of_map {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [Countable U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T S)} (hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ) {f : S → U} (hf : Measurable f) : ProbabilityTheory.kernel.FiniteKernelSupport (ProbabilityTheory.kernel.map κ f hf)

maps preserve finite kernel support.

theorem ProbabilityTheory.kernel.AEFiniteKernelSupport.map {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [Countable U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T S)} {μ : MeasureTheory.Measure T} (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) {f : S → U} (hf : Measurable f) : ProbabilityTheory.kernel.AEFiniteKernelSupport (ProbabilityTheory.kernel.map κ f hf) μ

theorem ProbabilityTheory.kernel.finiteKernelSupport_of_comap {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] {κ : ↥(ProbabilityTheory.kernel T S)} (hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ) {f : U → T} (hf : Measurable f) : ProbabilityTheory.kernel.FiniteKernelSupport (ProbabilityTheory.kernel.comap κ f hf)

comaps preserve finite kernel support.

theorem ProbabilityTheory.kernel.AEFiniteKernelSupport.comap_equiv {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [Countable U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T S)} {μ : MeasureTheory.Measure T} (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) (f : U ≃ᵐ T) : ProbabilityTheory.kernel.AEFiniteKernelSupport (ProbabilityTheory.kernel.comap κ ⇑f ⋯) (MeasureTheory.Measure.comap (⇑f) μ)

theorem ProbabilityTheory.kernel.finiteKernelSupport_of_fst {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [MeasurableSingletonClass S] [MeasurableSpace T] [MeasurableSpace U] {κ : ↥(ProbabilityTheory.kernel T (S × U))} (hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ) : ProbabilityTheory.kernel.FiniteKernelSupport (ProbabilityTheory.kernel.fst κ)

Projecting a kernel to first coordinate preserves finite kernel support.

theorem ProbabilityTheory.kernel.AEFiniteKernelSupport.fst {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [MeasurableSingletonClass S] [MeasurableSpace T] [MeasurableSpace U] {κ : ↥(ProbabilityTheory.kernel T (S × U))} {μ : MeasureTheory.Measure T} (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : ProbabilityTheory.kernel.AEFiniteKernelSupport (ProbabilityTheory.kernel.fst κ) μ

theorem ProbabilityTheory.kernel.finiteKernelSupport_of_snd {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [Countable U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T (S × U))} (hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ) : ProbabilityTheory.kernel.FiniteKernelSupport (ProbabilityTheory.kernel.snd κ)

Projecting a kernel to second coordinate preserves finite kernel support.

theorem ProbabilityTheory.kernel.AEFiniteKernelSupport.snd {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [Countable U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T (S × U))} {μ : MeasureTheory.Measure T} (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : ProbabilityTheory.kernel.AEFiniteKernelSupport (ProbabilityTheory.kernel.snd κ) μ

theorem ProbabilityTheory.kernel.aefiniteKernelSupport_of_cond {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T (S × U))} [hU : Nonempty U] (μ : MeasureTheory.Measure T) [MeasureTheory.IsFiniteMeasure μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.kernel.AEFiniteKernelSupport (ProbabilityTheory.kernel.condKernel κ) (μ.compProd (ProbabilityTheory.kernel.fst κ))

Conditioning a kernel preserves finite kernel support.

theorem ProbabilityTheory.kernel.finiteKernelSupport_of_swapRight {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [MeasurableSingletonClass S] [MeasurableSpace T] [Countable U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T (S × U))} (hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ) : ProbabilityTheory.kernel.FiniteKernelSupport (ProbabilityTheory.kernel.swapRight κ)

Swapping a kernel right preserves finite kernel support.

theorem ProbabilityTheory.kernel.AEFiniteKernelSupport.swapRight {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [MeasurableSingletonClass S] [MeasurableSpace T] [Countable U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T (S × U))} {μ : MeasureTheory.Measure T} (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) : ProbabilityTheory.kernel.AEFiniteKernelSupport (ProbabilityTheory.kernel.swapRight κ) μ

theorem ProbabilityTheory.kernel.finiteKernelSupport_of_prod {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [MeasurableSingletonClass S] [MeasurableSpace T] [Countable U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T S)} {η : ↥(ProbabilityTheory.kernel T U)} [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] (hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ) (hη : ProbabilityTheory.kernel.FiniteKernelSupport η) : ProbabilityTheory.kernel.FiniteKernelSupport (ProbabilityTheory.kernel.prod κ η)

Products preserve finite kernel support.

theorem ProbabilityTheory.kernel.AEFiniteKernelSupport.prod {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] {κ : ↥(ProbabilityTheory.kernel T S)} {η : ↥(ProbabilityTheory.kernel T U)} [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] {μ : MeasureTheory.Measure T} (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) (hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η μ) : ProbabilityTheory.kernel.AEFiniteKernelSupport (ProbabilityTheory.kernel.prod κ η) μ

theorem ProbabilityTheory.kernel.finiteKernelSupport_of_compProd {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [MeasurableSingletonClass S] [MeasurableSpace T] [Countable U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T S)} [ProbabilityTheory.IsMarkovKernel κ] {η : ↥(ProbabilityTheory.kernel (T × S) U)} [ProbabilityTheory.IsMarkovKernel η] (hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ) (hη : ProbabilityTheory.kernel.FiniteKernelSupport η) : ProbabilityTheory.kernel.FiniteKernelSupport (ProbabilityTheory.kernel.compProd κ η)

Composition-product preserves finite kernel support

theorem ProbabilityTheory.kernel.AEFiniteKernelSupport.compProd {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable U] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : ↥(ProbabilityTheory.kernel T S)} {η : ↥(ProbabilityTheory.kernel (T × S) U)} [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] {μ : MeasureTheory.Measure T} [MeasureTheory.SFinite μ] (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) (hη : ProbabilityTheory.kernel.AEFiniteKernelSupport η (μ.compProd κ)) : ProbabilityTheory.kernel.AEFiniteKernelSupport (ProbabilityTheory.kernel.compProd κ η) μ

theorem ProbabilityTheory.kernel.finiteKernelSupport_of_prodMkRight {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] {κ : ↥(ProbabilityTheory.kernel T S)} (hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ) : ProbabilityTheory.kernel.FiniteKernelSupport (ProbabilityTheory.kernel.prodMkRight U κ)

prodMkRight preserves finite kernel support.

theorem ProbabilityTheory.kernel.AEFiniteKernelSupport.prodMkRight {S : Type u_2} {T : Type u_3} {U : Type u_4} [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable U] [MeasurableSpace U] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure T} {κ : ↥(ProbabilityTheory.kernel T S)} (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) (ν : MeasureTheory.Measure U) [MeasureTheory.SFinite ν] : ProbabilityTheory.kernel.AEFiniteKernelSupport (ProbabilityTheory.kernel.prodMkRight U κ) (μ.prod ν)

theorem ProbabilityTheory.kernel.finiteKernelSupport_of_prodMkLeft {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] {κ : ↥(ProbabilityTheory.kernel T S)} (hκ : ProbabilityTheory.kernel.FiniteKernelSupport κ) : ProbabilityTheory.kernel.FiniteKernelSupport (ProbabilityTheory.kernel.prodMkLeft U κ)

prodMkLeft preserves finite kernel support.

theorem ProbabilityTheory.kernel.AEFiniteKernelSupport.prodMkLeft {S : Type u_2} {T : Type u_3} {U : Type u_4} [Nonempty S] [MeasurableSpace S] [MeasurableSingletonClass S] [Countable T] [MeasurableSpace T] [MeasurableSingletonClass T] [Countable U] [MeasurableSpace U] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure T} {κ : ↥(ProbabilityTheory.kernel T S)} (hκ : ProbabilityTheory.kernel.AEFiniteKernelSupport κ μ) (ν : MeasureTheory.Measure U) [MeasureTheory.SFinite μ] : ProbabilityTheory.kernel.AEFiniteKernelSupport (ProbabilityTheory.kernel.prodMkLeft U κ) (ν.prod μ)