Marginals of a joint pushed through a parallel composition #
Pushing a product measure through η ∥ₖ η' pushes each factor through its kernel. Pushing a
joint measure on α × β through Kernel.id ∥ₖ η keeps the first marginal and composes the
second with η. The joint is disintegrated as ρ.fst ⊗ₘ ρ.condKernel. Conditioning a joint
μ ⊗ₘ κ on an event and keeping the first coordinate reweights μ by the mass each row of κ
gives the event's section, and normalizes. On finite types, a
composition, a composition-product and a joint pushed through Kernel.id ∥ₖ η are computed at
atoms; an atom is charged by a composition exactly when some charged atom of the input emits it,
and each row of a kernel charged by the input measure is absolutely continuous with respect to the
output marginal. The powers of a Markov kernel, in mathlib's monoid of kernels under composition,
are Markov kernels.
[UPSTREAM] candidate for Mathlib/Probability/Kernel/Composition/Lemmas.lean.
theorem
MeasureTheory.Measure.parallelComp_comp_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSpace δ]
(η : ProbabilityTheory.Kernel α γ)
[ProbabilityTheory.IsSFiniteKernel η]
(η' : ProbabilityTheory.Kernel β δ)
[ProbabilityTheory.IsSFiniteKernel η']
(μ : Measure α)
[SFinite μ]
(ν : Measure β)
[SFinite ν]
:
(μ.prod ν).bind ⇑(η.parallelComp η') = (μ.bind ⇑η).prod (ν.bind ⇑η')
theorem
MeasureTheory.Measure.fst_parallelComp_id_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(η : ProbabilityTheory.Kernel β γ)
[ProbabilityTheory.IsMarkovKernel η]
[StandardBorelSpace β]
[Nonempty β]
(ρ : Measure (α × β))
[IsFiniteMeasure ρ]
:
(ρ.bind ⇑(ProbabilityTheory.Kernel.id.parallelComp η)).fst = ρ.fst
theorem
MeasureTheory.Measure.snd_parallelComp_id_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(η : ProbabilityTheory.Kernel β γ)
[ProbabilityTheory.IsMarkovKernel η]
[StandardBorelSpace β]
[Nonempty β]
(ρ : Measure (α × β))
[IsFiniteMeasure ρ]
:
(ρ.bind ⇑(ProbabilityTheory.Kernel.id.parallelComp η)).snd = ρ.snd.bind ⇑η
Atoms #
theorem
MeasureTheory.Measure.comp_apply_singleton_ne_zero
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass β]
(κ : ProbabilityTheory.Kernel α β)
(μ : Measure α)
{a : α}
{b : β}
(hμ : μ {a} ≠ 0)
(hκ : (κ a) {b} ≠ 0)
:
(μ.bind ⇑κ) {b} ≠ 0
theorem
MeasureTheory.Measure.comp_apply_singleton
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass α]
[MeasurableSingletonClass β]
[Fintype α]
(κ : ProbabilityTheory.Kernel α β)
(μ : Measure α)
(b : β)
:
(μ.bind ⇑κ) {b} = ∑ a : α, μ {a} * (κ a) {b}
theorem
MeasureTheory.Measure.comp_apply_singleton_ne_zero_iff
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass α]
[MeasurableSingletonClass β]
[Fintype α]
(κ : ProbabilityTheory.Kernel α β)
(μ : Measure α)
{b : β}
:
(μ.bind ⇑κ) {b} ≠ 0 ↔ ∃ (a : α), μ {a} ≠ 0 ∧ (κ a) {b} ≠ 0
theorem
MeasureTheory.Measure.comp_real_singleton
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass α]
[MeasurableSingletonClass β]
[Fintype α]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
(μ : Measure α)
[IsFiniteMeasure μ]
(b : β)
:
(μ.bind ⇑κ).real {b} = ∑ a : α, μ.real {a} * (κ a).real {b}
theorem
MeasureTheory.Measure.comp_real_singleton_eq_integral
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass α]
[MeasurableSingletonClass β]
[Fintype α]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
(μ : Measure α)
[IsFiniteMeasure μ]
(b : β)
:
(μ.bind ⇑κ).real {b} = ∫ (a : α), (κ a).real {b} ∂μ
theorem
MeasureTheory.Measure.compProd_apply_singleton
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass α]
[MeasurableSingletonClass β]
(μ : Measure α)
[SFinite μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
(a : α)
(b : β)
:
(μ.compProd κ) {(a, b)} = μ {a} * (κ a) {b}
theorem
MeasureTheory.Measure.compProd_real_singleton
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass α]
[MeasurableSingletonClass β]
(μ : Measure α)
[IsFiniteMeasure μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
(a : α)
(b : β)
:
(μ.compProd κ).real {(a, b)} = μ.real {a} * (κ a).real {b}
theorem
MeasureTheory.Measure.parallelComp_id_comp_apply_singleton
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSingletonClass α]
[MeasurableSingletonClass β]
[Fintype α]
[Fintype β]
[MeasurableSingletonClass γ]
(ρ : Measure (α × β))
(η : ProbabilityTheory.Kernel β γ)
[ProbabilityTheory.IsSFiniteKernel η]
(a : α)
(c : γ)
:
(ρ.bind ⇑(ProbabilityTheory.Kernel.id.parallelComp η)) {(a, c)} = ∑ b : β, ρ {(a, b)} * (η b) {c}
theorem
MeasureTheory.Measure.parallelComp_id_comp_real_singleton
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSingletonClass α]
[MeasurableSingletonClass β]
[Fintype α]
[Fintype β]
[MeasurableSingletonClass γ]
(ρ : Measure (α × β))
[IsFiniteMeasure ρ]
(η : ProbabilityTheory.Kernel β γ)
[ProbabilityTheory.IsFiniteKernel η]
(a : α)
(c : γ)
:
(ρ.bind ⇑(ProbabilityTheory.Kernel.id.parallelComp η)).real {(a, c)} = ∑ b : β, ρ.real {(a, b)} * (η b).real {c}
Conditioning on an event #
theorem
MeasureTheory.Measure.fst_restrict_compProd
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(μ : Measure α)
[SFinite μ]
{s : Set (α × β)}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
(hs : MeasurableSet s)
:
((μ.compProd κ).restrict s).fst = μ.withDensity fun (a : α) => (κ a) (Prod.mk a ⁻¹' s)
theorem
MeasureTheory.Measure.fst_cond_compProd
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(μ : Measure α)
[SFinite μ]
{s : Set (α × β)}
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsSFiniteKernel κ]
(hs : MeasurableSet s)
:
(μ.compProd κ)[|s].fst = (μ.withDensity fun (a : α) => (κ a) (Prod.mk a ⁻¹' s))[|Set.univ]
Conditioning a joint on an event and keeping the first coordinate reweights the first marginal by the mass each row gives the event's section, and normalizes.
theorem
MeasureTheory.Measure.fst_cond_prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(μ : Measure α)
[SFinite μ]
{s : Set (α × β)}
(ν : Measure β)
[SFinite ν]
(hs : MeasurableSet s)
:
(μ.prod ν)[|s].fst = (μ.withDensity fun (a : α) => ν (Prod.mk a ⁻¹' s))[|Set.univ]
theorem
MeasureTheory.Measure.integral_compProd_eq_sum
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[Fintype α]
[MeasurableSingletonClass α]
[Fintype β]
[MeasurableSingletonClass β]
(μ : Measure α)
[IsFiniteMeasure μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(f : α × β → E)
:
∫ (z : α × β), f z ∂μ.compProd κ = ∑ a : α, μ.real {a} • ∫ (b : β), f (a, b) ∂κ a
theorem
MeasureTheory.Measure.map_snd_cond_fst_compProd
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[Fintype α]
[MeasurableSingletonClass α]
[Fintype β]
[MeasurableSingletonClass β]
(μ : Measure α)
[IsFiniteMeasure μ]
(κ : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsMarkovKernel κ]
{a : α}
(ha : μ {a} ≠ 0)
:
theorem
ProbabilityTheory.Kernel.mul_def
{α : Type u_1}
[MeasurableSpace α]
(κ η : Kernel α α)
:
κ * η = κ.comp η
instance
ProbabilityTheory.Kernel.IsMarkovKernel.pow
{α : Type u_1}
[MeasurableSpace α]
(κ : Kernel α α)
[IsMarkovKernel κ]
(n : ℕ)
:
IsMarkovKernel (κ ^ n)
The powers of a Markov kernel are Markov kernels.
theorem
ProbabilityTheory.Kernel.comp_apply_singleton
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[Fintype β]
[MeasurableSingletonClass β]
[MeasurableSingletonClass γ]
(η : Kernel β γ)
(κ : Kernel α β)
(a : α)
(c : γ)
:
((η.comp κ) a) {c} = ∑ b : β, (κ a) {b} * (η b) {c}
theorem
ProbabilityTheory.Kernel.comp_apply_singleton_ne_zero_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[Fintype β]
[MeasurableSingletonClass β]
[MeasurableSingletonClass γ]
(η : Kernel β γ)
(κ : Kernel α β)
{a : α}
{c : γ}
:
((η.comp κ) a) {c} ≠ 0 ↔ ∃ (b : β), (κ a) {b} ≠ 0 ∧ (η b) {c} ≠ 0
theorem
ProbabilityTheory.Kernel.comp_real_singleton
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[Fintype β]
[MeasurableSingletonClass β]
[MeasurableSingletonClass γ]
(η : Kernel β γ)
[IsFiniteKernel η]
(κ : Kernel α β)
[IsFiniteKernel κ]
(a : α)
(c : γ)
:
((η.comp κ) a).real {c} = ∑ b : β, (κ a).real {b} * (η b).real {c}
theorem
ProbabilityTheory.Kernel.absolutelyContinuous_comp
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
[Fintype α]
[MeasurableSingletonClass α]
(κ : Kernel α β)
(μ : MeasureTheory.Measure α)
{a : α}
(ha : μ {a} ≠ 0)
:
(κ a).AbsolutelyContinuous (μ.bind ⇑κ)