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 ProbabilityTheory.Kernel.condKernel_apply {S : Type u_2} {T : Type u_3} {U : Type u_4} [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [Countable U] [Nonempty U] [DiscreteMeasurableSpace U] (κ : Kernel T (S × U)) [IsFiniteKernel κ] (x : T × S) (hx : (κ x.1) (Prod.fst ⁻¹' {x.2}) ≠ 0) : κ.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] [MeasurableSpace U] [Countable U] [Nonempty U] [DiscreteMeasurableSpace U] (κ : Kernel T (S × U)) [IsFiniteKernel κ] (x : T × S) (hx : (κ x.1) (Prod.fst ⁻¹' {x.2}) ≠ 0) (s : Set U) : (κ.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] [MeasurableSpace U] [Countable U] [Nonempty U] [DiscreteMeasurableSpace U] (κ : Kernel T S) [IsFiniteKernel κ] (η : Kernel (T × S) U) [IsMarkovKernel η] (x : T × S) (hx : (κ x.1) {x.2} ≠ 0) {s : Set U} (hs : MeasurableSet s) : ((κ.compProd η).condKernel 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] [MeasurableSpace U] [Countable U] [Nonempty U] [DiscreteMeasurableSpace U] (κ : Kernel T S) [IsFiniteKernel κ] (η : Kernel (T × S) U) [IsMarkovKernel η] (x : T × S) (hx : (κ x.1) {x.2} ≠ 0) : (κ.compProd η).condKernel x = η x

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

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] [MeasurableSpace T] [MeasurableSpace U] [Countable U] [Nonempty U] [DiscreteMeasurableSpace U] [Countable T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (κ : Kernel T S) [IsFiniteKernel κ] (η : Kernel (T × S) U) [IsMarkovKernel η] (μ : MeasureTheory.Measure T) [MeasureTheory.IsFiniteMeasure μ] : ⇑(κ.compProd η).condKernel =ᵐ[μ.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] [MeasurableSpace T] [MeasurableSpace U] [Countable U] [Nonempty U] [DiscreteMeasurableSpace U] [Countable T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (κ : Kernel T S) [IsFiniteKernel κ] {μ : MeasureTheory.Measure T} (η : Kernel T U) [IsMarkovKernel η] [MeasureTheory.IsFiniteMeasure μ] : ⇑(κ.prod η).condKernel =ᵐ[μ.compProd κ] ⇑(prodMkRight S η)

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] [MeasurableSpace T] [MeasurableSpace U] [Countable U] [Nonempty U] [DiscreteMeasurableSpace U] [Countable T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (κ : Kernel T (S × U)) [IsFiniteKernel κ] {μ : MeasureTheory.Measure T} (η : Kernel (T × S) U) [IsMarkovKernel η] [MeasureTheory.IsFiniteMeasure μ] (h : κ.fst.compProd η = κ) : ⇑η =ᵐ[μ.compProd κ.fst] ⇑κ.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] [MeasurableSpace T] [MeasurableSpace U] [Countable U] [Nonempty U] [DiscreteMeasurableSpace U] [Countable T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] {V : Type u_5} [Nonempty V] [MeasurableSpace V] [DiscreteMeasurableSpace V] [Countable V] (κ : Kernel T (S × U)) [IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsFiniteMeasure μ] (f : S × U → V) : ⇑(κ.map fun (p : S × U) => (p.1, f p)).condKernel =ᵐ[μ.compProd κ.fst] ⇑(κ.condKernel.compProd (deterministic (fun (x : (T × S) × U) => f (x.1.2, x.2)) ⋯)).snd

theorem ProbabilityTheory.condDistrib_apply' {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass T] {X : Ω → S} {Y : Ω → T} [Nonempty S] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (x : T) (hYx : μ (Y ⁻¹' {x}) ≠ 0) {s : Set S} (hs : MeasurableSet s) : ((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] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass T] {X : Ω → S} {Y : Ω → T} [Nonempty S] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (x : T) (hYx : μ (Y ⁻¹' {x}) ≠ 0) : (condDistrib X Y μ) x = MeasureTheory.Measure.map X (cond μ (Y ⁻¹' {x}))

theorem ProbabilityTheory.condDistrib_ae_eq {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [mΩ : MeasurableSpace Ω] [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass T] {X : Ω → S} {Y : Ω → T} [Countable T] [Nonempty S] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ⇑(condDistrib X Y μ) =ᵐ[MeasureTheory.Measure.map Y μ] fun (x : T) => MeasureTheory.Measure.map X (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] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass T] [Countable U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} [Countable T] [Nonempty S] [Nonempty U] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (f : S → U) : ⇑(condDistrib (f ∘ X) Y μ) =ᵐ[MeasureTheory.Measure.map Y μ] ⇑((condDistrib X Y μ).map 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] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass T] [Countable U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [Countable T] [Nonempty T] [Nonempty S] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (u : U) (hu : μ (Z ⁻¹' {u}) ≠ 0) : (condDistrib (fun (a : Ω) => (X a, Y a)) Z μ).fst u = (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] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass T] [Countable U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [Countable T] [Nonempty T] [Nonempty S] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ⇑(condDistrib (fun (a : Ω) => (X a, Y a)) Z μ).fst =ᵐ[MeasureTheory.Measure.map Z μ] ⇑(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] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass T] [Countable U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [Countable T] [Nonempty T] [Nonempty S] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (u : U) (hu : μ (Z ⁻¹' {u}) ≠ 0) : (condDistrib (fun (a : Ω) => (X a, Y a)) Z μ).snd u = (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] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass T] [Countable U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [Countable T] [Nonempty T] [Nonempty S] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ⇑(condDistrib (fun (a : Ω) => (X a, Y a)) Z μ).snd =ᵐ[MeasureTheory.Measure.map Z μ] ⇑(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] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass T] [Countable U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [Countable T] [Nonempty T] [Nonempty S] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ⇑(condDistrib (fun (a : Ω) => (X a, Y a)) Z μ).condKernel =ᵐ[MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, X ω)) μ] ⇑(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] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass T] [Countable U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [Countable T] [Nonempty T] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ⇑((condDistrib Y (fun (a : Ω) => (X a, Z a)) μ).comap Prod.swap ⋯) =ᵐ[MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, X ω)) μ] ⇑(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] [MeasurableSpace T] [MeasurableSingletonClass T] {X : Ω → S} {Y : Ω → T} [Countable T] [Nonempty T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ⇑(Kernel.const Unit (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, Y ω)) μ)).condKernel =ᵐ[MeasureTheory.Measure.map (fun (ω : Ω) => ((), X ω)) μ] ⇑(Kernel.prodMkLeft Unit (condDistrib Y X μ))

theorem ProbabilityTheory.condDistrib_unit_right {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [Countable S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {X : Ω → S} [Nonempty S] (hX : Measurable X) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : condDistrib X (fun (x : Ω) => ()) μ = 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] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace U] [Countable U] [DiscreteMeasurableSpace U] {X : Ω → S} {Z : Ω → U} [Nonempty S] (hX : Measurable X) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : (MeasureTheory.Measure.map Z μ).compProd (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] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass T] [Countable U] [DiscreteMeasurableSpace U] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} [Countable T] [Nonempty T] {V : Type u_5} [Countable V] [MeasurableSpace V] [MeasurableSingletonClass V] {W : Ω → V} [Nonempty S] (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (h : IndepFun (fun (ω : Ω) => (X ω, Z ω)) (fun (ω : Ω) => (Y ω, W ω)) μ) : ⇑(condDistrib (fun (ω : Ω) => (X ω, Y ω)) (fun (ω : Ω) => (Z ω, W ω)) μ) =ᵐ[MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, W ω)) μ] ⇑((Kernel.prodMkRight V (condDistrib X Z μ)).prod (Kernel.prodMkLeft U (condDistrib Y W μ)))

theorem MeasureTheory.Measure.compProd_apply_singleton {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] [MeasurableSingletonClass T] (μ : Measure T) [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_6} {β : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} [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_6} {β : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} [SFinite μ] {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {p : α × β → Prop} (hp : ∀ᵐ (x : α × β) ∂μ.compProd κ, p x) : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)

theorem ProbabilityTheory.Kernel.compProd_congr_ae {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] {μ : MeasureTheory.Measure T} [MeasureTheory.SFinite μ] {κ κ' : Kernel T S} [IsSFiniteKernel κ] [IsSFiniteKernel κ'] {η η' : Kernel (T × S) U} [IsSFiniteKernel η] [IsSFiniteKernel η'] (hκ : ⇑κ =ᵐ[μ] ⇑κ') (hη : ⇑η =ᵐ[μ.compProd κ] ⇑η') : ⇑(κ.compProd η) =ᵐ[μ] ⇑(κ'.compProd η')

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

The analogue of FiniteSupport for probability kernels.

Equations

• κ.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] (κ : Kernel T S) (μ : MeasureTheory.Measure T) : Prop

A kernel κ has almost everywhere finite support wrt a measure μ if, for almost every point t, then κ t has finite support. Note that we don't require any uniformity wrt t.

Equations

• κ.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] {κ : Kernel T S} (hκ : κ.FiniteKernelSupport) (μ : MeasureTheory.Measure T) : κ.AEFiniteKernelSupport μ

@[simp]

theorem ProbabilityTheory.Kernel.finiteKernelSupport_zero {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] : FiniteKernelSupport 0

@[simp]

theorem ProbabilityTheory.Kernel.aefiniteKernelSupport_zero {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] {μ : MeasureTheory.Measure T} : AEFiniteKernelSupport 0 μ

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

The definition doesn't use hκ, but we keep it here still as it doesn't give anything interesting otherwise.

Equations

• hκ.mk = if hS : Nonempty S then ProbabilityTheory.Kernel.piecewise ⋯ κ (ProbabilityTheory.Kernel.const T (MeasureTheory.Measure.dirac hS.some)) else 0

@[simp]

theorem ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk_zero {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [Countable T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} {h : AEFiniteKernelSupport 0 μ} : h.mk = 0

@[simp]

theorem ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk_eq_zero_of_isEmpty {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [Countable T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} [IsEmpty S] {κ : Kernel T S} (hκ : κ.AEFiniteKernelSupport μ) : hκ.mk = 0

theorem ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk_eq {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [Countable T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} [hS : Nonempty S] {κ : Kernel T S} (hκ : κ.AEFiniteKernelSupport μ) : hκ.mk = piecewise ⋯ κ (const T (MeasureTheory.Measure.dirac hS.some))

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

theorem ProbabilityTheory.Kernel.AEFiniteKernelSupport.ae_eq_mk {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [Countable T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} {κ : Kernel T S} (hκ : κ.AEFiniteKernelSupport μ) : ⇑κ =ᵐ[μ] ⇑hκ.mk

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

instance ProbabilityTheory.Kernel.AEFiniteKernelSupport.isZeroOrMarkovKernel_mk {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [Countable T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} {κ : Kernel T S} [IsZeroOrMarkovKernel κ] (hκ : κ.AEFiniteKernelSupport μ) : IsZeroOrMarkovKernel hκ.mk

instance ProbabilityTheory.Kernel.AEFiniteKernelSupport.isSFiniteKernel_mk {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [Countable T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} {κ : Kernel T S} [IsSFiniteKernel κ] (hκ : κ.AEFiniteKernelSupport μ) : IsSFiniteKernel hκ.mk

theorem ProbabilityTheory.Kernel.aefiniteKernelSupport_iff {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] [Countable T] [MeasurableSingletonClass T] [MeasurableSingletonClass S] {κ : Kernel T S} {μ : MeasureTheory.Measure T} : κ.AEFiniteKernelSupport μ ↔ ∃ (κ' : Kernel T S), κ'.FiniteKernelSupport ∧ ⇑κ' =ᵐ[μ] ⇑κ

theorem ProbabilityTheory.Kernel.local_support_of_finiteKernelSupport {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] {κ : Kernel T S} (h : κ.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] (κ : Kernel T S) : κ.FiniteKernelSupport

Finite range implies finite kernel support.

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

Deterministic kernels have finite kernel support.

theorem ProbabilityTheory.Kernel.FiniteKernelSupport.map {S : Type u_2} {T : Type u_3} {U : Type u_4} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : Kernel T S} (hκ : κ.FiniteKernelSupport) (f : S → U) : (κ.map f).FiniteKernelSupport

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] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : Kernel T S} {μ : MeasureTheory.Measure T} (hκ : κ.AEFiniteKernelSupport μ) {f : S → U} : (κ.map f).AEFiniteKernelSupport μ

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

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] [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {κ : Kernel T S} {μ : MeasureTheory.Measure T} (hκ : κ.AEFiniteKernelSupport μ) (f : U ≃ᵐ T) : (κ.comap ⇑f ⋯).AEFiniteKernelSupport (MeasureTheory.Measure.comap (⇑f) μ)

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

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} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass S] {κ : Kernel T (S × U)} {μ : MeasureTheory.Measure T} (hκ : κ.AEFiniteKernelSupport μ) : κ.fst.AEFiniteKernelSupport μ

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

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] [MeasurableSpace U] [MeasurableSingletonClass U] {κ : Kernel T (S × U)} {μ : MeasureTheory.Measure T} (hκ : κ.AEFiniteKernelSupport μ) : κ.snd.AEFiniteKernelSupport μ

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

Conditioning a kernel preserves finite kernel support.

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

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} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] {κ : Kernel T (S × U)} {μ : MeasureTheory.Measure T} [MeasurableSingletonClass S] [MeasurableSingletonClass U] (hκ : κ.AEFiniteKernelSupport μ) : κ.swapRight.AEFiniteKernelSupport μ

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

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] {κ : Kernel T S} {η : Kernel T U} [IsMarkovKernel κ] [IsMarkovKernel η] {μ : MeasureTheory.Measure T} (hκ : κ.AEFiniteKernelSupport μ) (hη : η.AEFiniteKernelSupport μ) : (κ.prod η).AEFiniteKernelSupport μ

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

Composition-product preserves finite kernel support

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

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

prodMkRight preserves finite kernel support.

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

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

prodMkLeft preserves finite kernel support.

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