Graph.Finite­Density.Positive

theorem condDistrib_child_given_parents (i : V) : let P := G.parents i let x₀ : ∀ k, X k := Classical.choice inferInstance let d : (∀ k : P, X k) → X i → ℝ≥0∞ := fun p z ↦ M.toFactorization.factor i (update (coordinateExtension P x₀ p) i z) condDistrib (fun x : ∀ k, X k ↦ x i) (coordinateProjection (X := X) P) M.observationalMeasure =ᵐ[Measure.map (coordinateProjection (X := X) P) M.observationalMeasure] Kernel.withDensity (Kernel.const (∀ k : P, X k) (μ i)) d := by classical dsimp only let P := G.parents i let x₀ : ∀ k, X k := Classical.choice inferInstance let d : (∀ k : P, X k) → X i → ℝ≥0∞ := fun p z ↦ M.toFactorization.factor i (update (coordinateExtension P x₀ p) i z) have hd : Measurable (uncurry d) := by unfold d exact (M.toFactorization.measurable_factor i).comp (measurable_update'.comp (((measurable_coordinateExtension P x₀).comp measurable_fst).prodMk measurable_snd)) let κ : Kernel (∀ k : P, X k) (X i) := Kernel.withDensity (Kernel.const (∀ k : P, X k) (μ i)) d have hκ_apply (p : ∀ k : P, X k) : κ p = (μ i).withDensity (d p) := by dsimp [κ] rw [Kernel.withDensity_apply _ hd, Kernel.const_apply] have hd_eq (x : ∀ k, X k) (z : X i) : d (coordinateProjection (X := X) P x) z = M.toFactorization.factor i (update x i z) := by unfold d apply M.toFactorization.local_factor i intro k hk rcases Finset.mem_insert.mp hk with rfl | hk · simp · have hki : k ≠ i := by intro hki subst k exact G.irrefl i (G.mem_parents.mp hk) have hkP : k ∈ P := by simpa [P] using hk simp [coordinateExtension, coordinateProjection, hkP, hki] letI : IsFiniteKernel κ := ⟨1, ENNReal.one_lt_top, fun p ↦ by rw [hκ_apply, withDensity_apply _ MeasurableSet.univ] simp only [Measure.restrict_univ] change ∫⁻ z, M.toFactorization.factor i (update (coordinateExtension P x₀ p) i z) ∂μ i ≤ 1 rw [M.toFactorization.normalized_factor]⟩ apply condDistrib_ae_eq_of_measure_eq_compProd_of_measurable (measurable_coordinateProjection P) (measurable_pi_apply i) apply Measure.ext_prod intro s t hs ht rw [Measure.map_apply (by fun_prop) (hs.prod ht), Measure.compProd_apply_prod hs ht] rw [← lintegral_indicator_one ((hs.prod ht).preimage ((measurable_coordinateProjection P).prodMk (measurable_pi_apply i)))] rw [← lintegral_indicator hs] rw [lintegral_map ((Kernel.measurable_coe κ ht).indicator hs) (measurable_coordinateProjection P)] simp_rw [hκ_apply, withDensity_apply _ ht] calc (∫⁻ a, ((fun x : ∀ k, X k ↦ (coordinateProjection (X := X) P x, x i)) ⁻¹' (s ×ˢ t)).indicator 1 a ∂M.observationalMeasure) = ∫⁻ x, s.indicator 1 (coordinateProjection (X := X) P x) * t.indicator 1 (x i) ∂M.observationalMeasure := by apply lintegral_congr intro x by_cases hp : coordinateProjection (X := X) P x ∈ s <;> by_cases hi : x i ∈ t <;> simp [indicator, hp, hi] _ = ∫⁻ x, s.indicator 1 (coordinateProjection (X := X) P x) * (∫⁻ z, t.indicator 1 z * M.toFactorization.factor i (update x i z) ∂μ i) ∂M.observationalMeasure := _root_.Causalean.Graph.FiniteDensity.Factorization.lintegral_node_given_parents M.toFactorization i (s.indicator 1) (t.indicator 1) (measurable_const.indicator hs) (measurable_const.indicator ht) _ = ∫⁻ a, s.indicator (fun p ↦ ∫⁻ z in t, d p z ∂μ i) (coordinateProjection (X := X) P a) ∂M.observationalMeasure := by apply lintegral_congr intro x by_cases hp : coordinateProjection (X := X) P x ∈ s · simp only [Set.indicator_of_mem hp, Pi.one_apply, one_mul] rw [← lintegral_indicator ht] apply lintegral_congr intro z by_cases hz : z ∈ t <;> simp [indicator, hz, hd_eq] · simp [indicator, hp]

theorem sum_jointMass : ∑ x : ∀ i, X i, M.jointMass x = 1 := by letI : ∀ i, MeasurableSpace (X i) := fun _ => ⊤ let μ : ∀ i, Measure (X i) := fun _ => Measure.count haveI : ∀ i, SigmaFinite (μ i) := fun _ => inferInstance let B : Factorization G X μ := { factor := fun i x => ofReal (M.factor i x) measurable_factor := by intro i exact measurable_of_countable _ local_factor := by intro i x y hxy exact congrArg ofReal (M.factor_local i hxy) normalized_factor := by intro i x rw [MeasureTheory.lintegral_count, tsum_fintype, ← ENNReal.ofReal_sum_of_nonneg] · rw [M.factor_normalized] simp · intro z _ exact (M.factor_pos i _).le } have hpi : Measure.pi μ = (Measure.count : Measure (∀ i, X i)) := by apply Measure.ext_of_singleton intro x rw [Measure.pi_singleton, Measure.count_singleton] dsimp [μ] simp have hobs (x : ∀ i, X i) : B.observationalDensity x = ofReal (M.jointMass x) := by change (∏ i ∈ univ, ofReal (M.factor i x)) = ofReal (∏ i ∈ univ, M.factor i x) rw [ENNReal.ofReal_prod_of_nonneg] intro i _ exact (M.factor_pos i x).le let x₀ : ∀ i, X i := fun i => choice (inferInstance : Nonempty (X i)) have hmarg := B.lmarginal_compl_observationalDensity_eq (A := ∅) (by intro i hi simp at hi) have hint : ∫⁻ x, B.observationalDensity x ∂Measure.pi μ = 1 := by rw [MeasureTheory.lintegral_eq_lmarginal_univ x₀] simpa [Factorization.partialDensity] using congrFun hmarg x₀ rw [hpi, MeasureTheory.lintegral_count, tsum_fintype] at hint simp_rw [hobs] at hint rw [← ENNReal.ofReal_sum_of_nonneg] at hint · exact ENNReal.ofReal_eq_one.mp hint · intro x _ exact (Finset.prod_pos fun i _ => M.factor_pos i x).le

theorem marginalMass_pos (S : Finset V) (x : ∀ i, X i) : 0 < M.marginalMass S x := by unfold marginalMass apply Finset.sum_pos' · intro y _ split_ifs · exact (Finset.prod_pos fun i _ => M.factor_pos i y).le · exact le_rfl · refine ⟨x, Finset.mem_univ x, ?_⟩ simp only [ite_true] exact Finset.prod_pos fun i _ => M.factor_pos i x

theorem conditionalMass_given_parents (i : V) (x : ∀ i, X i) (z : X i) : M.conditionalMass i (G.parents i) x z = M.factor i (update x i z) := by letI : ∀ i, MeasurableSpace (X i) := fun _ => ⊤ let μ : ∀ i, Measure (X i) := fun _ => Measure.count haveI : ∀ i, SigmaFinite (μ i) := fun _ => inferInstance let B : Factorization G X μ := { factor := fun i x => ofReal (M.factor i x) measurable_factor := by intro i exact measurable_of_countable _ local_factor := by intro i x y hxy exact congrArg ofReal (M.factor_local i hxy) normalized_factor := by intro i x rw [lintegral_count, tsum_fintype, ← ENNReal.ofReal_sum_of_nonneg] · rw [M.factor_normalized] simp · intro w _ exact (M.factor_pos i _).le } have hpi : Measure.pi μ = (Measure.count : Measure (∀ i, X i)) := by apply Measure.ext_of_singleton intro y rw [Measure.pi_singleton, Measure.count_singleton] dsimp [μ] simp have hobs (y : ∀ i, X i) : B.observationalDensity y = ofReal (M.jointMass y) := by change (∏ i ∈ univ, ofReal (M.factor i y)) = ofReal (∏ i ∈ univ, M.factor i y) rw [ENNReal.ofReal_prod_of_nonneg] intro j _ exact (M.factor_pos j y).le have hcyl (S : Finset V) (a : ∀ i, X i) : ofReal (M.marginalMass S a) = ∫⁻ y, (if coordinateProjection (X := X) S y = coordinateProjection (X := X) S a then 1 else 0) ∂B.observationalMeasure := by rw [Factorization.observationalMeasure, lintegral_withDensity_eq_lintegral_mul _ B.measurable_observationalDensity (measurable_of_countable _)] rw [hpi, lintegral_count, tsum_fintype] unfold marginalMass rw [ENNReal.ofReal_sum_of_nonneg] · apply Finset.sum_congr rfl intro y _ change ofReal (if coordinateProjection (X := X) S y = coordinateProjection (X := X) S a then M.jointMass y else 0) = B.observationalDensity y * (if coordinateProjection (X := X) S y = coordinateProjection (X := X) S a then 1 else 0) rw [hobs] by_cases hy : coordinateProjection (X := X) S y = coordinateProjection (X := X) S a · simp [hy] · simp [hy] · intro y _ by_cases hy : coordinateProjection (X := X) S y = coordinateProjection (X := X) S a · simp [hy] exact (Finset.prod_pos fun j _ => M.factor_pos j y).le · simp [hy] let h : (∀ k : G.parents i, X k) → ℝ≥0∞ := fun p => if p = coordinateProjection (X := X) (G.parents i) x then 1 else 0 let g : X i → ℝ≥0∞ := fun w => if w = z then 1 else 0 have hnode := _root_.Causalean.Graph.FiniteDensity.Factorization.lintegral_node_given_parents B i h g (measurable_of_countable _) (measurable_of_countable _) have hinner (y : ∀ i, X i) : (∫⁻ w, g w * B.factor i (update y i w) ∂μ i) = B.factor i (update y i z) := by rw [lintegral_count, tsum_fintype] simp [g] have hmeasure : ofReal (M.marginalMass (insert i (G.parents i)) (update x i z)) = ofReal (M.factor i (update x i z)) * ofReal (M.marginalMass (G.parents i) x) := by rw [hcyl, hcyl] calc (∫⁻ y, (if coordinateProjection (X := X) (insert i (G.parents i)) y = coordinateProjection (X := X) (insert i (G.parents i)) (update x i z) then 1 else 0) ∂B.observationalMeasure) = ∫⁻ y, h (coordinateProjection (X := X) (G.parents i) y) * g (y i) ∂B.observationalMeasure := by apply lintegral_congr intro y by_cases hyi : y i = z <;> by_cases hyp : coordinateProjection (X := X) (G.parents i) y = coordinateProjection (X := X) (G.parents i) x <;> simp [h, g, projection_insert_update_iff, hyi, hyp] _ = ∫⁻ y, h (coordinateProjection (X := X) (G.parents i) y) * (∫⁻ w, g w * B.factor i (update y i w) ∂μ i) ∂B.observationalMeasure := hnode _ = ∫⁻ y, ofReal (M.factor i (update x i z)) * h (coordinateProjection (X := X) (G.parents i) y) ∂B.observationalMeasure := by apply lintegral_congr intro y rw [hinner] by_cases hy : coordinateProjection (X := X) (G.parents i) y = coordinateProjection (X := X) (G.parents i) x · change h _ * ofReal (M.factor i (update y i z)) = _ rw [factor_update_eq_of_projection_eq M i x y z hy] simp [h, hy] · simp [h, hy] _ = ofReal (M.factor i (update x i z)) * ∫⁻ y, h (coordinateProjection (X := X) (G.parents i) y) ∂B.observationalMeasure := by rw [lintegral_const_mul] exact measurable_of_countable _ _ = ofReal (M.factor i (update x i z)) * ∫⁻ y, (if coordinateProjection (X := X) (G.parents i) y = coordinateProjection (X := X) (G.parents i) x then 1 else 0) ∂B.observationalMeasure := by rfl have hreal : M.marginalMass (insert i (G.parents i)) (update x i z) = M.factor i (update x i z) * M.marginalMass (G.parents i) x := by rw [← ENNReal.ofReal_eq_ofReal_iff] · rw [ENNReal.ofReal_mul (M.factor_pos i _).le] exact hmeasure · exact (M.marginalMass_pos _ _).le · exact mul_nonneg (M.factor_pos i _).le (M.marginalMass_pos _ _).le unfold conditionalMass rw [hreal] exact mul_div_cancel_right₀ _ (ne_of_gt (M.marginalMass_pos (G.parents i) x))

theorem edge_condIndep_iff_factorIndependent {i j : V} (hji : G.edge j i) : M.CondIndepCoordinates i j ((G.parents i).erase j) ↔ M.FactorIndependentOf i j := by classical let C := (G.parents i).erase j have hij : i ≠ j := by intro hij subst j exact G.irrefl i hji have hparents : insert j C = G.parents i := Finset.insert_erase (G.mem_parents.mpr hji) constructor · intro hCI x xj have heq (z : X j) : M.factor i (update x j z) * M.marginalMass C x = M.marginalMass (insert i C) x := by have h := hCI x (x i) z rw [show (G.parents i).erase j = C from rfl, hparents] at h have hnum : M.marginalMass (insert i (G.parents i)) (update (update x i (x i)) j z) = M.factor i (update x j z) * M.marginalMass (G.parents i) (update x j z) := by have hcoord : update x j z i = x i := Function.update_of_ne hij z x have hidem : update (update x j z) i (x i) = update x j z := by rw [← hcoord, Function.update_eq_self] simpa [hidem] using marginalMass_insert_parents_eq_factor_mul M i (update x j z) (x i) rw [hnum] at h simp only [Function.update_eq_self] at h apply (mul_right_cancel₀ (ne_of_gt (M.marginalMass_pos (G.parents i) (update x j z)))) ring_nf at h ⊢ exact h have hnew := heq xj have hold := heq (x j) simp only [Function.update_eq_self] at hold apply (mul_right_cancel₀ (ne_of_gt (M.marginalMass_pos C x))) exact hnew.trans hold.symm · intro hind x xi xj rw [show (G.parents i).erase j = C from rfl, hparents] have hnum : M.marginalMass (insert i (G.parents i)) (update (update x i xi) j xj) = M.factor i (update (update x i xi) j xj) * M.marginalMass (G.parents i) (update x j xj) := by simpa [Function.update_comm hij] using marginalMass_insert_parents_eq_factor_mul M i (update x j xj) xi rw [hnum, marginalMass_insert_child_eq_factor_mul_of_independent M hji hind] rw [hind (update x i xi) xj] ring

theorem factorIndependent_iff_localContrast_zero {i j : V} (hji : G.edge j i) : M.FactorIndependentOf i j ↔ ∀ (x : ∀ k, X k) (xi xi' : X i) (xj xj' : X j), M.localContrast i j x xi xi' xj xj' = 0 := by constructor · intro hind x xi xi' xj xj' have hij : i ≠ j := by intro hij subst j exact G.irrefl i hji unfold localContrast rw [hind (update x i xi) xj, hind (update x i xi') xj', hind (update x i xi) xj', hind (update x i xi') xj] ring · intro hzero x xj have hij : i ≠ j := by intro hij subst j exact G.irrefl i hji have hcross (z w : X i) : M.factor i (update (update x j xj) i z) * M.factor i (update x i w) = M.factor i (update x i z) * M.factor i (update (update x j xj) i w) := by apply sub_eq_zero.mp simpa [localContrast, Function.update_comm hij] using hzero x z w xj (x j) have hsum (z : X i) : M.factor i (update (update x j xj) i z) = M.factor i (update x i z) := by have hs := Finset.sum_congr rfl (fun w (_ : w ∈ univ) ↦ hcross z w) calc M.factor i (update (update x j xj) i z) = M.factor i (update (update x j xj) i z) * 1 := by ring _ = M.factor i (update (update x j xj) i z) * ∑ w : X i, M.factor i (update x i w) := by rw [M.factor_normalized] _ = ∑ w : X i, M.factor i (update (update x j xj) i z) * M.factor i (update x i w) := Finset.mul_sum _ _ _ _ = ∑ w : X i, M.factor i (update x i z) * M.factor i (update (update x j xj) i w) := hs _ = M.factor i (update x i z) * ∑ w : X i, M.factor i (update (update x j xj) i w) := (Finset.mul_sum _ _ _).symm _ = M.factor i (update x i z) := by rw [M.factor_normalized] ring have hz := hsum (x i) have hcoord : update x j xj i = x i := Function.update_of_ne hij xj x have hidem : update (update x j xj) i (x i) = update x j xj := by rw [← hcoord, Function.update_eq_self] simpa [hidem] using hz

theorem aeFactorIndependent_of_edge_condIndep {i j : V} (hji : G.edge j i) : M.CondIndepCoordinates i j ((G.parents i).erase j) → M.AEFactorIndependentOf i j := by /- Use `lintegral_node_given_parents` with bounded indicator tests to identify the conditional law of `i` given all parents. Conditional independence drops `j` from that law. Strict positivity makes the observational law equivalent to the product reference law, after which uniqueness of Radon–Nikodym densities gives the iterated-a.e. update identity. Useful library bridges are `condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight` (after `CondIndepFun.symm`) for dropping `j` from the conditional kernel, and `MeasureTheory.withDensity_ae_eq` (or `withDensity_absolutelyContinuous'`) for transferring the resulting observational-a.e. statement to `Measure.pi μ`. -/ intro hCI classical let C := (G.parents i).erase j let P := G.parents i let Y : (∀ k, X k) → X i := fun x ↦ x i let J : (∀ k, X k) → X j := fun x ↦ x j let K := coordinateProjection (X := X) C let R := coordinateProjection (X := X) P let e := parentSplitEquiv (X := X) hji have he : e ∘ R = fun x ↦ (K x, J x) := by funext x change e (R x) = (K x, J x) rw [show e (R x) = (fun k : (G.parents i).erase j ↦ R x ⟨k, mem_of_mem_erase k.property⟩, R x ⟨j, G.mem_parents.mpr hji⟩) by exact parentSplitEquiv_apply (X := X) hji (R x)] rfl have hdrop : condDistrib Y (fun x ↦ (K x, J x)) M.observationalMeasure =ᵐ[Measure.map (fun x ↦ (K x, J x)) M.observationalMeasure] (condDistrib Y K M.observationalMeasure).prodMkRight _ := by apply (condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight (f := Y) (g := J) (k := K) (by fun_prop) (by fun_prop) (by fun_prop)).mp simpa [CondIndepCoordinates, Y, J, K, C] using hCI.symm have hreparam := condDistrib_comp_right_measurableEquiv M.observationalMeasure e (Y := Y) (X := R) (by fun_prop) (by fun_prop) have hparent := M.condDistrib_child_given_parents i change condDistrib Y R M.observationalMeasure =ᵐ[Measure.map R M.observationalMeasure] _ at hparent have hmap : Measure.map e (Measure.map R M.observationalMeasure) = Measure.map (fun x ↦ (K x, J x)) M.observationalMeasure := by rw [Measure.map_map e.measurable (by fun_prop), he] have hdrop' : (fun p ↦ condDistrib Y (fun x ↦ (K x, J x)) M.observationalMeasure (e p)) =ᵐ[Measure.map R M.observationalMeasure] fun p ↦ condDistrib Y K M.observationalMeasure (e p).1 := by have h := ae_of_ae_map (μ := Measure.map R M.observationalMeasure) e.measurable.aemeasurable (by rw [hmap]; exact hdrop) filter_upwards [h] with p hp simpa using hp have hparent_drop : (fun p ↦ (Kernel.withDensity (Kernel.const (∀ k : P, X k) (μ i)) (fun p z ↦ M.toFactorization.factor i (update (coordinateExtension P (Classical.choice inferInstance) p) i z))) p) =ᵐ[Measure.map R M.observationalMeasure] fun p ↦ condDistrib Y K M.observationalMeasure (e p).1 := by filter_upwards [hparent, hreparam, hdrop'] with p hp hr hd exact hp.symm.trans (hr.symm.trans hd) have hobs := ae_of_ae_map (μ := M.observationalMeasure) (show AEMeasurable R M.observationalMeasure by fun_prop) hparent_drop have hfactor_ne_zero (k : V) (x : ∀ l, X l) : M.toFactorization.factor k x ≠ 0 := by intro hk have hle := M.lower_le_factor k x rw [hk] at hle simp only [ENNReal.toReal_zero] at hle exact (not_lt_of_ge hle) M.lower_pos have hdensity_ne_zero : ∀ᵐ x ∂Measure.pi μ, M.toFactorization.observationalDensity x ≠ 0 := Filter.Eventually.of_forall fun x ↦ Finset.prod_ne_zero_iff.mpr fun k _ ↦ hfactor_ne_zero k x have hpi : (fun x ↦ (Kernel.withDensity (Kernel.const (∀ k : P, X k) (μ i)) (fun p z ↦ M.toFactorization.factor i (update (coordinateExtension P (Classical.choice inferInstance) p) i z))) (R x)) =ᵐ[Measure.pi μ] fun x ↦ condDistrib Y K M.observationalMeasure (e (R x)).1 := (withDensity_ae_eq M.toFactorization.measurable_observationalDensity.aemeasurable hdensity_ne_zero).mp (by change (fun x ↦ (Kernel.withDensity (Kernel.const (∀ k : P, X k) (μ i)) (fun p z ↦ M.toFactorization.factor i (update (coordinateExtension P (Classical.choice inferInstance) p) i z))) (R x)) =ᵐ[M.observationalMeasure] fun x ↦ condDistrib Y K M.observationalMeasure (e (R x)).1 exact hobs) let split := MeasurableEquiv.piEquivPiSubtypeProd X (fun k ↦ k ∈ C) let μC : Measure (∀ k : {k // k ∈ C}, X k) := @Measure.pi {k : V // k ∈ C} (fun k ↦ X k) (fintype fun k ↦ k ∈ C) (fun k ↦ inferInstance) (fun k ↦ μ k) let μD : Measure (∀ k : {k // k ∉ C}, X k) := @Measure.pi {k : V // k ∉ C} (fun k ↦ X k) (fintype fun k ↦ k ∉ C) (fun k ↦ inferInstance) (fun k ↦ μ k) have hsplit_pres : MeasurePreserving split (Measure.pi μ) (μC.prod μD) := by simpa [split, μC, μD] using measurePreserving_piEquivPiSubtypeProd μ (fun k ↦ k ∈ C) have hsplit : ∀ᵐ q ∂μC.prod μD, (Kernel.withDensity (Kernel.const (∀ k : P, X k) (μ i)) (fun p z ↦ M.toFactorization.factor i (update (coordinateExtension P (Classical.choice inferInstance) p) i z))) (R (split.symm q)) = condDistrib Y K M.observationalMeasure q.1 := by have hs := ae_of_ae_map (μ := μC.prod μD) split.symm.measurable.aemeasurable (by rw [(MeasurePreserving.symm split hsplit_pres).map_eq] exact hpi) filter_upwards [hs] with q hq rw [hq] congr 1 change ((e ∘ R) (split.symm q)).1 = q.1 rw [he] change K (split.symm q) = q.1 funext k simp [K, coordinateProjection, split] have hsplit_nested := Measure.ae_ae_of_ae_prod hsplit let x₀ : ∀ k, X k := Classical.choice inferInstance let d : (∀ k : P, X k) → X i → ℝ≥0∞ := fun p z ↦ M.toFactorization.factor i (update (coordinateExtension P x₀ p) i z) have hd : Measurable (uncurry d) := by unfold d exact (M.toFactorization.measurable_factor i).comp (measurable_update'.comp (((measurable_coordinateExtension P x₀).comp measurable_fst).prodMk measurable_snd)) let κ : Kernel (∀ k : P, X k) (X i) := Kernel.withDensity (Kernel.const (∀ k : P, X k) (μ i)) d have hκ_apply (p : ∀ k : P, X k) : κ p = (μ i).withDensity (d p) := by dsimp [κ] rw [Kernel.withDensity_apply _ hd, Kernel.const_apply] have hd_eq (x : ∀ k, X k) (z : X i) : d (R x) z = M.toFactorization.factor i (update x i z) := by unfold d apply M.toFactorization.local_factor i intro k hk rcases Finset.mem_insert.mp hk with rfl | hk · simp · have hki : k ≠ i := by intro hki subst k exact G.irrefl i (G.mem_parents.mp hk) have hkP : k ∈ P := by simpa [P] using hk simp [R, coordinateProjection, coordinateExtension, hkP, hki] have hsection_ae : ∀ᵐ c ∂μC, ∀ᵐ r₁ ∂μD, ∀ᵐ r₂ ∂μD, ∀ᵐ z ∂μ i, M.toFactorization.factor i (update (split.symm (c, r₁)) i z) = M.toFactorization.factor i (update (split.symm (c, r₂)) i z) := by filter_upwards [hsplit_nested] with c hc filter_upwards [hc] with r₁ hr₁ filter_upwards [hc] with r₂ hr₂ have hκ : κ (R (split.symm (c, r₁))) = κ (R (split.symm (c, r₂))) := by exact hr₁.trans hr₂.symm have hden : d (R (split.symm (c, r₁))) =ᵐ[μ i] d (R (split.symm (c, r₂))) := (withDensity_eq_iff_of_sigmaFinite (Measurable.of_uncurry_left hd (x := R (split.symm (c, r₁)))).aemeasurable (Measurable.of_uncurry_left hd (x := R (split.symm (c, r₂)))).aemeasurable).mp (by rw [← hκ_apply, ← hκ_apply] exact hκ) filter_upwards [hden] with z hz simpa only [hd_eq] using hz let f : ((∀ k : {k // k ∈ C}, X k) × ((∀ k : {k // k ∉ C}, X k) × ((∀ k : {k // k ∉ C}, X k) × X i))) → ℝ := fun q ↦ (M.toFactorization.factor i (update (split.symm (q.1, q.2.1)) i q.2.2.2)).toReal let g : ((∀ k : {k // k ∈ C}, X k) × ((∀ k : {k // k ∉ C}, X k) × ((∀ k : {k // k ∉ C}, X k) × X i))) → ℝ := fun q ↦ (M.toFactorization.factor i (update (split.symm (q.1, q.2.2.1)) i q.2.2.2)).toReal have hsplit_cont : Continuous split.symm := by change Continuous (Homeomorph.piEquivPiSubtypeProd (fun k ↦ k ∈ C) X).symm exact (Homeomorph.piEquivPiSubtypeProd (fun k ↦ k ∈ C) X).symm.continuous have hf : Continuous f := by unfold f exact (M.factor_continuous i).comp ((hsplit_cont.comp (continuous_fst.prodMk continuous_snd.fst)).update i continuous_snd.snd.snd) have hg : Continuous g := by unfold g exact (M.factor_continuous i).comp ((hsplit_cont.comp (continuous_fst.prodMk continuous_snd.snd.fst)).update i continuous_snd.snd.snd) have hfm : Measurable f := by unfold f exact ((M.toFactorization.measurable_factor i).comp (measurable_update'.comp ((split.symm.measurable.comp (measurable_fst.prodMk measurable_snd.fst)).prodMk measurable_snd.snd.snd))).ennreal_toReal have hgm : Measurable g := by unfold g exact ((M.toFactorization.measurable_factor i).comp (measurable_update'.comp ((split.symm.measurable.comp (measurable_fst.prodMk measurable_snd.snd.fst)).prodMk measurable_snd.snd.snd))).ennreal_toReal have hfg_ae : f =ᵐ[μC.prod (μD.prod (μD.prod (μ i)))] g := by apply (Measure.ae_prod_iff_ae_ae (measurableSet_eq_fun hfm hgm)).2 filter_upwards [hsection_ae] with c hc have hfm_c : Measurable (fun y ↦ f (c, y)) := hfm.comp (measurable_const.prodMk measurable_id) have hgm_c : Measurable (fun y ↦ g (c, y)) := hgm.comp (measurable_const.prodMk measurable_id) apply (Measure.ae_prod_iff_ae_ae (measurableSet_eq_fun hfm_c hgm_c)).2 filter_upwards [hc] with r₁ hr₁ have hfm_cr₁ : Measurable (fun y ↦ f (c, r₁, y)) := hfm.comp (measurable_const.prodMk (measurable_const.prodMk measurable_id)) have hgm_cr₁ : Measurable (fun y ↦ g (c, r₁, y)) := hgm.comp (measurable_const.prodMk (measurable_const.prodMk measurable_id)) apply (Measure.ae_prod_iff_ae_ae (measurableSet_eq_fun hfm_cr₁ hgm_cr₁)).2 filter_upwards [hr₁] with r₂ hr₂ filter_upwards [hr₂] with z hz exact congrArg ENNReal.toReal hz have hfg : f = g := (hf.ae_eq_iff_eq (μC.prod (μD.prod (μD.prod (μ i)))) hg).mp hfg_ae have hsections (c : ∀ k : {k // k ∈ C}, X k) (r₁ r₂ : ∀ k : {k // k ∉ C}, X k) (z : X i) : M.toFactorization.factor i (update (split.symm (c, r₁)) i z) = M.toFactorization.factor i (update (split.symm (c, r₂)) i z) := by apply (ENNReal.toReal_eq_toReal_iff' (M.factor_ne_top i (update (split.symm (c, r₁)) i z)) (M.factor_ne_top i (update (split.symm (c, r₂)) i z))).mp exact congrFun hfg (c, r₁, r₂, z) -- … truncated; follow the source link for the rest …

theorem aeFactorIndependent_of_factorIndependent {i j : V} : M.FactorIndependentOf i j → M.AEFactorIndependentOf i j := by intro h exact Filter.Eventually.of_forall fun x ↦ Filter.Eventually.of_forall fun xj ↦ h x xj

theorem factorIndependent_of_aeFactorIndependent {i j : V} : M.AEFactorIndependentOf i j → M.FactorIndependentOf i j := by /- Regard the two sides as continuous real functions on `(∀ k, X k) × X j`. Convert the iterated a.e. hypothesis to product-measure a.e. equality, apply full-support extensionality, and use `factor_ne_top` to reflect equality through `ENNReal.toReal`. -/ intro h let f : ((∀ k, X k) × X j) → ℝ := fun z ↦ (M.toFactorization.factor i (update z.1 j z.2)).toReal let g : ((∀ k, X k) × X j) → ℝ := fun z ↦ (M.toFactorization.factor i z.1).toReal have hf : Continuous f := (M.factor_continuous i).comp (continuous_fst.update j continuous_snd) have hg : Continuous g := (M.factor_continuous i).comp continuous_fst have hae : f =ᵐ[(Measure.pi μ).prod (μ j)] g := by have hfm : Measurable f := ((M.toFactorization.measurable_factor i).comp measurable_update').ennreal_toReal have hgm : Measurable g := ((M.toFactorization.measurable_factor i).comp measurable_fst).ennreal_toReal apply (Measure.ae_prod_iff_ae_ae (measurableSet_eq_fun hfm hgm)).2 filter_upwards [h] with x hx filter_upwards [hx] with xj hxj exact congrArg ENNReal.toReal hxj have hfg : f = g := (hf.ae_eq_iff_eq ((Measure.pi μ).prod (μ j)) hg).mp hae intro x xj apply (ENNReal.toReal_eq_toReal_iff' (M.factor_ne_top i (update x j xj)) (M.factor_ne_top i x)).mp exact congrFun hfg (x, xj)

theorem edge_condIndep_of_factorIndependent {i j : V} (hji : G.edge j i) : M.FactorIndependentOf i j → M.CondIndepCoordinates i j ((G.parents i).erase j) := by /- Delete the single edge `j → i`, reuse the same normalized factors as a factorization of the resulting sub-DAG (the new locality obligation is exactly factor independence), and apply the ordered local-Markov theorem in that sub-DAG. Its parent set at `i` is `(G.parents i).erase j`; contract the predecessor residual to coordinate `j`. -/ intro hind classical let H : DAG V := { edge := fun u v ↦ G.edge u v ∧ ¬ (u = j ∧ v = i) decEdge := inferInstance acyclic := by intro v hv exact G.acyclic v ((Relation.TransGen.mono (r := fun u v ↦ G.edge u v ∧ ¬ (u = j ∧ v = i)) (p := G.edge) (fun _ _ h ↦ h.1)) v v hv) } let B : Factorization H X μ := { factor := M.toFactorization.factor measurable_factor := M.toFactorization.measurable_factor normalized_factor := M.toFactorization.normalized_factor local_factor := by intro k x y hxy by_cases hki : k = i · have hxyi : ∀ l, l ∈ insert i (H.parents i) → x l = y l := by intro l hl apply hxy l simpa only [hki] using hl have hi : M.toFactorization.factor i x = M.toFactorization.factor i y := by calc M.toFactorization.factor i x = M.toFactorization.factor i (update x j (y j)) := (hind x (y j)).symm _ = M.toFactorization.factor i y := by apply M.toFactorization.local_factor i intro l hl rcases Finset.mem_insert.mp hl with hli | hl · have hlj : l ≠ j := by intro h have hij : i ≠ j := fun hij ↦ G.irrefl i (hij ▸ hji) exact hij (hli.symm.trans h) rw [Function.update_of_ne hlj] exact hxyi l (Finset.mem_insert.mpr (inl hli)) · by_cases hlj : l = j · subst l simp · rw [Function.update_of_ne hlj] apply hxyi l apply mem_insert_of_mem rw [H.mem_parents] exact ⟨G.mem_parents.mp hl, fun h ↦ hlj h.1⟩ simpa only [hki] using hi · apply M.toFactorization.local_factor k intro l hl apply hxy l rcases Finset.mem_insert.mp hl with hl | hl · exact Finset.mem_insert.mpr (inl hl) · apply mem_insert_of_mem rw [H.mem_parents] refine ⟨G.mem_parents.mp hl, ?_⟩ rintro ⟨rfl, rfl⟩ exact hki rfl } let τG := canonicalTopologicalRanking G let τ : TopologicalRanking H := { rank := τG.rank injective_rank := τG.injective_rank edge_lt := fun h ↦ τG.edge_lt h.1 } let C := (G.parents i).erase j have hparents : H.parents i = C := by ext k simp only [H.mem_parents, C, G.mem_parents, Finset.mem_erase] constructor · rintro ⟨hk, hdel⟩ exact ⟨fun hkj ↦ hdel ⟨hkj, rfl⟩, hk⟩ · rintro ⟨hkj, hk⟩ exact ⟨hk, fun h ↦ hkj h.1⟩ have hCpred : C ⊆ predecessors τ i := by intro k hk rw [predecessors, mem_filter] exact ⟨Finset.mem_univ k, τG.edge_lt (G.mem_parents.mp (mem_of_mem_erase hk))⟩ have hmarkov := B.orderedLocalMarkov τ i C hCpred (by simpa [hparents]) have hjpred : j ∈ predecessors τ i := by rw [predecessors, mem_filter] exact ⟨Finset.mem_univ j, τG.edge_lt hji⟩ have hjC : j ∉ C := by simp [C] let e : (∀ k : ↑(predecessors τ i \ C), X k) → X j := fun z ↦ z ⟨j, Finset.mem_sdiff.mpr ⟨hjpred, hjC⟩⟩ have hcomp := hmarkov.comp measurable_id (measurable_pi_apply (⟨j, Finset.mem_sdiff.mpr ⟨hjpred, hjC⟩⟩ : ↑(predecessors τ i \ C))) have heval : e ∘ coordinateProjection (X := X) (predecessors τ i \ C) = fun x : ∀ k, X k ↦ x j := by funext x rfl rw [heval] at hcomp change CondIndepFun (comap (coordinateProjection (X := X) C) inferInstance) (coordinateConditioning_comap_le (X := X) C) (fun x : ∀ k, X k ↦ x i) (fun x : ∀ k, X k ↦ x j) M.observationalMeasure simp only [Function.id_comp] at hcomp have hmeasure : B.observationalMeasure = M.observationalMeasure := by rfl cases hmeasure exact hcomp

theorem edge_condIndep_of_aeFactorIndependent {i j : V} (hji : G.edge j i) : M.AEFactorIndependentOf i j → M.CondIndepCoordinates i j ((G.parents i).erase j) := by intro h exact M.edge_condIndep_of_factorIndependent hji (M.factorIndependent_of_aeFactorIndependent h)

theorem edge_condIndep_iff_aeFactorIndependent {i j : V} (hji : G.edge j i) : M.CondIndepCoordinates i j ((G.parents i).erase j) ↔ M.AEFactorIndependentOf i j := by exact ⟨M.aeFactorIndependent_of_edge_condIndep hji, M.edge_condIndep_of_aeFactorIndependent hji⟩

theorem localContrast_zero_of_factorIndependent {i j : V} (hji : G.edge j i) : M.FactorIndependentOf i j → ∀ (x : ∀ k, X k) (xi xi' : X i) (xj xj' : X j), M.localContrast i j x xi xi' xj xj' = 0 := by /- Rewrite all four factor values to a fixed value of coordinate `j`; `hji` supplies `i ≠ j` so the own-coordinate update is not disturbed. -/ intro h x xi xi' xj xj' have hij : i ≠ j := by intro hij subst j exact G.irrefl i hji have hsection (z : X i) (w : X j) : M.toFactorization.factor i (update (update x j w) i z) = M.toFactorization.factor i (update x i z) := by rw [← Function.update_comm hij] exact h (update x i z) w unfold localContrast simp_rw [Function.update_comm hij] rw [hsection xi xj, hsection xi' xj', hsection xi xj', hsection xi' xj] ring

theorem factorIndependent_of_localContrast_zero {i j : V} (hji : G.edge j i) : (∀ (x : ∀ k, X k) (xi xi' : X i) (xj xj' : X j), M.localContrast i j x xi xi' xj xj' = 0) → M.FactorIndependentOf i j := by /- Fix the base assignment and the new `j` value. The contrast equations say the two positive own-coordinate density sections are proportional. Integrate the equations in the second own-coordinate variable and use `normalized_factor` twice; the proportionality constant is one. Finiteness reflects the real calculation back to `ENNReal`. -/ intro h x xj have hij : i ≠ j := by intro hij subst j exact G.irrefl i hji let a : X i → ℝ≥0∞ := fun z ↦ M.toFactorization.factor i (update (update x j xj) i z) let b : X i → ℝ≥0∞ := fun z ↦ M.toFactorization.factor i (update x i z) have ha_meas : Measurable a := (M.toFactorization.measurable_factor i).comp (measurable_update (update x j xj)) have hb_meas : Measurable b := (M.toFactorization.measurable_factor i).comp (measurable_update x) have hab (z w : X i) : a z * b w = b z * a w := by apply (ENNReal.toReal_eq_toReal_iff' (ENNReal.mul_ne_top (M.factor_ne_top i (update (update x j xj) i z)) (M.factor_ne_top i (update x i w))) (ENNReal.mul_ne_top (M.factor_ne_top i (update x i z)) (M.factor_ne_top i (update (update x j xj) i w)))).mp rw [ENNReal.toReal_mul, ENNReal.toReal_mul] apply sub_eq_zero.mp simpa [localContrast, a, b, Function.update_comm hij] using h x z w xj (x j) have ha_norm : ∫⁻ z, a z ∂μ i = 1 := by exact M.toFactorization.normalized_factor i (update x j xj) have hb_norm : ∫⁻ z, b z ∂μ i = 1 := by exact M.toFactorization.normalized_factor i x have hab_eq (z : X i) : a z = b z := by have hint : a z * (∫⁻ w, b w ∂μ i) = b z * (∫⁻ w, a w ∂μ i) := by calc a z * (∫⁻ w, b w ∂μ i) = ∫⁻ w, a z * b w ∂μ i := by exact (lintegral_const_mul (a z) hb_meas).symm _ = ∫⁻ w, b z * a w ∂μ i := lintegral_congr (hab z) _ = b z * (∫⁻ w, a w ∂μ i) := by exact lintegral_const_mul (b z) ha_meas simpa [ha_norm, hb_norm] using hint have hz := hab_eq (x i) change M.toFactorization.factor i (update (update x j xj) i (x i)) = M.toFactorization.factor i (update x i (x i)) at hz rw [Function.update_eq_self] at hz have hcoord : update x j xj i = x i := Function.update_of_ne hij _ _ rw [← hcoord, Function.update_eq_self] at hz exact hz

theorem factorIndependent_iff_localContrast_zero {i j : V} (hji : G.edge j i) : M.FactorIndependentOf i j ↔ ∀ (x : ∀ k, X k) (xi xi' : X i) (xj xj' : X j), M.localContrast i j x xi xi' xj xj' = 0 := by exact ⟨M.localContrast_zero_of_factorIndependent hji, M.factorIndependent_of_localContrast_zero hji⟩

theorem edge_condIndep_iff_localContrast_zero {i j : V} (hji : G.edge j i) : M.CondIndepCoordinates i j ((G.parents i).erase j) ↔ ∀ (x : ∀ k, X k) (xi xi' : X i) (xj xj' : X j), M.localContrast i j x xi xi' xj xj' = 0 := by exact (M.edge_condIndep_iff_factorIndependent hji).trans (M.factorIndependent_iff_localContrast_zero hji)

theorem EdgeWitness.not_condIndep {i j : V} (hji : G.edge j i) (w : M.EdgeWitness i j) : ¬ M.CondIndepCoordinates i j ((G.parents i).erase j) := by intro hCI exact w.nonzero ((M.edge_condIndep_iff_localContrast_zero hji).mp hCI w.base w.child₀ w.child₁ w.parent₀ w.parent₁)

theorem EdgeWitness.eventually_nonzero {i j : V} (w : M.EdgeWitness i j) : ∃ ε > 0, ∀ N : PositiveFiniteDAGMechanism G X, M.FactorSupClose N ε → N.localContrast i j w.base w.child₀ w.child₁ w.parent₀ w.parent₁ ≠ 0 := by let a : Fin 4 → ℝ := ![ M.factor i (update (update w.base i w.child₀) j w.parent₀), M.factor i (update (update w.base i w.child₁) j w.parent₁), M.factor i (update (update w.base i w.child₀) j w.parent₁), M.factor i (update (update w.base i w.child₁) j w.parent₀)] let q : (Fin 4 → ℝ) → ℝ := fun z ↦ z 0 * z 1 - z 2 * z 3 have hqa : q a ≠ 0 := by simpa [q, a, localContrast] using w.nonzero have hq : Continuous q := by unfold q fun_prop have hne : {z | q z ≠ 0} ∈ nhds a := hq.continuousAt.eventually_ne hqa rcases Metric.mem_nhds_iff.mp hne with ⟨ε, hε, hball⟩ refine ⟨ε, hε, ?_⟩ intro N hclose let b : Fin 4 → ℝ := ![ N.factor i (update (update w.base i w.child₀) j w.parent₀), N.factor i (update (update w.base i w.child₁) j w.parent₁), N.factor i (update (update w.base i w.child₀) j w.parent₁), N.factor i (update (update w.base i w.child₁) j w.parent₀)] have hba : dist b a < ε := by rw [dist_pi_lt_iff hε] intro k fin_cases k · simpa [b, a, Real.dist_eq] using hclose i (update (update w.base i w.child₀) j w.parent₀) · simpa [b, a, Real.dist_eq] using hclose i (update (update w.base i w.child₁) j w.parent₁) · simpa [b, a, Real.dist_eq] using hclose i (update (update w.base i w.child₀) j w.parent₁) · simpa [b, a, Real.dist_eq] using hclose i (update (update w.base i w.child₁) j w.parent₀) have hqb : q b ≠ 0 := hball (Metric.mem_ball.mpr hba) simpa [q, b, localContrast] using hqb

theorem EdgeWitness.not_condIndep {i j : V} (hji : G.edge j i) (w : M.EdgeWitness i j) : ¬ M.CondIndepCoordinates i j ((G.parents i).erase j) := by intro hCI exact w.nonzero ((M.edge_condIndep_iff_localContrast_zero hji).mp hCI w.base w.child₀ w.child₁ w.parent₀ w.parent₁)

theorem EdgeWitness.eventually_not_condIndep {i j : V} (hji : G.edge j i) (w : M.EdgeWitness i j) : ∃ ε > 0, ∀ N : CompactPositiveFactorization G X μ, M.FactorSupClose N ε → ¬ N.CondIndepCoordinates i j ((G.parents i).erase j) := by let a : Fin 4 → ℝ := ![ (M.toFactorization.factor i (update (update w.base i w.child₀) j w.parent₀)).toReal, (M.toFactorization.factor i (update (update w.base i w.child₁) j w.parent₁)).toReal, (M.toFactorization.factor i (update (update w.base i w.child₀) j w.parent₁)).toReal, (M.toFactorization.factor i (update (update w.base i w.child₁) j w.parent₀)).toReal] let q : (Fin 4 → ℝ) → ℝ := fun z ↦ z 0 * z 1 - z 2 * z 3 have hqa : q a ≠ 0 := by simpa [q, a, localContrast] using w.nonzero have hq : Continuous q := by unfold q fun_prop have hne : {z | q z ≠ 0} ∈ nhds a := hq.continuousAt.eventually_ne hqa rcases Metric.mem_nhds_iff.mp hne with ⟨ε, hε, hball⟩ refine ⟨ε, hε, ?_⟩ intro N hclose let b : Fin 4 → ℝ := ![ (N.toFactorization.factor i (update (update w.base i w.child₀) j w.parent₀)).toReal, (N.toFactorization.factor i (update (update w.base i w.child₁) j w.parent₁)).toReal, (N.toFactorization.factor i (update (update w.base i w.child₀) j w.parent₁)).toReal, (N.toFactorization.factor i (update (update w.base i w.child₁) j w.parent₀)).toReal] have hba : dist b a < ε := by rw [dist_pi_lt_iff hε] intro k fin_cases k · simpa [b, a, Real.dist_eq] using hclose i (update (update w.base i w.child₀) j w.parent₀) · simpa [b, a, Real.dist_eq] using hclose i (update (update w.base i w.child₁) j w.parent₁) · simpa [b, a, Real.dist_eq] using hclose i (update (update w.base i w.child₀) j w.parent₁) · simpa [b, a, Real.dist_eq] using hclose i (update (update w.base i w.child₁) j w.parent₀) have hqb : q b ≠ 0 := hball (Metric.mem_ball.mpr hba) let wN : N.EdgeWitness i j := { base := w.base child₀ := w.child₀ child₁ := w.child₁ parent₀ := w.parent₀ parent₁ := w.parent₁ nonzero := by simpa [q, b, localContrast] using hqb } exact EdgeWitness.not_condIndep N hji wN