Mathlib.Probability.Kernel

Kernel-measure probability helpers: graph-map product identities and composition-product assembly lemmas for conditional-law arguments.

CompProdAssembly 2 core · 1 supporting This file packages recurring measure-kernel assembly steps for composition products. ★ compProd_eq_of_inner_ae_kernel★ compProd_eq_of_inner_ae

Composition-product assembly lemmas

This file packages recurring measure-kernel assembly steps for composition products. The main lemmas turn an almost-everywhere equality of inner kernels on a product space into equality of the resulting outer composition products:

* compProd_eq_of_inner_ae: the inner kernels are mixed against a fixed s-finite measure; * compProd_eq_of_inner_ae_kernel: the inner kernels are mixed against an indexed s-finite kernel; * compProd_map_snd_apply: the second-coordinate marginal of a kernel composition product is the bind of the section of the inner kernel against the outer kernel value.

These results isolate the Fubini-style steps that otherwise require repeating Measure.ext_prod, compProd_apply_prod, ae_ae_of_ae_compProd, and lintegral_congr_ae.

theorem compProd_eq_of_inner_ae_kernel reviewed

Causalean.Mathlib.CompProdAssembly

CompProd assembly from an a.e. inner equality, indexed-integrator form. Consider two Markov-style kernels KL, KR from a base space to an outer space, each built by mixing the section at a base point of an inner kernel — fL, respectively fR, on the product of the base space and an intermediate space — against a fixed intermediate kernel κ evaluated at that point: KL a equals the section fL(a,·) composed with κ a and KR a equals the section fR(a,·) composed with κ a. If the inner kernels fL and fR agree almost everywhere with respect to the composition product of the base measure ν and κ, then the composition products ν ⊗ₘ KL and ν ⊗ₘ KR are equal.

Formal statement

hypotheses

α γ β :

Type*

MeasurableSpace α

MeasurableSpace γ

MeasurableSpace β

ν :

Measure α

IsFiniteMeasure ν

κ :

Kernel α γ

IsSFiniteKernel κ

KL KR :

Kernel α β

IsFiniteKernel KL

IsSFiniteKernel KR

fL fR :

Kernel (α × γ) β

hL :

∀ a, KL a = (fL.sectR a) ∘ₘ κ a

hR :

∀ a, KR a = (fR.sectR a) ∘ₘ κ a

hae :

∀ᵐ p ∂(ν ⊗ₘ κ), fL p = fR p

conclusion

ν ⊗ₘ KL = ν ⊗ₘ KR

Proof (Lean source)

theorem compProd_eq_of_inner_ae_kernel {α γ β : Type*} [MeasurableSpace α] [MeasurableSpace γ] [MeasurableSpace β] (ν : Measure α) [IsFiniteMeasure ν] (κ : Kernel α γ) [IsSFiniteKernel κ] (KL KR : Kernel α β) [IsFiniteKernel KL] [IsSFiniteKernel KR] (fL fR : Kernel (α × γ) β) (hL : ∀ a, KL a = (fL.sectR a) ∘ₘ κ a) (hR : ∀ a, KR a = (fR.sectR a) ∘ₘ κ a) (hae : ∀ᵐ p ∂(ν ⊗ₘ κ), fL p = fR p) : ν ⊗ₘ KL = ν ⊗ₘ KR := by refine MeasureTheory.Measure.ext_prod (fun {A B} hA hB => ?_) rw [MeasureTheory.Measure.compProd_apply_prod hA hB, MeasureTheory.Measure.compProd_apply_prod hA hB] have hInnerL : ∀ a, (KL a) B = ∫⁻ c, (fL (a, c)) B ∂(κ a) := by intro a rw [hL a, MeasureTheory.Measure.bind_apply hB (ProbabilityTheory.Kernel.aemeasurable _)] simp only [ProbabilityTheory.Kernel.sectR_apply] have hInnerR : ∀ a, (KR a) B = ∫⁻ c, (fR (a, c)) B ∂(κ a) := by intro a rw [hR a, MeasureTheory.Measure.bind_apply hB (ProbabilityTheory.Kernel.aemeasurable _)] simp only [ProbabilityTheory.Kernel.sectR_apply] simp only [hInnerL, hInnerR] have hae' := MeasureTheory.Measure.ae_ae_of_ae_compProd hae have hInnerAE : ∀ᵐ a ∂ν, (∫⁻ c, (fL (a, c)) B ∂(κ a)) = ∫⁻ c, (fR (a, c)) B ∂(κ a) := by filter_upwards [hae'] with a ha refine MeasureTheory.lintegral_congr_ae ?_ filter_upwards [ha] with c hc rw [hc] exact MeasureTheory.lintegral_congr_ae (MeasureTheory.ae_restrict_of_ae hInnerAE)

Causalean.Mathlib.CompProdAssembly.compProd_eq_of_inner_ae_kernel · Causalean/Mathlib/Probability/Kernel/CompProdAssembly.lean:33

theorem compProd_eq_of_inner_ae reviewed

Causalean.Mathlib.CompProdAssembly

CompProd assembly from an a.e. inner equality. Consider two Markov-style kernels KL, KR from a base space to an outer space, each built by mixing the section at a base point of an inner kernel — fL, respectively fR, on the product of the base space and an intermediate space — against a fixed intermediate measure μ: KL a equals the section fL(a,·) composed with μ and KR a equals the section fR(a,·) composed with μ. If the inner kernels fL and fR agree almost everywhere with respect to the composition product of the base measure ν with the constant-μ kernel, then the composition products ν ⊗ₘ KL and ν ⊗ₘ KR are equal.

Formal statement

hypotheses

α γ β :

Type*

MeasurableSpace α

MeasurableSpace γ

MeasurableSpace β

ν :

Measure α

IsFiniteMeasure ν

μ :

Measure γ

SFinite μ

KL KR :

Kernel α β

IsFiniteKernel KL

IsSFiniteKernel KR

fL fR :

Kernel (α × γ) β

hL :

∀ a, KL a = (fL.sectR a) ∘ₘ μ

hR :

∀ a, KR a = (fR.sectR a) ∘ₘ μ

hae :

∀ᵐ p ∂(ν ⊗ₘ Kernel.const α μ), fL p = fR p

conclusion

ν ⊗ₘ KL = ν ⊗ₘ KR

Proof (Lean source)

theorem compProd_eq_of_inner_ae {α γ β : Type*} [MeasurableSpace α] [MeasurableSpace γ] [MeasurableSpace β] (ν : Measure α) [IsFiniteMeasure ν] (μ : Measure γ) [SFinite μ] (KL KR : Kernel α β) [IsFiniteKernel KL] [IsSFiniteKernel KR] (fL fR : Kernel (α × γ) β) (hL : ∀ a, KL a = (fL.sectR a) ∘ₘ μ) (hR : ∀ a, KR a = (fR.sectR a) ∘ₘ μ) (hae : ∀ᵐ p ∂(ν ⊗ₘ Kernel.const α μ), fL p = fR p) : ν ⊗ₘ KL = ν ⊗ₘ KR := by refine compProd_eq_of_inner_ae_kernel ν (Kernel.const α μ) KL KR fL fR ?_ ?_ hae · simpa only [Kernel.const_apply] using hL · simpa only [Kernel.const_apply] using hR

Causalean.Mathlib.CompProdAssembly.compProd_eq_of_inner_ae · Causalean/Mathlib/Probability/Kernel/CompProdAssembly.lean:77

1 supporting declaration (lemmas, instances)

compProd_map_snd_apply theorem — Snd-marginal of a composition product, pointwise (disintegration backbone).

hypotheses

α β γ :

Type*
MeasurableSpace α
MeasurableSpace β
MeasurableSpace γ

κ₁ :

Kernel α β

κ₂ :

Kernel (α × β) γ

IsSFiniteKernel κ₁

IsSFiniteKernel κ₂

a :

α

conclusion

((κ₁ ⊗ₖ κ₂).map snd) a = (κ₂.sectR a) ∘ₘ (κ₁ a)

Proof (Lean source)

theorem compProd_map_snd_apply {α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (κ₁ : Kernel α β) (κ₂ : Kernel (α × β) γ) [IsSFiniteKernel κ₁] [IsSFiniteKernel κ₂] (a : α) : ((κ₁ ⊗ₖ κ₂).map snd) a = (κ₂.sectR a) ∘ₘ (κ₁ a) := by rw [Kernel.map_apply _ measurable_snd, Kernel.compProd_apply_eq_compProd_sectR, ← Measure.snd, Measure.snd_compProd]

Causalean.Mathlib.CompProdAssembly.compProd_map_snd_apply · Causalean/Mathlib/Probability/Kernel/CompProdAssembly.lean:98

GraphMapProd 2 core · 2 supporting If νₗ is an s-finite measure on γ and Φ : β × γ → δ is measurable, then pushing a product measure α ⊗ νₗ forward along the *graph map* (o, l) ↦ (o, Φ (o, l)) produces a composition product α.compProd κ, where the disinte ★ map_graph_prod_eq_compProd

The graph push-forward of a product measure is a composition product

If νₗ is an s-finite measure on γ and Φ : β × γ → δ is measurable, then pushing a product measure α ⊗ νₗ forward along the graph map (o, l) ↦ (o, Φ (o, l)) produces a composition product α.compProd κ, where the disintegration kernel κ o = νₗ.map (fun l => Φ (o, l)) reads the first coordinate as a parameter and pushes the γ-marginal through the slice of Φ.

This is the abstract measure-theoretic core of "exogenous noise plus a structural mechanism gives an environment-invariant conditional law": the predictor marginal is α, the exogenous-noise law is νₗ, the mechanism is Φ, and the resulting conditional law of the response given the predictor is the kernel κ.

def mechanismKernel reviewed

Causalean.Mathlib.GraphMapProd

The structural-mechanism kernel κ o = νₗ.map (Φ (o, ·)): at each value o of the first coordinate, push the γ-marginal νₗ through the slice l ↦ Φ (o, l). Built as the deterministic-times-constant product kernel (Kernel.id ×ₖ Kernel.const β νₗ) mapped through Φ.

Definition (Lean source)

noncomputable def mechanismKernel (νₗ : Measure γ) (Φ : β × γ → δ) : Kernel β δ := ((ProbabilityTheory.Kernel.id : Kernel β β).prod (const β νₗ)).map Φ

Causalean.Mathlib.GraphMapProd.mechanismKernel · Causalean/Mathlib/Probability/Kernel/GraphMapProd.lean:34

theorem map_graph_prod_eq_compProd reviewed

Causalean.Mathlib.GraphMapProd

Graph push-forward of a product measure is a composition product. For an s-finite measure α on a first factor, an s-finite measure νₗ on a second factor, and a measurable mechanism map Φ combining the two factors into a third space, pushing the product measure α.prod νₗ forward along the graph map (o, l) ↦ (o, Φ (o, l)) equals the composition product of α with the mechanism kernel that sends each value o of the first coordinate to the pushforward of νₗ through the slice l ↦ Φ (o, l).

Formal statement

hypotheses

α :

Measure β

SFinite α

νₗ :

Measure γ

SFinite νₗ

Φ :

β × γ → δ

hΦ :

Measurable Φ

conclusion

Measure.map (fun p : β × γ => (p.1, Φ p)) (α.prod νₗ) = α.compProd (mechanismKernel νₗ Φ)

Proof (Lean source)

theorem map_graph_prod_eq_compProd (α : Measure β) [SFinite α] (νₗ : Measure γ) [SFinite νₗ] {Φ : β × γ → δ} (hΦ : Measurable Φ) : Measure.map (fun p : β × γ => (p.1, Φ p)) (α.prod νₗ) = α.compProd (mechanismKernel νₗ Φ) := by -- `mechanismKernel = η.map Φ` with `η = Kernel.id ×ₖ Kernel.const β νₗ`. set η : Kernel β (β × γ) := (ProbabilityTheory.Kernel.id : Kernel β β).prod (const β νₗ) with hη have hΦ' : Measurable (fun p : β × γ => (p.1, Φ p)) := measurable_fst.prodMk hΦ -- Step 1: `α.compProd (η.map Φ) = map (map id Φ) (α.compProd η)`. have h1 : α.compProd (mechanismKernel νₗ Φ) = Measure.map (map id Φ) (α.compProd η) := by unfold mechanismKernel rw [← hη] exact MeasureTheory.Measure.compProd_map (μ := α) (κ := η) hΦ -- Step 2: `α.compProd η = map (fun o => (o, (o, ·)))`-style; concretely -- `α.compProd (id ×ₖ const νₗ) = map (fun p => (p.1, (p.1, p.2))) (α.prod νₗ)`. have h2 : α.compProd η = Measure.map (fun p : β × γ => (p.1, (p.1, p.2))) (α.prod νₗ) := by ext s hs rw [MeasureTheory.Measure.compProd_apply hs, MeasureTheory.Measure.map_apply ((measurable_fst.prodMk (measurable_fst.prodMk measurable_snd))) hs] rw [MeasureTheory.Measure.prod_apply (measurable_fst.prodMk (measurable_fst.prodMk measurable_snd) hs)] apply MeasureTheory.lintegral_congr intro o rw [hη, ProbabilityTheory.Kernel.prod_apply, ProbabilityTheory.Kernel.id_apply, ProbabilityTheory.Kernel.const_apply, MeasureTheory.Measure.dirac_prod] rw [MeasureTheory.Measure.map_apply measurable_prodMk_left (measurable_prodMk_left hs)] congr 1 -- Step 3: combine. `(map id Φ) ∘ (fun p => (p.1, p.1, p.2)) = fun p => (p.1, Φ p)`. rw [h1, h2, MeasureTheory.Measure.map_map (by fun_prop) (by fun_prop)] rfl

Causalean.Mathlib.GraphMapProd.map_graph_prod_eq_compProd · Causalean/Mathlib/Probability/Kernel/GraphMapProd.lean:68 · uses mechanismKernel

2 supporting declarations (lemmas, instances)

mechanismKernel_apply theorem — Pointwise value of mechanismKernel: κ o = νₗ.map (fun l => Φ (o, l)).

hypotheses

νₗ :

Measure γ
SFinite νₗ

Φ :

β × γ → δ

hΦ :

Measurable Φ

o :

β

conclusion

mechanismKernel νₗ Φ o = νₗ.map (fun l => Φ (o, l))

Proof (Lean source)

theorem mechanismKernel_apply (νₗ : Measure γ) [SFinite νₗ] {Φ : β × γ → δ} (hΦ : Measurable Φ) (o : β) : mechanismKernel νₗ Φ o = νₗ.map (fun l => Φ (o, l)) := by unfold mechanismKernel rw [ProbabilityTheory.Kernel.map_apply _ hΦ, ProbabilityTheory.Kernel.prod_apply, ProbabilityTheory.Kernel.id_apply, ProbabilityTheory.Kernel.const_apply, MeasureTheory.Measure.dirac_prod, MeasureTheory.Measure.map_map hΦ measurable_prodMk_left] rfl

Causalean.Mathlib.GraphMapProd.mechanismKernel_apply · Causalean/Mathlib/Probability/Kernel/GraphMapProd.lean:43
instIsMarkovKernelMechanismKernel theorem — The mechanism kernel is Markov when the exogenous-noise law is a probability measure and the mechanism is measurable.

hypotheses

νₗ :

Measure γ
IsProbabilityMeasure νₗ

Φ :

β × γ → δ

hΦ :

Measurable Φ

conclusion

IsMarkovKernel (mechanismKernel νₗ Φ)

Proof (Lean source)

theorem instIsMarkovKernelMechanismKernel (νₗ : Measure γ) [IsProbabilityMeasure νₗ] {Φ : β × γ → δ} (hΦ : Measurable Φ) : IsMarkovKernel (mechanismKernel νₗ Φ) := by unfold mechanismKernel exact ProbabilityTheory.Kernel.IsMarkovKernel.map _ hΦ

Causalean.Mathlib.GraphMapProd.instIsMarkovKernelMechanismKernel · Causalean/Mathlib/Probability/Kernel/GraphMapProd.lean:55

ProductCondDistrib 2 core · 0 supporting Let ρ be a finite base measure on α, and let κ : Kernel α β and η : Kernel α γ be Markov kernels. ★ condDistrib_fst_of_compProd_prod★ condDistrib_snd_of_compProd_prod

Conditional distributions for product kernels

Let ρ be a finite base measure on α, and let κ : Kernel α β and η : Kernel α γ be Markov kernels. After sampling (B, C) from the product kernel Kernel.prod κ η over the base coordinate, the conditional distribution of B given the base coordinate is κ, and the conditional distribution of C given the base coordinate is η.

The public theorems condDistrib_fst_of_compProd_prod and condDistrib_snd_of_compProd_prod record these two coordinate conditionals for Measure.compProd ρ (Kernel.prod κ η).

theorem condDistrib_fst_of_compProd_prod reviewed

Causalean.Mathlib.ProbabilityTheory.ProductCondDistrib

For the joint law formed by combining a finite base measure ρ with the product of two Markov kernels κ and η, the conditional distribution of the first product-kernel coordinate given the base coordinate equals κ, for ρ-almost every base point.

Formal statement

hypotheses

StandardBorelSpace β

Nonempty β

ρ :

Measure α

IsFiniteMeasure ρ

κ :

Kernel α β

η :

Kernel α γ

IsMarkovKernel κ

IsMarkovKernel η

conclusion

(condDistrib (Y := fun z : α × (β × γ) => z.2.1) (X := fun z : α × (β × γ) => z.1) (μ := Measure.compProd ρ (prod κ η)))

=ᵐ[ρ] κ

Proof (Lean source)

theorem condDistrib_fst_of_compProd_prod [StandardBorelSpace β] [Nonempty β] {ρ : Measure α} [IsFiniteMeasure ρ] (κ : Kernel α β) (η : Kernel α γ) [IsMarkovKernel κ] [IsMarkovKernel η] : (condDistrib (Y := fun z : α × (β × γ) => z.2.1) (X := fun z : α × (β × γ) => z.1) (μ := Measure.compProd ρ (prod κ η))) =ᵐ[ρ] κ := by have hX : Measurable (fun z : α × (β × γ) => z.1) := measurable_fst have hY : Measurable (fun z : α × (β × γ) => z.2.1) := measurable_fst.comp measurable_snd have hbase : (Measure.compProd ρ (prod κ η)).map (fun z : α × (β × γ) => z.1) = ρ := by simpa [Measure.fst] using (Measure.fst_compProd ρ (prod κ η)) have hfst : (prod κ η).map fst = κ := by simpa [ProbabilityTheory.Kernel.fst_eq] using (ProbabilityTheory.Kernel.fst_prod κ η) have hjoint : (Measure.compProd ρ (prod κ η)).map (fun z : α × (β × γ) => (z.1, z.2.1)) = Measure.compProd ρ κ := by calc (Measure.compProd ρ (prod κ η)).map (fun z : α × (β × γ) => (z.1, z.2.1)) = (Measure.compProd ρ (prod κ η)).map (map id fst) := by rfl _ = Measure.compProd ρ ((prod κ η).map fst) := by rw [← Measure.compProd_map (μ := ρ) (κ := prod κ η) measurable_fst] _ = Measure.compProd ρ κ := by rw [hfst] have h := ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable (μ := Measure.compProd ρ (prod κ η)) hX hY (κ := κ) (by simpa [hbase] using hjoint) rwa [hbase] at h

Causalean.Mathlib.ProbabilityTheory.ProductCondDistrib.condDistrib_fst_of_compProd_prod · Causalean/Mathlib/Probability/Kernel/ProductCondDistrib.lean:31

theorem condDistrib_snd_of_compProd_prod reviewed

Causalean.Mathlib.ProbabilityTheory.ProductCondDistrib

For the joint law formed by combining a finite base measure ρ with the product of two Markov kernels κ and η, the conditional distribution of the second product-kernel coordinate given the base coordinate equals η, for ρ-almost every base point.

Formal statement

hypotheses

StandardBorelSpace γ

Nonempty γ

ρ :

Measure α

IsFiniteMeasure ρ

κ :

Kernel α β

η :

Kernel α γ

IsMarkovKernel κ

IsMarkovKernel η

conclusion

(condDistrib (Y := fun z : α × (β × γ) => z.2.2) (X := fun z : α × (β × γ) => z.1) (μ := Measure.compProd ρ (prod κ η)))

=ᵐ[ρ] η

Proof (Lean source)

theorem condDistrib_snd_of_compProd_prod [StandardBorelSpace γ] [Nonempty γ] {ρ : Measure α} [IsFiniteMeasure ρ] (κ : Kernel α β) (η : Kernel α γ) [IsMarkovKernel κ] [IsMarkovKernel η] : (condDistrib (Y := fun z : α × (β × γ) => z.2.2) (X := fun z : α × (β × γ) => z.1) (μ := Measure.compProd ρ (prod κ η))) =ᵐ[ρ] η := by have hX : Measurable (fun z : α × (β × γ) => z.1) := measurable_fst have hY : Measurable (fun z : α × (β × γ) => z.2.2) := measurable_snd.comp measurable_snd have hbase : (Measure.compProd ρ (prod κ η)).map (fun z : α × (β × γ) => z.1) = ρ := by simpa [Measure.fst] using (Measure.fst_compProd ρ (prod κ η)) have hsnd : (prod κ η).map snd = η := by simpa [ProbabilityTheory.Kernel.snd_eq] using (ProbabilityTheory.Kernel.snd_prod κ η) have hjoint : (Measure.compProd ρ (prod κ η)).map (fun z : α × (β × γ) => (z.1, z.2.2)) = Measure.compProd ρ η := by calc (Measure.compProd ρ (prod κ η)).map (fun z : α × (β × γ) => (z.1, z.2.2)) = (Measure.compProd ρ (prod κ η)).map (map id snd) := by rfl _ = Measure.compProd ρ ((prod κ η).map snd) := by rw [← Measure.compProd_map (μ := ρ) (κ := prod κ η) measurable_snd] _ = Measure.compProd ρ η := by rw [hsnd] have h := ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable (μ := Measure.compProd ρ (prod κ η)) hX hY (κ := η) (by simpa [hbase] using hjoint) rwa [hbase] at h

Causalean.Mathlib.ProbabilityTheory.ProductCondDistrib.condDistrib_snd_of_compProd_prod · Causalean/Mathlib/Probability/Kernel/ProductCondDistrib.lean:74