Mathlib.Probability.Kernel.ThreeBernoulli
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
Basic 12 core · 5 supporting The density coordinates put first mark and the remaining-mark pair before the base. ★ jointLaw_probability
Three Bernoulli marks over an arbitrary base law
The density coordinates put first mark and the remaining-mark pair before the
base. This lets the finite counting-measure construction feed the existing
three-block conditional-independence theorem when the base is standard Borel.
The public joint coordinates are (x, (a, (y₀, y₁))).
def bitMass reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The mass of a Boolean Bernoulli mark with success probability p at the specified Boolean value.
Definition (Lean source)
def cellMass reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The selected cell mass at first mark a and selected value y, from first-mark probability and the two remaining-mark probabilities: the Bernoulli mass of the first mark at a times the Bernoulli mass at y of the mark that a selects, whose success probability is q₁ when a is true and q₀ when a is false.
def tripleMass reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The product mass of three independent Bernoulli marks at the specified triple, with their three success probabilities.
abbrev DensityCoord reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
Coordinates for the finite-count density consist of first mark, the pair of remaining marks, and the base space.
abbrev FullCoord reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
Coordinates for the public three-mark law consist of the base space, first mark, and both remaining marks.
abbrev SelectedCoord reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
Coordinates for the selected-mark law consist of the base space, first mark, and the realized selected value.
def reference reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The finite-count reference measure combines counting measures on three Boolean marks with a base measure.
def density reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The product Bernoulli density at one three-mark point uses three base-dependent mark probabilities: it is the product of the three Bernoulli masses of the point's marks, evaluated at the point's base value and read as an extended nonnegative number (a negative product, possible only when a probability leaves the unit interval, is replaced by zero).
Definition (Lean source)
parameters
def
density e q₀ q₁ z :
ℝ≥0∞
given by
ofReal (tripleMass (e z.2.2) (q₀ z.2.2) (q₁ z.2.2) z.1 z.2.1.1 z.2.1.2)
def densityLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The three-mark measure in density coordinates is the product-counting reference measure weighted by the three Bernoulli probabilities.
Definition (Lean source)
def toFull reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The reordering to base-first three-mark coordinates sends density coordinates to (x,a,y₀,y₁).
Definition (Lean source)
def jointLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The joint law of base, first mark, and remaining marks is the reordered finite-count Bernoulli density law.
Definition (Lean source)
parameters
given by
theorem jointLaw_probability reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The base-first joint law is a probability measure under a probability base law, measurable mark probabilities, and unit-interval bounds.
Formal statement
hypotheses
X :
Type u
μ :
e q₀ q₁ :
X → ℝ
he :
hq₀ :
Measurable q₀
hq₁ :
Measurable q₁
he01 :
∀ x, e x ∈ Icc (0 : ℝ) 1
hq₀01 :
∀ x, q₀ x ∈ Icc (0 : ℝ) 1
hq₁01 :
∀ x, q₁ x ∈ Icc (0 : ℝ) 1
conclusion
IsProbabilityMeasure (jointLaw μ e q₀ q₁)
Proof (Lean source)
theorem jointLaw_probability {X : Type u} [MeasurableSpace X]
(μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ)
(he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁)
(he01 : ∀ x, e x ∈ Icc (0 : ℝ) 1)
(hq₀01 : ∀ x, q₀ x ∈ Icc (0 : ℝ) 1)
(hq₁01 : ∀ x, q₁ x ∈ Icc (0 : ℝ) 1) :
IsProbabilityMeasure (jointLaw μ e q₀ q₁) := by
-- Transport `densityLaw_probability` through measurable `toFull` and
-- simplify the measure of `univ` under `Measure.map`.
haveI : IsProbabilityMeasure (densityLaw μ e q₀ q₁) :=
densityLaw_probability μ e q₀ q₁ he hq₀ hq₁ he01 hq₀01 hq₁01
exact Measure.isProbabilityMeasure_map (by
unfold toFull
fun_prop)
5 supporting declarations (lemmas, instances)
-
bitMass_nonnegtheorem — Both Bernoulli masses are nonnegative when the probability lies in [0,1].Proof (Lean source)
theorem bitMass_nonneg (p : ℝ) (hp : p ∈ Icc (0 : ℝ) 1) (b : Bool) : 0 ≤ bitMass p b := by cases b <;> simp [bitMass, hp.1, sub_nonneg.mpr hp.2] -
tripleMass_sumtheorem — The eight product Bernoulli masses sum to one for any three real parameters.hypothesesp q₀ q₁ :ℝconclusionProof (Lean source)
theorem tripleMass_sum (p q₀ q₁ : ℝ) : (∑ a : Bool, ∑ y₀ : Bool, ∑ y₁ : Bool, tripleMass p q₀ q₁ a y₀ y₁) = 1 := by simp [tripleMass, bitMass] ring -
tripleMass_selected_sumtheorem — Summing the latent remaining marks whose selected selected value is y gives the selected cell cell mass.hypothesesp q₀ q₁ :ℝa y :conclusion= cellMass p q₀ q₁ a yProof (Lean source)
theorem tripleMass_selected_sum (p q₀ q₁ : ℝ) (a y : Bool) : (∑ y₀ : Bool, ∑ y₁ : Bool, if (if a then y₁ else y₀) = y then tripleMass p q₀ q₁ a y₀ y₁ else 0) = cellMass p q₀ q₁ a y := by cases a <;> cases y <;> simp [tripleMass, cellMass, bitMass] <;> ring -
densityLaw_probabilitytheorem — The finite-count density law is a probability measure for a probability base measure, measurable mark probabilities, and pointwise unit-interval bounds.hypothesesX :Type uμ :e q₀ q₁ :X → ℝhe :hq₀ :Measurable q₀hq₁ :Measurable q₁he01 :∀ x, e x ∈ Icc (0 : ℝ) 1hq₀01 :∀ x, q₀ x ∈ Icc (0 : ℝ) 1hq₁01 :∀ x, q₁ x ∈ Icc (0 : ℝ) 1conclusionIsProbabilityMeasure (densityLaw μ e q₀ q₁)Proof (Lean source)
theorem densityLaw_probability {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (he01 : ∀ x, e x ∈ Icc (0 : ℝ) 1) (hq₀01 : ∀ x, q₀ x ∈ Icc (0 : ℝ) 1) (hq₁01 : ∀ x, q₁ x ∈ Icc (0 : ℝ) 1) : IsProbabilityMeasure (densityLaw μ e q₀ q₁) := by -- Expand `withDensity_apply'` on `univ`, use Tonelli on the three finite -- counting factors, and rewrite the innermost sum by `tripleMass_sum`. -- Pointwise bounds turn `ofReal` of each product into a nonnegative real cast. have hbit (p : X → ℝ) (hp : Measurable p) (b : DensityCoord X → Bool) (hb : Measurable b) : Measurable (fun z : DensityCoord X => bitMass (p z.2.2) (b z)) := by unfold bitMass apply Measurable.ite · exact hb (MeasurableSet.singleton true) · exact hp.comp (by fun_prop) · exact measurable_const.sub (hp.comp (by fun_prop)) have hd : Measurable (density e q₀ q₁) := by unfold density tripleMass exact ENNReal.measurable_ofReal.comp (((hbit e he (fun z => z.1) (by fun_prop)).mul (hbit q₀ hq₀ (fun z => z.2.1.1) (by fun_prop))).mul (hbit q₁ hq₁ (fun z => z.2.1.2) (by fun_prop))) have hn (x : X) (a y₀ y₁ : Bool) : 0 ≤ tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁ := by unfold tripleMass exact mul_nonneg (mul_nonneg (bitMass_nonneg _ (he01 x) _) (bitMass_nonneg _ (hq₀01 x) _)) (bitMass_nonneg _ (hq₁01 x) _) have hsum (x : X) : (∑ a : Bool, ∑ y₀ : Bool, ∑ y₁ : Bool, density e q₀ q₁ (a, ((y₀, y₁), x))) = 1 := by simp only [density] calc (∑ a : Bool, ∑ y₀ : Bool, ∑ y₁ : Bool, ofReal (tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁)) = ∑ a : Bool, ∑ y₀ : Bool, ofReal (∑ y₁ : Bool, tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁) := by apply Finset.sum_congr rfl intro a _ apply Finset.sum_congr rfl intro y₀ _ exact (ENNReal.ofReal_sum_of_nonneg (fun y₁ _ => hn x a y₀ y₁)).symm _ = ∑ a : Bool, ofReal (∑ y₀ : Bool, ∑ y₁ : Bool, tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁) := by apply Finset.sum_congr rfl intro a _ exact (ENNReal.ofReal_sum_of_nonneg (fun y₀ _ => Finset.sum_nonneg fun y₁ _ => hn x a y₀ y₁)).symm _ = ofReal (∑ a : Bool, ∑ y₀ : Bool, ∑ y₁ : Bool, tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁) := by exact (ENNReal.ofReal_sum_of_nonneg (fun a _ => Finset.sum_nonneg fun y₀ _ => Finset.sum_nonneg fun y₁ _ => hn x a y₀ y₁)).symm _ = 1 := by rw [tripleMass_sum]; norm_num refine ⟨?_⟩ rw [densityLaw, withDensity_apply _ MeasurableSet.univ, setLIntegral_univ] rw [reference, lintegral_prod_symm' _ hd] simp only [lintegral_count, tsum_fintype] rw [lintegral_prod_symm' _ (by fun_prop)] have hinner (x : X) : (∫⁻ z : Bool × Bool, ∑ a : Bool, density e q₀ q₁ (a, (z, x)) ∂(Measure.count : Measure Bool).prod (Measure.count : Measure Bool)) = ∑ y₀ : Bool, ∑ y₁ : Bool, ∑ a : Bool, density e q₀ q₁ (a, ((y₀, y₁), x)) := by rw [lintegral_prod _ (by exact (measurable_of_finite _).aemeasurable)] simp only [lintegral_count, tsum_fintype] have hsum' (x : X) : (∑ y₀ : Bool, ∑ y₁ : Bool, ∑ a : Bool, density e q₀ q₁ (a, ((y₀, y₁), x))) = 1 := by calc _ = ∑ a : Bool, ∑ y₀ : Bool, ∑ y₁ : Bool, density e q₀ q₁ (a, ((y₀, y₁), x)) := by simp only [Fintype.sum_bool] ac_rfl _ = 1 := hsum x calc _ = ∫⁻ x, (∑ y₀ : Bool, ∑ y₁ : Bool, ∑ a : Bool, density e q₀ q₁ (a, ((y₀, y₁), x))) ∂μ := by apply lintegral_congr intro x exact hinner x _ = ∫⁻ _ : X, (1 : ℝ≥0∞) ∂μ := by apply lintegral_congr intro x exact hsum' x _ = 1 := by simp
Selection 4 core · 6 supporting The selected law is an independent four-cell density over first mark and the realized selected value. ★ jointLaw_selectMark_map
Selected Bernoulli cells
The selected law is an independent four-cell density over first mark and the realized selected value. Its equality with the three-mark observation pushforward and the four measurable base-cell integrals are stated here.
def selectMark reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The selected observation of a three-mark point retains the base and first mark of that point and keeps only the remaining mark that the first mark selects: the second remaining mark when the first mark is true, the first remaining mark when it is false.
Definition (Lean source)
parameters
X :
Type u
z :
def
given by
(z.1, (z.2.1, if z.2.1 then z.2.2.2 else z.2.2.1))
def selectedDensity reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The selected four-cell density at a cell (first mark, selected value) and base value uses first-mark probability and remaining-mark probabilities: it is the selected cell mass of that cell at that base value, read as an extended nonnegative number (a negative value is replaced by zero).
def selectedLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The explicit selected four-cell law weights the product of counting measure on the four cells and the base measure by the selected cell probabilities, then reorders coordinates to put the base first.
Definition (Lean source)
parameters
def
theorem jointLaw_selectMark_map reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The pushforward of the three-mark law under observation is the explicit four-cell selected law for a probability base measure, measurable mark probabilities, and unit-interval bounds.
Formal statement
hypotheses
X :
Type u
μ :
e q₀ q₁ :
X → ℝ
he :
hq₀ :
Measurable q₀
hq₁ :
Measurable q₁
he01 :
∀ x, e x ∈ Icc (0 : ℝ) 1
hq₀01 :
∀ x, q₀ x ∈ Icc (0 : ℝ) 1
hq₁01 :
∀ x, q₁ x ∈ Icc (0 : ℝ) 1
conclusion
Proof (Lean source)
theorem jointLaw_selectMark_map {X : Type u} [MeasurableSpace X]
(μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ)
(he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁)
(he01 : ∀ x, e x ∈ Icc (0 : ℝ) 1)
(hq₀01 : ∀ x, q₀ x ∈ Icc (0 : ℝ) 1)
(hq₁01 : ∀ x, q₁ x ∈ Icc (0 : ℝ) 1) :
(jointLaw μ e q₀ q₁).map selectMark = selectedLaw μ e q₀ q₁ := by
classical
have hTo : Measurable (toFull (X := X)) := by
unfold toFull
fun_prop
have hObs : Measurable (selectMark (X := X)) := by
unfold selectMark
apply Measurable.prodMk
· fun_prop
· apply Measurable.prodMk
· fun_prop
· apply Measurable.ite
· measurability
· fun_prop
· fun_prop
have hComp : Measurable (selectMark ∘ toFull : DensityCoord X → SelectedCoord X) :=
hObs.comp hTo
apply Measure.ext
intro S hS
let E : Set (DensityCoord X) :=
{z | (z.2.2, (z.1, if z.1 then z.2.1.2 else z.2.1.1)) ∈ S}
let F : Set ((Bool × Bool) × X) := {z | (z.2, z.1) ∈ S}
have hE : MeasurableSet E := by
unfold E
exact hS.preimage hComp
have hF : MeasurableSet F := by
unfold F
exact hS.preimage (by fun_prop)
have hd : Measurable (density e q₀ q₁) := by
have hbit (p : X → ℝ) (hp : Measurable p)
(b : DensityCoord X → Bool) (hb : Measurable b) :
Measurable (fun z : DensityCoord X => bitMass (p z.2.2) (b z)) := by
unfold bitMass
apply Measurable.ite
· exact hb (MeasurableSet.singleton true)
· exact hp.comp (by fun_prop)
· exact measurable_const.sub (hp.comp (by fun_prop))
unfold density tripleMass
exact ENNReal.measurable_ofReal.comp
(((hbit e he (fun z => z.1) (by fun_prop)).mul
(hbit q₀ hq₀ (fun z => z.2.1.1) (by fun_prop))).mul
(hbit q₁ hq₁ (fun z => z.2.1.2) (by fun_prop)))
have hD : Measurable (selectedDensity e q₀ q₁) := by
unfold selectedDensity cellMass bitMass
apply ENNReal.measurable_ofReal.comp
apply mul
· apply Measurable.ite
· measurability
· exact he.comp (by fun_prop)
· exact measurable_const.sub (he.comp (by fun_prop))
· apply Measurable.ite
· measurability
· apply Measurable.ite
· measurability
· exact hq₁.comp (by fun_prop)
· exact hq₀.comp (by fun_prop)
· exact measurable_const.sub (by
apply Measurable.ite
· measurability
· exact hq₁.comp (by fun_prop)
· exact hq₀.comp (by fun_prop))
rw [jointLaw, Measure.map_map hObs hTo]
rw [Measure.map_apply hComp hS]
change densityLaw μ e q₀ q₁ E = _
rw [selectedLaw, Measure.map_apply (by fun_prop) hS]
change densityLaw μ e q₀ q₁ E =
(((Measure.count : Measure Bool).prod (Measure.count : Measure Bool)).prod μ).withDensity
(selectedDensity e q₀ q₁) F
rw [densityLaw, withDensity_apply _ hE, ← lintegral_indicator hE]
rw [withDensity_apply _ hF, ← lintegral_indicator hF]
rw [reference, lintegral_prod_symm' _ (hd.indicator hE)]
simp only [lintegral_count, tsum_fintype]
conv_lhs => rw [lintegral_prod_symm' _ (by fun_prop)]
conv_rhs => rw [lintegral_prod_symm' _ (hD.indicator hF)]
have hleft (x : X) :
(∫⁻ z : Bool × Bool, ∑ a : Bool, E.indicator (density e q₀ q₁) (a, (z, x))
∂(Measure.count : Measure Bool).prod (Measure.count : Measure Bool)) =
∑ y₀ : Bool, ∑ y₁ : Bool, ∑ a : Bool,
E.indicator (density e q₀ q₁) (a, ((y₀, y₁), x)) := by
rw [lintegral_prod _ (by exact (measurable_of_finite _).aemeasurable)]
simp only [lintegral_count, tsum_fintype]
have hright (x : X) :
(∫⁻ z : Bool × Bool, F.indicator (selectedDensity e q₀ q₁) (z, x)
∂(Measure.count : Measure Bool).prod (Measure.count : Measure Bool)) =
∑ a : Bool, ∑ y : Bool,
F.indicator (selectedDensity e q₀ q₁) ((a, y), x) := by
rw [lintegral_prod _ (by exact (measurable_of_finite _).aemeasurable)]
simp only [lintegral_count, tsum_fintype]
have hnonneg (x : X) (a y₀ y₁ : Bool) :
0 ≤ tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁ := by
unfold tripleMass
exact mul_nonneg (mul_nonneg (bitMass_nonneg _ (he01 x) _)
(bitMass_nonneg _ (hq₀01 x) _)) (bitMass_nonneg _ (hq₁01 x) _)
have hcollapse (x : X) (a y : Bool) :
(∑ y₀ : Bool, ∑ y₁ : Bool,
if (if a then y₁ else y₀) = y then
density e q₀ q₁ (a, ((y₀, y₁), x)) else 0) =
selectedDensity e q₀ q₁ ((a, y), x) := by
have hterm (y₀ y₁ : Bool) :
(if (if a then y₁ else y₀) = y then
density e q₀ q₁ (a, ((y₀, y₁), x)) else 0) =
ofReal (if (if a then y₁ else y₀) = y then
tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁ else 0) := by
split_ifs <;> simp [density]
simp_rw [hterm]
calc
(∑ y₀ : Bool, ∑ y₁ : Bool,
ofReal (if (if a then y₁ else y₀) = y then
tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁ else 0)) =
∑ y₀ : Bool, ofReal (∑ y₁ : Bool,
if (if a then y₁ else y₀) = y then
tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁ else 0) := by
apply Finset.sum_congr rfl
intro y₀ _
exact (ENNReal.ofReal_sum_of_nonneg (fun y₁ _ => by
split_ifs <;> first | exact hnonneg x a y₀ y₁ | exact le_rfl)).symm
_ = ofReal (∑ y₀ : Bool, ∑ y₁ : Bool,
if (if a then y₁ else y₀) = y then
tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁ else 0) := by
exact (ENNReal.ofReal_sum_of_nonneg (fun y₀ _ =>
Finset.sum_nonneg fun y₁ _ => by
split_ifs <;> first | exact hnonneg x a y₀ y₁ | exact le_rfl)).symm
_ = selectedDensity e q₀ q₁ ((a, y), x) := by
rw [tripleMass_selected_sum]
rfl
apply lintegral_congr
intro x
rw [hleft x, hright x]
calc
(∑ y₀ : Bool, ∑ y₁ : Bool, ∑ a : Bool,
E.indicator (density e q₀ q₁) (a, ((y₀, y₁), x))) =
∑ a : Bool, ∑ y₀ : Bool, ∑ y₁ : Bool,
E.indicator (density e q₀ q₁) (a, ((y₀, y₁), x)) := by
simp only [Fintype.sum_bool]
ac_rfl
_ = ∑ a : Bool, ∑ y : Bool,
if (x, (a, y)) ∈ S then selectedDensity e q₀ q₁ ((a, y), x) else 0 := by
apply Finset.sum_congr rfl
intro a _
simp only [Fintype.sum_bool]
rw [← hcollapse x a false, ← hcollapse x a true]
cases a
· by_cases h0 : (x, (false, false)) ∈ S <;>
by_cases h1 : (x, (false, true)) ∈ S <;>
simp [E, indicator, h0, h1]
· by_cases h0 : (x, (true, false)) ∈ S <;>
by_cases h1 : (x, (true, true)) ∈ S <;>
simp [E, indicator, h0, h1] <;> ac_rfl
_ = ∑ a : Bool, ∑ y : Bool,
F.indicator (selectedDensity e q₀ q₁) ((a, y), x) := by
simp [F, indicator]
6 supporting declarations (lemmas, instances)
-
selectedLaw_probabilitytheorem — The explicit selected law is a probability measure for a probability base law, measurable mark probabilities, and unit-interval bounds.hypothesesX :Type uμ :e q₀ q₁ :X → ℝhe :hq₀ :Measurable q₀hq₁ :Measurable q₁he01 :∀ x, e x ∈ Icc (0 : ℝ) 1hq₀01 :∀ x, q₀ x ∈ Icc (0 : ℝ) 1hq₁01 :∀ x, q₁ x ∈ Icc (0 : ℝ) 1conclusionIsProbabilityMeasure (selectedLaw μ e q₀ q₁)Proof (Lean source)
theorem selectedLaw_probability {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (he01 : ∀ x, e x ∈ Icc (0 : ℝ) 1) (hq₀01 : ∀ x, q₀ x ∈ Icc (0 : ℝ) 1) (hq₁01 : ∀ x, q₁ x ∈ Icc (0 : ℝ) 1) : IsProbabilityMeasure (selectedLaw μ e q₀ q₁) := by rw [← jointLaw_selectMark_map μ e q₀ q₁ he hq₀ hq₁ he01 hq₀01 hq₁01] letI : IsProbabilityMeasure (jointLaw μ e q₀ q₁) := jointLaw_probability μ e q₀ q₁ he hq₀ hq₁ he01 hq₀01 hq₁01 have hObs : Measurable (selectMark (X := X)) := by unfold selectMark apply prodMk · fun_prop · apply prodMk · fun_prop · apply Measurable.ite · measurability · fun_prop · fun_prop exact Measure.isProbabilityMeasure_map hObs.aemeasurable -
selectedLaw_celltheorem — An selected cell cell over a measurable base set has the integral of its Bernoulli cell mass, for a base law, measurable mark probabilities, a measurable base set, and the specified cell.hypothesesconclusionselectedLaw μ e q₀ q₁ {z : SelectedCoord X | z.1 ∈ B ∧ z.2.1 = a ∧ z.2.2 = y}= ∫⁻ x in B, ofReal (cellMass (e x) (q₀ x) (q₁ x) a y) ∂μProof (Lean source)
theorem selectedLaw_cell {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (B : Set X) (hB : MeasurableSet B) (a y : Bool) : selectedLaw μ e q₀ q₁ {z : SelectedCoord X | z.1 ∈ B ∧ z.2.1 = a ∧ z.2.2 = y} = ∫⁻ x in B, ofReal (cellMass (e x) (q₀ x) (q₁ x) a y) ∂μ := by classical let E : Set ((Bool × Bool) × X) := {z | z.2 ∈ B ∧ z.1.1 = a ∧ z.1.2 = y} have hE : MeasurableSet E := by unfold E measurability have hF : MeasurableSet {z : SelectedCoord X | z.1 ∈ B ∧ z.2.1 = a ∧ z.2.2 = y} := by measurability have hd : Measurable (selectedDensity e q₀ q₁) := by unfold selectedDensity cellMass bitMass apply ENNReal.measurable_ofReal.comp apply mul · apply Measurable.ite · measurability · exact he.comp (by fun_prop) · exact measurable_const.sub (he.comp (by fun_prop)) · apply Measurable.ite · measurability · apply Measurable.ite · measurability · exact hq₁.comp (by fun_prop) · exact hq₀.comp (by fun_prop) · exact measurable_const.sub (by apply Measurable.ite · measurability · exact hq₁.comp (by fun_prop) · exact hq₀.comp (by fun_prop)) rw [selectedLaw, Measure.map_apply (by fun_prop) hF] change (((Measure.count : Measure Bool).prod (Measure.count : Measure Bool)).prod μ).withDensity (selectedDensity e q₀ q₁) E = _ rw [withDensity_apply _ hE, ← lintegral_indicator hE] rw [lintegral_prod_symm' _ (hd.indicator hE)] have hinner (x : X) : (∫⁻ z : Bool × Bool, E.indicator (selectedDensity e q₀ q₁) (z, x) ∂(Measure.count : Measure Bool).prod (Measure.count : Measure Bool)) = ∑ a' : Bool, ∑ y' : Bool, E.indicator (selectedDensity e q₀ q₁) ((a', y'), x) := by rw [lintegral_prod _ (by exact (measurable_of_finite _).aemeasurable)] simp only [lintegral_count, tsum_fintype] rw [← lintegral_indicator hB] apply lintegral_congr intro x rw [hinner] by_cases hx : x ∈ B · cases a <;> cases y <;> simp [E, indicator, hx, selectedDensity] · simp [E, indicator, hx] -
selectedLaw_cell_00theorem — The untreated, selected-failure cell integral holds over a measurable base set under a probability base law, and measurable mark probabilities.hypothesesconclusion= ∫⁻ x in B, ofReal ((1 - e x) * (1 - q₀ x)) ∂μProof (Lean source)
theorem selectedLaw_cell_00 {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (B : Set X) (hB : MeasurableSet B) : selectedLaw μ e q₀ q₁ {z : SelectedCoord X | z.1 ∈ B ∧ z.2.1 = false ∧ z.2.2 = false} = ∫⁻ x in B, ofReal ((1 - e x) * (1 - q₀ x)) ∂μ := by simpa [cellMass, bitMass] using selectedLaw_cell μ e q₀ q₁ he hq₀ hq₁ B hB false false -
selectedLaw_cell_01theorem — The untreated, selected-success cell integral holds over a measurable base set under a probability base law, and measurable mark probabilities.hypothesesconclusion= ∫⁻ x in B, ofReal ((1 - e x) * q₀ x) ∂μProof (Lean source)
theorem selectedLaw_cell_01 {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (B : Set X) (hB : MeasurableSet B) : selectedLaw μ e q₀ q₁ {z : SelectedCoord X | z.1 ∈ B ∧ z.2.1 = false ∧ z.2.2 = true} = ∫⁻ x in B, ofReal ((1 - e x) * q₀ x) ∂μ := by simpa [cellMass, bitMass] using selectedLaw_cell μ e q₀ q₁ he hq₀ hq₁ B hB false true -
selectedLaw_cell_10theorem — The treated, selected-failure cell integral holds over a measurable base set under a probability base law, and measurable mark probabilities.hypothesesconclusion= ∫⁻ x in B, ofReal (e x * (1 - q₁ x)) ∂μProof (Lean source)
theorem selectedLaw_cell_10 {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (B : Set X) (hB : MeasurableSet B) : selectedLaw μ e q₀ q₁ {z : SelectedCoord X | z.1 ∈ B ∧ z.2.1 = true ∧ z.2.2 = false} = ∫⁻ x in B, ofReal (e x * (1 - q₁ x)) ∂μ := by simpa [cellMass, bitMass] using selectedLaw_cell μ e q₀ q₁ he hq₀ hq₁ B hB true false -
selectedLaw_cell_11theorem — The treated, selected-success cell integral holds over a measurable base set under a probability base law, and measurable mark probabilities.hypothesesconclusion= ∫⁻ x in B, ofReal (e x * q₁ x) ∂μProof (Lean source)
theorem selectedLaw_cell_11 {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (B : Set X) (hB : MeasurableSet B) : selectedLaw μ e q₀ q₁ {z : SelectedCoord X | z.1 ∈ B ∧ z.2.1 = true ∧ z.2.2 = true} = ∫⁻ x in B, ofReal (e x * q₁ x) ∂μ := by simpa [cellMass, bitMass] using selectedLaw_cell μ e q₀ q₁ he hq₀ hq₁ B hB true true
Independence 3 core · 2 supporting The measurable-set identity works for an arbitrary measurable base space. ★ jointLaw_condIndepFun
Conditional independence of the finite marks
The measurable-set identity works for an arbitrary measurable base space. When the space is standard Borel, it is also exposed as Mathlib's formal conditional-independence relation.
def firstMarkSetMass reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The Bernoulli probability of a Boolean first mark set at first-mark probability p for the set s.
def remainingPairSetMass reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The product Bernoulli probability of a remaining-mark-pair set for the two success probabilities and the set t.
theorem jointLaw_condIndepFun reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
Under the base-first joint law, the first mark and the pair of remaining marks are conditionally independent given the σ-algebra generated by the base coordinate, for standard Borel bases, a probability base law, measurable mark probabilities, and unit-interval bounds.
Formal statement
hypotheses
X :
μ :
e q₀ q₁ :
X → ℝ
he :
hq₀ :
Measurable q₀
hq₁ :
Measurable q₁
he01 :
∀ x, e x ∈ Icc (0 : ℝ) 1
hq₀01 :
∀ x, q₀ x ∈ Icc (0 : ℝ) 1
hq₁01 :
∀ x, q₁ x ∈ Icc (0 : ℝ) 1
conclusion
letI : IsProbabilityMeasure (jointLaw μ e q₀ q₁)
Proof (Lean source)
theorem jointLaw_condIndepFun {X : Type u} [MeasurableSpace X]
[StandardBorelSpace X] (μ : Measure X) [IsProbabilityMeasure μ]
(e q₀ q₁ : X → ℝ)
(he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁)
(he01 : ∀ x, e x ∈ Icc (0 : ℝ) 1)
(hq₀01 : ∀ x, q₀ x ∈ Icc (0 : ℝ) 1)
(hq₁01 : ∀ x, q₁ x ∈ Icc (0 : ℝ) 1) :
letI : IsProbabilityMeasure (jointLaw μ e q₀ q₁) :=
jointLaw_probability μ e q₀ q₁ he hq₀ hq₁ he01 hq₀01 hq₁01
CondIndepFun
(comap (fun z : FullCoord X => z.1) inferInstance)
((measurable_fst : Measurable (fun z : FullCoord X => z.1)).comap_le)
(fun z : FullCoord X => z.2.1)
(fun z : FullCoord X => z.2.2)
(jointLaw μ e q₀ q₁) := by
letI : IsProbabilityMeasure (densityLaw μ e q₀ q₁) :=
densityLaw_probability μ e q₀ q₁ he hq₀ hq₁ he01 hq₀01 hq₁01
letI : IsProbabilityMeasure (jointLaw μ e q₀ q₁) :=
jointLaw_probability μ e q₀ q₁ he hq₀ hq₁ he01 hq₀01 hq₁01
change CondIndepFun
(comap (fun z : FullCoord X => z.1) inferInstance)
((measurable_fst : Measurable (fun z : FullCoord X => z.1)).comap_le)
(fun z : FullCoord X => z.2.1) (fun z : FullCoord X => z.2.2)
((densityLaw μ e q₀ q₁).map toFull)
apply condIndepFun_of_map (φ := toFull) (by unfold toFull; fun_prop)
(by fun_prop) (by fun_prop) (by fun_prop)
change CondIndepFun
(comap (fun z : DensityCoord X => z.2.2) inferInstance)
((measurable_snd.comp measurable_snd :
Measurable (fun z : DensityCoord X => z.2.2)).comap_le)
(fun z : DensityCoord X => z.1)
(fun z : DensityCoord X => z.2.1) (densityLaw μ e q₀ q₁)
exact densityLaw_condIndepFun μ e q₀ q₁ he hq₀ hq₁ he01 hq₀01 hq₁01
2 supporting declarations (lemmas, instances)
-
jointLaw_conditional_independent_finitetheorem — The first mark and the remaining-mark pair are conditionally independent given the base: over every measurable base set and all finite mark sets, their joint event has the integral of the product of their conditional probabilities. Assumes a probability base law, measurable probabilities, and a unit-interval bound on the first-mark probability.hypothesesX :Type uμ :e q₀ q₁ :X → ℝhe :hq₀ :Measurable q₀hq₁ :Measurable q₁he01 :∀ x, e x ∈ Icc (0 : ℝ) 1B :Set XhB :conclusion= ∫⁻ x in B, firstMarkSetMass (e x) s * remainingPairSetMass (q₀ x) (q₁ x) t ∂μProof (Lean source)
theorem jointLaw_conditional_independent_finite {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (he01 : ∀ x, e x ∈ Icc (0 : ℝ) 1) (B : Set X) (hB : MeasurableSet B) (s : Set Bool) (t : Set (Bool × Bool)) : jointLaw μ e q₀ q₁ {z : FullCoord X | z.1 ∈ B ∧ z.2.1 ∈ s ∧ z.2.2 ∈ t} = ∫⁻ x in B, firstMarkSetMass (e x) s * remainingPairSetMass (q₀ x) (q₁ x) t ∂μ := by classical let E : Set (DensityCoord X) := {z | z.2.2 ∈ B ∧ z.1 ∈ s ∧ z.2.1 ∈ t} have hE : MeasurableSet E := by unfold E measurability have hF : MeasurableSet {z : FullCoord X | z.1 ∈ B ∧ z.2.1 ∈ s ∧ z.2.2 ∈ t} := by measurability have hbit (p : X → ℝ) (hp : Measurable p) (b : DensityCoord X → Bool) (hb : Measurable b) : Measurable (fun z : DensityCoord X => bitMass (p z.2.2) (b z)) := by unfold bitMass apply Measurable.ite · exact hb (MeasurableSet.singleton true) · exact hp.comp (by fun_prop) · exact measurable_const.sub (hp.comp (by fun_prop)) have hd : Measurable (density e q₀ q₁) := by unfold density tripleMass exact ENNReal.measurable_ofReal.comp (((hbit e he (fun z => z.1) (by fun_prop)).mul (hbit q₀ hq₀ (fun z => z.2.1.1) (by fun_prop))).mul (hbit q₁ hq₁ (fun z => z.2.1.2) (by fun_prop))) rw [jointLaw, Measure.map_apply (by unfold toFull; fun_prop) hF] change densityLaw μ e q₀ q₁ E = _ rw [densityLaw, withDensity_apply _ hE, ← lintegral_indicator hE] rw [reference, lintegral_prod_symm' _ (hd.indicator hE)] simp only [lintegral_count, tsum_fintype] rw [lintegral_prod_symm' _ (by fun_prop)] have hinner (x : X) : (∫⁻ z : Bool × Bool, ∑ a : Bool, E.indicator (density e q₀ q₁) (a, (z, x)) ∂(Measure.count : Measure Bool).prod (Measure.count : Measure Bool)) = ∑ y₀ : Bool, ∑ y₁ : Bool, ∑ a : Bool, E.indicator (density e q₀ q₁) (a, ((y₀, y₁), x)) := by rw [lintegral_prod _ (by exact (measurable_of_finite _).aemeasurable)] simp only [lintegral_count, tsum_fintype] rw [← lintegral_indicator hB] apply lintegral_congr intro x rw [hinner] by_cases hx : x ∈ B · let A : Bool → ℝ≥0∞ := fun a => ofReal (bitMass (e x) a) let P : Bool → Bool → ℝ≥0∞ := fun y₀ y₁ => ofReal (bitMass (q₀ x) y₀ * bitMass (q₁ x) y₁) have hterm (a y₀ y₁ : Bool) : E.indicator (density e q₀ q₁) (a, ((y₀, y₁), x)) = (if a ∈ s then A a else 0) * (if (y₀, y₁) ∈ t then P y₀ y₁ else 0) := by have hf : density e q₀ q₁ (a, ((y₀, y₁), x)) = A a * P y₀ y₁ := by unfold density tripleMass A P rw [mul_assoc, ENNReal.ofReal_mul (bitMass_nonneg _ (he01 x) _)] by_cases ha : a ∈ s <;> by_cases hp : (y₀, y₁) ∈ t <;> simp [indicator, E, hx, ha, hp, hf] simp_rw [hterm] change (∑ y₀ : Bool, ∑ y₁ : Bool, ∑ a : Bool, (if a ∈ s then A a else 0) * (if (y₀, y₁) ∈ t then P y₀ y₁ else 0)) = _ simp only [Set.indicator_of_mem hx] change (∑ y₀ : Bool, ∑ y₁ : Bool, ∑ a : Bool, (if a ∈ s then A a else 0) * (if (y₀, y₁) ∈ t then P y₀ y₁ else 0)) = (∑ a : Bool, if a ∈ s then A a else 0) * (∑ y₀ : Bool, ∑ y₁ : Bool, if (y₀, y₁) ∈ t then P y₀ y₁ else 0) simp only [Finset.mul_sum, Finset.sum_mul] · simp [indicator, E, hx] -
densityLaw_condIndepFuntheorem — The first mark and the remaining-mark pair are conditionally independent given bases in density coordinates when the base space is standard Borel, the base law is a probability measure, the mark probabilities are measurable, and they lie in [0,1].hypothesesX :μ :e q₀ q₁ :X → ℝhe :hq₀ :Measurable q₀hq₁ :Measurable q₁he01 :∀ x, e x ∈ Icc (0 : ℝ) 1hq₀01 :∀ x, q₀ x ∈ Icc (0 : ℝ) 1hq₁01 :∀ x, q₁ x ∈ Icc (0 : ℝ) 1conclusionletI : IsProbabilityMeasure (densityLaw μ e q₀ q₁)Proof (Lean source)
theorem densityLaw_condIndepFun {X : Type u} [MeasurableSpace X] [StandardBorelSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (he01 : ∀ x, e x ∈ Icc (0 : ℝ) 1) (hq₀01 : ∀ x, q₀ x ∈ Icc (0 : ℝ) 1) (hq₁01 : ∀ x, q₁ x ∈ Icc (0 : ℝ) 1) : letI : IsProbabilityMeasure (densityLaw μ e q₀ q₁) := densityLaw_probability μ e q₀ q₁ he hq₀ hq₁ he01 hq₀01 hq₁01 CondIndepFun (comap (fun z : DensityCoord X => z.2.2) inferInstance) ((measurable_snd.comp measurable_snd : Measurable (fun z : DensityCoord X => z.2.2)).comap_le) (fun z : DensityCoord X => z.1) (fun z : DensityCoord X => z.2.1) (densityLaw μ e q₀ q₁) := by letI : IsProbabilityMeasure (densityLaw μ e q₀ q₁) := densityLaw_probability μ e q₀ q₁ he hq₀ hq₁ he01 hq₀01 hq₁01 have hbit (p : X → ℝ) (hp : Measurable p) (b : DensityCoord X → Bool) (hb : Measurable b) : Measurable (fun z : DensityCoord X => bitMass (p z.2.2) (b z)) := by unfold bitMass apply Measurable.ite · exact hb (MeasurableSet.singleton true) · exact hp.comp (by fun_prop) · exact measurable_const.sub (hp.comp (by fun_prop)) have hd : Measurable (density e q₀ q₁) := by unfold density tripleMass exact ENNReal.measurable_ofReal.comp (((hbit e he (fun z => z.1) (by fun_prop)).mul (hbit q₀ hq₀ (fun z => z.2.1.1) (by fun_prop))).mul (hbit q₁ hq₁ (fun z => z.2.1.2) (by fun_prop))) have ha : Measurable (fun z : Bool × X => ofReal (bitMass (e z.2) z.1)) := by unfold bitMass apply ENNReal.measurable_ofReal.comp apply Measurable.ite · exact measurable_fst (MeasurableSet.singleton true) · exact he.comp measurable_snd · exact measurable_const.sub (he.comp measurable_snd) have hb : Measurable (fun z : (Bool × Bool) × X => ofReal (bitMass (q₀ z.2) z.1.1 * bitMass (q₁ z.2) z.1.2)) := by apply ENNReal.measurable_ofReal.comp apply mul · unfold bitMass apply Measurable.ite · exact (measurable_fst.comp measurable_fst) (MeasurableSet.singleton true) · exact hq₀.comp measurable_snd · exact measurable_const.sub (hq₀.comp measurable_snd) · unfold bitMass apply Measurable.ite · exact (measurable_snd.comp measurable_fst) (MeasurableSet.singleton true) · exact hq₁.comp measurable_snd · exact measurable_const.sub (hq₁.comp measurable_snd) have hfactor : density e q₀ q₁ =ᵐ[reference μ] (fun z => ofReal (bitMass (e z.2.2) z.1) * ofReal (bitMass (q₀ z.2.2) z.2.1.1 * bitMass (q₁ z.2.2) z.2.1.2)) := by filter_upwards [] with z unfold density tripleMass rw [mul_assoc] rw [ENNReal.ofReal_mul (bitMass_nonneg _ (he01 _) _)] letI : IsFiniteMeasure ((Measure.count : Measure Bool).prod (((Measure.count : Measure Bool).prod (Measure.count : Measure Bool)).prod μ) |>.withDensity (density e q₀ q₁)) := by change IsFiniteMeasure (densityLaw μ e q₀ q₁) infer_instance exact condIndepFun_threeBlock_of_density_factors (Measure.count : Measure Bool) ((Measure.count : Measure Bool).prod (Measure.count : Measure Bool)) μ hd _ _ ha hb hfactor
Marginal 1 core · 2 supporting Finite Boolean summation removes the three marks and recovers the original base law. ★ jointLaw_base_marginal
Base marginal and support transfer
Finite Boolean summation removes the three marks and recovers the original base law. Full-mass measurable support sets then transfer to three marks.
theorem jointLaw_base_marginal reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
The base marginal of the public joint law equals μ for a probability base law μ when mark probabilities are measurable and unit-interval valued.
Formal statement
hypotheses
X :
Type u
μ :
e q₀ q₁ :
X → ℝ
he :
hq₀ :
Measurable q₀
hq₁ :
Measurable q₁
he01 :
∀ x, e x ∈ Icc (0 : ℝ) 1
hq₀01 :
∀ x, q₀ x ∈ Icc (0 : ℝ) 1
hq₁01 :
∀ x, q₁ x ∈ Icc (0 : ℝ) 1
Proof (Lean source)
theorem jointLaw_base_marginal {X : Type u} [MeasurableSpace X]
(μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ)
(he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁)
(he01 : ∀ x, e x ∈ Icc (0 : ℝ) 1)
(hq₀01 : ∀ x, q₀ x ∈ Icc (0 : ℝ) 1)
(hq₁01 : ∀ x, q₁ x ∈ Icc (0 : ℝ) 1) :
(jointLaw μ e q₀ q₁).map (fun z : FullCoord X => z.1) = μ := by
-- Compose the two measurable coordinate maps and apply
-- `densityLaw_base_marginal`.
unfold jointLaw
rw [Measure.map_map (by fun_prop) (by unfold toFull; fun_prop)]
change (densityLaw μ e q₀ q₁).map
(fun z : DensityCoord X => z.2.2) = μ
exact densityLaw_base_marginal μ e q₀ q₁ he hq₀ hq₁ he01 hq₀01 hq₁01
2 supporting declarations (lemmas, instances)
-
densityLaw_base_marginaltheorem — The base marginal in density coordinates equals μ when the three probabilities are measurable and unit-interval valued.hypothesesX :Type uμ :e q₀ q₁ :X → ℝhe :hq₀ :Measurable q₀hq₁ :Measurable q₁he01 :∀ x, e x ∈ Icc (0 : ℝ) 1hq₀01 :∀ x, q₀ x ∈ Icc (0 : ℝ) 1hq₁01 :∀ x, q₁ x ∈ Icc (0 : ℝ) 1conclusionProof (Lean source)
theorem densityLaw_base_marginal {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (he01 : ∀ x, e x ∈ Icc (0 : ℝ) 1) (hq₀01 : ∀ x, q₀ x ∈ Icc (0 : ℝ) 1) (hq₁01 : ∀ x, q₁ x ∈ Icc (0 : ℝ) 1) : (densityLaw μ e q₀ q₁).map (fun z : DensityCoord X => z.2.2) = μ := by -- Compare lintegrals against arbitrary measurable nonnegative test functions. -- Tonelli over the three Boolean counting measures leaves their total -- product mass, which is one by `tripleMass_sum`. The proof of -- `densityLaw_probability` already carries the measurable-density and -- `ofReal` finite-sum calculations needed here; the extra test function -- depends only on `x`, so it factors out after swapping the integrals. have hbit (p : X → ℝ) (hp : Measurable p) (b : DensityCoord X → Bool) (hb : Measurable b) : Measurable (fun z : DensityCoord X => bitMass (p z.2.2) (b z)) := by unfold bitMass apply Measurable.ite · exact hb (MeasurableSet.singleton true) · exact hp.comp (by fun_prop) · exact measurable_const.sub (hp.comp (by fun_prop)) have hd : Measurable (density e q₀ q₁) := by unfold density tripleMass exact ENNReal.measurable_ofReal.comp (((hbit e he (fun z => z.1) (by fun_prop)).mul (hbit q₀ hq₀ (fun z => z.2.1.1) (by fun_prop))).mul (hbit q₁ hq₁ (fun z => z.2.1.2) (by fun_prop))) have hn (x : X) (a y₀ y₁ : Bool) : 0 ≤ tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁ := by unfold tripleMass exact mul_nonneg (mul_nonneg (bitMass_nonneg _ (he01 x) _) (bitMass_nonneg _ (hq₀01 x) _)) (bitMass_nonneg _ (hq₁01 x) _) have hsum (x : X) : (∑ a : Bool, ∑ y₀ : Bool, ∑ y₁ : Bool, density e q₀ q₁ (a, ((y₀, y₁), x))) = 1 := by simp only [density] calc (∑ a : Bool, ∑ y₀ : Bool, ∑ y₁ : Bool, ofReal (tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁)) = ∑ a : Bool, ∑ y₀ : Bool, ofReal (∑ y₁ : Bool, tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁) := by apply Finset.sum_congr rfl intro a _ apply Finset.sum_congr rfl intro y₀ _ exact (ENNReal.ofReal_sum_of_nonneg (fun y₁ _ => hn x a y₀ y₁)).symm _ = ∑ a : Bool, ofReal (∑ y₀ : Bool, ∑ y₁ : Bool, tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁) := by apply Finset.sum_congr rfl intro a _ exact (ENNReal.ofReal_sum_of_nonneg (fun y₀ _ => Finset.sum_nonneg fun y₁ _ => hn x a y₀ y₁)).symm _ = ofReal (∑ a : Bool, ∑ y₀ : Bool, ∑ y₁ : Bool, tripleMass (e x) (q₀ x) (q₁ x) a y₀ y₁) := by exact (ENNReal.ofReal_sum_of_nonneg (fun a _ => Finset.sum_nonneg fun y₀ _ => Finset.sum_nonneg fun y₁ _ => hn x a y₀ y₁)).symm _ = 1 := by rw [tripleMass_sum]; norm_num refine Measure.ext_of_lintegral μ (fun f hf => ?_) rw [lintegral_map hf (by fun_prop), densityLaw] rw [lintegral_withDensity_eq_lintegral_mul (reference μ) hd (show Measurable (fun z : DensityCoord X => f z.2.2) from hf.comp (by fun_prop))] change (∫⁻ z : DensityCoord X, density e q₀ q₁ z * f z.2.2 ∂reference μ) = _ rw [reference, lintegral_prod_symm' _ (show Measurable (fun z : DensityCoord X => density e q₀ q₁ z * f z.2.2) from hd.mul (hf.comp (by fun_prop)))] simp only [lintegral_count, tsum_fintype] rw [lintegral_prod_symm' _ (by fun_prop)] have hinner (x : X) : (∫⁻ z : Bool × Bool, ∑ a : Bool, (density e q₀ q₁ (a, (z, x)) * f x) ∂(Measure.count : Measure Bool).prod (Measure.count : Measure Bool)) = ∑ y₀ : Bool, ∑ y₁ : Bool, ∑ a : Bool, density e q₀ q₁ (a, ((y₀, y₁), x)) * f x := by rw [lintegral_prod _ (by exact (measurable_of_finite _).aemeasurable)] simp only [lintegral_count, tsum_fintype] calc _ = ∫⁻ x, (∑ y₀ : Bool, ∑ y₁ : Bool, ∑ a : Bool, density e q₀ q₁ (a, ((y₀, y₁), x)) * f x) ∂μ := by apply lintegral_congr intro x exact hinner x _ = ∫⁻ x, f x ∂μ := by apply lintegral_congr intro x simp_rw [← Finset.sum_mul] have hs : (∑ y₀ : Bool, ∑ y₁ : Bool, ∑ a : Bool, density e q₀ q₁ (a, ((y₀, y₁), x))) = 1 := by simp only [Fintype.sum_bool] have h := hsum x simp only [Fintype.sum_bool] at h convert h using 1; ac_rfl rw [hs, one_mul] -
jointLaw_full_supporttheorem — A measurable base support set of full μ mass also has full mass under the joint law, assuming its measurability, full base mass, measurable marks, and unit-interval mark probabilities.hypothesesX :Type uμ :e q₀ q₁ :X → ℝhe :hq₀ :Measurable q₀hq₁ :Measurable q₁he01 :∀ x, e x ∈ Icc (0 : ℝ) 1hq₀01 :∀ x, q₀ x ∈ Icc (0 : ℝ) 1hq₁01 :∀ x, q₁ x ∈ Icc (0 : ℝ) 1B :Set XhB :hμB :μ B = 1Proof (Lean source)
theorem jointLaw_full_support {X : Type u} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (e q₀ q₁ : X → ℝ) (he : Measurable e) (hq₀ : Measurable q₀) (hq₁ : Measurable q₁) (he01 : ∀ x, e x ∈ Icc (0 : ℝ) 1) (hq₀01 : ∀ x, q₀ x ∈ Icc (0 : ℝ) 1) (hq₁01 : ∀ x, q₁ x ∈ Icc (0 : ℝ) 1) (B : Set X) (hB : MeasurableSet B) (hμB : μ B = 1) : jointLaw μ e q₀ q₁ {z : FullCoord X | z.1 ∈ B} = 1 := by -- Evaluate `jointLaw_base_marginal` on `B` using `Measure.map_apply`. have hm := jointLaw_base_marginal μ e q₀ q₁ he hq₀ hq₁ he01 hq₀01 hq₁01 have h := congrArg (fun ν : Measure X => ν B) hm rw [Measure.map_apply (by fun_prop) hB] at h exact h.trans hμB
Parameters 4 core · 11 supporting Parameters packages the base measure, mark probabilities, and hypotheses so model structures can obtain the full and selected laws with short field lemmas. ★ condIndepFun
Packaged Bernoulli marking assumptions
Parameters packages the base measure, mark probabilities, and hypotheses
so model structures can obtain the full and selected laws with short field lemmas.
structure Parameters reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli
A reusable package of Bernoulli-marking parameters over a measurable base space records a probability measure, three measurable success probabilities, and their pointwise unit-interval bounds.
Definition (Lean source)
parameters
X :
Type u
fields
μ :
Measure X
μ_prob :
e :
X → ℝ
q₀ :
X → ℝ
q₁ :
X → ℝ
he :
hq₀ :
Measurable q₀
hq₁ :
Measurable q₁
he01 :
∀ x, e x ∈ Icc (0 : ℝ) 1
hq₀01 :
∀ x, q₀ x ∈ Icc (0 : ℝ) 1
hq₁01 :
∀ x, q₁ x ∈ Icc (0 : ℝ) 1
def fullLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli.Parameters
The three-mark law associated with a parameter package uses its base law and mark probabilities.
Definition (Lean source)
def selected reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli.Parameters
The selected-mark law associated with a parameter package uses its base law and four Bernoulli cell masses.
Definition (Lean source)
theorem condIndepFun reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.ThreeBernoulli.Parameters
Under the packaged three-mark law, the first mark and the pair of remaining marks are conditionally independent given the σ-algebra generated by the base coordinate, for standard Borel bases and valid Bernoulli parameters.
Formal statement
Proof (Lean source)
theorem condIndepFun {X : Type u} [MeasurableSpace X] [StandardBorelSpace X]
(P : Parameters X) :
letI : IsProbabilityMeasure P.μ := P.μ_prob
letI : IsProbabilityMeasure P.fullLaw := P.fullLaw_probability
CondIndepFun
(comap (fun z : FullCoord X => z.1) inferInstance)
((measurable_fst : Measurable (fun z : FullCoord X => z.1)).comap_le)
(fun z : FullCoord X => z.2.1)
(fun z : FullCoord X => z.2.2) P.fullLaw := by
letI : IsProbabilityMeasure P.μ := P.μ_prob
simpa [fullLaw] using
jointLaw_condIndepFun P.μ P.e P.q₀ P.q₁
P.he P.hq₀ P.hq₁ P.he01 P.hq₀01 P.hq₁01
11 supporting declarations (lemmas, instances)
-
fullLaw_probabilitytheorem — The packaged three-mark law is a probability measure for valid Bernoulli parameters.Proof (Lean source)
theorem fullLaw_probability {X : Type u} [MeasurableSpace X] (P : Parameters X) : IsProbabilityMeasure P.fullLaw := by letI : IsProbabilityMeasure P.μ := P.μ_prob exact jointLaw_probability P.μ P.e P.q₀ P.q₁ P.he P.hq₀ P.hq₁ P.he01 P.hq₀01 P.hq₁01 -
selected_probabilitytheorem — The packaged selected law is a probability measure for valid Bernoulli parameters.Proof (Lean source)
theorem selected_probability {X : Type u} [MeasurableSpace X] (P : Parameters X) : IsProbabilityMeasure P.selected := by letI : IsProbabilityMeasure P.μ := P.μ_prob exact selectedLaw_probability P.μ P.e P.q₀ P.q₁ P.he P.hq₀ P.hq₁ P.he01 P.hq₀01 P.hq₁01 -
base_marginaltheorem — The packaged three-mark base marginal is the supplied base law for valid Bernoulli parameters.Proof (Lean source)
theorem base_marginal {X : Type u} [MeasurableSpace X] (P : Parameters X) : P.fullLaw.map (fun z : FullCoord X => z.1) = P.μ := by letI : IsProbabilityMeasure P.μ := P.μ_prob exact jointLaw_base_marginal P.μ P.e P.q₀ P.q₁ P.he P.hq₀ P.hq₁ P.he01 P.hq₀01 P.hq₁01 -
full_supporttheorem — A measurable full-mass base set has full mass under packaged three marks for valid parameters, a measurable set, and full base mass.hypothesesconclusionP.fullLaw {z : FullCoord X | z.1 ∈ B} = 1Proof (Lean source)
theorem full_support {X : Type u} [MeasurableSpace X] (P : Parameters X) (B : Set X) (hB : MeasurableSet B) (hμB : P.μ B = 1) : P.fullLaw {z : FullCoord X | z.1 ∈ B} = 1 := by letI : IsProbabilityMeasure P.μ := P.μ_prob exact jointLaw_full_support P.μ P.e P.q₀ P.q₁ P.he P.hq₀ P.hq₁ P.he01 P.hq₀01 P.hq₁01 B hB hμB -
selectMark_maptheorem — The observation pushforward of packaged three marks equals the packaged selected law for valid Bernoulli parameters.Proof (Lean source)
theorem selectMark_map {X : Type u} [MeasurableSpace X] (P : Parameters X) : P.fullLaw.map selectMark = P.selected := by letI : IsProbabilityMeasure P.μ := P.μ_prob exact jointLaw_selectMark_map P.μ P.e P.q₀ P.q₁ P.he P.hq₀ P.hq₁ P.he01 P.hq₀01 P.hq₁01 -
conditional_independence_finitetheorem — The packaged marks satisfy finite-set conditional independence given the base for valid parameters, a measurable base set, and mark sets.hypothesesconclusionP.fullLaw {z : FullCoord X | z.1 ∈ B ∧ z.2.1 ∈ s ∧ z.2.2 ∈ t}= ∫⁻ x in B, firstMarkSetMass (P.e x) s * remainingPairSetMass (P.q₀ x) (P.q₁ x) t ∂P.μProof (Lean source)
theorem conditional_independence_finite {X : Type u} [MeasurableSpace X] (P : Parameters X) (B : Set X) (hB : MeasurableSet B) (s : Set Bool) (t : Set (Bool × Bool)) : P.fullLaw {z : FullCoord X | z.1 ∈ B ∧ z.2.1 ∈ s ∧ z.2.2 ∈ t} = ∫⁻ x in B, firstMarkSetMass (P.e x) s * remainingPairSetMass (P.q₀ x) (P.q₁ x) t ∂P.μ := by letI : IsProbabilityMeasure P.μ := P.μ_prob exact jointLaw_conditional_independent_finite P.μ P.e P.q₀ P.q₁ P.he P.hq₀ P.hq₁ P.he01 B hB s t -
selected_celltheorem — The packaged selected cell event has its cell-mass integral for valid parameters, a measurable base set, and the selected cell.hypothesesconclusionP.selected {z : SelectedCoord X | z.1 ∈ B ∧ z.2.1 = a ∧ z.2.2 = y}= ∫⁻ x in B, ofReal (cellMass (P.e x) (P.q₀ x) (P.q₁ x) a y) ∂P.μProof (Lean source)
theorem selected_cell {X : Type u} [MeasurableSpace X] (P : Parameters X) (B : Set X) (hB : MeasurableSet B) (a y : Bool) : P.selected {z : SelectedCoord X | z.1 ∈ B ∧ z.2.1 = a ∧ z.2.2 = y} = ∫⁻ x in B, ofReal (cellMass (P.e x) (P.q₀ x) (P.q₁ x) a y) ∂P.μ := by letI : IsProbabilityMeasure P.μ := P.μ_prob exact selectedLaw_cell P.μ P.e P.q₀ P.q₁ P.he P.hq₀ P.hq₁ B hB a y -
selected_cell_00theorem — The packaged untreated-failure cell has mass given by the integral of (1-e)(1-q₀) over a measurable base set for valid parameters.hypothesesconclusion= ∫⁻ x in B, ofReal ((1 - P.e x) * (1 - P.q₀ x)) ∂P.μProof (Lean source)
theorem selected_cell_00 {X : Type u} [MeasurableSpace X] (P : Parameters X) (B : Set X) (hB : MeasurableSet B) : P.selected {z : SelectedCoord X | z.1 ∈ B ∧ z.2.1 = false ∧ z.2.2 = false} = ∫⁻ x in B, ofReal ((1 - P.e x) * (1 - P.q₀ x)) ∂P.μ := by letI : IsProbabilityMeasure P.μ := P.μ_prob exact selectedLaw_cell_00 P.μ P.e P.q₀ P.q₁ P.he P.hq₀ P.hq₁ B hB -
selected_cell_01theorem — The packaged untreated-success cell has mass given by the integral of (1-e)q₀ over a measurable base set for valid parameters.hypothesesconclusion= ∫⁻ x in B, ofReal ((1 - P.e x) * P.q₀ x) ∂P.μProof (Lean source)
theorem selected_cell_01 {X : Type u} [MeasurableSpace X] (P : Parameters X) (B : Set X) (hB : MeasurableSet B) : P.selected {z : SelectedCoord X | z.1 ∈ B ∧ z.2.1 = false ∧ z.2.2 = true} = ∫⁻ x in B, ofReal ((1 - P.e x) * P.q₀ x) ∂P.μ := by letI : IsProbabilityMeasure P.μ := P.μ_prob exact selectedLaw_cell_01 P.μ P.e P.q₀ P.q₁ P.he P.hq₀ P.hq₁ B hB -
selected_cell_10theorem — The packaged treated-failure cell has mass given by the integral of e(1-q₁) over a measurable base set for valid parameters.hypothesesconclusion= ∫⁻ x in B, ofReal (P.e x * (1 - P.q₁ x)) ∂P.μProof (Lean source)
theorem selected_cell_10 {X : Type u} [MeasurableSpace X] (P : Parameters X) (B : Set X) (hB : MeasurableSet B) : P.selected {z : SelectedCoord X | z.1 ∈ B ∧ z.2.1 = true ∧ z.2.2 = false} = ∫⁻ x in B, ofReal (P.e x * (1 - P.q₁ x)) ∂P.μ := by letI : IsProbabilityMeasure P.μ := P.μ_prob exact selectedLaw_cell_10 P.μ P.e P.q₀ P.q₁ P.he P.hq₀ P.hq₁ B hB -
selected_cell_11theorem — The packaged treated-success cell has mass given by the integral of eq₁ over a measurable base set for valid parameters.hypothesesconclusion= ∫⁻ x in B, ofReal (P.e x * P.q₁ x) ∂P.μProof (Lean source)
theorem selected_cell_11 {X : Type u} [MeasurableSpace X] (P : Parameters X) (B : Set X) (hB : MeasurableSet B) : P.selected {z : SelectedCoord X | z.1 ∈ B ∧ z.2.1 = true ∧ z.2.2 = true} = ∫⁻ x in B, ofReal (P.e x * P.q₁ x) ∂P.μ := by letI : IsProbabilityMeasure P.μ := P.μ_prob exact selectedLaw_cell_11 P.μ P.e P.q₀ P.q₁ P.he P.hq₀ P.hq₁ B hB