Mathlib.Probability.Kernel
Kernel-measure probability helpers: graph-map product identities and composition-product assembly lemmas for conditional-law arguments.
FiniteHistory 7 core · 13 supporting · 3 submodules This module packages reusable expectation, likelihood-weighted iteration, and stationary separated-window covariance formulas for finite trajectory laws specified directly by composition-product identities. FiniteSequence 15 core · 14 supporting · 5 submodules This module bundles dependent finite transcript histories, sequential-kernel laws, their prefix and next-step identities, and exact singleton factorization. ThreeBernoulli 37 core · 27 supporting · 6 submodules This module bundles the finite-density construction of three conditionally independent Boolean marks over a base probability law, together with its base marginal, conditional-independence, selected-mark, and cell-integra
Kernel 1 core · 0 supporting Probability-kernel constructions for conditional distributions, product composition, graph-based maps, Bernoulli marks, and quantile realizations. ★ kernel_apply_univ
Probability-kernel constructions for conditional distributions, product composition, graph-based maps, Bernoulli marks, and quantile realizations. These tools build and compare stochastic mechanisms with explicit conditioning structure.
theorem kernel_apply_univ reviewed
⚑ flagged
Causalean.Mathlib.Probability
For measurable spaces, a Markov kernel κ, and a source point a, the kernel slice has total mass one.
Formal statement
hypotheses
conclusion
κ a univ = 1
Proof (Lean source)
theorem kernel_apply_univ {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
(κ : Kernel α β) [IsMarkovKernel κ] (a : α) :
κ a univ = 1 :=
MeasureTheory.measure_univ
BernoulliMark 6 core · 9 supporting This file constructs a measurable Boolean Bernoulli mark over a base space and proves the measure identities behind reciprocal-probability tilting. ★ bernoulliMarkedLaw_restrict_true_map_fst★ bernoulliMarkedLaw_restrict_false_map_fst★ bernoulliMarkedLaw_condExp_mark
Reciprocal tilts with Bernoulli marks
This file constructs a measurable Boolean Bernoulli mark over a base space and proves the measure identities behind reciprocal-probability tilting. The first marginal is the tilted base law, the success and failure restrictions recover their density formulas, the mark has the prescribed conditional mean, and measurable pushforwards of the success restriction are transported back to the original base law.
def bernoulliMarkKernel reviewed
⚑ flagged
Causalean.Mathlib.Probability
Given a real-valued weight on a measurable space, the Boolean Bernoulli-mark kernel has success weight max(h(a), 0) and failure weight max(1-h(a), 0) at a. For measurable unit-interval weights its fibers are Bernoulli probability measures.
def reciprocalTilt reviewed
⚑ flagged
Causalean.Mathlib.Probability
For a base measure and a real-valued weight, the reciprocal tilt weights each base point by max(1/h, 0).
Definition (Lean source)
def bernoulliMarkedLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability
For a base measure and a real-valued mark probability, the reciprocally tilted Bernoulli-marked law first draws from the reciprocal tilt and then draws the Boolean mark with success weight h.
Definition (Lean source)
parameters
given by
reciprocalTilt ν₁ h ⊗ₘ bernoulliMarkKernel h
theorem bernoulliMarkedLaw_restrict_true_map_fst reviewed
⚑ flagged
Causalean.Mathlib.Probability
For a finite base measure, a measurable success weight, and strict positivity almost everywhere, restricting the marked law to successful marks and then forgetting the mark recovers the base measure.
Formal statement
hypotheses
α :
Type*
ν₁ :
h :
α → ℝ
hh :
hpos :
∀ᵐ a ∂ν₁, 0 < h a
conclusion
Proof (Lean source)
theorem bernoulliMarkedLaw_restrict_true_map_fst
{α : Type*} [MeasurableSpace α] (ν₁ : Measure α) [IsFiniteMeasure ν₁]
(h : α → ℝ) (hh : Measurable h)
(hpos : ∀ᵐ a ∂ν₁, 0 < h a) :
((bernoulliMarkedLaw ν₁ h).restrict (univ ×ˢ {true})).map fst = ν₁ := by
have hcancel :=
withDensity_one_div_ofReal_cancel ν₁ h hh hpos
ext s hs
rw [Measure.map_apply measurable_fst hs, Measure.restrict_apply (measurable_fst hs)]
rw [show fst ⁻¹' s ∩ univ ×ˢ {true} = s ×ˢ {true} by ext p; simp]
rw [bernoulliMarkedLaw, Measure.compProd_apply_prod hs (measurableSet_singleton true)]
simp_rw [bernoulliMarkKernel_apply_true h hh]
rw [← withDensity_apply _ hs]
change ((ν₁.withDensity fun a => ofReal (1 / h a)).withDensity
(fun a => ofReal (h a))) s = ν₁ s
rw [hcancel]
theorem bernoulliMarkedLaw_restrict_false_map_fst reviewed
⚑ flagged
Causalean.Mathlib.Probability
For a finite base measure, a measurable success weight, and a positive success weight bounded above by one almost everywhere, restricting the marked law to failed marks and then forgetting the mark gives the base measure tilted by the failure odds (1-h)/h.
Formal statement
hypotheses
α :
Type*
ν₁ :
h :
α → ℝ
hh :
hpos :
∀ᵐ a ∂ν₁, 0 < h a
hle :
∀ᵐ a ∂ν₁, h a ≤ 1
Proof (Lean source)
theorem bernoulliMarkedLaw_restrict_false_map_fst
{α : Type*} [MeasurableSpace α] (ν₁ : Measure α) [IsFiniteMeasure ν₁]
(h : α → ℝ) (hh : Measurable h)
(hpos : ∀ᵐ a ∂ν₁, 0 < h a) (hle : ∀ᵐ a ∂ν₁, h a ≤ 1) :
((bernoulliMarkedLaw ν₁ h).restrict (univ ×ˢ {false})).map fst =
ν₁.withDensity (fun a => ofReal ((1 - h a) / h a)) := by
have hfailure :
(reciprocalTilt ν₁ h).withDensity (fun a => ofReal (1 - h a)) =
ν₁.withDensity (fun a => ofReal ((1 - h a) / h a)) := by
unfold reciprocalTilt
rw [← withDensity_mul ν₁ (by fun_prop) (by fun_prop)]
apply withDensity_congr_ae
filter_upwards [hpos, hle] with a ha h'a
simp only [Pi.mul_apply]
rw [← ENNReal.ofReal_mul (by positivity : 0 ≤ 1 / h a)]
congr 1
field_simp
ext s hs
rw [Measure.map_apply measurable_fst hs, Measure.restrict_apply (measurable_fst hs)]
rw [show fst ⁻¹' s ∩ univ ×ˢ {false} = s ×ˢ {false} by ext p; simp]
rw [bernoulliMarkedLaw, Measure.compProd_apply_prod hs (measurableSet_singleton false)]
simp_rw [bernoulliMarkKernel_apply_false h hh]
rw [← withDensity_apply _ hs, hfailure]
theorem bernoulliMarkedLaw_condExp_mark reviewed
⚑ flagged
Causalean.Mathlib.Probability
For a finite base measure, a measurable success weight, a positive success weight bounded above by one almost everywhere, and unit total mass of the reciprocal tilt, the conditional mean of the Boolean mark given the base coordinate equals the success weight at that coordinate.
Formal statement
hypotheses
α :
Type*
ν₁ :
h :
α → ℝ
hh :
hpos :
∀ᵐ a ∂ν₁, 0 < h a
hle :
∀ᵐ a ∂ν₁, h a ≤ 1
hcal :
reciprocalTilt ν₁ h univ = 1
conclusion
=ᵐ[bernoulliMarkedLaw ν₁ h] fun p => h p.1
Proof (Lean source)
theorem bernoulliMarkedLaw_condExp_mark
{α : Type*} [MeasurableSpace α] (ν₁ : Measure α) [IsFiniteMeasure ν₁]
(h : α → ℝ) (hh : Measurable h)
(hpos : ∀ᵐ a ∂ν₁, 0 < h a) (hle : ∀ᵐ a ∂ν₁, h a ≤ 1)
(hcal : reciprocalTilt ν₁ h univ = 1) :
(bernoulliMarkedLaw ν₁ h)[(fun p => if p.2 then (1 : ℝ) else 0) |
comap Prod.fst inferInstance] =ᵐ[bernoulliMarkedLaw ν₁ h]
fun p => h p.1 := by
let Q := bernoulliMarkedLaw ν₁ h
have hprob : IsProbabilityMeasure Q :=
bernoulliMarkedLaw_isProbabilityMeasure ν₁ h hh hpos hle hcal
let _ : IsProbabilityMeasure Q := hprob
have hmap : Q.map Prod.fst = reciprocalTilt ν₁ h :=
bernoulliMarkedLaw_map_fst ν₁ h hh hpos hle
have hac : reciprocalTilt ν₁ h ≪ ν₁ :=
withDensity_absolutelyContinuous ν₁ (fun a => ofReal (1 / h a))
have hpos_tilt : ∀ᵐ a ∂reciprocalTilt ν₁ h, 0 < h a := hac.ae_le hpos
have hle_tilt : ∀ᵐ a ∂reciprocalTilt ν₁ h, h a ≤ 1 := hac.ae_le hle
have hpos_Q : ∀ᵐ p ∂Q, 0 < h p.1 := by
rw [← hmap] at hpos_tilt
exact (ae_map_iff measurable_fst.aemeasurable
(measurableSet_lt measurable_const hh)).mp hpos_tilt
have hle_Q : ∀ᵐ p ∂Q, h p.1 ≤ 1 := by
rw [← hmap] at hle_tilt
exact (ae_map_iff measurable_fst.aemeasurable
(measurableSet_le hh measurable_const)).mp hle_tilt
have hY : Integrable (fun p : α × Bool => if p.2 then (1 : ℝ) else 0) Q := by
apply Integrable.of_bound
(Measurable.ite (measurable_snd (measurableSet_singleton true))
measurable_const measurable_const).aestronglyMeasurable 1
filter_upwards [] with p
cases p.2 <;> simp
have hm : Integrable (fun p : α × Bool => h p.1) Q := by
apply Integrable.of_bound (hh.comp measurable_fst).aestronglyMeasurable 1
filter_upwards [hpos_Q, hle_Q] with p hp hp'
simpa [Real.norm_eq_abs, abs_of_pos hp] using hp'
have hm_design : AEStronglyMeasurable[comap Prod.fst inferInstance]
(fun p : α × Bool => h p.1) Q := by
exact (hh.comp (comap_measurable Prod.fst)).aestronglyMeasurable
apply Causalean.Mathlib.MeasureTheory.condExp_eq_of_integral_preimage_eq
Q Prod.fst measurable_fst _ _ hY hm hm_design
intro S hS
let A : Set (α × Bool) := Prod.fst ⁻¹' S
let B : Set (α × Bool) := univ ×ˢ {true}
have hA : MeasurableSet A := measurable_fst hS
have hB : MeasurableSet B := MeasurableSet.univ.prod (measurableSet_singleton true)
have hsuccess := bernoulliMarkedLaw_restrict_true_map_fst ν₁ h hh hpos
have hsuccess_set := congrArg (fun μ : Measure α => μ S) hsuccess
rw [Measure.map_apply measurable_fst hS,
Measure.restrict_apply (measurable_fst hS)] at hsuccess_set
have hleft :
∫ p in A, (if p.2 then (1 : ℝ) else 0) ∂Q = ν₁.real S := by
rw [← integral_indicator hA]
calc
∫ p, A.indicator (fun p => if p.2 then (1 : ℝ) else 0) p ∂Q =
∫ p, (A ∩ B).indicator (1 : (α × Bool) → ℝ) p ∂Q := by
apply MeasureTheory.integral_congr_ae
filter_upwards [] with p
rcases p with ⟨a, z⟩
by_cases hpA : (a, z) ∈ A <;> cases z <;> simp [hpA, A, B]
_ = Q.real (A ∩ B) := integral_indicator_one (hA.inter hB)
_ = ν₁.real S := by
apply congrArg toReal
simpa [A, B] using hsuccess_set
have hcancel :=
Causalean.Mathlib.MeasureTheory.withDensity_one_div_ofReal_cancel ν₁ h hh hpos
have hright_tilt :
∫ a in S, h a ∂reciprocalTilt ν₁ h = ν₁.real S := by
calc
∫ a in S, h a ∂reciprocalTilt ν₁ h =
∫ a in S, (ofReal (h a)).toReal • (1 : ℝ)
∂reciprocalTilt ν₁ h := by
apply setIntegral_congr_ae hS
filter_upwards [hpos_tilt] with a ha
simp [ENNReal.toReal_ofReal ha.le]
_ = ∫ _a in S, (1 : ℝ) ∂(reciprocalTilt ν₁ h).withDensity
(fun a => ofReal (h a)) := by
symm
apply setIntegral_withDensity_eq_setIntegral_toReal_smul
(ENNReal.measurable_ofReal.comp hh) _ _ hS
filter_upwards [] with a
exact ENNReal.ofReal_lt_top
_ = ∫ _a in S, (1 : ℝ) ∂ν₁ := by
rw [show (reciprocalTilt ν₁ h).withDensity
(fun a => ofReal (h a)) = ν₁ by
simpa [reciprocalTilt] using hcancel]
_ = ν₁.real S := by simp
have hmap_integral :
∫ a in S, h a ∂Q.map Prod.fst = ∫ p in A, h p.1 ∂Q := by
simpa [A] using setIntegral_map hS hh.aestronglyMeasurable measurable_fst.aemeasurable
rw [hmap] at hmap_integral
exact hleft.trans (hmap_integral.symm.trans hright_tilt).symm
9 supporting declarations (lemmas, instances)
-
instSFiniteinstance — The reciprocal tilt of an s-finite base measure by any real-valued weight is s-finite. -
bernoulliMarkKernel_applytheorem — For a measurable weight, the Bernoulli-mark kernel fiber at a base point is the Boolean Bernoulli measure with that point's weight.hypothesesconclusionbernoulliMarkKernel h a = bernoulliBool (h a)Proof (Lean source)
theorem bernoulliMarkKernel_apply {α : Type*} [MeasurableSpace α] (h : α → ℝ) (hh : Measurable h) (a : α) : bernoulliMarkKernel h a = bernoulliBool (h a) := by rw [bernoulliMarkKernel, Kernel.withDensity_apply] · rw [Kernel.const_apply] rw [withDensity_add_measure, dirac_withDensity, dirac_withDensity] simp [bernoulliBool] · exact Measurable.ite (measurable_snd (measurableSet_singleton true)) (ENNReal.measurable_ofReal.comp (hh.comp measurable_fst)) (ENNReal.measurable_ofReal.comp (measurable_const.sub (hh.comp measurable_fst))) -
instIsSFiniteKernelinstance — The Bernoulli-mark kernel built from a weight is s-finite.parametersα :Type*h :α → ℝinstancegiven byby unfold bernoulliMarkKernel apply Kernel.IsSFiniteKernel.withDensity intro a z split_ifs <;> exact ENNReal.ofReal_ne_top -
bernoulliMarkKernel_apply_truetheorem — For a measurable weight and a base point, the success singleton has kernel mass max(h(a),0).hypothesesconclusionProof (Lean source)
theorem bernoulliMarkKernel_apply_true {α : Type*} [MeasurableSpace α] (h : α → ℝ) (hh : Measurable h) (a : α) : bernoulliMarkKernel h a {true} = ofReal (h a) := by rw [bernoulliMarkKernel_apply h hh a] simp [bernoulliBool] -
bernoulliMarkKernel_apply_falsetheorem — For a measurable weight and a base point, the failure singleton has kernel mass max(1-h(a),0).hypothesesconclusionProof (Lean source)
theorem bernoulliMarkKernel_apply_false {α : Type*} [MeasurableSpace α] (h : α → ℝ) (hh : Measurable h) (a : α) : bernoulliMarkKernel h a {false} = ofReal (1 - h a) := by rw [bernoulliMarkKernel_apply h hh a] simp [bernoulliBool] -
ae_bernoulliMarkKernel_apply_univ_eq_onetheorem — If a measurable weight lies strictly above zero and at most one almost everywhere under a measure, then the corresponding Bernoulli-mark fibers have total mass one almost everywhere.hypothesesconclusion∀ᵐ a ∂μ, bernoulliMarkKernel h a univ = 1Proof (Lean source)
theorem ae_bernoulliMarkKernel_apply_univ_eq_one {α : Type*} [MeasurableSpace α] (μ : Measure α) (h : α → ℝ) (hh : Measurable h) (hpos : ∀ᵐ a ∂μ, 0 < h a) (hle : ∀ᵐ a ∂μ, h a ≤ 1) : ∀ᵐ a ∂μ, bernoulliMarkKernel h a univ = 1 := by filter_upwards [hpos, hle] with a ha h'a rw [bernoulliMarkKernel_apply h hh a] exact @IsProbabilityMeasure.measure_univ Bool _ _ (bernoulliBool_isProbabilityMeasure ha.le h'a) -
bernoulliMarkedLaw_map_fsttheorem — For a finite base measure, a measurable success weight, and a positive success weight bounded above by one almost everywhere, the first-coordinate pushforward of the reciprocal-tilt Bernoulli law is the reciprocal tilt.hypothesesα :Type*ν₁ :h :α → ℝhh :hpos :∀ᵐ a ∂ν₁, 0 < h ahle :∀ᵐ a ∂ν₁, h a ≤ 1conclusionProof (Lean source)
theorem bernoulliMarkedLaw_map_fst {α : Type*} [MeasurableSpace α] (ν₁ : Measure α) [IsFiniteMeasure ν₁] (h : α → ℝ) (hh : Measurable h) (hpos : ∀ᵐ a ∂ν₁, 0 < h a) (hle : ∀ᵐ a ∂ν₁, h a ≤ 1) : (bernoulliMarkedLaw ν₁ h).map fst = reciprocalTilt ν₁ h := by have hac : reciprocalTilt ν₁ h ≪ ν₁ := withDensity_absolutelyContinuous ν₁ (fun a => ofReal (1 / h a)) have hmass : ∀ᵐ a ∂reciprocalTilt ν₁ h, bernoulliMarkKernel h a univ = 1 := ae_bernoulliMarkKernel_apply_univ_eq_one (reciprocalTilt ν₁ h) h hh (hac.ae_le hpos) (hac.ae_le hle) ext s hs rw [Measure.map_apply measurable_fst hs] rw [bernoulliMarkedLaw, show fst ⁻¹' s = s ×ˢ univ by ext p; simp] rw [Measure.compProd_apply_prod hs MeasurableSet.univ] calc (∫⁻ a in s, bernoulliMarkKernel h a univ ∂reciprocalTilt ν₁ h) = ∫⁻ _a in s, (1 : ENNReal) ∂reciprocalTilt ν₁ h := by apply setLIntegral_congr_fun_ae hs filter_upwards [hmass] with a ha _ exact ha _ = reciprocalTilt ν₁ h s := setLIntegral_one s -
bernoulliMarkedLaw_isProbabilityMeasuretheorem — For a finite base measure, a measurable success weight, a positive success weight bounded above by one almost everywhere, and unit total mass of the reciprocal tilt, the reciprocal-tilt Bernoulli-marked law is a probability measure.hypothesesα :Type*ν₁ :h :α → ℝhh :hpos :∀ᵐ a ∂ν₁, 0 < h ahle :∀ᵐ a ∂ν₁, h a ≤ 1hcal :reciprocalTilt ν₁ h univ = 1conclusionProof (Lean source)
theorem bernoulliMarkedLaw_isProbabilityMeasure {α : Type*} [MeasurableSpace α] (ν₁ : Measure α) [IsFiniteMeasure ν₁] (h : α → ℝ) (hh : Measurable h) (hpos : ∀ᵐ a ∂ν₁, 0 < h a) (hle : ∀ᵐ a ∂ν₁, h a ≤ 1) (hcal : reciprocalTilt ν₁ h univ = 1) : IsProbabilityMeasure (bernoulliMarkedLaw ν₁ h) := by rw [isProbabilityMeasure_iff] calc bernoulliMarkedLaw ν₁ h univ = (bernoulliMarkedLaw ν₁ h).map fst univ := by rw [Measure.map_apply measurable_fst MeasurableSet.univ] simp _ = reciprocalTilt ν₁ h univ := by rw [bernoulliMarkedLaw_map_fst ν₁ h hh hpos hle] _ = 1 := hcal -
bernoulliMarkedLaw_map_restrict_truetheorem — For a finite base measure, a measurable success weight that is strictly positive almost everywhere, and a measurable statistic of a marked point, the statistic's law on successful marks is the pushforward of the base measure by evaluating that statistic at a successful mark.hypothesesconclusion= ν₁.map (fun a => g (a, true))Proof (Lean source)
theorem bernoulliMarkedLaw_map_restrict_true {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (ν₁ : Measure α) [IsFiniteMeasure ν₁] (h : α → ℝ) (hh : Measurable h) (hpos : ∀ᵐ a ∂ν₁, 0 < h a) (g : α × Bool → β) (hg : Measurable g) : ((bernoulliMarkedLaw ν₁ h).restrict (univ ×ˢ {true})).map g = ν₁.map (fun a => g (a, true)) := by have hsection : Measurable (fun a => g (a, true)) := by fun_prop have hcancel := withDensity_one_div_ofReal_cancel ν₁ h hh hpos ext s hs rw [Measure.map_apply hg hs, Measure.map_apply hsection hs] rw [Measure.restrict_apply (hs.preimage hg)] rw [show g ⁻¹' s ∩ univ ×ˢ {true} = ((fun a => g (a, true)) ⁻¹' s) ×ˢ {true} by ext ⟨a, z⟩ cases z <;> simp] rw [bernoulliMarkedLaw, Measure.compProd_apply_prod (hs.preimage hsection) (measurableSet_singleton true)] simp_rw [bernoulliMarkKernel_apply_true h hh] rw [← withDensity_apply _ (hs.preimage hsection)] change ((ν₁.withDensity fun a => ofReal (1 / h a)).withDensity (fun a => ofReal (h a))) ((fun a => g (a, true)) ⁻¹' s) = ν₁ ((fun a => g (a, true)) ⁻¹' s) rw [hcancel]
CompProdAssembly 2 core · 2 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
⚑ flagged
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
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)
theorem compProd_eq_of_inner_ae reviewed
⚑ flagged
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
α γ β :
ν :
KL 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
2 supporting declarations (lemmas, instances)
-
compProd_map_snd_applytheorem — Snd-marginal of a composition product, pointwise (disintegration backbone).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] -
compProd_deterministic_applylemma — For measurable spaces, an s-finite kernel κ, a function f, its measurability, and a base point a, composition with the deterministic kernel equals the paired pushforward.hypothesesconclusion(κ ⊗ₖ deterministic f hf) a = (κ a).map (fun b => (b, f (a, b)))Proof (Lean source)
lemma compProd_deterministic_apply {α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (κ : Kernel α β) [IsSFiniteKernel κ] {f : α × β → γ} (hf : Measurable f) (a : α) : (κ ⊗ₖ deterministic f hf) a = (κ a).map (fun b => (b, f (a, b))) := by have hpair : Measurable (fun b : β => (b, f (a, b))) := prodMk measurable_id (hf.comp (prodMk measurable_const measurable_id)) refine MeasureTheory.Measure.ext fun A hA => ?_ rw [ProbabilityTheory.Kernel.compProd_apply hA, MeasureTheory.Measure.map_apply hpair hA] simp only [ProbabilityTheory.Kernel.deterministic_apply] trans (∫⁻ b, indicator ((fun b => (b, f (a, b))) ⁻¹' A) (fun _ => (1 : ENNReal)) b ∂(κ a)) · apply MeasureTheory.lintegral_congr intro b have hSlice : MeasurableSet (Prod.mk b ⁻¹' A) := measurable_prodMk_left hA rw [MeasureTheory.Measure.dirac_apply' _ hSlice] simp only [indicator, Set.mem_preimage, Pi.one_apply] rfl · exact MeasureTheory.lintegral_indicator_one (hpair hA)
CondDistrib 2 core · 2 supporting This file proves general-purpose lemmas for conditional distributions under measurable equivalences and disintegration through bind form. ★ map_compProd_prodMap_left_eq_compProd_comap★ measure_eq_bind_marginal_condDistrib
Conditional-Distribution Transport Lemmas
This file proves general-purpose lemmas for conditional distributions under measurable equivalences and disintegration through bind form. The statements are independent of the causal-model infrastructure and serve as Mathlib-adjacent measure-theoretic support for identification proofs.
The exported results are map_compProd_prodMap_left_eq_compProd_comap,
condDistrib_comp_right_measurableEquiv, and
measure_eq_bind_marginal_condDistrib. Together
they move regular conditional distributions across measurable equivalences and
package finite-measure disintegration as a bind identity.
theorem map_compProd_prodMap_left_eq_compProd_comap reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel
Pushforward of compProd through a measurable equivalence on the first coordinate. For a measurable equivalence e between the first-coordinate spaces, an s-finite measure ν on the source first coordinate, and an s-finite kernel κ from that coordinate to a second space, pushing the composed-product measure of ν and κ forward through e on the first coordinate (identity on the second) equals the composed-product measure of the pushed-forward ν and κ transported back along e's inverse.
Formal statement
hypotheses
Proof (Lean source)
theorem map_compProd_prodMap_left_eq_compProd_comap
{β β' γ : Type*} [MeasurableSpace β] [MeasurableSpace β']
[MeasurableSpace γ]
(ν : Measure β) [SFinite ν]
(e : β ≃ᵐ β')
(κ : Kernel β γ)
[IsSFiniteKernel κ] :
map (map e (id : γ → γ)) (ν.compProd κ)
= (map e ν).compProd
(κ.comap e.symm e.symm.measurable) := by
ext s hs
rw [MeasureTheory.Measure.map_apply
(e.measurable.prodMap measurable_id) hs]
rw [MeasureTheory.Measure.compProd_apply
(e.measurable.prodMap measurable_id hs)]
rw [MeasureTheory.Measure.compProd_apply hs]
rw [MeasureTheory.lintegral_map
(ProbabilityTheory.Kernel.measurable_kernel_prodMk_left hs)
e.measurable]
apply MeasureTheory.lintegral_congr
intro b
rw [ProbabilityTheory.Kernel.comap_apply, e.symm_apply_apply]
rfl
theorem measure_eq_bind_marginal_condDistrib reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel
Measure-theoretic chain rule / disintegration (Mathlib gap). For a finite measure μ on a product space, μ equals the composition obtained by first drawing the second coordinate from its marginal distribution and then drawing the first coordinate from its regular conditional distribution given that second coordinate.
Formal statement
hypotheses
β γ :
μ :
Measure (β × γ)
Proof (Lean source)
theorem measure_eq_bind_marginal_condDistrib
{β γ : Type*} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
[StandardBorelSpace β] [Nonempty β]
(μ : Measure (β × γ))
[IsFiniteMeasure μ] :
μ = (μ.map Prod.snd).bind
(fun c : γ =>
(ProbabilityTheory.condDistrib Prod.fst Prod.snd μ c).map
(fun b : β => (b, c))) := by
classical
let κ : Kernel γ β :=
ProbabilityTheory.condDistrib Prod.fst Prod.snd μ
have hcomp :
map Prod.snd μ ⊗ₘ κ
= map (fun p : β × γ => (p.2, p.1)) μ := by
simpa [κ] using
(ProbabilityTheory.compProd_map_condDistrib
(μ := μ) (X := Prod.snd) (Y := Prod.fst) (by fun_prop))
have hswap :
μ = map swap
(map (fun p : β × γ => (p.2, p.1)) μ) := by
rw [MeasureTheory.Measure.map_map measurable_swap]
· simp [Function.comp_def]
· fun_prop
have hprod_swap :
((ProbabilityTheory.Kernel.id ×ₖ κ).map swap)
= (κ ×ₖ ProbabilityTheory.Kernel.id) := by
ext c
rw [ProbabilityTheory.Kernel.map_apply _ measurable_swap,
ProbabilityTheory.Kernel.prod_apply,
ProbabilityTheory.Kernel.prod_apply,
MeasureTheory.Measure.prod_swap]
have hkernel :
(fun c : γ => map (fun b : β => (b, c)) (κ c))
=ᵐ[map Prod.snd μ]
((κ ×ₖ ProbabilityTheory.Kernel.id)) := by
filter_upwards with c
rw [ProbabilityTheory.Kernel.prod_apply]
exact (MeasureTheory.Measure.prod_dirac (μ := κ c) c).symm
simpa [κ] using (calc
μ = map swap
(map (fun p : β × γ => (p.2, p.1)) μ) := hswap
_ = map swap
(map Prod.snd μ ⊗ₘ κ) := by
rw [hcomp]
_ = (κ ×ₖ ProbabilityTheory.Kernel.id) ∘ₘ
map Prod.snd μ := by
rw [MeasureTheory.Measure.compProd_eq_comp_prod]
rw [MeasureTheory.Measure.map_comp _ _ measurable_swap]
rw [hprod_swap]
_ = (fun c : γ =>
map (fun b : β => (b, c)) (κ c)) ∘ₘ
map Prod.snd μ := by
exact MeasureTheory.Measure.bind_congr_right hkernel.symm)
2 supporting declarations (lemmas, instances)
-
condDistrib_eq_of_map_prod_eqtheorem — For measurable source spaces, measurable target spaces, random elements X, Y, X', and Y', finite measures μ and ν, and equal joint laws, the conditional distributions are equal.hypothesesh :μ.map (fun a => (X a, Y a)) = ν.map (fun a => (X' a, Y' a))conclusioncondDistrib Y X μ = condDistrib Y' X' νProof (Lean source)
theorem condDistrib_eq_of_map_prod_eq {α α' β γ : Type*} [MeasurableSpace α] [MeasurableSpace α'] [MeasurableSpace β] [MeasurableSpace γ] [StandardBorelSpace β] [Nonempty β] {X : α → γ} {Y : α → β} {X' : α' → γ} {Y' : α' → β} {μ : Measure α} {ν : Measure α'} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : μ.map (fun a => (X a, Y a)) = ν.map (fun a => (X' a, Y' a))) : condDistrib Y X μ = condDistrib Y' X' ν := by rw [condDistrib, condDistrib] congr 1 -
condDistrib_comp_right_measurableEquivtheorem — Push-forward invariance of condDistrib under a measurable equivalence of the conditioning variable.hypothesesα β Ω γ :Type*Nonempty Ωμ :Y :γ → ΩX :γ → αe :α ≃ᵐ βhY :hX :conclusion∀ᵐ x ∂(μ.map X), condDistrib Y (e ∘ X) μ (e x)= condDistrib Y X μ xProof (Lean source)
theorem condDistrib_comp_right_measurableEquiv {α β Ω γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {mγ : MeasurableSpace γ} (μ : Measure γ) [IsFiniteMeasure μ] {Y : γ → Ω} {X : γ → α} (e : α ≃ᵐ β) (hY : Measurable Y) (hX : Measurable X) : ∀ᵐ x ∂(μ.map X), ProbabilityTheory.condDistrib Y (e ∘ X) μ (e x) = ProbabilityTheory.condDistrib Y X μ x := by classical set κ : Kernel α Ω := ProbabilityTheory.condDistrib Y X μ with hκ_def set κ' : Kernel β Ω := κ.comap e.symm e.symm.measurable with hκ'_def -- (1) Pushforward of the joint `(X, Y)` map under `(e × id)`. have hpush : map (fun a => ((e ∘ X) a, Y a)) μ = map (map e (id : Ω → Ω)) (map (fun a => (X a, Y a)) μ) := by rw [MeasureTheory.Measure.map_map (e.measurable.prodMap measurable_id) (hX.prodMk hY)] rfl -- (2) Compose with `compProd_map_condDistrib` and the pushforward lemma -- `map_compProd_prodMap_left_eq_compProd_comap` to express the -- `(e ∘ X, Y)`-pushforward as a compProd against `κ'`. have hcompProd_eX : map (fun a => ((e ∘ X) a, Y a)) μ = (map (e ∘ X) μ).compProd κ' := by rw [hpush, ← ProbabilityTheory.compProd_map_condDistrib (X := X) hY.aemeasurable, map_compProd_prodMap_left_eq_compProd_comap (map X μ) e κ] congr 1 exact MeasureTheory.Measure.map_map e.measurable hX -- (3) Uniqueness of disintegration gives ae-equality of `κ'` with -- `condDistrib Y (e ∘ X) μ` under `μ.map (e ∘ X)`. have hae : (fun b => ProbabilityTheory.condDistrib Y (e ∘ X) μ b) =ᵐ[map (e ∘ X) μ] κ' := ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd (e ∘ X) hY.aemeasurable hcompProd_eX -- (4) Transport the ae-equality through `e`. Since -- `μ.map (e ∘ X) = (μ.map X).map e`, an a.e. statement on the former -- becomes an a.e. statement on `μ.map X` after precomposing with `e`. have hmap : map (e ∘ X) μ = map e (map X μ) := (MeasureTheory.Measure.map_map e.measurable hX).symm rw [hmap] at hae have hae' : ∀ᵐ x ∂(map X μ), ProbabilityTheory.condDistrib Y (e ∘ X) μ (e x) = κ' (e x) := MeasureTheory.ae_of_ae_map (μ := map X μ) (f := e) e.measurable.aemeasurable hae -- (5) Finally, `κ' (e x) = κ (e.symm (e x)) = κ x`. filter_upwards [hae'] with x hx rw [hx, hκ'_def, ProbabilityTheory.Kernel.comap_apply, e.symm_apply_apply]
CondDistribFiber 1 core · 3 supporting This module localizes a joint law to a measurable conditioning fiber. ★ condDistrib_congr_on_conditioning_fiber
Conditional-distribution congruence on a conditioning fiber
This module localizes a joint law to a measurable conditioning fiber. It turns almost-everywhere equality of two outcomes on that fiber into equality of their conditional distributions there. The proof packages the restricted joint-law, composition-product restriction, and localized kernel-uniqueness steps for use in general finite-measure arguments.
theorem condDistrib_congr_on_conditioning_fiber reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.CondDistribFiber
Given a finite sampling measure μ, a measurable covariate map Xv, a measurable treatment map Av, two measurable outcome maps Yv and Zv, and a selected treatment value a, if the outcomes agree almost everywhere whenever treatment has that value, then their conditional distributions given covariates and treatment agree almost everywhere on the corresponding conditioning fiber.
Formal statement
hypotheses
Ω X A Y :
Type*
Nonempty Y
μ :
Xv :
Ω → X
Av :
Ω → A
Yv Zv :
Ω → Y
hX :
Measurable Xv
hA :
Measurable Av
hY :
Measurable Yv
hZ :
Measurable Zv
a :
A
h :
∀ᵐ ω ∂μ, Av ω = a → Yv ω = Zv ω
conclusion
∀ᵐ xa ∂μ.map (fun ω => (Xv ω, Av ω)), xa.2
= a → condDistrib Yv (fun ω => (Xv ω, Av ω)) μ xa = condDistrib Zv (fun ω => (Xv ω, Av ω)) μ xa
Proof (Lean source)
theorem condDistrib_congr_on_conditioning_fiber
{Ω X A Y : Type*}
[MeasurableSpace Ω] [MeasurableSpace X] [MeasurableSpace A]
[MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y]
[MeasurableSingletonClass A]
(μ : Measure Ω) [IsFiniteMeasure μ]
(Xv : Ω → X) (Av : Ω → A) (Yv Zv : Ω → Y)
(hX : Measurable Xv) (hA : Measurable Av)
(hY : Measurable Yv) (hZ : Measurable Zv) (a : A)
(h : ∀ᵐ ω ∂μ, Av ω = a → Yv ω = Zv ω) :
∀ᵐ xa ∂μ.map (fun ω => (Xv ω, Av ω)), xa.2 = a →
condDistrib Yv (fun ω => (Xv ω, Av ω)) μ xa =
condDistrib Zv (fun ω => (Xv ω, Av ω)) μ xa := by
let T : Ω → X × A := fun ω => (Xv ω, Av ω)
let s : Set (X × A) := {xa | xa.2 = a}
have hT : Measurable T := hX.prodMk hA
have hs : MeasurableSet s := measurable_snd (measurableSet_singleton a)
have h' : ∀ᵐ ω ∂μ, T ω ∈ s → Yv ω = Zv ω := by
simpa [T, s] using h
have hJ := map_prod_restrict_eq_of_ae_eq_on_preimage
μ T Yv Zv hT hY hZ hs h'
rw [← compProd_map_condDistrib (X := T) hY.aemeasurable,
← compProd_map_condDistrib (X := T) hZ.aemeasurable] at hJ
have hK := ae_eq_on_of_compProd_restrict_eq
(μ.map T) (condDistrib Yv T μ) (condDistrib Zv T μ) hs hJ
simpa [T, s] using hK
3 supporting declarations (lemmas, instances)
-
map_prod_restrict_eq_of_ae_eq_on_preimagetheorem — Given a measure μ, a measurable conditioning variable T, two measurable outcome variables Yv and Zv, and a measurable conditioning set s, if the outcomes agree almost everywhere on the preimage of that set, then their joint laws agree after restriction to that conditioning set.hypothesesΩ B Y :μ :Measure ΩT :Ω → BYv Zv :Ω → YhT :hY :Measurable YvhZ :Measurable Zvs :Set Bhs :h :∀ᵐ ω ∂μ, T ω ∈ s → Yv ω = Zv ωProof (Lean source)
theorem map_prod_restrict_eq_of_ae_eq_on_preimage {Ω B Y : Type*} [MeasurableSpace Ω] [MeasurableSpace B] [MeasurableSpace Y] (μ : Measure Ω) (T : Ω → B) (Yv Zv : Ω → Y) (hT : Measurable T) (hY : Measurable Yv) (hZ : Measurable Zv) {s : Set B} (hs : MeasurableSet s) (h : ∀ᵐ ω ∂μ, T ω ∈ s → Yv ω = Zv ω) : (μ.map (fun ω => (T ω, Yv ω))).restrict (s ×ˢ univ) = (μ.map (fun ω => (T ω, Zv ω))).restrict (s ×ˢ univ) := by have hYprod : Measurable (fun ω => (T ω, Yv ω)) := hT.prodMk hY have hZprod : Measurable (fun ω => (T ω, Zv ω)) := hT.prodMk hZ have hYpre : (fun ω => (T ω, Yv ω)) ⁻¹' (s ×ˢ univ) = T ⁻¹' s := by ext ω simp have hZpre : (fun ω => (T ω, Zv ω)) ⁻¹' (s ×ˢ univ) = T ⁻¹' s := by ext ω simp rw [Measure.restrict_map hYprod (hs.prod MeasurableSet.univ), Measure.restrict_map hZprod (hs.prod MeasurableSet.univ), hYpre, hZpre] apply Measure.map_congr apply (ae_restrict_iff' (hT hs)).2 filter_upwards [h] with ω hω hωs exact congrArg (fun y => (T ω, y)) (hω hωs) -
compProd_restrict_lefttheorem — Given an s-finite base measure ν, an s-finite kernel κ, and a measurable base set s, restricting their composition product to that set in the first coordinate gives the composition product formed from the restricted base measure.Proof (Lean source)
theorem compProd_restrict_left {B Y : Type*} [MeasurableSpace B] [MeasurableSpace Y] (ν : Measure B) [SFinite ν] (κ : Kernel B Y) [IsSFiniteKernel κ] {s : Set B} (hs : MeasurableSet s) : (ν ⊗ₘ κ).restrict (s ×ˢ univ) = (ν.restrict s) ⊗ₘ κ := by ext t ht rw [Measure.restrict_apply' (hs.prod MeasurableSet.univ), Measure.compProd_apply (ht.inter (hs.prod MeasurableSet.univ)), Measure.compProd_apply ht, ← lintegral_indicator hs] congr 1 ext b by_cases hb : b ∈ s <;> simp [hb] -
ae_eq_on_of_compProd_restrict_eqtheorem — Given a finite base measure ν, two finite kernels κ and η, and a measurable base set s, if their composition products agree after restriction to that set, then the kernels agree almost everywhere on the selected set.Proof (Lean source)
theorem ae_eq_on_of_compProd_restrict_eq {B Y : Type*} [MeasurableSpace B] [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y] (ν : Measure B) [IsFiniteMeasure ν] (κ η : Kernel B Y) [IsFiniteKernel κ] [IsFiniteKernel η] {s : Set B} (hs : MeasurableSet s) (h : (ν ⊗ₘ κ).restrict (s ×ˢ univ) = (ν ⊗ₘ η).restrict (s ×ˢ univ)) : ∀ᵐ b ∂ν, b ∈ s → κ b = η b := by rw [compProd_restrict_left ν κ hs, compProd_restrict_left ν η hs] at h exact ae_imp_of_ae_restrict (Kernel.ae_eq_of_compProd_eq h)
CondDistribWitness 3 core · 2 supporting This file states the measure-theoretic core of a backdoor or Rule-2 argument purely in terms of Mathlib's conditional distributions, with no SCM machinery. ★ condDistrib_map_of_condDistrib_fst_eq★ condDistrib_map_of_funext
Witness-kernel form of conditional distributions
This file states the measure-theoretic core of a backdoor or Rule-2 argument purely in terms of Mathlib's conditional distributions, with no SCM machinery. When an outcome is a measurable function of the conditioning variable and a residual coordinate, its conditional law is the pushforward of the residual coordinate's conditional law by that function.
The main construction is witnessKernel, a Markov kernel sending a treatment-
covariate pair to the residual conditional law pushed through a structural
response. The theorem condDistrib_map_of_condDistrib_fst_eq proves this
witness-kernel form under a conditional-independence hypothesis, while
condDistrib_map_of_funext gives the no-treatment specialization where the
conditioning variable already contains the full non-residual information.
def witnessKernel reviewed
⚑ flagged
ProbabilityTheory
Given a sample space equipped with a σ-algebra, a treatment space equipped with a σ-algebra, a covariate space equipped with a σ-algebra, a nonempty standard Borel residual-coordinate space, and an outcome space equipped with a σ-algebra, let the sampling measure be finite, the covariate map and the residual-coordinate map map sample points to their respective spaces, and let the structural response map map a treatment, covariate, and residual coordinate to an outcome. If this structural response is jointly measurable, then the witness kernel assigns to each treatment--covariate pair the distribution of the structural response after drawing the residual coordinate from its conditional distribution given the covariate.
Definition (Lean source)
parameters
Ω :
Type u_1
𝒳 :
Type u_2
𝒵 :
Type u_3
𝒞 :
Type u_4
𝒴 :
Type u_5
μ :
Z :
Ω → 𝒵
C :
Ω → 𝒞
h :
𝒳 → 𝒵 → 𝒞 → 𝒴
hh :
Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2)
def
given by
clause 1
toFun p := (condDistrib C Z μ p.2).map (h p.1 p.2)
clause 2
measurable' := by have hhp : ∀ p : 𝒳 × 𝒵, Measurable (h p.1 p.2) := fun p
=> hh.comp (measurable_const.prodMk measurable_id) refine Measure.measurable_of_measurable_coe _ (fun B hB => ?_) have hmap : ∀ p : 𝒳 × 𝒵, ((condDistrib C Z μ p.2).map (h p.1 p.2)) B = (condDistrib C Z μ p.2) ((h p.1 p.2) ⁻¹' B) := by intro p rw [Measure.map_apply (hhp p) hB] simp_rw [hmap] set κ' : Kernel (𝒳 × 𝒵) 𝒞 := (condDistrib C Z μ).comap (Prod.snd : 𝒳 × 𝒵 → 𝒵) measurable_snd with hκ' have hker : ∀ p : 𝒳 × 𝒵, (condDistrib C Z μ p.2) ((h p.1 p.2) ⁻¹' B) = ∫⁻ c, B.indicator (1 : 𝒴 → ℝ≥0∞) (h p.1 p.2 c) ∂(κ' p) := by intro p rw [hκ', Kernel.comap_apply, ← lintegral_indicator_one ((hhp p) hB)] refine lintegral_congr (fun c => ?_) by_cases hc : h p.1 p.2 c ∈ B <;> simp [Set.mem_preimage, hc] simp_rw [hker] refine Measurable.lintegral_kernel_prod_right ?_ exact (measurable_const.indicator hB).comp hh
theorem condDistrib_map_of_condDistrib_fst_eq reviewed
⚑ flagged
ProbabilityTheory
Witness-kernel form of a conditional distribution under conditional independence. For measurable maps X, Z, and C and a jointly measurable structural-response function h, if the conditional distribution of C given the pair (X,Z) agrees almost everywhere with the conditional distribution of C given Z alone — conditional independence of C from X given Z, then the conditional distribution of the outcome h(X,Z,C) given (X,Z) agrees almost everywhere with the pushforward, by the map h x z, of the conditional distribution of C given Z.
Formal statement
hypotheses
Ω :
Type u_1
𝒳 :
Type u_2
𝒵 :
Type u_3
𝒞 :
Type u_4
𝒴 :
Type u_5
μ :
X :
Ω → 𝒳
Z :
Ω → 𝒵
C :
Ω → 𝒞
h :
𝒳 → 𝒵 → 𝒞 → 𝒴
hX :
hZ :
hC :
hh :
Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2)
hCI :
(fun p : 𝒳 × 𝒵 => condDistrib C (fun ω => (X ω, Z ω)) μ p)
=ᵐ[μ.map (fun ω => (X ω, Z ω))] (fun p => condDistrib C Z μ p.2)
conclusion
(fun p : 𝒳 × 𝒵 => condDistrib (fun ω => h (X ω) (Z ω) (C ω)) (fun ω => (X ω, Z ω)) μ p)
=ᵐ[μ.map (fun ω => (X ω, Z ω))] (fun p => (condDistrib C Z μ p.2).map (h p.1 p.2))
Proof (Lean source)
theorem condDistrib_map_of_condDistrib_fst_eq
(μ : Measure Ω) [IsFiniteMeasure μ]
{X : Ω → 𝒳} {Z : Ω → 𝒵} {C : Ω → 𝒞} {h : 𝒳 → 𝒵 → 𝒞 → 𝒴}
(hX : Measurable X) (hZ : Measurable Z) (hC : Measurable C)
(hh : Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2))
(hCI : (fun p : 𝒳 × 𝒵 => condDistrib C (fun ω => (X ω, Z ω)) μ p)
=ᵐ[μ.map (fun ω => (X ω, Z ω))]
(fun p => condDistrib C Z μ p.2)) :
(fun p : 𝒳 × 𝒵 => condDistrib (fun ω => h (X ω) (Z ω) (C ω)) (fun ω => (X ω, Z ω)) μ p)
=ᵐ[μ.map (fun ω => (X ω, Z ω))]
(fun p => (condDistrib C Z μ p.2).map (h p.1 p.2)) := by
set W : Ω → 𝒳 × 𝒵 := fun ω => (X ω, Z ω) with hW
set Y : Ω → 𝒴 := fun ω => h (X ω) (Z ω) (C ω) with hY
have hWmeas : Measurable W := by fun_prop
have hYmeas : Measurable Y := by
have : Y = (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2) ∘ (fun ω => (W ω, C ω)) := rfl
rw [this]; exact hh.comp ((hWmeas).prodMk hC)
-- The candidate witness kernel.
set κ : Kernel (𝒳 × 𝒵) 𝒴 := witnessKernel μ (Z := Z) (C := C) hh with hκ
-- It suffices, by uniqueness of `condDistrib`, to verify the disintegration identity.
suffices hgoal : condDistrib Y W μ =ᵐ[μ.map W] κ by
filter_upwards [hgoal] with p hp
rw [hp, hκ, witnessKernel_apply]
refine condDistrib_ae_eq_of_measure_eq_compProd W hYmeas.aemeasurable ?_
-- Verify `μ.map (W, Y) = μ.map W ⊗ₘ κ` on rectangles.
refine Measure.ext_prod (fun {A B} hA hB => ?_)
-- RHS: `(μ.map W ⊗ₘ κ) (A ×ˢ B) = ∫⁻ p in A, κ p B ∂(μ.map W)`.
rw [Measure.compProd_apply_prod hA hB]
-- Rewrite `κ p B` using `condDistrib C Z μ p.2 = condDistrib C W μ p` (a.e. via `hCI`).
have hκB : ∀ p : 𝒳 × 𝒵, κ p B = (condDistrib C Z μ p.2) ((h p.1 p.2) ⁻¹' B) := by
intro p
have hhp : Measurable (h p.1 p.2) := hh.comp (measurable_const.prodMk measurable_id)
rw [hκ, witnessKernel_apply μ Z C hh, Measure.map_apply hhp hB]
simp_rw [hκB]
-- Replace `condDistrib C Z μ p.2` by `condDistrib C W μ p` on `A` using `hCI`.
have hint : ∫⁻ p in A, (condDistrib C Z μ p.2) ((h p.1 p.2) ⁻¹' B) ∂(μ.map W)
= ∫⁻ p in A, (condDistrib C W μ p) ((h p.1 p.2) ⁻¹' B) ∂(μ.map W) := by
refine lintegral_congr_ae (ae_restrict_of_ae ?_)
filter_upwards [hCI] with p hp
rw [hp]
rw [hint]
-- This integral is `(μ.map W ⊗ₘ condDistrib C W μ)` on `{(p,c) | p ∈ A ∧ h p.1 p.2 c ∈ B}`.
have hCWmarkov : IsMarkovKernel (condDistrib C W μ) := inferInstance
have hset : MeasurableSet {q : (𝒳 × 𝒵) × 𝒞 | q.1 ∈ A ∧ h q.1.1 q.1.2 q.2 ∈ B} := by
apply MeasurableSet.inter
· exact measurable_fst hA
· exact hh hB
have hcompProd :
∫⁻ p in A, (condDistrib C W μ p) ((h p.1 p.2) ⁻¹' B) ∂(μ.map W)
= (μ.map W ⊗ₘ condDistrib C W μ)
{q : (𝒳 × 𝒵) × 𝒞 | q.1 ∈ A ∧ h q.1.1 q.1.2 q.2 ∈ B} := by
rw [Measure.compProd_apply hset]
rw [← lintegral_indicator hA]
refine lintegral_congr (fun p => ?_)
by_cases hpA : p ∈ A
· rw [Set.indicator_of_mem hpA]
congr 1
ext c
simp [hpA]
· rw [Set.indicator_of_notMem hpA]
have : (Prod.mk p ⁻¹' {q : (𝒳 × 𝒵) × 𝒞 | q.1 ∈ A ∧ h q.1.1 q.1.2 q.2 ∈ B}) = ∅ := by
ext c; simp [hpA]
rw [this]; simp
rw [hcompProd, compProd_map_condDistrib hC.aemeasurable]
-- Finally identify with `μ.map (W, Y) (A ×ˢ B)`.
rw [Measure.map_apply (hWmeas.prodMk hC) hset]
rw [Measure.map_apply (hWmeas.prodMk hYmeas) (hA.prod hB)]
-- The two preimage events `{W ∈ A ∧ Y ∈ B}` and `{(W,C) ∈ {q | q.1 ∈ A ∧ h … ∈ B}}` coincide.
congr 1
theorem condDistrib_map_of_funext reviewed
⚑ flagged
ProbabilityTheory
No-treatment witness-kernel form of a conditional distribution. For measurable maps Z and C and a jointly measurable response function H, the conditional distribution of the outcome H(Z,C) given Z agrees almost everywhere with the pushforward, by the map H z, of the conditional distribution of C given Z.
Formal statement
hypotheses
Ω :
Type u_1
𝒵 :
Type u_3
𝒞 :
Type u_4
𝒴 :
Type u_5
μ :
Z :
Ω → 𝒵
C :
Ω → 𝒞
H :
𝒵 → 𝒞 → 𝒴
hZ :
hC :
hH :
Measurable (fun p : 𝒵 × 𝒞 => H p.1 p.2)
conclusion
(fun z : 𝒵 => condDistrib (fun ω => H (Z ω) (C ω)) Z μ z)
=ᵐ[μ.map Z] (fun z => (condDistrib C Z μ z).map (H z))
Proof (Lean source)
theorem condDistrib_map_of_funext
(μ : Measure Ω) [IsFiniteMeasure μ]
{Z : Ω → 𝒵} {C : Ω → 𝒞} {H : 𝒵 → 𝒞 → 𝒴}
(hZ : Measurable Z) (hC : Measurable C)
(hH : Measurable (fun p : 𝒵 × 𝒞 => H p.1 p.2)) :
(fun z : 𝒵 => condDistrib (fun ω => H (Z ω) (C ω)) Z μ z)
=ᵐ[μ.map Z]
(fun z => (condDistrib C Z μ z).map (H z)) := by
set Y : Ω → 𝒴 := fun ω => H (Z ω) (C ω) with hY
have hYmeas : Measurable Y := by
have : Y = (fun p : 𝒵 × 𝒞 => H p.1 p.2) ∘ (fun ω => (Z ω, C ω)) := rfl
rw [this]; exact hH.comp (hZ.prodMk hC)
-- The candidate witness kernel `z ↦ (condDistrib C Z μ z).map (H z)`.
have hHz : ∀ z : 𝒵, Measurable (H z) := fun z =>
hH.comp (measurable_const.prodMk measurable_id)
let κ : Kernel 𝒵 𝒴 :=
{ toFun := fun z => (condDistrib C Z μ z).map (H z)
measurable' := by
refine Measure.measurable_of_measurable_coe _ (fun B hB => ?_)
have hmap : ∀ z : 𝒵,
((condDistrib C Z μ z).map (H z)) B
= (condDistrib C Z μ z) ((H z) ⁻¹' B) := fun z => by
rw [Measure.map_apply (hHz z) hB]
simp_rw [hmap]
have hker : ∀ z : 𝒵,
(condDistrib C Z μ z) ((H z) ⁻¹' B)
= ∫⁻ c, B.indicator (1 : 𝒴 → ℝ≥0∞) (H z c) ∂(condDistrib C Z μ z) := by
intro z
rw [← lintegral_indicator_one ((hHz z) hB)]
refine lintegral_congr (fun c => ?_)
by_cases hc : H z c ∈ B <;> simp [Set.mem_preimage, hc]
simp_rw [hker]
refine Measurable.lintegral_kernel_prod_right ?_
exact (measurable_const.indicator hB).comp hH }
have hκ_apply : ∀ z, κ z = (condDistrib C Z μ z).map (H z) := fun _ => rfl
haveI hκmarkov : IsMarkovKernel κ := by
constructor
intro z
rw [hκ_apply]
have : IsMarkovKernel (condDistrib C Z μ) := inferInstance
exact Measure.isProbabilityMeasure_map (hHz z).aemeasurable
suffices hgoal : condDistrib Y Z μ =ᵐ[μ.map Z] κ by
filter_upwards [hgoal] with z hz
rw [hz, hκ_apply]
refine condDistrib_ae_eq_of_measure_eq_compProd Z hYmeas.aemeasurable ?_
refine Measure.ext_prod (fun {A B} hA hB => ?_)
rw [Measure.compProd_apply_prod hA hB]
have hκB : ∀ z : 𝒵, κ z B = (condDistrib C Z μ z) ((H z) ⁻¹' B) := by
intro z; rw [hκ_apply]; exact Measure.map_apply (hHz z) hB
simp_rw [hκB]
have hCmarkov : IsMarkovKernel (condDistrib C Z μ) := inferInstance
have hset : MeasurableSet {q : 𝒵 × 𝒞 | q.1 ∈ A ∧ H q.1 q.2 ∈ B} := by
apply MeasurableSet.inter
· exact measurable_fst hA
· exact hH hB
have hcompProd :
∫⁻ z in A, (condDistrib C Z μ z) ((H z) ⁻¹' B) ∂(μ.map Z)
= (μ.map Z ⊗ₘ condDistrib C Z μ)
{q : 𝒵 × 𝒞 | q.1 ∈ A ∧ H q.1 q.2 ∈ B} := by
rw [Measure.compProd_apply hset, ← lintegral_indicator hA]
refine lintegral_congr (fun z => ?_)
by_cases hzA : z ∈ A
· rw [Set.indicator_of_mem hzA]
congr 1; ext c; simp [hzA]
· rw [Set.indicator_of_notMem hzA]
have : (Prod.mk z ⁻¹' {q : 𝒵 × 𝒞 | q.1 ∈ A ∧ H q.1 q.2 ∈ B}) = ∅ := by
ext c; simp [hzA]
rw [this]; simp
rw [hcompProd, compProd_map_condDistrib hC.aemeasurable]
rw [Measure.map_apply (hZ.prodMk hC) hset]
rw [Measure.map_apply (hZ.prodMk hYmeas) (hA.prod hB)]
congr 1
2 supporting declarations (lemmas, instances)
-
witnessKernel_applylemma — Evaluating the witness kernel at a conditioning pair gives the residual conditional law pushed through the corresponding structural slice.hypothesesΩ :sharedType u_1𝒳 :sharedType u_2𝒵 :sharedType u_3𝒞 :sharedType u_4𝒴 :sharedType u_5μ :Z :Ω → 𝒵C :Ω → 𝒞h :𝒳 → 𝒵 → 𝒞 → 𝒴hh :Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2)p :𝒳 × 𝒵conclusionProof (Lean source)
@[simp] lemma witnessKernel_apply (μ : Measure Ω) [IsFiniteMeasure μ] (Z : Ω → 𝒵) (C : Ω → 𝒞) {h : 𝒳 → 𝒵 → 𝒞 → 𝒴} (hh : Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2)) (p : 𝒳 × 𝒵) : witnessKernel μ (Z := Z) (C := C) hh p = (condDistrib C Z μ p.2).map (h p.1 p.2) := rfl -
instIsMarkovKernel_witnessKernelinstance — For every sample space, treatment space, covariate space, nonempty standard Borel residual-coordinate space, and outcome space, each equipped with the stated measurable structure, finite sampling measure, covariate map, residual-coordinate map, structural response map, and joint measurability of that response map, the witness kernel is a Markov kernel.parametersΩ :sharedType u_1𝒳 :sharedType u_2𝒵 :sharedType u_3𝒞 :sharedType u_4𝒴 :sharedType u_5μ :Z :Ω → 𝒵C :Ω → 𝒞h :𝒳 → 𝒵 → 𝒞 → 𝒴hh :Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2)instancegiven byby constructor intro p rw [witnessKernel_apply] have hhp : Measurable (h p.1 p.2) := hh.comp (measurable_const.prodMk measurable_id) have : IsMarkovKernel (condDistrib C Z μ) := inferInstance exact Measure.isProbabilityMeasure_map hhp.aemeasurable
FiniteAtomic 1 core · 3 supporting This module evaluates Bochner integrals against finite mixtures of Dirac measures and disintegrates set integrals along a measurable base coordinate. ★ setIntegral_finiteAtomicKernel
Bochner disintegration of finite atomic kernels
This module evaluates Bochner integrals against finite mixtures of Dirac measures and disintegrates set integrals along a measurable base coordinate. It applies to a continuous base measure with finitely many, possibly distinct, atoms above each base point.
theorem setIntegral_finiteAtomicKernel reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteAtomic
An s-finite base measure and s-finite finite atomic kernel with nonnegative weights, together with a measurable projection that recovers the base point from every atom, a measurable base set, and an outcome integrable under the law obtained by drawing a base point and then an atom, give that the integral of the outcome under that law, over the points whose recovered base point lies in the set, equals the base-measure integral over the set of the weighted sum of the outcome values at the atoms above each base point.
Formal statement
hypotheses
X :
Type u_1
Y :
Type u_2
I :
Type u_3
κ :
Kernel X Y
atom :
X → I → Y
weight :
X → I → ℝ
hweight :
∀ x i, 0 ≤ weight x i
hκ :
∀ x, κ x = ∑ i : I, ofReal (weight x i) • Measure.dirac (atom x i)
base :
Y → X
hbase_meas :
Measurable base
hbase :
∀ x i, base (atom x i) = x
B :
Set X
hB :
f :
Y → ℝ
hf :
Integrable f (κ ∘ₘ μ)
conclusion
∫ y in {y | base y ∈ B}, f y ∂(κ ∘ₘ μ) = ∫ x in B, (∑ i : I, weight x i * f (atom x i)) ∂μ
Proof (Lean source)
theorem setIntegral_finiteAtomicKernel
(μ : Measure X) [SFinite μ] (κ : Kernel X Y) [IsSFiniteKernel κ]
(atom : X → I → Y) (weight : X → I → ℝ)
(hweight : ∀ x i, 0 ≤ weight x i)
(hκ : ∀ x, κ x = ∑ i : I,
ofReal (weight x i) • Measure.dirac (atom x i))
(base : Y → X) (hbase_meas : Measurable base)
(hbase : ∀ x i, base (atom x i) = x)
(B : Set X) (hB : MeasurableSet B)
(f : Y → ℝ) (hf : Integrable f (κ ∘ₘ μ)) :
∫ y in {y | base y ∈ B}, f y ∂(κ ∘ₘ μ) =
∫ x in B, (∑ i : I, weight x i * f (atom x i)) ∂μ := by
let S : Set Y := base ⁻¹' B
have hS : MeasurableSet S := hB.preimage hbase_meas
let g : Y → ℝ := S.indicator f
have hg : Integrable g (κ ∘ₘ μ) := hf.indicator hS
have hpair : Integrable (fun p : X × Y => g p.2) (μ ⊗ₘ κ) :=
(Measure.integrable_compProd_snd_iff hg.1).2 hg
have hcomp : ∫ y, g y ∂(κ ∘ₘ μ) = ∫ x, ∫ y, g y ∂κ x ∂μ := by
rw [← Measure.snd_compProd μ κ]
rw [← Measure.integral_compProd hpair]
rw [Measure.snd]
exact integral_map measurable_snd.aemeasurable (by
simpa [← Measure.snd_compProd μ κ, Measure.snd] using hg.1)
have hfiber : ∀ᵐ x ∂μ, Integrable g (κ x) :=
Measure.ae_integrable_of_integrable_comp hg
have heval : ∀ᵐ x ∂μ,
(∫ y, g y ∂κ x) = B.indicator
(fun x => ∑ i : I, weight x i * f (atom x i)) x := by
filter_upwards [hfiber] with x hx
rw [integral_finiteAtomicKernel κ atom weight hweight hκ g x hx]
by_cases hxB : x ∈ B
· simp [g, S, indicator, hbase, hxB]
· simp [g, S, indicator, hbase, hxB]
change ∫ y in S, f y ∂(κ ∘ₘ μ) = _
rw [← integral_indicator hS, hcomp]
rw [integral_congr_ae heval]
exact integral_indicator hB
3 supporting declarations (lemmas, instances)
-
integral_finiteAtomicKerneltheorem — A finite atomic kernel, described by its atom locations and nonnegative weights through a pointwise Dirac decomposition, has the finite weighted integral of an integrable real-valued outcome at the specified base point as its Bochner integral.hypothesesX :sharedType u_1Y :sharedType u_2I :sharedType u_3κ :Kernel X Yatom :X → I → Yweight :X → I → ℝhweight :∀ x i, 0 ≤ weight x ihκ :∀ x, κ x = ∑ i : I, ofReal (weight x i) • Measure.dirac (atom x i)f :Y → ℝx :Xhf :Integrable f (κ x)conclusion∫ y, f y ∂κ x = ∑ i : I, weight x i * f (atom x i)Proof (Lean source)
theorem integral_finiteAtomicKernel (κ : Kernel X Y) (atom : X → I → Y) (weight : X → I → ℝ) (hweight : ∀ x i, 0 ≤ weight x i) (hκ : ∀ x, κ x = ∑ i : I, ofReal (weight x i) • Measure.dirac (atom x i)) (f : Y → ℝ) (x : X) (hf : Integrable f (κ x)) : ∫ y, f y ∂κ x = ∑ i : I, weight x i * f (atom x i) := by rw [hκ x] have hi : ∀ i ∈ (Finset.univ : Finset I), Integrable f (ofReal (weight x i) • Measure.dirac (atom x i)) := (integrable_finsetSum_measure.mp (by simpa using (hκ x ▸ hf))) rw [integral_finsetSum_measure hi] simp only [integral_smul_measure, integral_dirac, ENNReal.toReal_ofReal (hweight x _), smul_eq_mul] -
setIntegral_finiteAtomicKernel_of_pointwisetheorem — An s-finite base measure, finite atomic kernel with nonnegative weights, measurable base-recovering projection, measurable base set, and integrable outcome, with a pointwise-equal candidate mean, make the selected outcome integral equal the set integral of that mean.hypothesesX :sharedType u_1Y :sharedType u_2I :sharedType u_3κ :Kernel X Yatom :X → I → Yweight :X → I → ℝhweight :∀ x i, 0 ≤ weight x ihκ :∀ x, κ x = ∑ i : I, ofReal (weight x i) • Measure.dirac (atom x i)base :Y → Xhbase_meas :Measurable basehbase :∀ x i, base (atom x i) = xB :Set XhB :f :Y → ℝhf :Integrable f (κ ∘ₘ μ)q :X → ℝhq :∀ x, (∑ i : I, weight x i * f (atom x i)) = q xconclusion∫ y in {y | base y ∈ B}, f y ∂(κ ∘ₘ μ) = ∫ x in B, q x ∂μProof (Lean source)
theorem setIntegral_finiteAtomicKernel_of_pointwise (μ : Measure X) [SFinite μ] (κ : Kernel X Y) [IsSFiniteKernel κ] (atom : X → I → Y) (weight : X → I → ℝ) (hweight : ∀ x i, 0 ≤ weight x i) (hκ : ∀ x, κ x = ∑ i : I, ofReal (weight x i) • Measure.dirac (atom x i)) (base : Y → X) (hbase_meas : Measurable base) (hbase : ∀ x i, base (atom x i) = x) (B : Set X) (hB : MeasurableSet B) (f : Y → ℝ) (hf : Integrable f (κ ∘ₘ μ)) (q : X → ℝ) (hq : ∀ x, (∑ i : I, weight x i * f (atom x i)) = q x) : ∫ y in {y | base y ∈ B}, f y ∂(κ ∘ₘ μ) = ∫ x in B, q x ∂μ := by rw [setIntegral_finiteAtomicKernel μ κ atom weight hweight hκ base hbase_meas hbase B hB f hf] simp_rw [hq] -
setIntegral_twoAtomicKerneltheorem — An s-finite base measure and two-atom s-finite kernel with nonnegative weights, a measurable base set, and an integrable paired outcome give the selected integral as the weighted average of the two atom values over that base set.hypothesesX :sharedType u_1MeasurableSingletonClass (X × Fin 2)κ :weight :X → Fin 2 → ℝhweight :∀ x i, 0 ≤ weight x iB :Set XhB :f :X × Fin 2 → ℝhf :Integrable f (κ ∘ₘ μ)conclusion∫ y in {y | y.1 ∈ B}, f y ∂(κ ∘ₘ μ) = ∫ x in B, (∑ i : Fin 2, weight x i * f (x, i)) ∂μProof (Lean source)
theorem setIntegral_twoAtomicKernel (μ : Measure X) [SFinite μ] [MeasurableSingletonClass (X × Fin 2)] (κ : Kernel X (X × Fin 2)) [IsSFiniteKernel κ] (weight : X → Fin 2 → ℝ) (hweight : ∀ x i, 0 ≤ weight x i) (hκ : ∀ x, κ x = ∑ i : Fin 2, ofReal (weight x i) • Measure.dirac (x, i)) (B : Set X) (hB : MeasurableSet B) (f : X × Fin 2 → ℝ) (hf : Integrable f (κ ∘ₘ μ)) : ∫ y in {y | y.1 ∈ B}, f y ∂(κ ∘ₘ μ) = ∫ x in B, (∑ i : Fin 2, weight x i * f (x, i)) ∂μ := by exact setIntegral_finiteAtomicKernel μ κ (fun x i => (x, i)) weight hweight hκ fst measurable_fst (by intros; rfl) B hB f hf
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
⚑ flagged
Causalean.Mathlib.GraphMapProd
For three measurable spaces serving respectively as predictor, exogenous-noise, and response spaces, a measure on the exogenous-noise space, and a mechanism mapping a predictor--noise pair to a response, the structural-mechanism kernel assigns to each predictor value the push-forward of the noise measure through the corresponding slice of the mechanism.
theorem map_graph_prod_eq_compProd reviewed
⚑ flagged
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
β :
Type u_1
γ :
Type u_2
δ :
Type u_3
Φ :
β × γ → δ
hΦ :
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)) := by fun_prop
-- 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
2 supporting declarations (lemmas, instances)
-
mechanismKernel_applytheorem — Pointwise value of mechanismKernel: κ o = νₗ.map (fun l => Φ (o, l)).hypothesesβ :sharedType u_1γ :sharedType u_2δ :sharedType u_3Φ :β × γ → δhΦ :o :βconclusionmechanismKernel νₗ Φ 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 -
instIsMarkovKernelMechanismKerneltheorem — The mechanism kernel is Markov when the exogenous-noise law is a probability measure and the mechanism is measurable.hypothesesβ :sharedType u_1γ :sharedType u_2δ :sharedType u_3νₗ :Φ :β × γ → δhΦ :conclusionIsMarkovKernel (mechanismKernel νₗ Φ)Proof (Lean source)
theorem instIsMarkovKernelMechanismKernel (νₗ : Measure γ) [IsProbabilityMeasure νₗ] {Φ : β × γ → δ} (hΦ : Measurable Φ) : IsMarkovKernel (mechanismKernel νₗ Φ) := by unfold mechanismKernel exact ProbabilityTheory.Kernel.IsMarkovKernel.map _ hΦ
ParameterizedKernelQuantileRealization 4 core · 6 supporting This file constructs a jointly measurable realization of a real-valued Markov kernel supported on the closed unit interval by one uniform variable. ★ map_quantileRealization
Parameterized quantile realization of real Markov kernels
This file constructs a jointly measurable realization of a real-valued Markov kernel supported on the closed unit interval by one uniform variable. The construction is the generalized inverse of each fiber's distribution function, valued first in the unit interval and then extended to real randomization inputs by clamping them to that interval. It proves both the exact fiberwise pushforward law and the pointwise range guarantee needed by parameterized coupling and conditional law constructions.
def SupportedOnUnitInterval reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ParameterizedKernelQuantileRealization
For a real-valued kernel, the unit-interval support property says that each parameter-specific fiber measure assigns mass one to the closed interval from zero to one. The kernel is not required to be Markov here; for a Markov kernel, as in the realization theorems, this says each fiber is a probability distribution supported on that interval.
Definition (Lean source)
parameters
def
SupportedOnUnitInterval κ :
Prop
given by
κ s (Icc (0 : ℝ) 1) = 1
def kernelUnitQuantile reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ParameterizedKernelQuantileRealization
For a real-valued kernel, a parameter value, and a uniform level in the closed unit interval, the unit-interval-valued parameterized quantile is the supremum of the points x of the unit interval whose fiber mass on the closed interval from zero to x is strictly smaller than the supplied level. The kernel is not required to be Markov here; the quantile interpretation holds for Markov kernels, as assumed by the realization theorems.
Definition (Lean source)
parameters
def
given by
def quantileRealization reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ParameterizedKernelQuantileRealization
For a real-valued kernel and a parameter--randomization pair, the real-valued quantile realization evaluates the unit-interval quantile after clamping the randomization coordinate to the closed unit interval.
Definition (Lean source)
parameters
def
quantileRealization κ p :
ℝ
given by
kernelUnitQuantile κ p.1 (projIcc (0 : ℝ) 1 zero_le_one p.2)
theorem map_quantileRealization reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ParameterizedKernelQuantileRealization
Given a real-valued Markov kernel, the condition that each fiber is supported on the closed unit interval, and a parameter value, pushing Lebesgue measure restricted to the closed unit interval through the real quantile section exactly recovers that kernel fiber.
Formal statement
hypotheses
conclusion
Measure.map (fun u : ℝ => quantileRealization κ (s, u)) (volume.restrict (Icc (0 : ℝ) 1))
= κ s
Proof (Lean source)
theorem map_quantileRealization (κ : Kernel S ℝ)
[IsMarkovKernel κ] (hκ : SupportedOnUnitInterval κ) (s : S) :
Measure.map (fun u : ℝ => quantileRealization κ (s, u))
(volume.restrict (Icc (0 : ℝ) 1)) = κ s := by
rw [← unitInterval.measurePreserving_coe.map_eq,
Measure.map_map (measurable_quantileRealization_section κ s) measurable_subtype_coe]
rw [show (fun u : ℝ => quantileRealization κ (s, u)) ∘ val =
fun u : unitInterval => (kernelUnitQuantile κ s u : ℝ) by
funext u
simp only [Function.comp_apply, quantileRealization]
rw [Set.projIcc_of_mem zero_le_one u.property]]
exact map_kernelUnitQuantile κ hκ s
6 supporting declarations (lemmas, instances)
-
quantileRealization_mem_unitIntervaltheorem — For a real-valued Markov kernel and a parameter--randomization pair, the corresponding realization value belongs to the closed unit interval.hypothesesconclusionquantileRealization κ p ∈ Icc (0 : ℝ) 1Proof (Lean source)
theorem quantileRealization_mem_unitInterval (κ : Kernel S ℝ) (p : S × ℝ) : quantileRealization κ p ∈ Icc (0 : ℝ) 1 := by exact (kernelUnitQuantile κ p.1 (projIcc (0 : ℝ) 1 zero_le_one p.2)).property -
measurable_kernelUnitQuantiletheorem — For a real-valued Markov kernel that is Markov, the unit-interval generalized inverse is jointly measurable in the kernel parameter and uniform level.Proof (Lean source)
theorem measurable_kernelUnitQuantile (κ : Kernel S ℝ) [IsMarkovKernel κ] : Measurable (uncurry (kernelUnitQuantile κ)) := by refine measurable_of_Ioi fun a ↦ ?_ simp only [preimage, uncurry, mem_Ioi] have h_monotone s : Monotone (fun x : unitInterval ↦ (κ s).real (Icc (0 : ℝ) x)) := fun x y hxy ↦ measureReal_mono (by gcongr) have sSup_eq_iUnion_rat : {x : S × unitInterval | a < kernelUnitQuantile κ x.1 x.2} = ⋃ (q : ℚ) (hqI : (↑q : ℝ) ∈ unitInterval) (_ : a < (q : ℝ)), {e | (κ e.1).real (Icc (0 : ℝ) ((⟨(q : ℝ), hqI⟩ : unitInterval) : ℝ)) < e.2} := by ext e simp_all only [lt_sSup_iff, mem_ofPred_eq, Subtype.exists, mem_Icc, Rat.cast_nonneg, mem_iUnion, exists_prop, exists_and_left, kernelUnitQuantile] constructor · rintro ⟨y, y_mem, hyI, (hy : a.1 < y)⟩ obtain ⟨q, hqa, hqy⟩ := exists_rat_btwn hy have hq0 : 0 ≤ q := by exact (Rat.cast_nonneg (K := ℝ)).mp (a.2.1.trans hqa.le) have hqI : (q : ℝ) ∈ unitInterval := ⟨a.2.1.trans hqa.le, hqy.le.trans hyI.2⟩ refine ⟨q, ⟨hq0, hqI.2⟩, hqa, lt_of_lt_of_le' y_mem ?_⟩ exact h_monotone e.1 (a := ⟨(q : ℝ), hqI⟩) (b := ⟨y, hyI⟩) hqy.le · intro he obtain ⟨q, hqI, hqa, h⟩ := he exact ⟨q, h, ⟨by simp [hqI.1], hqI.2⟩, hqa⟩ rw [sSup_eq_iUnion_rat] refine MeasurableSet.iUnion (fun b ↦ MeasurableSet.iUnion (fun bI ↦ MeasurableSet.iUnion (fun _ ↦ ?_))) refine measurableSet_lt ?_ measurable_snd.subtype_val simp_rw [measureReal_def] have hκ := κ.measurable_coe (s := Icc (0 : ℝ) ((⟨(b : ℝ), bI⟩ : unitInterval) : ℝ)) measurableSet_Icc fun_prop -
measurable_quantileRealizationtheorem — For a real-valued Markov kernel, the real-valued quantile realization is jointly measurable in its parameter and real randomization input.Proof (Lean source)
theorem measurable_quantileRealization (κ : Kernel S ℝ) [IsMarkovKernel κ] : Measurable (quantileRealization κ) := by change Measurable (fun p : S × ℝ ↦ ((kernelUnitQuantile κ p.1 (projIcc (0 : ℝ) 1 zero_le_one p.2) : unitInterval) : ℝ)) exact measurable_subtype_coe.comp <| (measurable_kernelUnitQuantile κ).comp <| measurable_fst.prodMk ((continuous_projIcc (a := (0 : ℝ)) (b := 1) (h := zero_le_one)).measurable.comp measurable_snd) -
measurable_quantileRealization_sectiontheorem — For a real-valued Markov kernel and a fixed parameter value, the resulting real-valued function of the randomization input is measurable.hypothesesconclusionMeasurable (fun u : ℝ => quantileRealization κ (s, u))Proof (Lean source)
@[fun_prop] theorem measurable_quantileRealization_section (κ : Kernel S ℝ) [IsMarkovKernel κ] (s : S) : Measurable (fun u : ℝ => quantileRealization κ (s, u)) := by exact (measurable_quantileRealization κ).comp (measurable_const.prodMk measurable_id) -
map_kernelUnitQuantiletheorem — Given a real-valued Markov kernel, the condition that each fiber is supported on the closed unit interval, and a parameter value, pushing canonical uniform unit-interval volume through the fiber's quantile map exactly recovers that kernel fiber.hypothesesconclusionMeasure.map (fun u : unitInterval => (kernelUnitQuantile κ s u : ℝ)) volume = κ sProof (Lean source)
theorem map_kernelUnitQuantile (κ : Kernel S ℝ) [IsMarkovKernel κ] (hκ : SupportedOnUnitInterval κ) (s : S) : Measure.map (fun u : unitInterval => (kernelUnitQuantile κ s u : ℝ)) volume = κ s := by let f := fun u : unitInterval => (kernelUnitQuantile κ s u : ℝ) have hf : Measurable f := measurable_subtype_coe.comp (measurable_kernelUnitQuantile κ).of_uncurry_left have hκ_compl : κ s (Icc (0 : ℝ) 1)ᶜ = 0 := by rw [measure_compl measurableSet_Icc (measure_ne_top (κ s) _), hκ s, measure_univ] simp have hκ_ae : ∀ᵐ y ∂κ s, y ∈ Icc (0 : ℝ) 1 := by rw [ae_iff] exact hκ_compl have hκ_Iic (z : unitInterval) : κ s (Iic (z : ℝ)) = κ s (Icc 0 (z : ℝ)) := by apply measure_congr refine hκ_ae.mono ?_ intro y hy apply propext exact ⟨fun h ↦ ⟨hy.1, h⟩, And.right⟩ refine (Measure.map f volume).ext_of_Iic (κ s) fun x ↦ ?_ rw [Measure.map_apply hf measurableSet_Iic] change volume {u : unitInterval | (kernelUnitQuantile κ s u : ℝ) ≤ x} = κ s (Iic x) by_cases hx0 : x < 0 · have hpre : {u : unitInterval | (kernelUnitQuantile κ s u : ℝ) ≤ x} = ∅ := by ext u simp only [mem_ofPred_eq, mem_empty_iff_false, iff_false] exact not_le.mpr (hx0.trans_le (kernelUnitQuantile κ s u).property.1) have hnull : κ s (Iic x) = 0 := by refine measure_mono_null ?_ hκ_compl intro y hy simp only [mem_Iic] at hy simp only [mem_compl_iff, mem_Icc, not_and_or] exact inl (not_le.mpr (hy.trans_lt hx0)) rw [hpre, measure_empty, hnull] · have hx0' : 0 ≤ x := le_of_not_gt hx0 by_cases hx1 : x ≤ 1 · let xI : unitInterval := ⟨x, hx0', hx1⟩ have hIic : κ s (Iic x) = κ s (Icc 0 x) := hκ_Iic xI have κ_in_I : ((κ s).real (Icc (0 : ℝ) x)) ∈ unitInterval := ⟨measureReal_nonneg, measureReal_le_one⟩ rw [hIic, ← ofReal_measureReal (measure_ne_top (κ s) _), ← unitInterval.volume_Iic ⟨_, κ_in_I⟩] congr with ξ constructor · intro (hξ : kernelUnitQuantile κ s ξ ≤ xI) change ξ ≤ (κ s).real (Icc (0 : ℝ) x) by_cases hx : xI = 1 · have hx' : x = 1 := congrArg val hx rw [hx', measureReal_def, hκ s] simpa using ξ.2.2 let g := fun y : unitInterval ↦ (κ s).real (Icc (0 : ℝ) y) let nebot : NeBot (𝓝[>] xI) := by refine nhdsGT_neBot_of_exists_gt ?_ use 1 exact lt_of_le_of_ne xI.2.2 hx refine le_of_tendsto_of_tendsto (b := 𝓝[>] xI) (g := g) continuousWithinAt_const ?_ ?_ · let h := cdf (κ s) have h_continuousWithinAt := continuousWithinAt_Ioi_iff_Ici.mpr (h.right_continuous (xI : ℝ)) have hreal (y : unitInterval) : (κ s).real (Icc (0 : ℝ) (y : ℝ)) = h (y : ℝ) := by change (κ s).real (Icc (0 : ℝ) (y : ℝ)) = cdf (κ s) (y : ℝ) rw [ProbabilityTheory.cdf_eq_real, measureReal_def, measureReal_def, hκ_Iic y] simp_rw [g, hreal] rw [hreal xI] exact h_continuousWithinAt.comp (Continuous.continuousWithinAt (by fun_prop)) (fun y hy ↦ hy) · refine eventually_nhdsWithin_of_forall fun y hy ↦ ?_ by_contra! h simp only [sSup_le_iff, kernelUnitQuantile] at hξ specialize hξ y h grind · intro (hξ : ξ ≤ (κ s).real (Icc (0 : ℝ) x)) change kernelUnitQuantile κ s ξ ≤ xI simp only [sSup_le_iff, kernelUnitQuantile] intro c hc by_contra! h have h_lt : ¬(κ s).real (Icc (0 : ℝ) x) ≤ (κ s).real (Icc (0 : ℝ) c) := not_le.mpr (lt_of_le_of_lt' hξ hc) refine h_lt ?_ refine measureReal_mono ?_ intro z hz exact ⟨hz.1, hz.2.trans (by exact_mod_cast h.le)⟩ · have hx1' : 1 < x := lt_of_not_ge hx1 have hpre : {u : unitInterval | (kernelUnitQuantile κ s u : ℝ) ≤ x} = univ := by ext u simp only [mem_ofPred_eq, mem_univ, iff_true] exact (kernelUnitQuantile κ s u).property.2.trans hx1'.le have hfull : κ s (Iic x) = 1 := by calc κ s (Iic x) = κ s univ := by apply measure_congr refine hκ_ae.mono ?_ intro y hy exact propext ⟨fun _ ↦ mem_univ y, fun _ ↦ hy.2.trans hx1'.le⟩ _ = 1 := measure_univ rw [hpre, measure_univ, hfull] -
ae_quantileRealization_mem_unitIntervaltheorem — For a real-valued Markov kernel and a parameter value, the realization section lies in the closed unit interval almost everywhere under the uniform law.hypothesesconclusion∀ᵐ u ∂(volume.restrict (Icc (0 : ℝ) 1)), quantileRealization κ (s, u) ∈ Icc (0 : ℝ) 1Proof (Lean source)
theorem ae_quantileRealization_mem_unitInterval (κ : Kernel S ℝ) (s : S) : ∀ᵐ u ∂(volume.restrict (Icc (0 : ℝ) 1)), quantileRealization κ (s, u) ∈ Icc (0 : ℝ) 1 := by exact Filter.Eventually.of_forall fun u => quantileRealization_mem_unitInterval κ (s, u)
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
⚑ flagged
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
α :
Type u_1
β :
Type u_2
γ :
Type u_3
Nonempty β
ρ :
κ :
Kernel α β
η :
Kernel α γ
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) := by fun_prop
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
theorem condDistrib_snd_of_compProd_prod reviewed
⚑ flagged
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
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) := by fun_prop
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
TwoStateMarkov 4 core · 2 supporting This file develops transitionMatrix, stationaryProjection, transitionMatrix_pow_eq_spectral, the pointwise and compact-uniform spectral gap bounds, and transitionMatrix_pow_tendsto_stationary_uniform for a two-state Mark ★ transitionMatrix_pow_eq_spectral★ transitionMatrix_pow_tendsto_stationary_uniform
Two-State Markov Chains
This file develops transitionMatrix, stationaryProjection,
transitionMatrix_pow_eq_spectral, the pointwise and compact-uniform spectral
gap bounds, and transitionMatrix_pow_tendsto_stationary_uniform for a
two-state Markov chain with transition probabilities in the open unit square.
def transitionMatrix reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.TwoStateMarkov
For two transition parameters in an arbitrary field, the two-state transition matrix is the matrix whose first row is and whose second row is .
def stationaryProjection reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.TwoStateMarkov
For two transition parameters in an arbitrary field, the stationary projection matrix is the matrix whose two rows both equal .
theorem transitionMatrix_pow_eq_spectral reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.TwoStateMarkov
For parameters a, b in a field with a + b nonzero, the k-th power of the two-state transition matrix transitionMatrix a b decomposes as the stationary projection stationaryProjection a b plus (1 - a - b)^k times its complement, for every k.
Formal statement
hypotheses
conclusion
(transitionMatrix a b) ^ k
= stationaryProjection a b + ((1 - a - b) ^ k) • (1 - stationaryProjection a b)
Proof (Lean source)
theorem transitionMatrix_pow_eq_spectral
{K : Type*} [Field K] (a b : K) (hs : a + b ≠ 0) :
∀ k : ℕ,
(transitionMatrix a b) ^ k =
stationaryProjection a b +
((1 - a - b) ^ k) • (1 - stationaryProjection a b) := by
let P := stationaryProjection a b
let Q : Matrix (Fin 2) (Fin 2) K := 1 - P
let lam := 1 - a - b
have hM : transitionMatrix a b = P + lam • Q := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [P, Q, lam, transitionMatrix, stationaryProjection, Matrix.smul_apply,
Matrix.sub_apply, Matrix.add_apply] <;>
field_simp [hs] <;> ring
have hP2 : P * P = P := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [P, stationaryProjection, Matrix.mul_apply, Fin.sum_univ_two] <;>
field_simp [hs] <;> ring
have hPQ : P * Q = 0 := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [P, Q, stationaryProjection, Matrix.mul_apply, Matrix.sub_apply,
Matrix.one_apply, Fin.sum_univ_two] <;>
field_simp [hs] <;> ring
have hQP : Q * P = 0 := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [P, Q, stationaryProjection, Matrix.mul_apply, Matrix.sub_apply,
Matrix.one_apply, Fin.sum_univ_two] <;>
field_simp [hs] <;> ring
have hQ2 : Q * Q = Q := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [P, Q, stationaryProjection, Matrix.mul_apply, Matrix.sub_apply,
Matrix.one_apply, Fin.sum_univ_two] <;>
field_simp [hs] <;> ring
intro k
induction k with
| zero =>
ext i j
fin_cases i <;> fin_cases j <;>
simp [stationaryProjection, Matrix.add_apply, Matrix.sub_apply]
| succ k ih =>
calc
transitionMatrix a b ^ (k + 1)
= (P + (lam ^ k) • Q) * (P + lam • Q) := by rw [pow_succ, ih, hM]
_ = P + (lam ^ (k + 1)) • Q := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [P, Q, lam, stationaryProjection, Matrix.mul_apply, Matrix.add_apply,
Matrix.sub_apply, Matrix.smul_apply, Matrix.one_apply, Fin.sum_univ_two,
pow_succ] <;>
field_simp [hs] <;> ring
theorem transitionMatrix_pow_tendsto_stationary_uniform reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.TwoStateMarkov
For a set K of transition-parameter pairs (a,b) that is compact and contained in the open unit square, the k-th power of the transition matrix converges to the stationary projection entrywise, uniformly over K: for every ε > 0 there is a threshold N such that every entry of (transitionMatrix a b)^k - stationaryProjection a b has absolute value at most ε once k ≥ N, for every (a,b) in K.
Formal statement
hypotheses
K :
Set (ℝ × ℝ)
hK_compact :
hK_open :
K ⊆ {p : ℝ × ℝ | 0 < p.1 ∧ p.1 < 1 ∧ 0 < p.2 ∧ p.2 < 1}
ε > (0 : ℝ) :
conclusion
∃ N : ℕ,
∀ k : ℕ,
N
≤ k → ∀ p ∈ K, ∀ i j : Fin 2, |((transitionMatrix p.1 p.2) ^ k - stationaryProjection p.1 p.2) i j| ≤ ε
Proof (Lean source)
theorem transitionMatrix_pow_tendsto_stationary_uniform
(K : Set (ℝ × ℝ)) (hK_compact : IsCompact K)
(hK_open : K ⊆ {p : ℝ × ℝ | 0 < p.1 ∧ p.1 < 1 ∧ 0 < p.2 ∧ p.2 < 1}) :
∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ k : ℕ, N ≤ k →
∀ p ∈ K, ∀ i j : Fin 2,
|((transitionMatrix p.1 p.2) ^ k - stationaryProjection p.1 p.2) i j| ≤ ε := by
intro ε hε
classical
by_cases hne : K.Nonempty
· obtain ⟨ρ, hρ_lt, hρ_bound⟩ :=
one_minus_a_b_uniform_gap_on_compact K hK_compact (fun p hp => by
have hopen := hK_open hp
exact ⟨by linarith [hopen.1, hopen.2.2.1], by linarith [hopen.2.1, hopen.2.2.2]⟩)
rcases hne with ⟨p0, hp0⟩
have hρ_nonneg : 0 ≤ ρ :=
(abs_nonneg (1 - p0.1 - p0.2)).trans (hρ_bound p0 hp0)
have htend := tendsto_pow_atTop_nhds_zero_of_lt_one hρ_nonneg hρ_lt
have hevent : ∀ᶠ k in atTop, ρ ^ k < ε := htend.eventually_lt_const hε
rw [Filter.eventually_atTop] at hevent
rcases hevent with ⟨N, hN⟩
refine ⟨N, ?_⟩
intro k hk p hp i j
have hopen := hK_open hp
have ha_pos : 0 < p.1 := hopen.1
have hb_pos : 0 < p.2 := hopen.2.2.1
have hs_pos : 0 < p.1 + p.2 := by linarith
have hs : p.1 + p.2 ≠ 0 := ne_of_gt hs_pos
have hqa : |p.1 / (p.1 + p.2)| ≤ 1 := by
rw [abs_of_nonneg (div_nonneg ha_pos.le hs_pos.le)]
rw [div_le_one hs_pos]
linarith
have hqb : |p.2 / (p.1 + p.2)| ≤ 1 := by
rw [abs_of_nonneg (div_nonneg hb_pos.le hs_pos.le)]
rw [div_le_one hs_pos]
linarith
have hQ_le : |(1 - stationaryProjection p.1 p.2) i j| ≤ 1 := by
fin_cases i <;> fin_cases j
· have h : 1 - p.2 / (p.1 + p.2) = p.1 / (p.1 + p.2) := by
field_simp [hs]
ring
simpa [stationaryProjection, Matrix.sub_apply, h] using hqa
· simpa [stationaryProjection, Matrix.sub_apply, abs_neg] using hqa
· simpa [stationaryProjection, Matrix.sub_apply, abs_neg] using hqb
· have h : 1 - p.1 / (p.1 + p.2) = p.2 / (p.1 + p.2) := by
field_simp [hs]
ring
simpa [stationaryProjection, Matrix.sub_apply, h] using hqb
have hentry :
((transitionMatrix p.1 p.2) ^ k - stationaryProjection p.1 p.2) i j =
(1 - p.1 - p.2) ^ k * (1 - stationaryProjection p.1 p.2) i j := by
have hspec :=
transitionMatrix_pow_eq_spectral p.1 p.2 hs k
calc
((transitionMatrix p.1 p.2) ^ k - stationaryProjection p.1 p.2) i j
=
(stationaryProjection p.1 p.2 +
(1 - p.1 - p.2) ^ k • (1 - stationaryProjection p.1 p.2) -
stationaryProjection p.1 p.2) i j := by
rw [hspec]
_ = (1 - p.1 - p.2) ^ k * (1 - stationaryProjection p.1 p.2) i j := by
simp [Matrix.sub_apply, Matrix.add_apply, Matrix.smul_apply]
have hgap_pow : |(1 - p.1 - p.2) ^ k| ≤ ρ ^ k := by
rw [abs_pow]
exact pow_le_pow_left₀ (abs_nonneg (1 - p.1 - p.2)) (hρ_bound p hp) k
have hbound :
|((transitionMatrix p.1 p.2) ^ k - stationaryProjection p.1 p.2) i j| ≤ ρ ^ k := by
rw [hentry, abs_mul]
calc
|(1 - p.1 - p.2) ^ k| * |(1 - stationaryProjection p.1 p.2) i j|
≤ ρ ^ k * 1 :=
mul_le_mul hgap_pow hQ_le (abs_nonneg _) (pow_nonneg hρ_nonneg k)
_ = ρ ^ k := by ring
exact hbound.trans (le_of_lt (hN k hk))
· refine ⟨0, ?_⟩
intro k hk p hp i j
exact False.elim (hne ⟨p, hp⟩)
2 supporting declarations (lemmas, instances)
-
one_minus_a_b_abs_lt_onetheorem — Pointwise spectral gap: |1 - a - b| < 1 when a + b lies strictly between zero and two.hypothesesconclusion|1 - a - b| < 1Proof (Lean source)
theorem one_minus_a_b_abs_lt_one {K : Type*} [CommRing K] [LinearOrder K] [IsStrictOrderedRing K] {a b : K} (hs_pos : 0 < a + b) (hs_lt_two : a + b < 2) : |1 - a - b| < 1 := by by_cases hle : a + b ≤ 1 · rw [abs_of_nonneg (by linarith)] linarith · have hgt : 1 < a + b := lt_of_not_ge hle rw [abs_of_neg (by linarith)] linarith -
one_minus_a_b_uniform_gap_on_compacttheorem — Uniform spectral gap on compact subsets of the open strip: the continuous function (a,b) ↦ |1 - a - b| attains its supremum when 0 < a + b < 2 at some point of K, and that supremum is strictly less than 1 by the pointwise bound.hypothesesconclusion∃ ρ : ℝ,ρ < 1conclusion 1p ∈ K :|1 - p.1 - p.2| ≤ ρProof (Lean source)
theorem one_minus_a_b_uniform_gap_on_compact (K : Set (ℝ × ℝ)) (hK_compact : IsCompact K) (hK_open : K ⊆ {p : ℝ × ℝ | 0 < p.1 + p.2 ∧ p.1 + p.2 < 2}) : ∃ ρ : ℝ, ρ < 1 ∧ ∀ p ∈ K, |1 - p.1 - p.2| ≤ ρ := by by_cases hne : K.Nonempty · let f : ℝ × ℝ → ℝ := fun p => |1 - p.1 - p.2| have hf : ContinuousOn f K := by dsimp [f] fun_prop rcases hK_compact.exists_isMaxOn hne hf with ⟨pstar, hpstar, hpmax⟩ have hopen := hK_open hpstar have hmax_lt : f pstar < 1 := by dsimp [f] exact one_minus_a_b_abs_lt_one hopen.1 hopen.2 refine ⟨(f pstar + 1) / 2, ?_, ?_⟩ · linarith · intro p hp have hle : f p ≤ f pstar := isMaxOn_iff.mp hpmax p hp dsimp [f] at hle ⊢ linarith · refine ⟨0, by norm_num, ?_⟩ intro p hp exact False.elim (hne ⟨p, hp⟩)