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] (κ : ProbabilityTheory.Kernel T (S × U)) [ProbabilityTheory.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] (κ : ProbabilityTheory.Kernel T (S × U)) [ProbabilityTheory.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] (κ : 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) : ((κ.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] (κ : ProbabilityTheory.Kernel T S) [ProbabilityTheory.IsFiniteKernel κ] (η : ProbabilityTheory.Kernel (T × S) U) [ProbabilityTheory.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] (κ : ProbabilityTheory.Kernel T (S × U)) [ProbabilityTheory.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] (κ : ProbabilityTheory.Kernel T S) [ProbabilityTheory.IsFiniteKernel κ] (η : ProbabilityTheory.Kernel (T × S) U) [ProbabilityTheory.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] (κ : ProbabilityTheory.Kernel T S) [ProbabilityTheory.IsFiniteKernel κ] {μ : MeasureTheory.Measure T} (η : ProbabilityTheory.Kernel T U) [ProbabilityTheory.IsMarkovKernel η] [MeasureTheory.IsFiniteMeasure μ] : ⇑(κ.prod η).condKernel =ᵐ[μ.compProd κ] ⇑(ProbabilityTheory.Kernel.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] (κ : ProbabilityTheory.Kernel T (S × U)) [ProbabilityTheory.IsFiniteKernel κ] {μ : MeasureTheory.Measure T} (η : ProbabilityTheory.Kernel (T × S) U) [ProbabilityTheory.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] (κ : ProbabilityTheory.Kernel T (S × U)) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure T) [MeasureTheory.IsFiniteMeasure μ] (f : S × U → V) : ⇑(κ.map fun (p : S × U) => (p.1, f p)).condKernel =ᵐ[μ.compProd κ.fst] ⇑(κ.condKernel.compProd (ProbabilityTheory.Kernel.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) : ((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] [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) : (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] [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 μ] : ⇑(ProbabilityTheory.condDistrib X Y μ) =ᵐ[MeasureTheory.Measure.map 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] [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) : ⇑(ProbabilityTheory.condDistrib (f ∘ X) Y μ) =ᵐ[MeasureTheory.Measure.map Y μ] ⇑((ProbabilityTheory.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) : (ProbabilityTheory.condDistrib (fun (a : Ω) => (X a, Y a)) Z μ).fst 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] [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 μ] : ⇑(ProbabilityTheory.condDistrib (fun (a : Ω) => (X a, Y a)) Z μ).fst =ᵐ[MeasureTheory.Measure.map 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] [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) : (ProbabilityTheory.condDistrib (fun (a : Ω) => (X a, Y a)) Z μ).snd 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] [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 μ] : ⇑(ProbabilityTheory.condDistrib (fun (a : Ω) => (X a, Y a)) Z μ).snd =ᵐ[MeasureTheory.Measure.map 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] [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 μ] : ⇑(ProbabilityTheory.condDistrib (fun (a : Ω) => (X a, Y a)) Z μ).condKernel =ᵐ[MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, X ω)) μ] ⇑(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] [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 μ] : ⇑((ProbabilityTheory.condDistrib Y (fun (a : Ω) => (X a, Z a)) μ).comap Prod.swap ⋯) =ᵐ[MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, X ω)) μ] ⇑(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] [MeasurableSpace T] [MeasurableSingletonClass T] {X : Ω → S} {Y : Ω → T} [Countable T] [Nonempty T] (hX : Measurable X) (hY : Measurable Y) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ⇑(ProbabilityTheory.Kernel.const Unit (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, Y ω)) μ)).condKernel =ᵐ[MeasureTheory.Measure.map (fun (ω : Ω) => ((), X ω)) μ] ⇑(ProbabilityTheory.Kernel.prodMkLeft Unit (ProbabilityTheory.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 μ] : 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] [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 (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] [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 : ProbabilityTheory.IndepFun (fun (ω : Ω) => (X ω, Z ω)) (fun (ω : Ω) => (Y ω, W ω)) μ) : ⇑(ProbabilityTheory.condDistrib (fun (ω : Ω) => (X ω, Y ω)) (fun (ω : Ω) => (Z ω, W ω)) μ) =ᵐ[MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, W ω)) μ] ⇑((ProbabilityTheory.Kernel.prodMkRight V (ProbabilityTheory.condDistrib X Z μ)).prod (ProbabilityTheory.Kernel.prodMkLeft U (ProbabilityTheory.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] (μ : 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_6} {β : Type u_7} {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_6} {β : Type u_7} {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.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel κ'] {η : ProbabilityTheory.Kernel (T × S) U} {η' : ProbabilityTheory.Kernel (T × S) U} [ProbabilityTheory.IsSFiniteKernel η] [ProbabilityTheory.IsSFiniteKernel η'] (hκ : ⇑κ =ᵐ[μ] ⇑κ') (hη : ⇑η =ᵐ[μ.compProd κ] ⇑η') : ⇑(κ.compProd η) =ᵐ[μ] ⇑(κ'.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

• κ.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

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] {κ : ProbabilityTheory.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] : ProbabilityTheory.Kernel.FiniteKernelSupport 0

@[simp]

theorem ProbabilityTheory.Kernel.aefiniteKernelSupport_zero {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] {μ : MeasureTheory.Measure T} : ProbabilityTheory.Kernel.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} {κ : ProbabilityTheory.Kernel T S} (hκ : κ.AEFiniteKernelSupport μ) : ProbabilityTheory.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 : ProbabilityTheory.Kernel.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] {κ : ProbabilityTheory.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] {κ : ProbabilityTheory.Kernel T S} (hκ : κ.AEFiniteKernelSupport μ) : 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] [MeasurableSpace T] [Countable T] [MeasurableSingletonClass T] {μ : MeasureTheory.Measure T} [MeasurableSingletonClass S] {κ : ProbabilityTheory.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} {κ : ProbabilityTheory.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} {κ : ProbabilityTheory.Kernel T S} [ProbabilityTheory.IsMarkovKernel κ] (hκ : κ.AEFiniteKernelSupport μ) : ProbabilityTheory.IsMarkovKernel hκ.mk

Equations

• ⋯ = ⋯

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} {κ : ProbabilityTheory.Kernel T S} [ProbabilityTheory.IsZeroOrMarkovKernel κ] (hκ : κ.AEFiniteKernelSupport μ) : ProbabilityTheory.IsZeroOrMarkovKernel hκ.mk

Equations

• ⋯ = ⋯

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} {κ : ProbabilityTheory.Kernel T S} [ProbabilityTheory.IsSFiniteKernel κ] (hκ : κ.AEFiniteKernelSupport μ) : ProbabilityTheory.IsSFiniteKernel hκ.mk

Equations

• ⋯ = ⋯

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

theorem ProbabilityTheory.Kernel.local_support_of_finiteKernelSupport {S : Type u_2} {T : Type u_3} [MeasurableSpace S] [MeasurableSpace T] {κ : ProbabilityTheory.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] (κ : ProbabilityTheory.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) : (ProbabilityTheory.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] {κ : ProbabilityTheory.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] {κ : ProbabilityTheory.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] {κ : ProbabilityTheory.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] {κ : ProbabilityTheory.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] {κ : ProbabilityTheory.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] {κ : ProbabilityTheory.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] {κ : ProbabilityTheory.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] {κ : ProbabilityTheory.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] {κ : ProbabilityTheory.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 μ) [ProbabilityTheory.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] {κ : ProbabilityTheory.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] {κ : ProbabilityTheory.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] {κ : ProbabilityTheory.Kernel T S} {η : ProbabilityTheory.Kernel T U} [MeasurableSingletonClass S] [MeasurableSingletonClass U] [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.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] {κ : ProbabilityTheory.Kernel T S} {η : ProbabilityTheory.Kernel T U} [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.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] {κ : ProbabilityTheory.Kernel T S} {η : ProbabilityTheory.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] {κ : ProbabilityTheory.Kernel T S} {η : ProbabilityTheory.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] {κ : ProbabilityTheory.Kernel T S} (hκ : κ.FiniteKernelSupport) : (ProbabilityTheory.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} {κ : ProbabilityTheory.Kernel T S} (hκ : κ.AEFiniteKernelSupport μ) (ν : MeasureTheory.Measure U) [MeasureTheory.SFinite ν] : (ProbabilityTheory.Kernel.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] {κ : ProbabilityTheory.Kernel T S} (hκ : κ.FiniteKernelSupport) : (ProbabilityTheory.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} {κ : ProbabilityTheory.Kernel T S} (hκ : κ.AEFiniteKernelSupport μ) (ν : MeasureTheory.Measure U) [MeasureTheory.SFinite μ] : (ProbabilityTheory.Kernel.prodMkLeft U κ).AEFiniteKernelSupport (ν.prod μ)