Mathlib.Probability.Independence.Conditional.DensityIntersection
Positive-density graphoid intersection for conditional independence.
Basic 15 core · 13 supporting This module fixes the product ordering and the measurable coordinate maps used by the positive-density intersection theorem. ★ secondThird_subset_fourBlock
Product coordinates and density factorizations
This module fixes the product ordering and the measurable coordinate maps used by the positive-density intersection theorem. It also records the three density-factorization predicates which express the two premises and the desired conclusion. The definitions are measure-theoretic and contain no graph- or paper-specific assumptions.
abbrev FourBlock reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
The canonical sample space for four random blocks, ordered as X, Y, V, and Z.
def xCoord reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
The first coordinate of a four-block sample is its X block.
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
V :
Type uV
Z :
Type uZ
def
given by
fun q => q.1
def yCoord reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
The second coordinate of a four-block sample is its Y block.
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
V :
Type uV
Z :
Type uZ
def
given by
fun q => q.2.1
def vCoord reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
The third coordinate of a four-block sample is its V block.
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
V :
Type uV
Z :
Type uZ
def
given by
fun q => q.2.2.1
def zCoord reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
The fourth coordinate of a four-block sample is its Z block.
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
V :
Type uV
Z :
Type uZ
def
given by
fun q => q.2.2.2
def zvCoord reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
A four-block sample determines the conditioning pair (Z,V).
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
V :
Type uV
Z :
Type uZ
def
given by
fun q => (q.2.2.2, q.2.2.1)
def zyCoord reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
A four-block sample determines the conditioning pair (Z,Y).
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
V :
Type uV
Z :
Type uZ
def
given by
fun q => (q.2.2.2, q.2.1)
def yvCoord reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
A four-block sample determines the combined block (Y,V).
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
V :
Type uV
Z :
Type uZ
def
given by
fun q => (q.2.1, q.2.2.1)
def fourBlockReference reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
Four coordinate reference measures determine their right-associated product reference measure on the canonical four-block sample space.
def FactorsXYGivenZV reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
A density factors according to X ⟂ Y | (Z,V) when it equals, almost everywhere with respect to the product of the four reference measures, a product of one measurable nonnegative extended-real factor depending on (X,V,Z) and another depending on (Y,V,Z).
Definition (Lean source)
def FactorsXVGivenZY reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
A density factors according to X ⟂ V | (Z,Y) when it equals, almost everywhere with respect to the product of the four reference measures, a product of one measurable nonnegative extended-real factor depending on (X,Y,Z) and another depending on (V,Y,Z).
Definition (Lean source)
def FactorsXYVGivenZ reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
A density factors according to X ⟂ (Y,V) | Z when it equals, almost everywhere with respect to the product of the four reference measures, a product of one measurable nonnegative extended-real factor depending on (X,Z) and another depending on (Y,V,Z).
Definition (Lean source)
def fourBlockIndices reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
The union of four finite index blocks, which is the ambient index set on which the finite-coordinate specialization is stated.
Definition (Lean source)
theorem secondThird_subset_fourBlock reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
For four finite coordinate blocks, the union of the second and third blocks is contained in the union of all four.
Formal statement
hypotheses
conclusion
J ∪ K ⊆ fourBlockIndices I J K L
Proof (Lean source)
theorem secondThird_subset_fourBlock : J ∪ K ⊆ fourBlockIndices I J K L := by
intro i hi
simp only [fourBlockIndices, mem_union] at hi ⊢
aesop
def finiteBlockReference reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
Coordinate reference measures determine the product reference measure on assignments to the union of four finite coordinate blocks.
Definition (Lean source)
parameters
def
given by
Measure.pi fun i => μ i
13 supporting declarations (lemmas, instances)
-
measurable_xCoordtheorem — The first-coordinate map of a four-block observation is measurable.hypothesesX :sharedType uXY :sharedType uYV :sharedType uVZ :sharedType uZconclusionMeasurable (@xCoord X Y V Z)Proof (Lean source)
-
measurable_yCoordtheorem — The Y coordinate map on the four-block product is measurable.hypothesesX :sharedType uXY :sharedType uYV :sharedType uVZ :sharedType uZconclusionMeasurable (@yCoord X Y V Z)Proof (Lean source)
@[fun_prop] theorem measurable_yCoord : Measurable (@yCoord X Y V Z) := by exact measurable_fst.comp measurable_snd -
measurable_vCoordtheorem — The V coordinate map on the four-block product is measurable.hypothesesX :sharedType uXY :sharedType uYV :sharedType uVZ :sharedType uZconclusionMeasurable (@vCoord X Y V Z)Proof (Lean source)
@[fun_prop] theorem measurable_vCoord : Measurable (@vCoord X Y V Z) := by exact measurable_fst.comp (measurable_snd.comp measurable_snd) -
measurable_zCoordtheorem — The Z coordinate map on the four-block product is measurable.hypothesesX :sharedType uXY :sharedType uYV :sharedType uVZ :sharedType uZconclusionMeasurable (@zCoord X Y V Z)Proof (Lean source)
@[fun_prop] theorem measurable_zCoord : Measurable (@zCoord X Y V Z) := by exact measurable_snd.comp (measurable_snd.comp measurable_snd) -
measurable_zvCoordtheorem — The conditioning-pair map (Z,V) is measurable.hypothesesX :sharedType uXY :sharedType uYV :sharedType uVZ :sharedType uZconclusionMeasurable (@zvCoord X Y V Z)Proof (Lean source)
@[fun_prop] theorem measurable_zvCoord : Measurable (@zvCoord X Y V Z) := by change Measurable (fun q : X × (Y × (V × Z)) => (q.2.2.2, q.2.2.1)) fun_prop -
measurable_zyCoordtheorem — The conditioning-pair map (Z,Y) is measurable.hypothesesX :sharedType uXY :sharedType uYV :sharedType uVZ :sharedType uZconclusionMeasurable (@zyCoord X Y V Z)Proof (Lean source)
@[fun_prop] theorem measurable_zyCoord : Measurable (@zyCoord X Y V Z) := by change Measurable (fun q : X × (Y × (V × Z)) => (q.2.2.2, q.2.1)) fun_prop -
measurable_yvCoordtheorem — The combined-block map (Y,V) is measurable.hypothesesX :sharedType uXY :sharedType uYV :sharedType uVZ :sharedType uZconclusionMeasurable (@yvCoord X Y V Z)Proof (Lean source)
@[fun_prop] theorem measurable_yvCoord : Measurable (@yvCoord X Y V Z) := by change Measurable (fun q : X × (Y × (V × Z)) => (q.2.1, q.2.2.1)) fun_prop -
first_subset_fourBlocktheorem — The first block is contained in the union of all four blocks.hypothesesconclusionI ⊆ fourBlockIndices I J K LProof (Lean source)
theorem first_subset_fourBlock : I ⊆ fourBlockIndices I J K L := by simp [fourBlockIndices] -
second_subset_fourBlocktheorem — The second block is contained in the union of all four blocks.hypothesesconclusionJ ⊆ fourBlockIndices I J K LProof (Lean source)
theorem second_subset_fourBlock : J ⊆ fourBlockIndices I J K L := by intro i hi simp [fourBlockIndices, hi] -
third_subset_fourBlocktheorem — The third block is contained in the union of all four blocks.hypothesesconclusionK ⊆ fourBlockIndices I J K LProof (Lean source)
theorem third_subset_fourBlock : K ⊆ fourBlockIndices I J K L := by intro i hi simp [fourBlockIndices, hi] -
fourth_subset_fourBlocktheorem — The fourth block is contained in the union of all four blocks.hypothesesconclusionL ⊆ fourBlockIndices I J K LProof (Lean source)
theorem fourth_subset_fourBlock : L ⊆ fourBlockIndices I J K L := by intro i hi simp [fourBlockIndices, hi] -
fourthThird_subset_fourBlocktheorem — The union of the fourth and third blocks is contained in the union of all four blocks.hypothesesconclusionL ∪ K ⊆ fourBlockIndices I J K LProof (Lean source)
theorem fourthThird_subset_fourBlock : L ∪ K ⊆ fourBlockIndices I J K L := by intro i hi simp only [fourBlockIndices, mem_union] at hi ⊢ aesop -
fourthSecond_subset_fourBlocktheorem — The union of the fourth and second blocks is contained in the union of all four blocks.hypothesesconclusionL ∪ J ⊆ fourBlockIndices I J K LProof (Lean source)
theorem fourthSecond_subset_fourBlock : L ∪ J ⊆ fourBlockIndices I J K L := by intro i hi simp only [fourBlockIndices, mem_union] at hi ⊢ aesop
ThreeBlockMarginals 11 core · 6 supporting This module fixes the canonical three-block coordinates and isolates the Tonelli calculations identifying every marginal law used by the conditional-independence bridge. ★ map_thirdThreeCoord_withDensity
Marginal laws of a three-block product density
This module fixes the canonical three-block coordinates and isolates the Tonelli calculations identifying every marginal law used by the conditional-independence bridge. In particular, it records the laws of the conditioning block, each random block paired with the conditioning block, and the fully reordered triple.
abbrev ThreeBlock reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
The canonical sample space for two random blocks and one conditioning block.
Definition (Lean source)
parameters
A :
Type uA
B :
Type uB
C :
Type uC
def
given by
A × (B × C)
def firstThreeCoord reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
The first random coordinate of a canonical three-block sample.
Definition (Lean source)
parameters
A :
Type uA
B :
Type uB
C :
Type uC
def
given by
fun q ↦ q.1
def secondThreeCoord reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
The second random coordinate of a canonical three-block sample.
Definition (Lean source)
parameters
A :
Type uA
B :
Type uB
C :
Type uC
def
given by
fun q ↦ q.2.1
def thirdThreeCoord reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
The conditioning coordinate of a canonical three-block sample.
Definition (Lean source)
parameters
A :
Type uA
B :
Type uB
C :
Type uC
def
given by
fun q ↦ q.2.2
def threeBlockReference reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
Three coordinate reference measures determine the right-associated product reference measure on the canonical three-block sample space.
def densityFirstConditioning reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
Integrating a three-block density over the second random block gives its first-and-conditioning marginal density.
Definition (Lean source)
parameters
A :
Type uA
B :
Type uB
C :
Type uC
muB :
Measure B
d :
ThreeBlock A B C → ℝ≥0∞
def
densityFirstConditioning muB d :
A × C → ℝ≥0∞
given by
fun ac ↦ ∫⁻ b, d (ac.1, (b, ac.2)) ∂muB
def densitySecondConditioning reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
Integrating a three-block density over the first random block gives its second-and-conditioning marginal density.
Definition (Lean source)
parameters
A :
Type uA
B :
Type uB
C :
Type uC
muA :
Measure A
d :
ThreeBlock A B C → ℝ≥0∞
def
densitySecondConditioning muA d :
B × C → ℝ≥0∞
given by
fun bc ↦ ∫⁻ a, d (a, (bc.1, bc.2)) ∂muA
def densityConditioning reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
Integrating a three-block density over both random blocks gives its conditioning marginal density.
Definition (Lean source)
parameters
A :
Type uA
B :
Type uB
C :
Type uC
muA :
Measure A
muB :
Measure B
d :
ThreeBlock A B C → ℝ≥0∞
def
densityConditioning muA muB d :
C → ℝ≥0∞
given by
fun c ↦ ∫⁻ a, ∫⁻ b, d (a, (b, c)) ∂muB ∂muA
def ThreeBlockFactors reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
A three-block density factors given its third block when it equals, almost everywhere with respect to the product of the three reference measures, the product of two measurable nonnegative extended-real terms, one depending on (A,C) and the other on (B,C).
Definition (Lean source)
parameters
A :
Type uA
B :
Type uB
C :
Type uC
muA :
Measure A
muB :
Measure B
muC :
Measure C
d :
ThreeBlock A B C → ℝ≥0∞
def
ThreeBlockFactors muA muB muC d :
Prop
given by
∃ a : A × C → ℝ≥0∞, ∃ b : B × C → ℝ≥0∞,
clause 1
clause 2
clause 3
d =ᵐ[threeBlockReference muA muB muC] (fun q ↦ a (q.1, q.2.2) * b (q.2.1, q.2.2))
def ThreeBlockDensityIdentity reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
The conditional-density identity says that the joint density times the conditioning marginal density equals the product of the two random-block-with-conditioning marginal densities, almost everywhere with respect to the product of the three reference measures.
Definition (Lean source)
parameters
A :
Type uA
B :
Type uB
C :
Type uC
muA :
Measure A
muB :
Measure B
muC :
Measure C
d :
ThreeBlock A B C → ℝ≥0∞
def
ThreeBlockDensityIdentity muA muB muC d :
Prop
given by
∀ᵐ q ∂threeBlockReference muA muB muC, d q * densityConditioning muA muB d q.2.2
= densityFirstConditioning muB d (q.1, q.2.2) * densitySecondConditioning muA d (q.2.1, q.2.2)
theorem map_thirdThreeCoord_withDensity reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
For three σ-finite reference measures and a measurable three-block density, pushing the density-weighted product measure forward to the conditioning coordinate gives the conditioning reference measure weighted by the conditioning marginal density.
Formal statement
hypotheses
A :
Type uA
B :
Type uB
C :
Type uC
hd :
conclusion
= muC.withDensity (densityConditioning muA muB d)
Proof (Lean source)
theorem map_thirdThreeCoord_withDensity (hd : Measurable d) :
((threeBlockReference muA muB muC).withDensity d).map
(@thirdThreeCoord A B C) =
muC.withDensity (densityConditioning muA muB d) := by
/- Prove equality on measurable sets, expand `map` and `withDensity`, then commute the
`C` integral past the `A` and `B` integrals by Tonelli. -/
have hdc : Measurable (densityConditioning muA muB d) := by
unfold densityConditioning
fun_prop
refine Measure.ext_of_lintegral _ fun f hf ↦ ?_
rw [lintegral_map hf measurable_thirdThreeCoord,
lintegral_withDensity_eq_lintegral_mul _ hd (by fun_prop),
lintegral_withDensity_eq_lintegral_mul _ hdc hf]
change (∫⁻ q : A × (B × C), d q * f q.2.2 ∂muA.prod (muB.prod muC)) =
∫⁻ c, (∫⁻ a, ∫⁻ b, d (a, (b, c)) ∂muB ∂muA) * f c ∂muC
rw [lintegral_prod _ (by fun_prop)]
have hBC (a : A) :
(∫⁻ b, ∫⁻ c, d (a, (b, c)) * f c ∂muC ∂muB) =
∫⁻ c, ∫⁻ b, d (a, (b, c)) * f c ∂muB ∂muC := by
exact lintegral_lintegral_swap (by fun_prop)
calc
_ = ∫⁻ a, ∫⁻ b, ∫⁻ c, d (a, (b, c)) * f c ∂muC ∂muB ∂muA := by
apply lintegral_congr
intro a
rw [lintegral_prod _ (by fun_prop)]
_ = ∫⁻ a, ∫⁻ c, ∫⁻ b, d (a, (b, c)) * f c ∂muB ∂muC ∂muA := by
apply lintegral_congr
exact hBC
_ = ∫⁻ c, ∫⁻ a, ∫⁻ b, d (a, (b, c)) * f c ∂muB ∂muA ∂muC := by
exact lintegral_lintegral_swap (by fun_prop)
_ = _ := by
apply lintegral_congr
intro c
calc
_ = ∫⁻ a, (∫⁻ b, d (a, (b, c)) ∂muB) * f c ∂muA := by
apply lintegral_congr
intro a
rw [lintegral_mul_const (f c) (by fun_prop)]
_ = _ := lintegral_mul_const (f c) (by fun_prop)
6 supporting declarations (lemmas, instances)
-
measurable_firstThreeCoordtheorem — The first coordinate map on the three-block product is measurable.hypothesesA :sharedType uAB :sharedType uBC :sharedType uCconclusionMeasurable (@firstThreeCoord A B C)Proof (Lean source)
@[fun_prop] theorem measurable_firstThreeCoord : Measurable (@firstThreeCoord A B C) := measurable_fst -
measurable_secondThreeCoordtheorem — The second coordinate map on the three-block product is measurable.hypothesesA :sharedType uAB :sharedType uBC :sharedType uCconclusionMeasurable (@secondThreeCoord A B C)Proof (Lean source)
@[fun_prop] theorem measurable_secondThreeCoord : Measurable (@secondThreeCoord A B C) := measurable_fst.comp measurable_snd -
measurable_thirdThreeCoordtheorem — The conditioning-coordinate map on the three-block product is measurable.hypothesesA :sharedType uAB :sharedType uBC :sharedType uCconclusionMeasurable (@thirdThreeCoord A B C)Proof (Lean source)
@[fun_prop] theorem measurable_thirdThreeCoord : Measurable (@thirdThreeCoord A B C) := measurable_snd.comp measurable_snd -
map_firstThird_withDensitytheorem — Pushing a measurable three-block product density to the first and conditioning coordinates gives their product reference measure weighted by the first-conditioning marginal density.hypothesesA :sharedType uAB :sharedType uBC :sharedType uChd :conclusion((threeBlockReference muA muB muC).withDensity d).map (fun q ↦ (firstThreeCoord q, thirdThreeCoord q))= (muA.prod muC).withDensity (densityFirstConditioning muB d)Proof (Lean source)
theorem map_firstThird_withDensity (hd : Measurable d) : ((threeBlockReference muA muB muC).withDensity d).map (fun q ↦ (firstThreeCoord q, thirdThreeCoord q)) = (muA.prod muC).withDensity (densityFirstConditioning muB d) := by /- Prove equality on measurable sets and use Tonelli to integrate out `B`; the only coordinate permutation is between the `B` and `C` integrations. -/ have hdAC : Measurable (densityFirstConditioning muB d) := by unfold densityFirstConditioning fun_prop refine Measure.ext_of_lintegral _ fun f hf ↦ ?_ rw [lintegral_map hf (by fun_prop), lintegral_withDensity_eq_lintegral_mul _ hd (by fun_prop), lintegral_withDensity_eq_lintegral_mul _ hdAC hf] change (∫⁻ q : A × (B × C), d q * f (q.1, q.2.2) ∂muA.prod (muB.prod muC)) = ∫⁻ ac : A × C, (∫⁻ b, d (ac.1, (b, ac.2)) ∂muB) * f ac ∂muA.prod muC rw [lintegral_prod _ (by fun_prop)] calc _ = ∫⁻ a, ∫⁻ b, ∫⁻ c, d (a, (b, c)) * f (a, c) ∂muC ∂muB ∂muA := by apply lintegral_congr intro a rw [lintegral_prod _ (by fun_prop)] _ = ∫⁻ a, ∫⁻ c, ∫⁻ b, d (a, (b, c)) * f (a, c) ∂muB ∂muC ∂muA := by apply lintegral_congr intro a exact lintegral_lintegral_swap (by fun_prop) _ = ∫⁻ a, ∫⁻ c, (∫⁻ b, d (a, (b, c)) ∂muB) * f (a, c) ∂muC ∂muA := by apply lintegral_congr intro a apply lintegral_congr intro c rw [lintegral_mul_const (f (a, c)) (by fun_prop)] _ = _ := by rw [lintegral_prod _ (by fun_prop)] -
map_secondThird_withDensitytheorem — Pushing a measurable three-block product density to the second and conditioning coordinates gives their product reference measure weighted by the second-conditioning marginal density.hypothesesA :sharedType uAB :sharedType uBC :sharedType uChd :conclusion((threeBlockReference muA muB muC).withDensity d).map (fun q ↦ (secondThreeCoord q, thirdThreeCoord q))= (muB.prod muC).withDensity (densitySecondConditioning muA d)Proof (Lean source)
theorem map_secondThird_withDensity (hd : Measurable d) : ((threeBlockReference muA muB muC).withDensity d).map (fun q ↦ (secondThreeCoord q, thirdThreeCoord q)) = (muB.prod muC).withDensity (densitySecondConditioning muA d) := by /- Prove equality on measurable sets and use Tonelli to integrate out `A`. -/ have hdBC : Measurable (densitySecondConditioning muA d) := by unfold densitySecondConditioning fun_prop refine Measure.ext_of_lintegral _ fun f hf ↦ ?_ rw [lintegral_map hf (by fun_prop), lintegral_withDensity_eq_lintegral_mul _ hd (by fun_prop), lintegral_withDensity_eq_lintegral_mul _ hdBC hf] change (∫⁻ q : A × (B × C), d q * f (q.2.1, q.2.2) ∂muA.prod (muB.prod muC)) = ∫⁻ bc : B × C, (∫⁻ a, d (a, (bc.1, bc.2)) ∂muA) * f bc ∂muB.prod muC rw [lintegral_prod_symm _ (by fun_prop), lintegral_prod _ (by fun_prop)] calc _ = ∫⁻ b, ∫⁻ c, (∫⁻ a, d (a, (b, c)) ∂muA) * f (b, c) ∂muC ∂muB := by apply lintegral_congr intro b apply lintegral_congr intro c rw [lintegral_mul_const (f (b, c)) (by fun_prop)] _ = _ := by rw [lintegral_prod _ (by fun_prop)] -
map_thirdFirstSecond_withDensitytheorem — Reordering a measurable three-block product density as conditioning-first preserves the law and transports its density by the same coordinate permutation.hypothesesA :sharedType uAB :sharedType uBC :sharedType uChd :conclusion((threeBlockReference muA muB muC).withDensity d).map (fun q ↦ (thirdThreeCoord q, (firstThreeCoord q, secondThreeCoord q)))= (muC.prod (muA.prod muB)).withDensity (fun q ↦ d (q.2.1, (q.2.2, q.1)))Proof (Lean source)
theorem map_thirdFirstSecond_withDensity (hd : Measurable d) : ((threeBlockReference muA muB muC).withDensity d).map (fun q ↦ (thirdThreeCoord q, (firstThreeCoord q, secondThreeCoord q))) = (muC.prod (muA.prod muB)).withDensity (fun q ↦ d (q.2.1, (q.2.2, q.1))) := by /- Prove equality on measurable rectangles, or use successive measurable-equivalence maps and product associativity/commutativity. -/ let e : ThreeBlock A B C ≃ᵐ C × (A × B) := MeasurableEquiv.prodAssoc.symm.trans MeasurableEquiv.prodComm have he : MeasurePreserving e (threeBlockReference muA muB muC) (muC.prod (muA.prod muB)) := by refine ⟨e.measurable, ?_⟩ change Measure.map e (muA.prod (muB.prod muC)) = muC.prod (muA.prod muB) calc Measure.map e (muA.prod (muB.prod muC)) = Measure.map swap (Measure.map MeasurableEquiv.prodAssoc.symm (muA.prod (muB.prod muC))) := by rw [Measure.map_map measurable_swap MeasurableEquiv.prodAssoc.symm.measurable] rfl _ = muC.prod (muA.prod muB) := by rw [← Measure.prodAssoc_prod, MeasurableEquiv.map_symm_map, Measure.prod_swap] change Measure.map e ((threeBlockReference muA muB muC).withDensity d) = _ refine Measure.ext_of_lintegral _ fun f hf ↦ ?_ rw [lintegral_map hf e.measurable, lintegral_withDensity_eq_lintegral_mul _ hd (by fun_prop), lintegral_withDensity_eq_lintegral_mul _ (by fun_prop) hf, ← he.lintegral_comp (by fun_prop)] rfl
Factorization 1 core · 2 supporting This module gives the three product-density factorization characterizations needed by the intersection proof. ★ condIndepFun_xyv_given_z_iff_factors
Conditional independence as density factorization
This module gives the three product-density factorization characterizations needed by the intersection proof. They deliberately use the same canonical four-block product measure, so the subsequent splicing argument does not have to transport almost-everywhere statements across ad hoc reorderings.
theorem condIndepFun_xyv_given_z_iff_factors reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
For four σ-finite reference measures on standard Borel spaces and a measurable density whose weighting of the product reference measure has finite total mass, the first block is conditionally independent of the combined second and third blocks given the fourth, under the density-weighted measure, exactly when the density is almost everywhere a product of a measurable factor of the first and fourth blocks and a measurable factor of the other three blocks.
Formal statement
hypotheses
X :
Type uX
Y :
Type uY
V :
Type uV
Z :
Type uZ
hd :
conclusion
CondIndepFun (comap (@zCoord X Y V Z) inferInstance) measurable_zCoord.comap_le (@xCoord X Y V Z) (@yvCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d)
↔ FactorsXYVGivenZ μX μY μV μZ d
Proof (Lean source)
theorem condIndepFun_xyv_given_z_iff_factors (hd : Measurable d) :
CondIndepFun
(comap (@zCoord X Y V Z) inferInstance)
measurable_zCoord.comap_le (@xCoord X Y V Z) (@yvCoord X Y V Z)
((fourBlockReference μX μY μV μZ).withDensity d) ↔
FactorsXYVGivenZ μX μY μV μZ d := by
let e : (X × ((Y × V) × Z)) ≃ᵐ FourBlock X Y V Z := assocYV
let d' : X × ((Y × V) × Z) → ℝ≥0∞ := d ∘ e
have he : MeasurePreserving e
(threeBlockReference μX (μY.prod μV) μZ)
(fourBlockReference μX μY μV μZ) := by
simpa [e, threeBlockReference, fourBlockReference] using
measurePreserving_assocYV μX μY μV μZ
have hd' : Measurable d' := hd.comp e.measurable
have hlaw :
((threeBlockReference μX (μY.prod μV) μZ).withDensity d').map e =
(fourBlockReference μX μY μV μZ).withDensity d := by
simpa [d'] using Causalean.Mathlib.MeasureTheory.map_withDensity_comp_measurableEquiv e he d
have hlaw' :
((fourBlockReference μX μY μV μZ).withDensity d).map e.symm =
(threeBlockReference μX (μY.prod μV) μZ).withDensity d' := by
rw [← hlaw, Measure.map_map e.symm.measurable e.measurable]
simpa using congrArg
(fun f ↦ Measure.map f
((threeBlockReference μX (μY.prod μV) μZ).withDensity d')) e.symm_comp_self
letI : IsFiniteMeasure
((threeBlockReference μX (μY.prod μV) μZ).withDensity d') := by
rw [← hlaw']
infer_instance
have htransport :
CondIndepFun
(comap (@thirdThreeCoord X (Y × V) Z) inferInstance)
measurable_thirdThreeCoord.comap_le
(@firstThreeCoord X (Y × V) Z) (@secondThreeCoord X (Y × V) Z)
((threeBlockReference μX (μY.prod μV) μZ).withDensity d') ↔
CondIndepFun
(comap (@zCoord X Y V Z) inferInstance)
measurable_zCoord.comap_le
(@xCoord X Y V Z) (@yvCoord X Y V Z)
((fourBlockReference μX μY μV μZ).withDensity d) := by
change CondIndepFun
(comap (fun q : X × ((Y × V) × Z) ↦ q.2.2) inferInstance) _
(fun q : X × ((Y × V) × Z) ↦ q.1) (fun q ↦ q.2.1)
((threeBlockReference μX (μY.prod μV) μZ).withDensity d') ↔ _
simpa [e, assocYV, xCoord, yCoord, vCoord, zCoord, yvCoord, Function.comp_def] using
(condIndepFun_measurableEquiv_iff e hlaw measurable_xCoord measurable_yvCoord
measurable_zCoord)
have hfactors :
ThreeBlockFactors μX (μY.prod μV) μZ d' ↔
FactorsXYVGivenZ μX μY μV μZ d := by
constructor
· rintro ⟨a, b, ha, hb, hab⟩
refine ⟨a, b, ha, hb, ?_⟩
change ∀ᵐ q ∂fourBlockReference μX μY μV μZ,
d q = a (xCoord q, zCoord q) * b ((yCoord q, vCoord q), zCoord q)
rw [← he.map_eq, e.measurableEmbedding.ae_map_iff]
change ∀ᵐ q ∂threeBlockReference μX (μY.prod μV) μZ,
d' q = a (q.1, q.2.2) * b (q.2.1, q.2.2) at hab
simpa [d', e, assocYV, xCoord, yCoord, vCoord, zCoord, Function.comp_def] using hab
· rintro ⟨a, b, ha, hb, hab⟩
refine ⟨a, b, ha, hb, ?_⟩
change ∀ᵐ q ∂threeBlockReference μX (μY.prod μV) μZ,
d' q = a (q.1, q.2.2) * b (q.2.1, q.2.2)
change ∀ᵐ q ∂fourBlockReference μX μY μV μZ,
d q = a (xCoord q, zCoord q) * b ((yCoord q, vCoord q), zCoord q) at hab
rw [← he.map_eq, e.measurableEmbedding.ae_map_iff] at hab
simpa [d', e, assocYV, xCoord, yCoord, vCoord, zCoord, Function.comp_def] using hab
calc
_ ↔ CondIndepFun
(comap (@thirdThreeCoord X (Y × V) Z) inferInstance) _
(@firstThreeCoord X (Y × V) Z) (@secondThreeCoord X (Y × V) Z)
((threeBlockReference μX (μY.prod μV) μZ).withDensity d') := htransport.symm
_ ↔ ThreeBlockFactors μX (μY.prod μV) μZ d' :=
condIndepFun_threeBlock_iff_factors μX (μY.prod μV) μZ hd'
_ ↔ FactorsXYVGivenZ μX μY μV μZ d := hfactors
2 supporting declarations (lemmas, instances)
-
condIndepFun_xy_given_zv_iff_factorstheorem — For four product reference measures and a measurable density, conditional independence of the first and second blocks given the fourth and third is equivalent to the corresponding measurable density factorization.hypothesesX :sharedType uXY :sharedType uYV :sharedType uVZ :sharedType uZhd :conclusionCondIndepFun (comap (@zvCoord X Y V Z) inferInstance) measurable_zvCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d)↔ FactorsXYGivenZV μX μY μV μZ dProof (Lean source)
theorem condIndepFun_xy_given_zv_iff_factors (hd : Measurable d) : CondIndepFun (comap (@zvCoord X Y V Z) inferInstance) measurable_zvCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d) ↔ FactorsXYGivenZV μX μY μV μZ d := by letI : IsFiniteMeasure ((threeBlockReference μX μY (μV.prod μZ)).withDensity d) := by simpa [threeBlockReference, fourBlockReference] using (inferInstance : IsFiniteMeasure ((fourBlockReference μX μY μV μZ).withDensity d)) have hcomap : comap (@zvCoord X Y V Z) inferInstance = comap (@thirdThreeCoord X Y (V × Z)) inferInstance := by apply le_antisymm · exact (show Measurable[ comap (@thirdThreeCoord X Y (V × Z)) inferInstance] (@zvCoord X Y V Z) by change Measurable[ comap (@thirdThreeCoord X Y (V × Z)) inferInstance] (swap ∘ @thirdThreeCoord X Y (V × Z)) exact measurable_swap.comp (Measurable.of_comap_le le_rfl)).comap_le · exact (show Measurable[ comap (@zvCoord X Y V Z) inferInstance] (@thirdThreeCoord X Y (V × Z)) by change Measurable[ comap (@zvCoord X Y V Z) inferInstance] (swap ∘ @zvCoord X Y V Z) exact measurable_swap.comp (Measurable.of_comap_le le_rfl)).comap_le change CondIndepFun (comap (@zvCoord X Y V Z) inferInstance) _ (@firstThreeCoord X Y (V × Z)) (@secondThreeCoord X Y (V × Z)) ((threeBlockReference μX μY (μV.prod μZ)).withDensity d) ↔ ThreeBlockFactors μX μY (μV.prod μZ) d simpa only [hcomap] using (condIndepFun_threeBlock_iff_factors μX μY (μV.prod μZ) hd) -
condIndepFun_xv_given_zy_iff_factorstheorem — For a finite measure with density over a four-fold product reference measure, X ⟂ V | (Z,Y) holds exactly when the density factors into (X,Y,Z) and (V,Y,Z) terms.hypothesesX :sharedType uXY :sharedType uYV :sharedType uVZ :sharedType uZhd :conclusionCondIndepFun (comap (@zyCoord X Y V Z) inferInstance) measurable_zyCoord.comap_le (@xCoord X Y V Z) (@vCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d)↔ FactorsXVGivenZY μX μY μV μZ dProof (Lean source)
theorem condIndepFun_xv_given_zy_iff_factors (hd : Measurable d) : CondIndepFun (comap (@zyCoord X Y V Z) inferInstance) measurable_zyCoord.comap_le (@xCoord X Y V Z) (@vCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d) ↔ FactorsXVGivenZY μX μY μV μZ d := by let e : (X × (V × (Y × Z))) ≃ᵐ FourBlock X Y V Z := permXV let d' : X × (V × (Y × Z)) → ℝ≥0∞ := d ∘ e let yz : FourBlock X Y V Z → Y × Z := fun q ↦ (yCoord q, zCoord q) have he : MeasurePreserving e (threeBlockReference μX μV (μY.prod μZ)) (fourBlockReference μX μY μV μZ) := by simpa [e, threeBlockReference, fourBlockReference] using measurePreserving_permXV μX μY μV μZ have hd' : Measurable d' := hd.comp e.measurable have hlaw : ((threeBlockReference μX μV (μY.prod μZ)).withDensity d').map e = (fourBlockReference μX μY μV μZ).withDensity d := by simpa [d'] using Causalean.Mathlib.MeasureTheory.map_withDensity_comp_measurableEquiv e he d have hlaw' : ((fourBlockReference μX μY μV μZ).withDensity d).map e.symm = (threeBlockReference μX μV (μY.prod μZ)).withDensity d' := by rw [← hlaw, Measure.map_map e.symm.measurable e.measurable] simpa using congrArg (fun f ↦ Measure.map f ((threeBlockReference μX μV (μY.prod μZ)).withDensity d')) e.symm_comp_self letI : IsFiniteMeasure ((threeBlockReference μX μV (μY.prod μZ)).withDensity d') := by rw [← hlaw'] infer_instance have htransport : CondIndepFun (comap (@thirdThreeCoord X V (Y × Z)) inferInstance) measurable_thirdThreeCoord.comap_le (@firstThreeCoord X V (Y × Z)) (@secondThreeCoord X V (Y × Z)) ((threeBlockReference μX μV (μY.prod μZ)).withDensity d') ↔ CondIndepFun (comap yz inferInstance) (show Measurable yz by simp only [yz]; fun_prop).comap_le (@xCoord X Y V Z) (@vCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d) := by change CondIndepFun (comap (fun q : X × (V × (Y × Z)) ↦ q.2.2) inferInstance) _ (fun q : X × (V × (Y × Z)) ↦ q.1) (fun q ↦ q.2.1) ((threeBlockReference μX μV (μY.prod μZ)).withDensity d') ↔ _ simpa [e, permXV, yz, xCoord, yCoord, vCoord, zCoord, Function.comp_def] using (condIndepFun_measurableEquiv_iff e hlaw measurable_xCoord measurable_vCoord (show Measurable yz by simp only [yz]; fun_prop)) have hcomap : comap (@zyCoord X Y V Z) inferInstance = comap yz inferInstance := by apply le_antisymm · exact (show Measurable[comap yz inferInstance] (@zyCoord X Y V Z) by change Measurable[comap yz inferInstance] (swap ∘ yz) exact measurable_swap.comp (Measurable.of_comap_le le_rfl)).comap_le · exact (show Measurable[ comap (@zyCoord X Y V Z) inferInstance] yz by change Measurable[comap (@zyCoord X Y V Z) inferInstance] (swap ∘ @zyCoord X Y V Z) exact measurable_swap.comp (Measurable.of_comap_le le_rfl)).comap_le have hfactors : ThreeBlockFactors μX μV (μY.prod μZ) d' ↔ FactorsXVGivenZY μX μY μV μZ d := by constructor · rintro ⟨a, b, ha, hb, hab⟩ refine ⟨a, b, ha, hb, ?_⟩ change ∀ᵐ q ∂fourBlockReference μX μY μV μZ, d q = a (xCoord q, (yCoord q, zCoord q)) * b (vCoord q, (yCoord q, zCoord q)) rw [← he.map_eq, e.measurableEmbedding.ae_map_iff] change ∀ᵐ q ∂threeBlockReference μX μV (μY.prod μZ), d' q = a (q.1, q.2.2) * b (q.2.1, q.2.2) at hab simpa [d', e, permXV, xCoord, yCoord, vCoord, zCoord, Function.comp_def] using hab · rintro ⟨a, b, ha, hb, hab⟩ refine ⟨a, b, ha, hb, ?_⟩ change ∀ᵐ q ∂threeBlockReference μX μV (μY.prod μZ), d' q = a (q.1, q.2.2) * b (q.2.1, q.2.2) change ∀ᵐ q ∂fourBlockReference μX μY μV μZ, d q = a (xCoord q, (yCoord q, zCoord q)) * b (vCoord q, (yCoord q, zCoord q)) at hab rw [← he.map_eq, e.measurableEmbedding.ae_map_iff] at hab simpa [d', e, permXV, xCoord, yCoord, vCoord, zCoord, Function.comp_def] using hab change CondIndepFun (comap (@zyCoord X Y V Z) inferInstance) _ (@xCoord X Y V Z) (@vCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d) ↔ FactorsXVGivenZY μX μY μV μZ d calc _ ↔ CondIndepFun (comap yz inferInstance) _ (@xCoord X Y V Z) (@vCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d) := by simp only [hcomap] _ ↔ CondIndepFun (comap (@thirdThreeCoord X V (Y × Z)) inferInstance) _ (@firstThreeCoord X V (Y × Z)) (@secondThreeCoord X V (Y × Z)) ((threeBlockReference μX μV (μY.prod μZ)).withDensity d') := htransport.symm _ ↔ ThreeBlockFactors μX μV (μY.prod μZ) d' := condIndepFun_threeBlock_iff_factors μX μV (μY.prod μZ) hd' _ ↔ FactorsXVGivenZY μX μY μV μZ d := hfactors
FiniteCoordinates 1 core · 1 supporting This module specializes graphoid intersection to coordinate projections on the union of four finite index blocks. ★ condIndep_valuesProjection_intersection_of_positiveDensity
Positive-density intersection for finite coordinate blocks
This module specializes graphoid intersection to coordinate projections on the union of four finite index blocks. All six pairwise-disjointness facts are explicit hypotheses; in particular, the API cannot be applied to overlap degeneracies in which a conditioned coordinate is repeated inside another block.
theorem condIndep_valuesProjection_intersection_of_positiveDensity reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
For four finite coordinate blocks that are pairwise disjoint, σ-finite coordinate reference measures on standard Borel coordinate spaces, a measurable density on assignments to the union of the blocks whose weighting of the product reference measure has finite total mass, strict positivity of that density almost everywhere for the product reference measure, and, under the density-weighted measure, conditional independence of the first and second blocks given the fourth and third together, and of the first and third blocks given the fourth and second together, the coordinates in the first block are conditionally independent of those in the union of the second and third blocks given the fourth.
Formal statement
hypotheses
M :
∀ i, MeasurableSpace (Ω i)
∀ i, StandardBorelSpace (Ω i)
I J K L :
Finset M
hIJ :
Disjoint I J
hIK :
Disjoint I K
hIL :
Disjoint I L
hJK :
Disjoint J K
hJL :
Disjoint J L
hKL :
Disjoint K L
μ :
∀ i, Measure (Ω i)
∀ i, SigmaFinite (μ i)
d :
ValuesOn (fourBlockIndices I J K L) Ω → ℝ≥0∞
hd :
IsFiniteMeasure ((finiteBlockReference I J K L μ).withDensity d)
hpos :
∀ᵐ q ∂finiteBlockReference I J K L μ, 0 < d q
hIJ_given_LK :
CondIndepFun (comap (valuesProjection (fourthThird_subset_fourBlock I J K L)) inferInstance) (comap_valuesProjection_le (fourthThird_subset_fourBlock I J K L)) (valuesProjection (first_subset_fourBlock I J K L)) (valuesProjection (second_subset_fourBlock I J K L)) ((finiteBlockReference I J K L μ).withDensity d)
hIK_given_LJ :
CondIndepFun (comap (valuesProjection (fourthSecond_subset_fourBlock I J K L)) inferInstance) (comap_valuesProjection_le (fourthSecond_subset_fourBlock I J K L)) (valuesProjection (first_subset_fourBlock I J K L)) (valuesProjection (third_subset_fourBlock I J K L)) ((finiteBlockReference I J K L μ).withDensity d)
conclusion
CondIndepFun (comap (valuesProjection (fourth_subset_fourBlock I J K L)) inferInstance) (comap_valuesProjection_le (fourth_subset_fourBlock I J K L)) (valuesProjection (first_subset_fourBlock I J K L)) (valuesProjection (secondThird_subset_fourBlock I J K L)) ((finiteBlockReference I J K L μ).withDensity d)
Proof (Lean source)
theorem condIndep_valuesProjection_intersection_of_positiveDensity
{M : Type uM} [DecidableEq M]
{Ω : M → Type uΩ} [∀ i, MeasurableSpace (Ω i)]
[∀ i, StandardBorelSpace (Ω i)]
(I J K L : Finset M)
(hIJ : Disjoint I J) (hIK : Disjoint I K) (hIL : Disjoint I L)
(hJK : Disjoint J K) (hJL : Disjoint J L) (hKL : Disjoint K L)
(μ : ∀ i, Measure (Ω i)) [∀ i, SigmaFinite (μ i)]
{d : ValuesOn (fourBlockIndices I J K L) Ω → ℝ≥0∞}
(hd : Measurable d)
[IsFiniteMeasure ((finiteBlockReference I J K L μ).withDensity d)]
(hpos : ∀ᵐ q ∂finiteBlockReference I J K L μ, 0 < d q)
(hIJ_given_LK : CondIndepFun
(comap
(valuesProjection (fourthThird_subset_fourBlock I J K L)) inferInstance)
(comap_valuesProjection_le (fourthThird_subset_fourBlock I J K L))
(valuesProjection (first_subset_fourBlock I J K L))
(valuesProjection (second_subset_fourBlock I J K L))
((finiteBlockReference I J K L μ).withDensity d))
(hIK_given_LJ : CondIndepFun
(comap
(valuesProjection (fourthSecond_subset_fourBlock I J K L)) inferInstance)
(comap_valuesProjection_le (fourthSecond_subset_fourBlock I J K L))
(valuesProjection (first_subset_fourBlock I J K L))
(valuesProjection (third_subset_fourBlock I J K L))
((finiteBlockReference I J K L μ).withDensity d)) :
CondIndepFun
(comap
(valuesProjection (fourth_subset_fourBlock I J K L)) inferInstance)
(comap_valuesProjection_le (fourth_subset_fourBlock I J K L))
(valuesProjection (first_subset_fourBlock I J K L))
(valuesProjection (secondThird_subset_fourBlock I J K L))
((finiteBlockReference I J K L μ).withDensity d) := by
let μI : Measure (ValuesOn I Ω) := Measure.pi fun i : I ↦ μ i
let μJ : Measure (ValuesOn J Ω) := Measure.pi fun i : J ↦ μ i
let μK : Measure (ValuesOn K Ω) := Measure.pi fun i : K ↦ μ i
let μL : Measure (ValuesOn L Ω) := Measure.pi fun i : L ↦ μ i
let e : FourBlock (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω) ≃ᵐ
ValuesOn (fourBlockIndices I J K L) Ω :=
fourBlockValuesEquiv I J K L hKL
(Finset.disjoint_union_right.mpr ⟨hJK, hJL⟩)
(Finset.disjoint_union_right.mpr
⟨hIJ, Finset.disjoint_union_right.mpr ⟨hIK, hIL⟩⟩)
let ν := fourBlockReference μI μJ μK μL
let d' : FourBlock (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω) →
ℝ≥0∞ := d ∘ e
have he : MeasurePreserving e ν (finiteBlockReference I J K L μ) := by
simpa only [e, ν, μI, μJ, μK, μL] using
measurePreserving_fourBlockValuesEquiv I J K L hIJ hIK hIL hJK hJL hKL μ
have hd' : Measurable d' := hd.comp e.measurable
have hlaw : (ν.withDensity d').map e =
(finiteBlockReference I J K L μ).withDensity d := by
simpa only [d'] using Causalean.Mathlib.MeasureTheory.map_withDensity_comp_measurableEquiv e he d
have hlaw' : ((finiteBlockReference I J K L μ).withDensity d).map e.symm =
ν.withDensity d' := by
rw [← hlaw, Measure.map_map e.symm.measurable e.measurable]
simpa using congrArg (fun f ↦ Measure.map f (ν.withDensity d')) e.symm_comp_self
letI : IsFiniteMeasure (ν.withDensity d') := by
rw [← hlaw']
infer_instance
have hpos' : ∀ᵐ q ∂ν, 0 < d' q := by
rw [← he.map_eq, e.measurableEmbedding.ae_map_iff] at hpos
simpa only [d', Function.comp_apply] using hpos
have hJ_KL : Disjoint J (K ∪ L) :=
Finset.disjoint_union_right.mpr ⟨hJK, hJL⟩
have hI_JKL : Disjoint I (J ∪ (K ∪ L)) :=
Finset.disjoint_union_right.mpr
⟨hIJ, Finset.disjoint_union_right.mpr ⟨hIK, hIL⟩⟩
have hx : valuesProjection (first_subset_fourBlock I J K L) ∘ e =
(@xCoord (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω)) := by
funext q
ext i
change valuesProjection (first_subset_fourBlock I J K L)
(fourBlockValuesEquiv I J K L hKL hJ_KL hI_JKL q) i = q.1 i
unfold fourBlockValuesEquiv
simp only [MeasurableEquiv.trans_apply, MeasurableEquiv.prodCongr, valuesProjection]
rw [valuesEquivOfEq_apply]
change (Equiv.piFinsetUnion Ω hI_JKL)
(q.1, (Equiv.piFinsetUnion Ω hJ_KL)
(q.2.1, (Equiv.piFinsetUnion Ω hKL) (q.2.2.1, q.2.2.2)))
⟨i.val, mem_union_left _ i.property⟩ = q.1 i
exact Equiv.piFinsetUnion_left Ω hI_JKL i.property _
have hy : valuesProjection (second_subset_fourBlock I J K L) ∘ e =
(@yCoord (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω)) := by
funext q
ext i
change valuesProjection (second_subset_fourBlock I J K L)
(fourBlockValuesEquiv I J K L hKL hJ_KL hI_JKL q) i = q.2.1 i
unfold fourBlockValuesEquiv
simp only [MeasurableEquiv.trans_apply, MeasurableEquiv.prodCongr, valuesProjection]
rw [valuesEquivOfEq_apply]
change (Equiv.piFinsetUnion Ω hI_JKL)
(q.1, (Equiv.piFinsetUnion Ω hJ_KL)
(q.2.1, (Equiv.piFinsetUnion Ω hKL) (q.2.2.1, q.2.2.2)))
⟨i.val, mem_union_right I (mem_union_left _ i.property)⟩ = q.2.1 i
calc
_ = (Equiv.piFinsetUnion Ω hJ_KL)
(q.2.1, (Equiv.piFinsetUnion Ω hKL) (q.2.2.1, q.2.2.2))
⟨i.val, mem_union_left _ i.property⟩ :=
Equiv.piFinsetUnion_right Ω hI_JKL (mem_union_left _ i.property) _
_ = q.2.1 i := Equiv.piFinsetUnion_left Ω hJ_KL i.property _
have hv : valuesProjection (third_subset_fourBlock I J K L) ∘ e =
(@vCoord (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω)) := by
funext q
ext i
change valuesProjection (third_subset_fourBlock I J K L)
(fourBlockValuesEquiv I J K L hKL hJ_KL hI_JKL q) i = q.2.2.1 i
unfold fourBlockValuesEquiv
simp only [MeasurableEquiv.trans_apply, MeasurableEquiv.prodCongr, valuesProjection]
rw [valuesEquivOfEq_apply]
change (Equiv.piFinsetUnion Ω hI_JKL)
(q.1, (Equiv.piFinsetUnion Ω hJ_KL)
(q.2.1, (Equiv.piFinsetUnion Ω hKL) (q.2.2.1, q.2.2.2)))
⟨i.val, mem_union_right I
(mem_union_right J (mem_union_left L i.property))⟩ = q.2.2.1 i
calc
_ = (Equiv.piFinsetUnion Ω hJ_KL)
(q.2.1, (Equiv.piFinsetUnion Ω hKL) (q.2.2.1, q.2.2.2))
⟨i.val, mem_union_right J (mem_union_left L i.property)⟩ :=
Equiv.piFinsetUnion_right Ω hI_JKL
(mem_union_right J (mem_union_left L i.property)) _
_ = (Equiv.piFinsetUnion Ω hKL) (q.2.2.1, q.2.2.2)
⟨i.val, mem_union_left L i.property⟩ :=
Equiv.piFinsetUnion_right Ω hJ_KL (mem_union_left L i.property) _
_ = q.2.2.1 i := Equiv.piFinsetUnion_left Ω hKL i.property _
have hz : valuesProjection (fourth_subset_fourBlock I J K L) ∘ e =
(@zCoord (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω)) := by
funext q
ext i
change valuesProjection (fourth_subset_fourBlock I J K L)
(fourBlockValuesEquiv I J K L hKL hJ_KL hI_JKL q) i = q.2.2.2 i
unfold fourBlockValuesEquiv
simp only [MeasurableEquiv.trans_apply, MeasurableEquiv.prodCongr, valuesProjection]
rw [valuesEquivOfEq_apply]
change (Equiv.piFinsetUnion Ω hI_JKL)
(q.1, (Equiv.piFinsetUnion Ω hJ_KL)
(q.2.1, (Equiv.piFinsetUnion Ω hKL) (q.2.2.1, q.2.2.2)))
⟨i.val, mem_union_right I
(mem_union_right J (mem_union_right K i.property))⟩ = q.2.2.2 i
calc
_ = (Equiv.piFinsetUnion Ω hJ_KL)
(q.2.1, (Equiv.piFinsetUnion Ω hKL) (q.2.2.1, q.2.2.2))
⟨i.val, mem_union_right J (mem_union_right K i.property)⟩ :=
Equiv.piFinsetUnion_right Ω hI_JKL
(mem_union_right J (mem_union_right K i.property)) _
_ = (Equiv.piFinsetUnion Ω hKL) (q.2.2.1, q.2.2.2)
⟨i.val, mem_union_right K i.property⟩ :=
Equiv.piFinsetUnion_right Ω hJ_KL (mem_union_right K i.property) _
_ = q.2.2.2 i := Equiv.piFinsetUnion_right Ω hKL i.property _
let eLK : (ValuesOn L Ω × ValuesOn K Ω) ≃ᵐ ValuesOn (L ∪ K) Ω :=
MeasurableEquiv.piFinsetUnion Ω hKL.symm
let eLJ : (ValuesOn L Ω × ValuesOn J Ω) ≃ᵐ ValuesOn (L ∪ J) Ω :=
MeasurableEquiv.piFinsetUnion Ω hJL.symm
let eJK : (ValuesOn J Ω × ValuesOn K Ω) ≃ᵐ ValuesOn (J ∪ K) Ω :=
MeasurableEquiv.piFinsetUnion Ω hJK
have hLK : valuesProjection (fourthThird_subset_fourBlock I J K L) ∘ e =
eLK ∘ (@zvCoord (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω)) := by
funext q
ext i
simp only [Function.comp_apply, zvCoord]
by_cases hi : i.val ∈ L
· have hr : eLK (q.2.2.2, q.2.2.1) i = q.2.2.2 ⟨i.val, hi⟩ := by
change (Equiv.piFinsetUnion Ω hKL.symm) (q.2.2.2, q.2.2.1) i = _
apply Equiv.piFinsetUnion_left Ω hKL.symm hi
rw [hr]
simpa only [valuesProjection, Function.comp_apply, zCoord] using
congrFun (congrFun hz q) ⟨i.val, hi⟩
· have hiK : i.val ∈ K := (Finset.mem_union.mp i.property).resolve_left hi
have hr : eLK (q.2.2.2, q.2.2.1) i = q.2.2.1 ⟨i.val, hiK⟩ := by
change (Equiv.piFinsetUnion Ω hKL.symm) (q.2.2.2, q.2.2.1) i = _
apply Equiv.piFinsetUnion_right Ω hKL.symm hiK
rw [hr]
simpa only [valuesProjection, Function.comp_apply, vCoord] using
congrFun (congrFun hv q) ⟨i.val, hiK⟩
have hLJ : valuesProjection (fourthSecond_subset_fourBlock I J K L) ∘ e =
eLJ ∘ (@zyCoord (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω)) := by
funext q
ext i
simp only [Function.comp_apply, zyCoord]
by_cases hi : i.val ∈ L
· have hr : eLJ (q.2.2.2, q.2.1) i = q.2.2.2 ⟨i.val, hi⟩ := by
change (Equiv.piFinsetUnion Ω hJL.symm) (q.2.2.2, q.2.1) i = _
apply Equiv.piFinsetUnion_left Ω hJL.symm hi
rw [hr]
simpa only [valuesProjection, Function.comp_apply, zCoord] using
congrFun (congrFun hz q) ⟨i.val, hi⟩
· have hiJ : i.val ∈ J := (Finset.mem_union.mp i.property).resolve_left hi
have hr : eLJ (q.2.2.2, q.2.1) i = q.2.1 ⟨i.val, hiJ⟩ := by
change (Equiv.piFinsetUnion Ω hJL.symm) (q.2.2.2, q.2.1) i = _
apply Equiv.piFinsetUnion_right Ω hJL.symm hiJ
rw [hr]
simpa only [valuesProjection, Function.comp_apply, yCoord] using
congrFun (congrFun hy q) ⟨i.val, hiJ⟩
have hJK' : valuesProjection (secondThird_subset_fourBlock I J K L) ∘ e =
eJK ∘ (@yvCoord (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω)) := by
funext q
ext i
simp only [Function.comp_apply, yvCoord]
by_cases hi : i.val ∈ J
· have hr : eJK (q.2.1, q.2.2.1) i = q.2.1 ⟨i.val, hi⟩ := by
change (Equiv.piFinsetUnion Ω hJK) (q.2.1, q.2.2.1) i = _
apply Equiv.piFinsetUnion_left Ω hJK hi
rw [hr]
simpa only [valuesProjection, Function.comp_apply, yCoord] using
congrFun (congrFun hy q) ⟨i.val, hi⟩
· have hiK : i.val ∈ K := (Finset.mem_union.mp i.property).resolve_left hi
have hr : eJK (q.2.1, q.2.2.1) i = q.2.2.1 ⟨i.val, hiK⟩ := by
change (Equiv.piFinsetUnion Ω hJK) (q.2.1, q.2.2.1) i = _
apply Equiv.piFinsetUnion_right Ω hJK hiK
rw [hr]
simpa only [valuesProjection, Function.comp_apply, vCoord] using
congrFun (congrFun hv q) ⟨i.val, hiK⟩
have hXY : CondIndepFun
(comap
(@zvCoord (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω))
inferInstance)
measurable_zvCoord.comap_le
(@xCoord (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω))
(@yCoord (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω))
(ν.withDensity d') := by
have h := (condIndepFun_measurableEquiv_iff e hlaw
(measurable_valuesProjection (first_subset_fourBlock I J K L))
(measurable_valuesProjection (second_subset_fourBlock I J K L))
(measurable_valuesProjection (fourthThird_subset_fourBlock I J K L))).2
hIJ_given_LK
simpa only [hx, hy, hLK, comap_measurableEquiv_comp] using h
have hXV : CondIndepFun
(comap
(@zyCoord (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω))
inferInstance)
measurable_zyCoord.comap_le
(@xCoord (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω))
(@vCoord (ValuesOn I Ω) (ValuesOn J Ω) (ValuesOn K Ω) (ValuesOn L Ω))
(ν.withDensity d') := by
have h := (condIndepFun_measurableEquiv_iff e hlaw
(measurable_valuesProjection (first_subset_fourBlock I J K L))
(measurable_valuesProjection (third_subset_fourBlock I J K L))
-- … truncated; follow the source link for the rest …
1 supporting declaration (lemmas, instances)
-
condIndep_valuesProjection_decomposition_of_positiveDensitytheorem — For four finite coordinate blocks with all pairwise overlaps excluded, coordinate reference measures, a measurable finite-block density, strict positivity of that density almost everywhere, and the two conditional independence relations conditioning on the alternate coordinate blocks, the coordinates in the first block are conditionally independent of the second block given the fourth.hypothesesM :∀ i, MeasurableSpace (Ω i)∀ i, StandardBorelSpace (Ω i)I J K L :Finset MhIJ :Disjoint I JhIK :Disjoint I KhIL :Disjoint I LhJK :Disjoint J KhJL :Disjoint J LhKL :Disjoint K Lμ :∀ i, Measure (Ω i)∀ i, SigmaFinite (μ i)d :ValuesOn (fourBlockIndices I J K L) Ω → ℝ≥0∞hd :IsFiniteMeasure ((finiteBlockReference I J K L μ).withDensity d)hpos :∀ᵐ q ∂finiteBlockReference I J K L μ, 0 < d qhIJ_given_LK :CondIndepFun (comap (valuesProjection (fourthThird_subset_fourBlock I J K L)) inferInstance) (comap_valuesProjection_le (fourthThird_subset_fourBlock I J K L)) (valuesProjection (first_subset_fourBlock I J K L)) (valuesProjection (second_subset_fourBlock I J K L)) ((finiteBlockReference I J K L μ).withDensity d)hIK_given_LJ :CondIndepFun (comap (valuesProjection (fourthSecond_subset_fourBlock I J K L)) inferInstance) (comap_valuesProjection_le (fourthSecond_subset_fourBlock I J K L)) (valuesProjection (first_subset_fourBlock I J K L)) (valuesProjection (third_subset_fourBlock I J K L)) ((finiteBlockReference I J K L μ).withDensity d)conclusionCondIndepFun (comap (valuesProjection (fourth_subset_fourBlock I J K L)) inferInstance) (comap_valuesProjection_le (fourth_subset_fourBlock I J K L)) (valuesProjection (first_subset_fourBlock I J K L)) (valuesProjection (second_subset_fourBlock I J K L)) ((finiteBlockReference I J K L μ).withDensity d)Proof (Lean source)
theorem condIndep_valuesProjection_decomposition_of_positiveDensity {M : Type uM} [DecidableEq M] {Ω : M → Type uΩ} [∀ i, MeasurableSpace (Ω i)] [∀ i, StandardBorelSpace (Ω i)] (I J K L : Finset M) (hIJ : Disjoint I J) (hIK : Disjoint I K) (hIL : Disjoint I L) (hJK : Disjoint J K) (hJL : Disjoint J L) (hKL : Disjoint K L) (μ : ∀ i, Measure (Ω i)) [∀ i, SigmaFinite (μ i)] {d : ValuesOn (fourBlockIndices I J K L) Ω → ℝ≥0∞} (hd : Measurable d) [IsFiniteMeasure ((finiteBlockReference I J K L μ).withDensity d)] (hpos : ∀ᵐ q ∂finiteBlockReference I J K L μ, 0 < d q) (hIJ_given_LK : CondIndepFun (comap (valuesProjection (fourthThird_subset_fourBlock I J K L)) inferInstance) (comap_valuesProjection_le (fourthThird_subset_fourBlock I J K L)) (valuesProjection (first_subset_fourBlock I J K L)) (valuesProjection (second_subset_fourBlock I J K L)) ((finiteBlockReference I J K L μ).withDensity d)) (hIK_given_LJ : CondIndepFun (comap (valuesProjection (fourthSecond_subset_fourBlock I J K L)) inferInstance) (comap_valuesProjection_le (fourthSecond_subset_fourBlock I J K L)) (valuesProjection (first_subset_fourBlock I J K L)) (valuesProjection (third_subset_fourBlock I J K L)) ((finiteBlockReference I J K L μ).withDensity d)) : CondIndepFun (comap (valuesProjection (fourth_subset_fourBlock I J K L)) inferInstance) (comap_valuesProjection_le (fourth_subset_fourBlock I J K L)) (valuesProjection (first_subset_fourBlock I J K L)) (valuesProjection (second_subset_fourBlock I J K L)) ((finiteBlockReference I J K L μ).withDensity d) := by have h := condIndep_valuesProjection_intersection_of_positiveDensity I J K L hIJ hIK hIL hJK hJL hKL μ hd hpos hIJ_given_LK hIK_given_LJ convert h.comp measurable_id (measurable_valuesProjection (Ω' := Ω) subset_union_left) using 1 <;> rfl
Main 1 core · 3 supporting This module proves the measure-level intersection axiom for the four canonical coordinate maps. ★ condIndepFun_intersection_of_positiveDensity
Graphoid intersection under a positive density
This module proves the measure-level intersection axiom for the four canonical coordinate maps.
It also exports the decomposition corollary which drops the V component from the combined
right-hand block.
theorem condIndepFun_intersection_of_positiveDensity reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
For four σ-finite reference measures on standard Borel spaces, a measurable joint density whose weighting of the product reference measure has finite total mass, strict positivity of that density almost everywhere for the product reference measure, and, under the density-weighted measure, conditional independence of the first and second blocks given the fourth and third together, and of the first and third blocks given the fourth and second together, the first block is conditionally independent of the combined second and third blocks given the fourth.
Formal statement
hypotheses
X :
Type uX
Y :
Type uY
V :
Type uV
Z :
Type uZ
μX :
Measure X
μY :
Measure Y
μV :
Measure V
μZ :
Measure Z
SigmaFinite μX
SigmaFinite μY
SigmaFinite μV
SigmaFinite μZ
d :
FourBlock X Y V Z → ℝ≥0∞
hd :
IsFiniteMeasure ((fourBlockReference μX μY μV μZ).withDensity d)
hpos :
∀ᵐ q ∂fourBlockReference μX μY μV μZ, 0 < d q
hXY :
CondIndepFun (comap (@zvCoord X Y V Z) inferInstance) measurable_zvCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d)
hXV :
CondIndepFun (comap (@zyCoord X Y V Z) inferInstance) measurable_zyCoord.comap_le (@xCoord X Y V Z) (@vCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d)
conclusion
CondIndepFun (comap (@zCoord X Y V Z) inferInstance) measurable_zCoord.comap_le (@xCoord X Y V Z) (@yvCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d)
Proof (Lean source)
theorem condIndepFun_intersection_of_positiveDensity
{X : Type uX} {Y : Type uY} {V : Type uV} {Z : Type uZ}
[MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace V] [MeasurableSpace Z]
[StandardBorelSpace X] [StandardBorelSpace Y]
[StandardBorelSpace V] [StandardBorelSpace Z]
(μX : Measure X) (μY : Measure Y) (μV : Measure V) (μZ : Measure Z)
[SigmaFinite μX] [SigmaFinite μY] [SigmaFinite μV] [SigmaFinite μZ]
{d : FourBlock X Y V Z → ℝ≥0∞}
(hd : Measurable d)
[IsFiniteMeasure ((fourBlockReference μX μY μV μZ).withDensity d)]
(hpos : ∀ᵐ q ∂fourBlockReference μX μY μV μZ, 0 < d q)
(hXY : CondIndepFun
(comap (@zvCoord X Y V Z) inferInstance)
measurable_zvCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z)
((fourBlockReference μX μY μV μZ).withDensity d))
(hXV : CondIndepFun
(comap (@zyCoord X Y V Z) inferInstance)
measurable_zyCoord.comap_le (@xCoord X Y V Z) (@vCoord X Y V Z)
((fourBlockReference μX μY μV μZ).withDensity d)) :
CondIndepFun
(comap (@zCoord X Y V Z) inferInstance)
measurable_zCoord.comap_le (@xCoord X Y V Z) (@yvCoord X Y V Z)
((fourBlockReference μX μY μV μZ).withDensity d) := by
apply (condIndepFun_xyv_given_z_iff_factors μX μY μV μZ hd).2
exact positiveDensity_factorization_splice μX μY μV μZ hd hpos
((condIndepFun_xy_given_zv_iff_factors μX μY μV μZ hd).1 hXY)
((condIndepFun_xv_given_zy_iff_factors μX μY μV μZ hd).1 hXV)
3 supporting declarations (lemmas, instances)
-
condIndepFun_decomposition_of_positiveDensitytheorem — For four product reference measures, a measurable joint density, strict positivity of that density almost everywhere, and the two alternate-block conditional independence relations, the first block is conditionally independent of the second block given the fourth.hypothesesX :Type uXY :Type uYV :Type uVZ :Type uZμX :Measure XμY :Measure YμV :Measure VμZ :Measure ZSigmaFinite μXSigmaFinite μYSigmaFinite μVSigmaFinite μZd :FourBlock X Y V Z → ℝ≥0∞hd :IsFiniteMeasure ((fourBlockReference μX μY μV μZ).withDensity d)hpos :∀ᵐ q ∂fourBlockReference μX μY μV μZ, 0 < d qhXY :CondIndepFun (comap (@zvCoord X Y V Z) inferInstance) measurable_zvCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d)hXV :CondIndepFun (comap (@zyCoord X Y V Z) inferInstance) measurable_zyCoord.comap_le (@xCoord X Y V Z) (@vCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d)conclusionCondIndepFun (comap (@zCoord X Y V Z) inferInstance) measurable_zCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d)Proof (Lean source)
theorem condIndepFun_decomposition_of_positiveDensity {X : Type uX} {Y : Type uY} {V : Type uV} {Z : Type uZ} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace V] [MeasurableSpace Z] [StandardBorelSpace X] [StandardBorelSpace Y] [StandardBorelSpace V] [StandardBorelSpace Z] (μX : Measure X) (μY : Measure Y) (μV : Measure V) (μZ : Measure Z) [SigmaFinite μX] [SigmaFinite μY] [SigmaFinite μV] [SigmaFinite μZ] {d : FourBlock X Y V Z → ℝ≥0∞} (hd : Measurable d) [IsFiniteMeasure ((fourBlockReference μX μY μV μZ).withDensity d)] (hpos : ∀ᵐ q ∂fourBlockReference μX μY μV μZ, 0 < d q) (hXY : CondIndepFun (comap (@zvCoord X Y V Z) inferInstance) measurable_zvCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d)) (hXV : CondIndepFun (comap (@zyCoord X Y V Z) inferInstance) measurable_zyCoord.comap_le (@xCoord X Y V Z) (@vCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d)) : CondIndepFun (comap (@zCoord X Y V Z) inferInstance) measurable_zCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z) ((fourBlockReference μX μY μV μZ).withDensity d) := by have h := condIndepFun_intersection_of_positiveDensity μX μY μV μZ hd hpos hXY hXV change CondIndepFun (comap (@zCoord X Y V Z) inferInstance) measurable_zCoord.comap_le (@xCoord X Y V Z) (fun q : FourBlock X Y V Z => q.2.1) ((fourBlockReference μX μY μV μZ).withDensity d) convert h.comp measurable_id measurable_fst using 1 <;> rfl -
condIndepFun_intersection_of_eq_withDensitytheorem — For four product reference measures, a finite joint law, a measurable density representing that law relative to the product reference, strict positivity of the density almost everywhere, and the two alternate-block conditional independence relations, the first block is conditionally independent of the combined second and third blocks given the fourth.hypothesesX :Type uXY :Type uYV :Type uVZ :Type uZμX :Measure XμY :Measure YμV :Measure VμZ :Measure ZSigmaFinite μXSigmaFinite μYSigmaFinite μVSigmaFinite μZρ :d :FourBlock X Y V Z → ℝ≥0∞hd :hρ :ρ = (fourBlockReference μX μY μV μZ).withDensity dhpos :∀ᵐ q ∂fourBlockReference μX μY μV μZ, 0 < d qhXY :CondIndepFun (comap (@zvCoord X Y V Z) inferInstance) measurable_zvCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z) ρhXV :CondIndepFun (comap (@zyCoord X Y V Z) inferInstance) measurable_zyCoord.comap_le (@xCoord X Y V Z) (@vCoord X Y V Z) ρconclusionCondIndepFun (comap (@zCoord X Y V Z) inferInstance) measurable_zCoord.comap_le (@xCoord X Y V Z) (@yvCoord X Y V Z) ρProof (Lean source)
theorem condIndepFun_intersection_of_eq_withDensity {X : Type uX} {Y : Type uY} {V : Type uV} {Z : Type uZ} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace V] [MeasurableSpace Z] [StandardBorelSpace X] [StandardBorelSpace Y] [StandardBorelSpace V] [StandardBorelSpace Z] (μX : Measure X) (μY : Measure Y) (μV : Measure V) (μZ : Measure Z) [SigmaFinite μX] [SigmaFinite μY] [SigmaFinite μV] [SigmaFinite μZ] {ρ : Measure (FourBlock X Y V Z)} [IsFiniteMeasure ρ] {d : FourBlock X Y V Z → ℝ≥0∞} (hd : Measurable d) (hρ : ρ = (fourBlockReference μX μY μV μZ).withDensity d) (hpos : ∀ᵐ q ∂fourBlockReference μX μY μV μZ, 0 < d q) (hXY : CondIndepFun (comap (@zvCoord X Y V Z) inferInstance) measurable_zvCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z) ρ) (hXV : CondIndepFun (comap (@zyCoord X Y V Z) inferInstance) measurable_zyCoord.comap_le (@xCoord X Y V Z) (@vCoord X Y V Z) ρ) : CondIndepFun (comap (@zCoord X Y V Z) inferInstance) measurable_zCoord.comap_le (@xCoord X Y V Z) (@yvCoord X Y V Z) ρ := by subst ρ exact condIndepFun_intersection_of_positiveDensity μX μY μV μZ hd hpos hXY hXV -
condIndepFun_decomposition_of_eq_withDensitytheorem — For four product reference measures, a finite joint law, a measurable density representing that law relative to the product reference, strict positivity of the density almost everywhere, and the two alternate-block conditional independence relations, the first block is conditionally independent of the second block given the fourth.hypothesesX :Type uXY :Type uYV :Type uVZ :Type uZμX :Measure XμY :Measure YμV :Measure VμZ :Measure ZSigmaFinite μXSigmaFinite μYSigmaFinite μVSigmaFinite μZρ :d :FourBlock X Y V Z → ℝ≥0∞hd :hρ :ρ = (fourBlockReference μX μY μV μZ).withDensity dhpos :∀ᵐ q ∂fourBlockReference μX μY μV μZ, 0 < d qhXY :CondIndepFun (comap (@zvCoord X Y V Z) inferInstance) measurable_zvCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z) ρhXV :CondIndepFun (comap (@zyCoord X Y V Z) inferInstance) measurable_zyCoord.comap_le (@xCoord X Y V Z) (@vCoord X Y V Z) ρconclusionCondIndepFun (comap (@zCoord X Y V Z) inferInstance) measurable_zCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z) ρProof (Lean source)
theorem condIndepFun_decomposition_of_eq_withDensity {X : Type uX} {Y : Type uY} {V : Type uV} {Z : Type uZ} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace V] [MeasurableSpace Z] [StandardBorelSpace X] [StandardBorelSpace Y] [StandardBorelSpace V] [StandardBorelSpace Z] (μX : Measure X) (μY : Measure Y) (μV : Measure V) (μZ : Measure Z) [SigmaFinite μX] [SigmaFinite μY] [SigmaFinite μV] [SigmaFinite μZ] {ρ : Measure (FourBlock X Y V Z)} [IsFiniteMeasure ρ] {d : FourBlock X Y V Z → ℝ≥0∞} (hd : Measurable d) (hρ : ρ = (fourBlockReference μX μY μV μZ).withDensity d) (hpos : ∀ᵐ q ∂fourBlockReference μX μY μV μZ, 0 < d q) (hXY : CondIndepFun (comap (@zvCoord X Y V Z) inferInstance) measurable_zvCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z) ρ) (hXV : CondIndepFun (comap (@zyCoord X Y V Z) inferInstance) measurable_zyCoord.comap_le (@xCoord X Y V Z) (@vCoord X Y V Z) ρ) : CondIndepFun (comap (@zCoord X Y V Z) inferInstance) measurable_zCoord.comap_le (@xCoord X Y V Z) (@yCoord X Y V Z) ρ := by subst ρ exact condIndepFun_decomposition_of_positiveDensity μX μY μV μZ hd hpos hXY hXV
Splice 1 core · 0 supporting This module isolates the analytic heart of graphoid intersection. ★ positiveDensity_factorization_splice
Splicing positive density factorizations
This module isolates the analytic heart of graphoid intersection. Strict positivity on a product support lets two factorizations with different conditioning blocks be compared along product fibres and spliced into the factorization for the union block.
theorem positiveDensity_factorization_splice reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
For four σ-finite reference measures, a measurable density whose weighting of the product reference measure has finite total mass, strict positivity of the density almost everywhere for the product reference measure, and almost-everywhere factorizations of the density both as a factor of the first, third and fourth blocks times a factor of the second, third and fourth blocks, and as a factor of the first, second and fourth blocks times a factor of the third, second and fourth blocks, the density is almost everywhere a measurable factor of the first and fourth blocks times a measurable factor of the second, third and fourth blocks.
Formal statement
hypotheses
X :
Type uX
Y :
Type uY
V :
Type uV
Z :
Type uZ
μX :
Measure X
μY :
Measure Y
μV :
Measure V
μZ :
Measure Z
SigmaFinite μX
SigmaFinite μY
SigmaFinite μV
SigmaFinite μZ
d :
FourBlock X Y V Z → ℝ≥0∞
hd :
IsFiniteMeasure ((fourBlockReference μX μY μV μZ).withDensity d)
hpos :
∀ᵐ q ∂fourBlockReference μX μY μV μZ, 0 < d q
hXY :
FactorsXYGivenZV μX μY μV μZ d
hXV :
FactorsXVGivenZY μX μY μV μZ d
conclusion
FactorsXYVGivenZ μX μY μV μZ d
Proof (Lean source)
theorem positiveDensity_factorization_splice
{X : Type uX} {Y : Type uY} {V : Type uV} {Z : Type uZ}
[MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace V] [MeasurableSpace Z]
(μX : Measure X) (μY : Measure Y) (μV : Measure V) (μZ : Measure Z)
[SigmaFinite μX] [SigmaFinite μY] [SigmaFinite μV] [SigmaFinite μZ]
{d : FourBlock X Y V Z → ℝ≥0∞}
(hd : Measurable d)
[IsFiniteMeasure ((fourBlockReference μX μY μV μZ).withDensity d)]
(hpos : ∀ᵐ q ∂fourBlockReference μX μY μV μZ, 0 < d q)
(hXY : FactorsXYGivenZV μX μY μV μZ d)
(hXV : FactorsXVGivenZY μX μY μV μZ d) :
FactorsXYVGivenZ μX μY μV μZ d := by
/- Proof plan: finiteness of `withDensity d` and `ae_lt_top` make `d` finite a.e.; positivity
makes the premise factors nonzero on almost every product fibre. Use Tonelli/Fubini to obtain
simultaneous fibrewise versions of both factorizations, cancel along the `Y` and `V` fibres,
and construct measurable `(X,Z)` and `(Y,V,Z)` factors from fibre integrals. -/
by_cases hX : μX = 0
· refine ⟨0, 0, measurable_const, measurable_const, ?_⟩
rw [show fourBlockReference μX μY μV μZ = 0 by simp [fourBlockReference, hX]]
rw [ae_zero]
exact Filter.eventually_bot
by_cases hY : μY = 0
· refine ⟨0, 0, measurable_const, measurable_const, ?_⟩
rw [show fourBlockReference μX μY μV μZ = 0 by simp [fourBlockReference, hY]]
rw [ae_zero]
exact Filter.eventually_bot
by_cases hV : μV = 0
· refine ⟨0, 0, measurable_const, measurable_const, ?_⟩
rw [show fourBlockReference μX μY μV μZ = 0 by simp [fourBlockReference, hV]]
rw [ae_zero]
exact Filter.eventually_bot
by_cases hZ : μZ = 0
· refine ⟨0, 0, measurable_const, measurable_const, ?_⟩
rw [show fourBlockReference μX μY μV μZ = 0 by simp [fourBlockReference, hZ]]
rw [ae_zero]
exact Filter.eventually_bot
let _ : NeZero μX := ⟨hX⟩
rcases hXY with ⟨a, b, ha, hb, hab⟩
rcases hXV with ⟨c, e, hc, he, hce⟩
let ν := μY.prod (μV.prod μZ)
let D : Y × (V × Z) → ℝ≥0∞ := fun w ↦ ∫⁻ x, d (x, w) ∂μX
let A : V × Z → ℝ≥0∞ := fun vz ↦ ∫⁻ x, a (x, vz) ∂μX
let C : Y × Z → ℝ≥0∞ := fun yz ↦ ∫⁻ x, c (x, yz) ∂μX
have hD : Measurable D := hd.lintegral_prod_left'
have hA : Measurable A := ha.lintegral_prod_left'
have hC : Measurable C := hc.lintegral_prod_left'
have hdInt : ∫⁻ w, d w ∂fourBlockReference μX μY μV μZ ≠ ∞ := by
have h := measure_ne_top
((fourBlockReference μX μY μV μZ).withDensity d) univ
simpa [withDensity_apply] using h
have hdFinite : ∀ᵐ w ∂fourBlockReference μX μY μV μZ, d w < ∞ :=
ae_lt_top hd hdInt
have hDInt : ∫⁻ w, D w ∂ν ≠ ∞ := by
rw [← lintegral_prod_symm d hd.aemeasurable]
exact hdInt
have hDFinite : ∀ᵐ w ∂ν, D w < ∞ := ae_lt_top hD hDInt
have hgood : ∀ᵐ w ∂fourBlockReference μX μY μV μZ,
0 < d w ∧ d w < ∞ ∧
d w = a (w.1, (w.2.2.1, w.2.2.2)) * b (w.2.1, (w.2.2.1, w.2.2.2)) ∧
d w = c (w.1, (w.2.1, w.2.2.2)) * e (w.2.2.1, (w.2.1, w.2.2.2)) := by
filter_upwards [hpos, hdFinite, hab, hce] with w hp hf habw hcew
exact ⟨hp, hf, habw, hcew⟩
have hgoodSwap : ∀ᵐ w ∂ν, ∀ᵐ x ∂μX,
0 < d (x, w) ∧ d (x, w) < ∞ ∧
d (x, w) = a (x, (w.2.1, w.2.2)) * b (w.1, (w.2.1, w.2.2)) ∧
d (x, w) = c (x, (w.1, w.2.2)) * e (w.2.1, (w.1, w.2.2)) := by
apply (Measure.ae_ae_comm (by measurability)).1
exact Measure.ae_ae_of_ae_prod hgood
have hrest : ∀ᵐ w ∂ν,
A (w.2.1, w.2.2) * b (w.1, (w.2.1, w.2.2)) =
C (w.1, w.2.2) * e (w.2.1, (w.1, w.2.2)) ∧
0 < A (w.2.1, w.2.2) ∧ A (w.2.1, w.2.2) < ∞ ∧
0 < C (w.1, w.2.2) ∧ C (w.1, w.2.2) < ∞ := by
filter_upwards [hDFinite, hgoodSwap] with w hDf hw
have haSec : Measurable (fun x ↦ a (x, (w.2.1, w.2.2))) := by fun_prop
have hcSec : Measurable (fun x ↦ c (x, (w.1, w.2.2))) := by fun_prop
have hDab : D w = A (w.2.1, w.2.2) * b (w.1, (w.2.1, w.2.2)) := by
change (∫⁻ x, d (x, w) ∂μX) = _
rw [lintegral_congr_ae (hw.mono fun x hx ↦ hx.2.2.1), lintegral_mul_const]
exact haSec
have hDce : D w = C (w.1, w.2.2) * e (w.2.1, (w.1, w.2.2)) := by
change (∫⁻ x, d (x, w) ∂μX) = _
rw [lintegral_congr_ae (hw.mono fun x hx ↦ hx.2.2.2), lintegral_mul_const]
exact hcSec
have hapos : ∀ᵐ x ∂μX, 0 < a (x, (w.2.1, w.2.2)) :=
hw.mono fun x hx ↦ (factors_pos_lt_top hx.2.2.1 hx.1 hx.2.1).1
have hcpos : ∀ᵐ x ∂μX, 0 < c (x, (w.1, w.2.2)) :=
hw.mono fun x hx ↦ (factors_pos_lt_top hx.2.2.2 hx.1 hx.2.1).1
have hApos : 0 < A (w.2.1, w.2.2) := by
change 0 < ∫⁻ x, a (x, (w.2.1, w.2.2)) ∂μX
simpa using lintegral_strict_mono hX haSec.aemeasurable (by simp) hapos
have hCpos : 0 < C (w.1, w.2.2) := by
change 0 < ∫⁻ x, c (x, (w.1, w.2.2)) ∂μX
simpa using lintegral_strict_mono hX hcSec.aemeasurable (by simp) hcpos
obtain ⟨x0, hx0⟩ := hw.exists
have hbf := factors_pos_lt_top hx0.2.2.1 hx0.1 hx0.2.1
have hef := factors_pos_lt_top hx0.2.2.2 hx0.1 hx0.2.1
have hbpos : 0 < b (w.1, (w.2.1, w.2.2)) := hbf.2.2.1
have hepos : 0 < e (w.2.1, (w.1, w.2.2)) := hef.2.2.1
have hAfin : A (w.2.1, w.2.2) < ∞ := by
have hmul : A (w.2.1, w.2.2) * b (w.1, (w.2.1, w.2.2)) < ∞ := by
rwa [← hDab]
rcases ENNReal.mul_lt_top_iff.mp hmul with h | h | h
· exact h.1
· exact (hApos.ne' h).elim
· exact (hbpos.ne' h).elim
have hCfin : C (w.1, w.2.2) < ∞ := by
have hmul : C (w.1, w.2.2) * e (w.2.1, (w.1, w.2.2)) < ∞ := by
rwa [← hDce]
rcases ENNReal.mul_lt_top_iff.mp hmul with h | h | h
· exact h.1
· exact (hCpos.ne' h).elim
· exact (hepos.ne' h).elim
exact ⟨hDab.symm.trans hDce, hApos, hAfin, hCpos, hCfin⟩
let p : X × (V × Z) → ℝ≥0∞ := fun xvz ↦ a xvz / A xvz.2
let q : X × (Y × Z) → ℝ≥0∞ := fun xyz ↦ c xyz / C xyz.2
have hp : Measurable p := ha.div (hA.comp measurable_snd)
have hq : Measurable q := hc.div (hC.comp measurable_snd)
have hpqRest : ∀ᵐ w ∂ν, ∀ᵐ x ∂μX,
p (x, (w.2.1, w.2.2)) = q (x, (w.1, w.2.2)) := by
filter_upwards [hrest, hgoodSwap] with w hr hw
filter_upwards [hw] with x hx
have hef := factors_pos_lt_top hx.2.2.2 hx.1 hx.2.1
exact div_eq_div_of_mul_eq_mul
(hx.2.2.1.symm.trans hx.2.2.2) hr.1
hr.2.1.ne' hr.2.2.1.ne hr.2.2.2.1.ne' hr.2.2.2.2.ne
hef.2.2.1.ne' hef.2.2.2.ne
have hpqNested : ∀ᵐ x ∂μX, ∀ᵐ w ∂ν,
p (x, (w.2.1, w.2.2)) = q (x, (w.1, w.2.2)) := by
apply (Measure.ae_ae_comm (by measurability)).2
exact hpqRest
have hpq : ∀ᵐ w ∂μX.prod (μY.prod (μV.prod μZ)),
p (w.1, (w.2.2.1, w.2.2.2)) = q (w.1, (w.2.1, w.2.2.2)) := by
apply (Measure.ae_prod_iff_ae_ae (by measurability)).2
exact hpqNested
obtain ⟨r, hr, hpr⟩ := commonFactor_of_ae_eq μX μY μV μZ hV hp hq hpq
let s : (Y × V) × Z → ℝ≥0∞ := fun yvz ↦ A (yvz.1.2, yvz.2) * b (yvz.1.1, (yvz.1.2, yvz.2))
have hs : Measurable s := by fun_prop
refine ⟨r, s, hr, hs, ?_⟩
have hrestNested : ∀ᵐ x ∂μX, ∀ᵐ w ∂ν,
0 < A (w.2.1, w.2.2) ∧ A (w.2.1, w.2.2) < ∞ :=
ae_of_all μX fun _ ↦ hrest.mono fun w hw ↦ ⟨hw.2.1, hw.2.2.1⟩
have hrestFull : ∀ᵐ w ∂fourBlockReference μX μY μV μZ,
0 < A (w.2.2.1, w.2.2.2) ∧ A (w.2.2.1, w.2.2.2) < ∞ := by
apply (Measure.ae_prod_iff_ae_ae (by measurability)).2
exact hrestNested
filter_upwards [hab, hpr, hrestFull] with w hdab hpa hAf
change d w = r (w.1, w.2.2.2) *
(A (w.2.2.1, w.2.2.2) * b (w.2.1, (w.2.2.1, w.2.2.2)))
rw [hdab]
change a (w.1, (w.2.2.1, w.2.2.2)) * b (w.2.1, (w.2.2.1, w.2.2.2)) = _
rw [← hpa]
change _ = (a (w.1, (w.2.2.1, w.2.2.2)) / A (w.2.2.1, w.2.2.2)) *
(A (w.2.2.1, w.2.2.2) * b (w.2.1, (w.2.2.1, w.2.2.2)))
rw [← mul_assoc, ENNReal.div_mul_cancel hAf.1.ne' hAf.2.ne]
ThreeBlockDensityIdentity 1 core · 2 supporting For a measurable finite density on a three-block product, a measurable factorization through the conditioning block is equivalent to the cross-multiplied identity between the joint density, its conditioning marginal, and ★ threeBlockFactors_iff_densityIdentity
Three-block density factorization versus the marginal-density identity
For a measurable finite density on a three-block product, a measurable factorization through the conditioning block is equivalent to the cross-multiplied identity between the joint density, its conditioning marginal, and its two block-with-conditioning marginals. This is the purely density-theoretic half of the three-block conditional-independence criterion.
theorem threeBlockFactors_iff_densityIdentity reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
For a measurable three-block density against a product of three σ-finite reference measures, with finite total mass, almost-everywhere factorization into a measurable term of the first and conditioning blocks times a measurable term of the second and conditioning blocks is equivalent to the almost-everywhere identity that the joint density times its conditioning marginal equals the product of its two block-with-conditioning marginals.
Formal statement
hypotheses
A :
Type uA
B :
Type uB
C :
Type uC
hd :
conclusion
ThreeBlockFactors muA muB muC d ↔ ThreeBlockDensityIdentity muA muB muC d
Proof (Lean source)
theorem threeBlockFactors_iff_densityIdentity (hd : Measurable d) :
ThreeBlockFactors muA muB muC d ↔ ThreeBlockDensityIdentity muA muB muC d :=
⟨threeBlockDensityIdentity_of_factors muA muB muC hd,
threeBlockFactors_of_densityIdentity muA muB muC hd⟩
2 supporting declarations (lemmas, instances)
-
threeBlockDensityIdentity_of_factorstheorem — A measurable conditional product factorization of a finite three-block density implies the cross-multiplied conditional-density identity.hypothesesA :sharedType uAB :sharedType uBC :sharedType uChd :hfac :ThreeBlockFactors muA muB muC dconclusionThreeBlockDensityIdentity muA muB muC dProof (Lean source)
theorem threeBlockDensityIdentity_of_factors (hd : Measurable d) (hfac : ThreeBlockFactors muA muB muC d) : ThreeBlockDensityIdentity muA muB muC d := by /- Expand all three marginal densities and use Tonelli to integrate the product factorization. Finiteness rules out the `0 * ∞` exceptional cases almost everywhere, after which the target is commutativity and associativity of multiplication in `ℝ≥0∞`. -/ rcases hfac with ⟨a, b, ha, hb, hab⟩ have hfirstMeas : Measurable (densityFirstConditioning muB d) := by apply Measurable.lintegral_prod_right change Measurable (fun q : (A × C) × B ↦ d (q.1.1, (q.2, q.1.2))) fun_prop have hsecondMeas : Measurable (densitySecondConditioning muA d) := by apply Measurable.lintegral_prod_right change Measurable (fun q : (B × C) × A ↦ d (q.2, (q.1.1, q.1.2))) fun_prop have hcondMeas : Measurable (densityConditioning muA muB d) := by apply Measurable.lintegral_prod_right change Measurable (fun q : C × A ↦ ∫⁻ b, d (q.2, (b, q.1)) ∂muB) apply Measurable.lintegral_prod_right change Measurable (fun q : (C × A) × B ↦ d (q.1.2, (q.2, q.1.1))) fun_prop have habABC : ∀ᵐ x ∂muA, ∀ᵐ y ∂muB, ∀ᵐ z ∂muC, d (x, (y, z)) = a (x, z) * b (y, z) := by filter_upwards [Measure.ae_ae_of_ae_prod hab] with x hx exact Measure.ae_ae_of_ae_prod hx have habACB : ∀ᵐ x ∂muA, ∀ᵐ z ∂muC, ∀ᵐ y ∂muB, d (x, (y, z)) = a (x, z) * b (y, z) := by filter_upwards [habABC] with x hx exact (Measure.ae_ae_comm (by measurability)).1 hx have habBCA : ∀ᵐ y ∂muB, ∀ᵐ z ∂muC, ∀ᵐ x ∂muA, d (x, (y, z)) = a (x, z) * b (y, z) := by have hswap : ∀ᵐ yz ∂muB.prod muC, ∀ᵐ x ∂muA, d (x, yz) = a (x, yz.2) * b yz := by apply (Measure.ae_ae_comm (by measurability)).1 exact Measure.ae_ae_of_ae_prod hab exact Measure.ae_ae_of_ae_prod hswap have hfirst : ∀ᵐ x ∂muA, ∀ᵐ z ∂muC, densityFirstConditioning muB d (x, z) = a (x, z) * ∫⁻ y, b (y, z) ∂muB := by filter_upwards [habACB] with x hx filter_upwards [hx] with z hz change (∫⁻ y, d (x, (y, z)) ∂muB) = _ rw [lintegral_congr_ae hz, lintegral_const_mul] fun_prop have hsecond : ∀ᵐ y ∂muB, ∀ᵐ z ∂muC, densitySecondConditioning muA d (y, z) = (∫⁻ x, a (x, z) ∂muA) * b (y, z) := by filter_upwards [habBCA] with y hy filter_upwards [hy] with z hz change (∫⁻ x, d (x, (y, z)) ∂muA) = _ rw [lintegral_congr_ae hz, lintegral_mul_const] fun_prop have hfirstCA : ∀ᵐ z ∂muC, ∀ᵐ x ∂muA, densityFirstConditioning muB d (x, z) = a (x, z) * ∫⁻ y, b (y, z) ∂muB := by apply (Measure.ae_ae_comm (by measurability)).1 exact hfirst have hcond : ∀ᵐ z ∂muC, densityConditioning muA muB d z = (∫⁻ x, a (x, z) ∂muA) * (∫⁻ y, b (y, z) ∂muB) := by filter_upwards [hfirstCA] with z hz have hz' : (fun x ↦ ∫⁻ y, d (x, (y, z)) ∂muB) =ᵐ[muA] (fun x ↦ a (x, z) * ∫⁻ y, b (y, z) ∂muB) := by filter_upwards [hz] with x hx exact hx change (∫⁻ x, ∫⁻ y, d (x, (y, z)) ∂muB ∂muA) = _ rw [lintegral_congr_ae hz', lintegral_mul_const] fun_prop apply (Measure.ae_prod_iff_ae_ae (by measurability)).2 filter_upwards [habABC, hfirst] with x hxy hxfirst apply (Measure.ae_prod_iff_ae_ae (by measurability)).2 filter_upwards [hxy, hsecond] with y hyz hysecond filter_upwards [hyz, hxfirst, hysecond, hcond] with z hdab hfirstz hsecondz hcondz rw [hdab, hfirstz, hsecondz, hcondz] ac_rfl -
threeBlockFactors_of_densityIdentitytheorem — For a measurable finite three-block density, the cross-multiplied conditional-density identity yields a measurable product factorization given the third block.hypothesesA :sharedType uAB :sharedType uBC :sharedType uChd :hid :ThreeBlockDensityIdentity muA muB muC dconclusionThreeBlockFactors muA muB muC dProof (Lean source)
theorem threeBlockFactors_of_densityIdentity (hd : Measurable d) (hid : ThreeBlockDensityIdentity muA muB muC d) : ThreeBlockFactors muA muB muC d := by /- Use `densityFirstConditioning muB d` as the first factor and the ratio of `densitySecondConditioning muA d` to `densityConditioning muA muB d` as the second. On fibres where the conditioning marginal vanishes, Tonelli implies that `d` vanishes almost everywhere; on the remaining fibres, finiteness permits cancellation in the density identity. -/ let dAC := densityFirstConditioning muB d let dBC := densitySecondConditioning muA d let dC := densityConditioning muA muB d have hdAC : Measurable dAC := by apply Measurable.lintegral_prod_right change Measurable (fun q : (A × C) × B ↦ d (q.1.1, (q.2, q.1.2))) fun_prop have hdBC : Measurable dBC := by apply Measurable.lintegral_prod_right change Measurable (fun q : (B × C) × A ↦ d (q.2, (q.1.1, q.1.2))) fun_prop have hdC : Measurable dC := by apply Measurable.lintegral_prod_right change Measurable (fun q : C × A ↦ ∫⁻ b, d (q.2, (b, q.1)) ∂muB) apply Measurable.lintegral_prod_right change Measurable (fun q : (C × A) × B ↦ d (q.1.2, (q.2, q.1.1))) fun_prop have hdInt : ∫⁻ q, d q ∂threeBlockReference muA muB muC ≠ ∞ := by have h := measure_ne_top ((threeBlockReference muA muB muC).withDensity d) univ simpa [withDensity_apply] using h have htotal : (∫⁻ c, dC c ∂muC) = ∫⁻ q, d q ∂threeBlockReference muA muB muC := by change (∫⁻ c, ∫⁻ a, ∫⁻ b, d (a, (b, c)) ∂muB ∂muA ∂muC) = _ rw [← lintegral_prod (fun q : C × A ↦ ∫⁻ b, d (q.2, (b, q.1)) ∂muB) (by fun_prop)] rw [lintegral_prod_symm (fun q : C × A ↦ ∫⁻ b, d (q.2, (b, q.1)) ∂muB) (by fun_prop)] change _ = ∫⁻ q, d q ∂muA.prod (muB.prod muC) rw [lintegral_prod d hd.aemeasurable] apply lintegral_congr intro a rw [← lintegral_prod (fun q : C × B ↦ d (a, (q.2, q.1))) (by fun_prop)] rw [lintegral_prod_symm (fun q : C × B ↦ d (a, (q.2, q.1))) (by fun_prop)] rw [← lintegral_prod (fun q : B × C ↦ d (a, q)) (by fun_prop)] have hdCInt : ∫⁻ c, dC c ∂muC ≠ ∞ := by rwa [htotal] have hdCFinite : ∀ᵐ c ∂muC, dC c < ∞ := ae_lt_top hdC hdCInt have hzeroC : ∀ᵐ c ∂muC, ∀ᵐ a ∂muA, ∀ᵐ b ∂muB, dC c = 0 → dAC (a, c) = 0 ∧ d (a, (b, c)) = 0 := by refine ae_of_all muC fun c ↦ ?_ by_cases hc : dC c = 0 · have hACzero : (fun a ↦ dAC (a, c)) =ᵐ[muA] 0 := by apply (lintegral_eq_zero_iff (by fun_prop)).1 simpa only [dC, dAC, densityConditioning, densityFirstConditioning] using hc filter_upwards [hACzero] with a ha0 change dAC (a, c) = 0 at ha0 have hdzero : (fun b ↦ d (a, (b, c))) =ᵐ[muB] 0 := by apply (lintegral_eq_zero_iff (by fun_prop)).1 simpa only [dAC, densityFirstConditioning] using ha0 filter_upwards [hdzero] with b hb0 exact fun _ ↦ ⟨ha0, hb0⟩ · exact ae_of_all muA fun _ ↦ ae_of_all muB fun _ h ↦ (hc h).elim have hzeroFlat : ∀ᵐ q ∂muC.prod (muA.prod muB), dC q.1 = 0 → dAC (q.2.1, q.1) = 0 ∧ d (q.2.1, (q.2.2, q.1)) = 0 := by apply (Measure.ae_prod_iff_ae_ae (by measurability)).2 filter_upwards [hzeroC] with c hc exact (Measure.ae_prod_iff_ae_ae (by measurability)).2 hc have hzeroSwap : ∀ᵐ ab ∂muA.prod muB, ∀ᵐ c ∂muC, dC c = 0 → dAC (ab.1, c) = 0 ∧ d (ab.1, (ab.2, c)) = 0 := by apply (Measure.ae_ae_comm (by measurability)).1 exact Measure.ae_ae_of_ae_prod hzeroFlat have hzeroABC : ∀ᵐ a ∂muA, ∀ᵐ b ∂muB, ∀ᵐ c ∂muC, dC c = 0 → dAC (a, c) = 0 ∧ d (a, (b, c)) = 0 := by exact Measure.ae_ae_of_ae_prod hzeroSwap have hidABC : ∀ᵐ a ∂muA, ∀ᵐ b ∂muB, ∀ᵐ c ∂muC, d (a, (b, c)) * dC c = dAC (a, c) * dBC (b, c) := by filter_upwards [Measure.ae_ae_of_ae_prod hid] with a ha exact Measure.ae_ae_of_ae_prod ha refine ⟨dAC, fun bc ↦ dBC bc / dC bc.2, hdAC, hdBC.div (hdC.comp measurable_snd), ?_⟩ apply (Measure.ae_prod_iff_ae_ae (by measurability)).2 filter_upwards [hidABC, hzeroABC] with a ha hza apply (Measure.ae_prod_iff_ae_ae (by measurability)).2 filter_upwards [ha, hza] with b hb hzb filter_upwards [hb, hzb, hdCFinite] with c hidc hzc hfin by_cases hc0 : dC c = 0 · rw [(hzc hc0).2, (hzc hc0).1] simp · symm calc dAC (a, c) * (dBC (b, c) / dC c) = (dAC (a, c) * dBC (b, c)) / dC c := by simp only [div_eq_mul_inv] ac_rfl _ = (d (a, (b, c)) * dC c) / dC c := by rw [hidc] _ = d (a, (b, c)) := ENNReal.mul_div_cancel_right hc0 hfin.ne
ThreeBlockFactorization 1 core · 3 supporting This module proves the three-block criterion used by the four-block intersection theorem: for a measurable finite density on a product of standard Borel spaces, the first two blocks are conditionally independent given th ★ condIndepFun_threeBlock_iff_factors
Three-block conditional-density factorization
This module proves the three-block criterion used by the four-block intersection theorem: for a
measurable finite density on a product of standard Borel spaces, the first two blocks are
conditionally independent given the third exactly when the density satisfies the
marginal-density identity, equivalently when it factors through the conditioning block. The
density-theoretic equivalence of those two conditions lives in ThreeBlockDensityIdentity.
theorem condIndepFun_threeBlock_iff_factors reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.DensityIntersection
For three σ-finite reference measures on standard Borel spaces and a measurable three-block density of finite total mass, conditional independence of the first two blocks given the third under the density-weighted measure is equivalent to the density being almost everywhere a product of a measurable term of the first and third blocks and a measurable term of the second and third blocks.
Formal statement
hypotheses
A :
Type uA
B :
Type uB
C :
Type uC
hd :
conclusion
CondIndepFun (comap (@thirdThreeCoord A B C) inferInstance) measurable_thirdThreeCoord.comap_le (@firstThreeCoord A B C) (@secondThreeCoord A B C) ((threeBlockReference muA muB muC).withDensity d)
↔ ThreeBlockFactors muA muB muC d
Proof (Lean source)
theorem condIndepFun_threeBlock_iff_factors (hd : Measurable d) :
CondIndepFun
(comap (@thirdThreeCoord A B C) inferInstance)
measurable_thirdThreeCoord.comap_le
(@firstThreeCoord A B C) (@secondThreeCoord A B C)
((threeBlockReference muA muB muC).withDensity d) ↔
ThreeBlockFactors muA muB muC d := by
rw [condIndepFun_threeBlock_iff_densityIdentity muA muB muC hd,
threeBlockFactors_iff_densityIdentity muA muB muC hd]
3 supporting declarations (lemmas, instances)
-
threeBlockDensityIdentity_of_condIndepFuntheorem — Conditional independence of the first two coordinates given the third coordinate implies the cross-multiplied identity for any measurable finite density relative to a product reference.hypothesesA :sharedType uAB :sharedType uBC :sharedType uChd :hci :CondIndepFun (comap (@thirdThreeCoord A B C) inferInstance) measurable_thirdThreeCoord.comap_le (@firstThreeCoord A B C) (@secondThreeCoord A B C) ((threeBlockReference muA muB muC).withDensity d)conclusionThreeBlockDensityIdentity muA muB muC dProof (Lean source)
theorem threeBlockDensityIdentity_of_condIndepFun (hd : Measurable d) (hci : CondIndepFun (comap (@thirdThreeCoord A B C) inferInstance) measurable_thirdThreeCoord.comap_le (@firstThreeCoord A B C) (@secondThreeCoord A B C) ((threeBlockReference muA muB muC).withDensity d)) : ThreeBlockDensityIdentity muA muB muC d := by cases isEmpty_or_nonempty A with | inl hA => letI := hA exact ae_of_all _ fun q ↦ isEmptyElim q.1 | inr hA => letI := hA cases isEmpty_or_nonempty B with | inl hB => letI := hB exact ae_of_all _ fun q ↦ isEmptyElim q.2.1 | inr hB => letI := hB exact (threeBlockDensityIdentity_iff_ratio muA muB muC hd).2 ((condIndepFun_threeBlock_iff_ratio muA muB muC hd).1 hci) -
condIndepFun_threeBlock_of_densityIdentitytheorem — The cross-multiplied identity for a measurable finite product density implies conditional independence of the first two coordinates given the third coordinate.hypothesesA :sharedType uAB :sharedType uBC :sharedType uChd :hid :ThreeBlockDensityIdentity muA muB muC dconclusionCondIndepFun (comap (@thirdThreeCoord A B C) inferInstance) measurable_thirdThreeCoord.comap_le (@firstThreeCoord A B C) (@secondThreeCoord A B C) ((threeBlockReference muA muB muC).withDensity d)Proof (Lean source)
theorem condIndepFun_threeBlock_of_densityIdentity (hd : Measurable d) (hid : ThreeBlockDensityIdentity muA muB muC d) : CondIndepFun (comap (@thirdThreeCoord A B C) inferInstance) measurable_thirdThreeCoord.comap_le (@firstThreeCoord A B C) (@secondThreeCoord A B C) ((threeBlockReference muA muB muC).withDensity d) := by cases isEmpty_or_nonempty A with | inl hA => letI := hA rw [condIndepFun_iff_condExp_inter_preimage_eq_mul measurable_firstThreeCoord measurable_secondThreeCoord] intro s t hs ht exact ae_of_all _ fun q ↦ isEmptyElim q.1 | inr hA => letI := hA cases isEmpty_or_nonempty B with | inl hB => letI := hB rw [condIndepFun_iff_condExp_inter_preimage_eq_mul measurable_firstThreeCoord measurable_secondThreeCoord] intro s t hs ht exact ae_of_all _ fun q ↦ isEmptyElim q.2.1 | inr hB => letI := hB exact (condIndepFun_threeBlock_iff_ratio muA muB muC hd).2 ((threeBlockDensityIdentity_iff_ratio muA muB muC hd).1 hid) -
condIndepFun_threeBlock_iff_densityIdentitytheorem — For a measurable finite density over a three-fold product reference, conditional independence of the first two coordinates given the third is equivalent to the marginal-density identity.hypothesesA :sharedType uAB :sharedType uBC :sharedType uChd :conclusionCondIndepFun (comap (@thirdThreeCoord A B C) inferInstance) measurable_thirdThreeCoord.comap_le (@firstThreeCoord A B C) (@secondThreeCoord A B C) ((threeBlockReference muA muB muC).withDensity d)↔ ThreeBlockDensityIdentity muA muB muC dProof (Lean source)
theorem condIndepFun_threeBlock_iff_densityIdentity (hd : Measurable d) : CondIndepFun (comap (@thirdThreeCoord A B C) inferInstance) measurable_thirdThreeCoord.comap_le (@firstThreeCoord A B C) (@secondThreeCoord A B C) ((threeBlockReference muA muB muC).withDensity d) ↔ ThreeBlockDensityIdentity muA muB muC d := ⟨threeBlockDensityIdentity_of_condIndepFun muA muB muC hd, condIndepFun_threeBlock_of_densityIdentity muA muB muC hd⟩