Graph.Finite­Density

Finite DAG product-density factorizations: coordinate dependence, normalized leaf elimination, and nonancestor-intervention marginal invariance without an SCM representation.

Ordered­Local­Markov 6 core · 9 supporting · 3 submodules Ordered local-Markov consequences of finite-DAG density factorizations: topological predecessor blocks, the parent-conditioned core, arbitrary parent-superset conditioning, and the unit-cube specialization. Positive 24 core · 21 supporting · 6 submodules Strictly positive finite-DAG mechanisms: conditional local laws, edgewise causal-minimality characterizations, stable nonzero local contrasts, and finite-state examples.
Factorization 7 core · 4 supporting This module packages a family of measurable normalized conditional densities on a finite DAG. ★ observationalDensity_intervene

Finite DAG density factorizations

This module packages a family of measurable normalized conditional densities on a finite DAG. Each factor is an ℝ≥0∞-valued function of its node and parent coordinates. It also defines the single-node replacement by a normalized parent-independent intervention density.

structure Factorization reviewed
Causalean.Graph.FiniteDensity

A finite DAG, coordinate value spaces, and coordinate reference measures determine a factorization interface of measurable, parent-local conditional densities normalized in their own coordinates.

Definition (Lean source)
parameters
G :
DAG V
X :
V → Type*
∀ i, MeasurableSpace (X i)
μ :
∀ i, Measure (X i)
fields
The conditional density factor belonging to a node.
factor :
∀ i
if
(∀ k, X k)
then
ℝ≥0∞
Every conditional density factor is measurable on the full product.
measurable_factor :
∀ i, Measurable (factor i)
A node factor is local to the node and its graph parents.
local_factor :
∀ i, DependsOn (insert i (G.parents i)) (factor i)
Integrating a node factor in its own coordinate gives one for every fixed context.
normalized_factor :
∀ i (v : ∀ k, X k), ∫⁻ x, factor i (update v i x) ∂μ i = 1
Causalean.Graph.FiniteDensity.Factorization · Causalean/Graph/FiniteDensity/Factorization.lean:26 · uses DAG
def partialDensity reviewed
Causalean.Graph.FiniteDensity.Factorization

A DAG factorization, a finite node set, and a full assignment determine the product density over that node set.

Definition (Lean source)
parameters
V :
Type u_1
V → Type u_2
(i : V) → Measure (X i)
DAG V
shared
B :
Factorization G X μ
S :
Finset V
v :
∀ i, X i
def
partialDensity B S v :
ℝ≥0∞
given by
∏ i ∈ S, B.factor i v
Causalean.Graph.FiniteDensity.Factorization.partialDensity · Causalean/Graph/FiniteDensity/Factorization.lean:41 · uses DAG , Factorization
def observationalDensity reviewed
Causalean.Graph.FiniteDensity.Factorization

A DAG factorization and a full assignment determine the observational product density over all nodes.

Definition (Lean source)
parameters
V :
Type u_1
V → Type u_2
(i : V) → Measure (X i)
DAG V
shared
B :
Factorization G X μ
v :
∀ i, X i
def
observationalDensity B v :
ℝ≥0∞
given by
B.partialDensity univ v
Causalean.Graph.FiniteDensity.Factorization.observationalDensity · Causalean/Graph/FiniteDensity/Factorization.lean:47 · uses DAG , Factorization
structure InterventionDensity reviewed
Causalean.Graph.FiniteDensity

An intervention target, coordinate value spaces, and coordinate reference measures determine a measurable unit-mass replacement density for that target.

Definition (Lean source)
parameters
j :
V
X :
V → Type*
∀ i, MeasurableSpace (X i)
μ :
∀ i, Measure (X i)
fields
The replacement density on the intervention target coordinate.
density :
X j → ℝ≥0∞
The replacement density is measurable.
measurable_density :
Measurable density
The replacement density has unit mass.
normalized_density :
∫⁻ x, density x ∂μ j = 1
Causalean.Graph.FiniteDensity.InterventionDensity · Causalean/Graph/FiniteDensity/Factorization.lean:80
def intervene reviewed
Causalean.Graph.FiniteDensity.Factorization

A DAG factorization, intervention target, and normalized replacement density determine the factorization obtained by replacing that target's factor.

Definition (Lean source)
parameters
V :
Type u_1
V → Type u_2
(i : V) → Measure (X i)
DAG V
shared
B :
Factorization G X μ
j :
V
q :
InterventionDensity j X μ
def
intervene B j q :
Factorization G X μ
given by
clause 1
factor i v := if i = j then q.density (v j) else B.factor i v
clause 2
measurable_factor := by intro i by_cases h : i
= j · subst i simp only [↓reduceIte] exact q.measurable_density.comp (measurable_pi_apply j) · simp only [h, ↓reduceIte] exact B.measurable_factor i
clause 3
local_factor := by intro i by_cases h : i
= j · subst i simp only [↓reduceIte] intro x y hxy exact congrArg q.density (hxy j (mem_insert_self j _)) · simp only [h, ↓reduceIte] exact B.local_factor i
clause 4
normalized_factor := by intro i v by_cases h : i
= j · subst i simp only [↓reduceIte] simpa using q.normalized_density · simp only [h, ↓reduceIte] exact B.normalized_factor i v
Causalean.Graph.FiniteDensity.Factorization.intervene · Causalean/Graph/FiniteDensity/Factorization.lean:91 · uses DAG , Factorization , InterventionDensity
def interventionDensity reviewed
Causalean.Graph.FiniteDensity.Factorization

A DAG factorization, intervention target, replacement density, and full assignment determine the truncated product density for that intervention.

Definition (Lean source)
parameters
V :
Type u_1
V → Type u_2
(i : V) → Measure (X i)
DAG V
shared
B :
Factorization G X μ
j :
V
q :
InterventionDensity j X μ
v :
∀ i, X i
def
interventionDensity B j q v :
ℝ≥0∞
given by
q.density (v j) * B.partialDensity (Finset.univ.erase j) v
Causalean.Graph.FiniteDensity.Factorization.interventionDensity · Causalean/Graph/FiniteDensity/Factorization.lean:122 · uses DAG , Factorization , InterventionDensity
theorem observationalDensity_intervene reviewed
Causalean.Graph.FiniteDensity.Factorization

A DAG factorization, intervention target, and replacement density give the same product density whether intervention is represented by factor replacement or by the explicit truncated product.

Formal statement
hypotheses
V :
Type u_1
V → Type u_2
(i : V) → Measure (X i)
DAG V
shared
B :
Factorization G X μ
j :
V
q :
InterventionDensity j X μ
conclusion
(B.intervene j q).observationalDensity = B.interventionDensity j q
Proof (Lean source)
theorem Factorization.observationalDensity_intervene {G : DAG V} (B : Factorization G X μ) (j : V) (q : InterventionDensity j X μ) : (B.intervene j q).observationalDensity = B.interventionDensity j q := by funext v change (∏ i ∈ univ, if i = j then q.density (v j) else B.factor i v) = q.density (v j) * ∏ i ∈ Finset.univ.erase j, B.factor i v rw [← Finset.prod_erase_mul _ _ (Finset.mem_univ j)] have hprod : (∏ i ∈ Finset.univ.erase j, if i = j then q.density (v j) else B.factor i v) = ∏ i ∈ Finset.univ.erase j, B.factor i v := by apply Finset.prod_congr rfl intro i hi have hij : i ≠ j := (Finset.mem_erase.mp hi).1 simp only [hij, ↓reduceIte] rw [hprod] simp only [↓reduceIte] exact mul_comm _ _
Causalean.Graph.FiniteDensity.Factorization.observationalDensity_intervene · Causalean/Graph/FiniteDensity/Factorization.lean:129 · uses DAG , Factorization , intervene , interventionDensity , observationalDensity , InterventionDensity
4 supporting declarations (lemmas, instances)
  • measurable_partialDensity theorem — A DAG factorization and a finite node set have a measurable partial product density.
    hypotheses
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    S :
    Finset V
    conclusion
    Measurable (B.partialDensity S)
    Proof (Lean source)
    @[fun_prop] theorem Factorization.measurable_partialDensity {G : DAG V} (B : Factorization G X μ) (S : Finset V) : Measurable (B.partialDensity S) := by change Measurable (fun v ↦ ∏ i ∈ S, B.factor i v) exact Finset.measurable_prod S (fun i _ ↦ B.measurable_factor i)
    Causalean.Graph.FiniteDensity.Factorization.measurable_partialDensity · Causalean/Graph/FiniteDensity/Factorization.lean:53
  • measurable_observationalDensity theorem — A DAG factorization has a measurable observational product density.
    hypotheses
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    conclusion
    Measurable B.observationalDensity
    Proof (Lean source)
    @[fun_prop] theorem Factorization.measurable_observationalDensity {G : DAG V} (B : Factorization G X μ) : Measurable B.observationalDensity := by change Measurable (B.partialDensity univ) exact B.measurable_partialDensity univ
    Causalean.Graph.FiniteDensity.Factorization.measurable_observationalDensity · Causalean/Graph/FiniteDensity/Factorization.lean:62
  • targetRatio_dependsOn theorem — A DAG factorization, a target node, and a numerator depending on that node's value give a density ratio determined only by the target and its parents.
    hypotheses
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    i :
    V
    numerator :
    X i → ℝ≥0∞
    conclusion
    DependsOn (insert i (G.parents i)) (fun v ↦ numerator (v i) / B.factor i v)
    Proof (Lean source)
    theorem Factorization.targetRatio_dependsOn {G : DAG V} (B : Factorization G X μ) (i : V) (numerator : X i → ℝ≥0∞) : DependsOn (insert i (G.parents i)) (fun v ↦ numerator (v i) / B.factor i v) := by intro x y hxy exact congrArg₂ (· / ·) (congrArg numerator (hxy i (mem_insert_self i _))) (B.local_factor i hxy)
    Causalean.Graph.FiniteDensity.Factorization.targetRatio_dependsOn · Causalean/Graph/FiniteDensity/Factorization.lean:69
  • measurable_interventionDensity theorem — A DAG factorization, intervention target, and replacement density give a measurable truncated intervention density.
    hypotheses
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    j :
    V
    q :
    InterventionDensity j X μ
    conclusion
    Measurable (B.interventionDensity j q)
    Proof (Lean source)
    @[fun_prop] theorem Factorization.measurable_interventionDensity {G : DAG V} (B : Factorization G X μ) (j : V) (q : InterventionDensity j X μ) : Measurable (B.interventionDensity j q) := by change Measurable (fun v ↦ q.density (v j) * B.partialDensity (Finset.univ.erase j) v) exact (q.measurable_density.comp (measurable_pi_apply j)).mul (B.measurable_partialDensity (Finset.univ.erase j))
    Causalean.Graph.FiniteDensity.Factorization.measurable_interventionDensity · Causalean/Graph/FiniteDensity/Factorization.lean:152
Leaf 2 core · 2 supporting This module proves the one-coordinate analytic step behind finite Bayesian-network marginalization: a normalized factor at a leaf can be integrated away without changing the product of the remaining factors. ★ lintegral_partialDensity_leaf

Normalized leaf elimination

This module proves the one-coordinate analytic step behind finite Bayesian-network marginalization: a normalized factor at a leaf can be integrated away without changing the product of the remaining factors.

def IsLeafIn reviewed
Causalean.Graph.FiniteDensity

A finite DAG, a node, and a finite node set determine the property that the node is a leaf within that set.

Definition (Lean source)
parameters
V :
Type u_1
shared
G :
DAG V
k :
V
S :
Finset V
def
IsLeafIn G k S :
Prop
given by
clause 1
k ∈ S
clause 2
l ∈ S :
l ≠ k
¬ G.edge k l
Causalean.Graph.FiniteDensity.IsLeafIn · Causalean/Graph/FiniteDensity/Leaf.lean:24 · uses DAG
theorem lintegral_partialDensity_leaf reviewed
Causalean.Graph.FiniteDensity.Factorization

A DAG factorization, a leaf within a finite node set, and a fixed assignment of the other coordinates show that integrating the normalized leaf factor removes exactly that factor from the product.

Formal statement
hypotheses
V :
Type u_1
V → Type u_2
(i : V) → Measure (X i)
DAG V
shared
B :
Factorization G X μ
S :
Finset V
k :
V
hleaf :
IsLeafIn G k S
v :
∀ i, X i
conclusion
∫⁻ x, B.partialDensity S (update v k x) ∂μ k = B.partialDensity (S.erase k) v
Proof (Lean source)
theorem Factorization.lintegral_partialDensity_leaf (B : Factorization G X μ) {S : Finset V} {k : V} (hleaf : IsLeafIn G k S) (v : ∀ i, X i) : ∫⁻ x, B.partialDensity S (update v k x) ∂μ k = B.partialDensity (S.erase k) v := by -- Split off the leaf factor, freeze the erased product, and use `B.normalized_factor k`. calc ∫⁻ x, B.partialDensity S (update v k x) ∂μ k = ∫⁻ x, B.factor k (update v k x) * B.partialDensity (S.erase k) (update v k x) ∂μ k := by congr 1 funext x unfold Factorization.partialDensity exact (Finset.mul_prod_erase S (fun i ↦ B.factor i (update v k x)) hleaf.1).symm _ = ∫⁻ x, B.factor k (update v k x) * B.partialDensity (S.erase k) v ∂μ k := by congr 1 funext x rw [B.partialDensity_erase_update_leaf hleaf] _ = (∫⁻ x, B.factor k (update v k x) ∂μ k) * B.partialDensity (S.erase k) v := by rw [lintegral_mul_const] exact (B.measurable_factor k).comp (measurable_update v) _ = B.partialDensity (S.erase k) v := by rw [B.normalized_factor k v, one_mul]
Causalean.Graph.FiniteDensity.Factorization.lintegral_partialDensity_leaf · Causalean/Graph/FiniteDensity/Leaf.lean:62 · uses DAG , Factorization , partialDensity , IsLeafIn
2 supporting declarations (lemmas, instances)
  • factor_update_eq_of_ne_of_not_parent theorem — A DAG factorization, two distinct nodes, evidence that the updated node is not a parent of the other, a full assignment, and a new coordinate value leave the other node's local factor unchanged.
    hypotheses
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    k l :
    V
    hkl :
    k ≠ l
    hkpar :
    k ∉ G.parents l
    v :
    ∀ i, X i
    x :
    X k
    conclusion
    B.factor l (update v k x) = B.factor l v
    Proof (Lean source)
    theorem Factorization.factor_update_eq_of_ne_of_not_parent (B : Factorization G X μ) {k l : V} (hkl : k ≠ l) (hkpar : k ∉ G.parents l) (v : ∀ i, X i) (x : X k) : B.factor l (update v k x) = B.factor l v := by -- Apply locality and show every coordinate in `insert l (parents l)` is untouched by the update. apply B.local_factor l intro i hi have hik : i ≠ k := by intro h subst i exact (Finset.mem_insert.mp hi).elim hkl hkpar exact Function.update_of_ne hik x v
    Causalean.Graph.FiniteDensity.Factorization.factor_update_eq_of_ne_of_not_parent · Causalean/Graph/FiniteDensity/Leaf.lean:29
  • partialDensity_erase_update_leaf theorem — A DAG factorization, a leaf of a finite node set, a full assignment, and a new leaf-coordinate value leave the product of all remaining factors unchanged.
    hypotheses
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    S :
    Finset V
    k :
    V
    hleaf :
    IsLeafIn G k S
    v :
    ∀ i, X i
    x :
    X k
    conclusion
    B.partialDensity (S.erase k) (update v k x) = B.partialDensity (S.erase k) v
    Proof (Lean source)
    theorem Factorization.partialDensity_erase_update_leaf (B : Factorization G X μ) {S : Finset V} {k : V} (hleaf : IsLeafIn G k S) (v : ∀ i, X i) (x : X k) : B.partialDensity (S.erase k) (update v k x) = B.partialDensity (S.erase k) v := by -- Compare factors pointwise; leafhood rules out `k` as a parent of every retained node. unfold Factorization.partialDensity apply Finset.prod_congr rfl intro l hl have hlk : l ≠ k := (Finset.mem_erase.mp hl).1 have hlS : l ∈ S := (Finset.mem_erase.mp hl).2 apply B.factor_update_eq_of_ne_of_not_parent hlk.symm intro hkpar exact hleaf.2 l hlS hlk (G.mem_parents.mp hkpar)
    Causalean.Graph.FiniteDensity.Factorization.partialDensity_erase_update_leaf · Causalean/Graph/FiniteDensity/Leaf.lean:45
Elimination 2 core · 3 supporting This module iterates normalized leaf elimination. ★ lmarginal_partialDensity_union_eq

Reverse-topological elimination outside a parent-closed set

This module iterates normalized leaf elimination. A parent-closed set retains all factors that can influence it, so factors outside it may be removed in reverse topological order. The result is stated both for an arbitrary retained set and for the complement marginal of a full density.

def ParentClosed reviewed
Causalean.Graph.FiniteDensity

A finite DAG and a finite node set determine the property that the set contains every parent of each of its nodes.

Definition (Lean source)
parameters
V :
Type u_1
shared
G :
DAG V
A :
Finset V
i :
i ∈ A
def
ParentClosed G A :
Prop
given by
G.parents i ⊆ A
Causalean.Graph.FiniteDensity.ParentClosed · Causalean/Graph/FiniteDensity/Elimination.lean:24 · uses DAG
theorem lmarginal_partialDensity_union_eq reviewed
Causalean.Graph.FiniteDensity.Factorization

A DAG factorization, a parent-closed retained set, and its disjointness from an eliminable set show that integrating every eliminable coordinate removes all of their factors.

Formal statement
hypotheses
V :
Type u_1
V → Type u_2
(i : V) → Measure (X i)
DAG V
shared
B :
Factorization G X μ
A T :
Finset V
hA :
ParentClosed G A
hAT :
Disjoint A T
conclusion
(∫⋯∫⁻_T, B.partialDensity (A ∪ T) ∂μ) = B.partialDensity A
Proof (Lean source)
theorem Factorization.lmarginal_partialDensity_union_eq (B : Factorization G X μ) {A T : Finset V} (hA : ParentClosed G A) (hAT : Disjoint A T) : (∫⋯∫⁻_T, B.partialDensity (A ∪ T) ∂μ) = B.partialDensity A := by -- Induct on `T`, peel a reverse-topological leaf via `lmarginal_erase'`, and use -- leaf elimination. induction T using Finset.strongInductionOn with | _ T ih => by_cases hT : T.Nonempty · obtain ⟨k, hkT, hleaf⟩ := exists_leaf_in_union_of_parentClosed hA hAT hT rw [MeasureTheory.lmarginal_erase' _ (B.measurable_partialDensity (A ∪ T)) hkT] simp_rw [B.lintegral_partialDensity_leaf hleaf] have hkA : k ∉ A := fun hkA ↦ Finset.disjoint_left.mp hAT hkA hkT have herase : (A ∪ T).erase k = A ∪ T.erase k := by ext i simp only [Finset.mem_erase, mem_union] constructor · rintro ⟨hik, hiA | hiT⟩ · exact inl hiA · exact inr ⟨hik, hiT⟩ · rintro (hiA | ⟨hik, hiT⟩) · exact ⟨fun hik ↦ hkA (hik ▸ hiA), inl hiA⟩ · exact ⟨hik, inr hiT⟩ rw [herase] exact ih (T.erase k) (Finset.erase_ssubset hkT) (Disjoint.mono_right (Finset.erase_subset k T) hAT) · have hTempty : T = ∅ := Finset.not_nonempty_iff_eq_empty.mp hT subst T simp
Causalean.Graph.FiniteDensity.Factorization.lmarginal_partialDensity_union_eq · Causalean/Graph/FiniteDensity/Elimination.lean:43 · uses DAG , Factorization , partialDensity , ParentClosed
3 supporting declarations (lemmas, instances)
  • exists_leaf_in_union_of_parentClosed theorem — A parent-closed retained set, its disjointness from an eliminable set, and a nonempty eliminable set produce an eliminable node that is a leaf of their union.
    hypotheses
    V :
    Type u_1
    DAG V
    Finset V
    shared
    hA :
    ParentClosed G A
    hAT :
    Disjoint A T
    hT :
    T.Nonempty
    conclusion
    ∃ k ∈ T, IsLeafIn G k (A ∪ T)
    Proof (Lean source)
    theorem exists_leaf_in_union_of_parentClosed {A T : Finset V} (hA : ParentClosed G A) (hAT : Disjoint A T) (hT : T.Nonempty) : ∃ k ∈ T, IsLeafIn G k (A ∪ T) := by -- Choose a `topoOrder`-maximal node of `T`; parent-closure excludes edges from it into `A`. obtain ⟨k, hkT, hkmax⟩ := Finset.exists_max_image T G.topoOrder hT refine ⟨k, hkT, mem_union_right A hkT, ?_⟩ intro l hlU hlk hkl rcases Finset.mem_union.mp hlU with hlA | hlT · have hkA : k ∈ A := hA hlA (G.mem_parents.mpr hkl) exact (Finset.disjoint_left.mp hAT hkA hkT) · exact (not_lt_of_ge (hkmax l hlT)) (G.topoOrder_lt k l hkl)
    Causalean.Graph.FiniteDensity.exists_leaf_in_union_of_parentClosed · Causalean/Graph/FiniteDensity/Elimination.lean:29
  • lmarginal_compl_observationalDensity_eq theorem — A DAG factorization and a parent-closed retained set show that integrating the observational density outside the set leaves precisely its retained factor product.
    hypotheses
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    A :
    Finset V
    hA :
    ParentClosed G A
    conclusion
    (∫⋯∫⁻_(univ \ A), B.observationalDensity ∂μ) = B.partialDensity A
    Proof (Lean source)
    theorem Factorization.lmarginal_compl_observationalDensity_eq (B : Factorization G X μ) {A : Finset V} (hA : ParentClosed G A) : (∫⋯∫⁻_(univ \ A), B.observationalDensity ∂μ) = B.partialDensity A := by -- Rewrite `univ` as `A ∪ (univ \ A)` and invoke the union elimination theorem. have huniv : A ∪ (univ \ A) = univ := Finset.union_sdiff_of_subset (Finset.subset_univ A) calc (∫⋯∫⁻_(univ \ A), B.observationalDensity ∂μ) = (∫⋯∫⁻_(univ \ A), B.partialDensity (A ∪ (univ \ A)) ∂μ) := by rw [huniv] rfl _ = B.partialDensity A := B.lmarginal_partialDensity_union_eq hA Finset.disjoint_sdiff
    Causalean.Graph.FiniteDensity.Factorization.lmarginal_compl_observationalDensity_eq · Causalean/Graph/FiniteDensity/Elimination.lean:78
  • lmarginal_compl_interventionDensity_eq theorem — A DAG factorization, a parent-closed retained set, an intervention target outside that set, and a normalized replacement density show that integrating the intervention density outside the set leaves the same retained factor product.
    hypotheses
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    A :
    Finset V
    hA :
    ParentClosed G A
    j :
    V
    hj :
    j ∉ A
    q :
    InterventionDensity j X μ
    conclusion
    (∫⋯∫⁻_(univ \ A), B.interventionDensity j q ∂μ) = B.partialDensity A
    Proof (Lean source)
    theorem Factorization.lmarginal_compl_interventionDensity_eq (B : Factorization G X μ) {A : Finset V} (hA : ParentClosed G A) {j : V} (hj : j ∉ A) (q : InterventionDensity j X μ) : (∫⋯∫⁻_(univ \ A), B.interventionDensity j q ∂μ) = B.partialDensity A := by -- Rewrite the density as `(B.intervene j q).observationalDensity` and note its factors -- agree on `A`. calc (∫⋯∫⁻_(univ \ A), B.interventionDensity j q ∂μ) = (∫⋯∫⁻_(univ \ A), (B.intervene j q).observationalDensity ∂μ) := by rw [B.observationalDensity_intervene] _ = (B.intervene j q).partialDensity A := (B.intervene j q).lmarginal_compl_observationalDensity_eq hA _ = B.partialDensity A := by unfold Factorization.partialDensity funext v apply Finset.prod_congr rfl intro i hi have hij : i ≠ j := by intro hij subst i exact hj hi simp only [Factorization.intervene, hij, ↓reduceIte]
    Causalean.Graph.FiniteDensity.Factorization.lmarginal_compl_interventionDensity_eq · Causalean/Graph/FiniteDensity/Elimination.lean:95
Main 4 core · 9 supporting This module turns reverse-topological density elimination into equality of measures. ★ ancestralMarginal_eq

Nonancestor marginal invariance for finite DAG product densities

This module turns reverse-topological density elimination into equality of measures. Replacing one normalized conditional density by a normalized parent-independent density preserves the marginal on every parent-closed set omitting the target, hence on the ancestral closure of every distinct node of which the target is not an ancestor. Measurable functions determined by that closure consequently have identical pushforward laws.

def observationalMeasure reviewed
Causalean.Graph.FiniteDensity.Factorization

A DAG factorization determines its observational product measure.

Definition (Lean source)
parameters
V :
Type u_1
V → Type u_2
(i : V) → Measure (X i)
DAG V
shared
B :
Factorization G X μ
def
observationalMeasure B :
Measure (∀ i, X i)
given by
(Measure.pi μ).withDensity B.observationalDensity
Causalean.Graph.FiniteDensity.Factorization.observationalMeasure · Causalean/Graph/FiniteDensity/Main.lean:29 · uses DAG , Factorization
def interventionMeasure reviewed
Causalean.Graph.FiniteDensity.Factorization

A DAG factorization, an intervention target, and a normalized replacement density determine the corresponding single-target interventional product measure.

Definition (Lean source)
parameters
V :
Type u_1
V → Type u_2
(i : V) → Measure (X i)
DAG V
shared
B :
Factorization G X μ
j :
V
q :
InterventionDensity j X μ
def
interventionMeasure B j q :
Measure (∀ i, X i)
given by
(Measure.pi μ).withDensity (B.interventionDensity j q)
Causalean.Graph.FiniteDensity.Factorization.interventionMeasure · Causalean/Graph/FiniteDensity/Main.lean:33 · uses DAG , Factorization , InterventionDensity
def nodeAncestralClosure reviewed
Causalean.Graph.FiniteDensity

A finite DAG and a node determine the node's ancestral closure, including the node and all strict ancestors.

Definition (Lean source)
parameters
V :
Type u_1
shared
G :
DAG V
i :
V
def
nodeAncestralClosure G i :
Finset V
given by
insert i (G.ancestors i)
Causalean.Graph.FiniteDensity.nodeAncestralClosure · Causalean/Graph/FiniteDensity/Main.lean:39 · uses DAG
theorem ancestralMarginal_eq reviewed
Causalean.Graph.FiniteDensity.Factorization

A DAG factorization, distinct intervention and queried nodes, evidence that the intervention target is not an ancestor of the queried node, and a normalized replacement density give identical observational and interventional laws on the queried node's ancestral closure.

Formal statement
hypotheses
V :
Type u_1
V → Type u_2
(i : V) → Measure (X i)
DAG V
shared
B :
Factorization G X μ
i j :
V
hji :
j ≠ i
hnotAncestor :
¬ G.isAncestor j i
q :
InterventionDensity j X μ
conclusion
Measure.map (coordinateProjection (X := X) (nodeAncestralClosure G i)) B.observationalMeasure
= Measure.map (coordinateProjection (X := X) (nodeAncestralClosure G i)) (B.interventionMeasure j q)
Proof (Lean source)
theorem Factorization.ancestralMarginal_eq (B : Factorization G X μ) {i j : V} (hji : j ≠ i) (hnotAncestor : ¬ G.isAncestor j i) (q : InterventionDensity j X μ) : Measure.map (coordinateProjection (X := X) (nodeAncestralClosure G i)) B.observationalMeasure = Measure.map (coordinateProjection (X := X) (nodeAncestralClosure G i)) (B.interventionMeasure j q) := by -- Instantiate parent-closed marginal equality and discharge target omission by the -- membership iff. apply B.parentClosed_marginal_eq (parentClosed_nodeAncestralClosure i) ?_ q rw [mem_nodeAncestralClosure_iff] exact fun h ↦ h.elim hji hnotAncestor
Causalean.Graph.FiniteDensity.Factorization.ancestralMarginal_eq · Causalean/Graph/FiniteDensity/Main.lean:86 · uses DAG , isAncestor , Factorization , interventionMeasure , observationalMeasure , InterventionDensity , nodeAncestralClosure , coordinateProjection
9 supporting declarations (lemmas, instances)
  • mem_nodeAncestralClosure_iff theorem — A queried node and a candidate node satisfy ancestral-closure membership exactly when the candidate is the queried node or an ancestor of it.
    hypotheses
    V :
    Type u_1
    DAG V
    V
    shared
    conclusion
    j ∈ nodeAncestralClosure G i ↔ j = i ∨ G.isAncestor j i
    Proof (Lean source)
    theorem mem_nodeAncestralClosure_iff {i j : V} : j ∈ nodeAncestralClosure G i ↔ j = i ∨ G.isAncestor j i := by -- Unfold the closure and the graph's `ancestors` membership characterization. simp only [nodeAncestralClosure, Finset.mem_insert, G.mem_ancestors]
    Causalean.Graph.FiniteDensity.mem_nodeAncestralClosure_iff · Causalean/Graph/FiniteDensity/Main.lean:44
  • parentClosed_nodeAncestralClosure theorem — A node has an ancestral closure that contains every parent of each of its nodes.
    hypotheses
    V :
    Type u_1
    DAG V
    shared
    i :
    V
    conclusion
    ParentClosed G (nodeAncestralClosure G i)
    Proof (Lean source)
    theorem parentClosed_nodeAncestralClosure (i : V) : ParentClosed G (nodeAncestralClosure G i) := by -- A parent of `i` is an ancestor; a parent of an ancestor reaches `i` by transitivity. intro k hk l hl rw [mem_nodeAncestralClosure_iff] at hk ⊢ rcases hk with rfl | hki · exact inr (G.mem_ancestors.mp (G.parents_subset_ancestors k hl)) · exact inr (G.isAncestor_trans (G.mem_ancestors.mp (G.parents_subset_ancestors k hl)) hki)
    Causalean.Graph.FiniteDensity.parentClosed_nodeAncestralClosure · Causalean/Graph/FiniteDensity/Main.lean:51
  • selfParents_subset_nodeAncestralClosure theorem — A node and all of its parents belong to that node's ancestral closure.
    hypotheses
    V :
    Type u_1
    DAG V
    shared
    i :
    V
    conclusion
    insert i (G.parents i) ⊆ nodeAncestralClosure G i
    Proof (Lean source)
    theorem selfParents_subset_nodeAncestralClosure (i : V) : insert i (G.parents i) ⊆ nodeAncestralClosure G i := by -- Combine self-membership with `G.parents_subset_ancestors i`. intro j hj rw [mem_nodeAncestralClosure_iff] rcases Finset.mem_insert.mp hj with rfl | hj · exact inl rfl · exact inr (G.mem_ancestors.mp (G.parents_subset_ancestors i hj))
    Causalean.Graph.FiniteDensity.selfParents_subset_nodeAncestralClosure · Causalean/Graph/FiniteDensity/Main.lean:62
  • parentClosed_marginal_eq theorem — A DAG factorization, a parent-closed retained set, an intervention target outside that set, and a normalized replacement density give identical observational and interventional marginals on the retained set.
    hypotheses
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    A :
    Finset V
    hA :
    ParentClosed G A
    j :
    V
    hj :
    j ∉ A
    q :
    InterventionDensity j X μ
    conclusion
    Measure.map (coordinateProjection (X := X) A) B.observationalMeasure
    = Measure.map (coordinateProjection (X := X) A) (B.interventionMeasure j q)
    Proof (Lean source)
    theorem Factorization.parentClosed_marginal_eq (B : Factorization G X μ) {A : Finset V} (hA : ParentClosed G A) {j : V} (hj : j ∉ A) (q : InterventionDensity j X μ) : Measure.map (coordinateProjection (X := X) A) B.observationalMeasure = Measure.map (coordinateProjection (X := X) A) (B.interventionMeasure j q) := by -- Apply the coordinate-density bridge to the two complement-marginal elimination identities. apply map_coordinateProjection_withDensity_eq_of_lmarginal_eq A B.measurable_observationalDensity (B.measurable_interventionDensity j q) rw [B.lmarginal_compl_observationalDensity_eq hA, B.lmarginal_compl_interventionDensity_eq hA hj q]
    Causalean.Graph.FiniteDensity.Factorization.parentClosed_marginal_eq · Causalean/Graph/FiniteDensity/Main.lean:72
  • map_eq_of_dependsOn_nodeAncestralClosure theorem — A DAG factorization, distinct intervention and queried nodes, evidence that the intervention target is not an ancestor of the queried node, a normalized replacement density, a measurable outcome map, its dependence only on the queried node's ancestral closure, and an anchor assignment give the same observational and interventional outcome law.
    hypotheses
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    i j :
    V
    hji :
    j ≠ i
    hnotAncestor :
    ¬ G.isAncestor j i
    q :
    InterventionDensity j X μ
    Y :
    Type*
    MeasurableSpace Y
    f :
    (∀ k, X k) → Y
    hf :
    Measurable f
    hdepends :
    DependsOn (nodeAncestralClosure G i) f
    x₀ :
    ∀ k, X k
    conclusion
    Measure.map f B.observationalMeasure = Measure.map f (B.interventionMeasure j q)
    Proof (Lean source)
    theorem Factorization.map_eq_of_dependsOn_nodeAncestralClosure (B : Factorization G X μ) {i j : V} (hji : j ≠ i) (hnotAncestor : ¬ G.isAncestor j i) (q : InterventionDensity j X μ) {Y : Type*} [MeasurableSpace Y] (f : (∀ k, X k) → Y) (hf : Measurable f) (hdepends : DependsOn (nodeAncestralClosure G i) f) (x₀ : ∀ k, X k) : Measure.map f B.observationalMeasure = Measure.map f (B.interventionMeasure j q) := by -- Transport ancestral projection equality through the coordinate extension representation -- of `f`. exact map_eq_of_map_coordinateProjection_eq x₀ hf hdepends (B.ancestralMarginal_eq hji hnotAncestor q)
    Causalean.Graph.FiniteDensity.Factorization.map_eq_of_dependsOn_nodeAncestralClosure · Causalean/Graph/FiniteDensity/Main.lean:103
  • targetRatio_map_eq theorem — A DAG factorization, distinct intervention and ratio nodes, evidence that the intervention target is not an ancestor of the ratio node, a normalized replacement density, a node-coordinate numerator, measurability of the resulting ratio, and an anchor assignment give the same observational and interventional law for the canonical density ratio.
    hypotheses
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    i j :
    V
    hji :
    j ≠ i
    hnotAncestor :
    ¬ G.isAncestor j i
    q :
    InterventionDensity j X μ
    numerator :
    X i → ℝ≥0∞
    hratio :
    Measurable (fun v : ∀ k, X k ↦ numerator (v i) / B.factor i v)
    x₀ :
    ∀ k, X k
    conclusion
    Measure.map (fun v : ∀ k, X k ↦ numerator (v i) / B.factor i v) B.observationalMeasure
    = Measure.map (fun v : ∀ k, X k ↦ numerator (v i) / B.factor i v) (B.interventionMeasure j q)
    Proof (Lean source)
    theorem Factorization.targetRatio_map_eq (B : Factorization G X μ) {i j : V} (hji : j ≠ i) (hnotAncestor : ¬ G.isAncestor j i) (q : InterventionDensity j X μ) (numerator : X i → ℝ≥0∞) (hratio : Measurable (fun v : ∀ k, X k ↦ numerator (v i) / B.factor i v)) (x₀ : ∀ k, X k) : Measure.map (fun v : ∀ k, X k ↦ numerator (v i) / B.factor i v) B.observationalMeasure = Measure.map (fun v : ∀ k, X k ↦ numerator (v i) / B.factor i v) (B.interventionMeasure j q) := by -- Enlarge `targetRatio_dependsOn` to the ancestral closure, then use the dependent-map theorem. apply B.map_eq_of_dependsOn_nodeAncestralClosure hji hnotAncestor q (fun v : ∀ k, X k ↦ numerator (v i) / B.factor i v) hratio _ x₀ exact (B.targetRatio_dependsOn i numerator).mono (selfParents_subset_nodeAncestralClosure i)
    Causalean.Graph.FiniteDensity.Factorization.targetRatio_map_eq · Causalean/Graph/FiniteDensity/Main.lean:120
  • map_ancestralProjection_eq theorem — A DAG factorization, distinct intervention and queried nodes, evidence that the intervention target is not an ancestor of the queried node, a normalized replacement density, and a measurable map of the ancestral subproduct give the same observational and interventional law after that map.
    hypotheses
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    i j :
    V
    hji :
    j ≠ i
    hnotAncestor :
    ¬ G.isAncestor j i
    q :
    InterventionDensity j X μ
    Y :
    Type*
    MeasurableSpace Y
    mix :
    (∀ k : nodeAncestralClosure G i, X k) → Y
    hmix :
    Measurable mix
    conclusion
    Measure.map (mix ∘ coordinateProjection (X := X) (nodeAncestralClosure G i)) B.observationalMeasure
    = Measure.map (mix ∘ coordinateProjection (X := X) (nodeAncestralClosure G i)) (B.interventionMeasure j q)
    Proof (Lean source)
    theorem Factorization.map_ancestralProjection_eq (B : Factorization G X μ) {i j : V} (hji : j ≠ i) (hnotAncestor : ¬ G.isAncestor j i) (q : InterventionDensity j X μ) {Y : Type*} [MeasurableSpace Y] (mix : (∀ k : nodeAncestralClosure G i, X k) → Y) (hmix : Measurable mix) : Measure.map (mix ∘ coordinateProjection (X := X) (nodeAncestralClosure G i)) B.observationalMeasure = Measure.map (mix ∘ coordinateProjection (X := X) (nodeAncestralClosure G i)) (B.interventionMeasure j q) := by -- Use `Measure.map_map` on both sides of `ancestralMarginal_eq`. exact map_comp_eq_of_map_eq (measurable_coordinateProjection (X := X) (nodeAncestralClosure G i)) hmix (B.ancestralMarginal_eq hji hnotAncestor q)
    Causalean.Graph.FiniteDensity.Factorization.map_ancestralProjection_eq · Causalean/Graph/FiniteDensity/Main.lean:141
  • lintegral_observationalDensity_lt_top theorem — The observational density of a normalized finite DAG factorization has finite integral against the product reference measure.
    hypotheses
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    conclusion
    ∫⁻ x, B.observationalDensity x ∂Measure.pi μ < ∞
    Proof (Lean source)
    theorem Factorization.lintegral_observationalDensity_lt_top (B : Factorization G X μ) : ∫⁻ x, B.observationalDensity x ∂Measure.pi μ < ∞ := by /- Evaluate `B.lmarginal_compl_observationalDensity_eq` at the empty retained set after splitting on whether the full dependent product `∀ i, X i` is empty. In the inhabited case, evaluate the all-coordinate marginal at an anchor assignment and rewrite it as the full lintegral. In the empty case the product measure, hence the integral, is zero. Do not assume coordinate nonemptiness. -/ classical by_cases h : Nonempty (∀ i, X i) · let x : ∀ i, X i := choice h have hmarg := B.lmarginal_compl_observationalDensity_eq (A := ∅) (by intro i hi simp at hi) have hlin : ∫⁻ v, B.observationalDensity v ∂Measure.pi μ = 1 := by rw [MeasureTheory.lintegral_eq_lmarginal_univ x] simpa [Factorization.partialDensity] using congrFun hmarg x rw [hlin] exact ENNReal.one_lt_top · let _ : IsEmpty (∀ i, X i) := not_nonempty_iff.mp h rw [MeasureTheory.lintegral_of_isEmpty] exact ENNReal.zero_lt_top
    Causalean.Graph.FiniteDensity.Factorization.lintegral_observationalDensity_lt_top · Causalean/Graph/FiniteDensity/Main.lean:183
  • instIsFiniteMeasureObservationalMeasure instance — The observational measure induced by a normalized finite DAG factorization is a finite measure.
    parameters
    V :
    Type u_1
    V → Type u_2
    (i : V) → Measure (X i)
    DAG V
    shared
    B :
    Factorization G X μ
    instance
    instIsFiniteMeasureObservationalMeasure B :
    IsFiniteMeasure B.observationalMeasure
    given by
    by rw [Factorization.observationalMeasure] exact isFiniteMeasure_withDensity (ne_of_lt B.lintegral_observationalDensity_lt_top)
    Causalean.Graph.FiniteDensity.Factorization.instIsFiniteMeasureObservationalMeasure · Causalean/Graph/FiniteDensity/Main.lean:210
Cube 19 core · 15 supporting This module specializes the general finite-product theorem to real coordinates equipped with Lebesgue measure restricted to [0,1]. ★ ancestralMarginal_eq★ observationalMeasure_unitCubeFactorizationOfCubeFactors

Finite unit-cube specialization

This module specializes the general finite-product theorem to real coordinates equipped with Lebesgue measure restricted to [0,1]. The resulting product reference measure is concentrated on Set.pi Set.univ (fun _ ↦ Set.Icc 0 1), the finite product cube in the requirement.

def unitCube reviewed
Causalean.Graph.FiniteDensity

A vertex population determines the unit cube of real assignments: the set of assignments whose every coordinate lies in the closed interval from zero to one.

Definition (Lean source)
parameters
V :
Type u_1
shared
def
unitCube V :
Set (V → ℝ)
given by
pi univ (fun _ ↦ Icc (0 : ℝ) 1)
Causalean.Graph.FiniteDensity.unitCube · Causalean/Graph/FiniteDensity/Cube.lean:28
def unitIntervalReference reviewed
Causalean.Graph.FiniteDensity

The one-coordinate reference measure on the unit interval is Lebesgue measure restricted to the closed interval from zero to one.

Definition (Lean source)
def
unitIntervalReference :
Measure ℝ
given by
volume.restrict (Icc (0 : ℝ) 1)
Causalean.Graph.FiniteDensity.unitIntervalReference · Causalean/Graph/FiniteDensity/Cube.lean:33
def unitCubeReference reviewed
Causalean.Graph.FiniteDensity

A finite vertex population determines the product reference measure on its unit cube.

Definition (Lean source)
parameters
V :
Type u_1
shared
def
unitCubeReference V :
Measure (V → ℝ)
given by
Measure.pi (fun _ : V ↦ unitIntervalReference)
Causalean.Graph.FiniteDensity.unitCubeReference · Causalean/Graph/FiniteDensity/Cube.lean:38
abbrev UnitCubeFactorization reviewed
Causalean.Graph.FiniteDensity

A finite DAG determines the factorization interface whose coordinates use unit-interval-restricted Lebesgue reference measure.

Definition (Lean source)
parameters
V :
Type u_1
shared
G :
DAG V
def
UnitCubeFactorization V G :
Type (max u_1 0)
given by
Factorization G (fun _ : V ↦ ℝ) (fun _ : V ↦ unitIntervalReference)
Causalean.Graph.FiniteDensity.UnitCubeFactorization · Causalean/Graph/FiniteDensity/Cube.lean:63 · uses DAG
theorem ancestralMarginal_eq reviewed
Causalean.Graph.FiniteDensity.UnitCubeFactorization

A unit-cube DAG factorization, distinct intervention and queried nodes, evidence that the intervention target is not an ancestor of the queried node, and a normalized replacement density give identical observational and interventional laws on the queried node's ancestral closure.

Formal statement
hypotheses
V :
Type u_1
DAG V
shared
B :
UnitCubeFactorization V G
i j :
V
hji :
j ≠ i
hnotAncestor :
¬ G.isAncestor j i
q :
InterventionDensity j (fun _ : V ↦ ℝ) (fun _ : V ↦ unitIntervalReference)
conclusion
Measure.map (coordinateProjection (X := fun _ : V ↦ ℝ) (nodeAncestralClosure G i)) B.observationalMeasure
= Measure.map (coordinateProjection (X := fun _ : V ↦ ℝ) (nodeAncestralClosure G i)) (B.interventionMeasure j q)
Proof (Lean source)
theorem UnitCubeFactorization.ancestralMarginal_eq {G : DAG V} (B : UnitCubeFactorization V G) {i j : V} (hji : j ≠ i) (hnotAncestor : ¬ G.isAncestor j i) (q : InterventionDensity j (fun _ : V ↦ ℝ) (fun _ : V ↦ unitIntervalReference)) : Measure.map (coordinateProjection (X := fun _ : V ↦ ℝ) (nodeAncestralClosure G i)) B.observationalMeasure = Measure.map (coordinateProjection (X := fun _ : V ↦ ℝ) (nodeAncestralClosure G i)) (B.interventionMeasure j q) := by -- Establish the coordinatewise `SigmaFinite` family by unfolding `unitIntervalReference`, -- then apply `Factorization.ancestralMarginal_eq` without changing the measures or projection. have hσ : ∀ _ : V, SigmaFinite unitIntervalReference := fun _ ↦ by unfold unitIntervalReference infer_instance exact @Factorization.ancestralMarginal_eq V _ _ (fun _ : V ↦ ℝ) _ (fun _ : V ↦ unitIntervalReference) hσ G B i j hji hnotAncestor q
Causalean.Graph.FiniteDensity.UnitCubeFactorization.ancestralMarginal_eq · Causalean/Graph/FiniteDensity/Cube.lean:68 · uses DAG , isAncestor , interventionMeasure , observationalMeasure , InterventionDensity , UnitCubeFactorization , nodeAncestralClosure , unitIntervalReference , coordinateProjection
def clampCube reviewed
Causalean.Graph.FiniteDensity

A coordinate type and a real assignment determine the coordinatewise clamp to the closed unit cube, by clamping each coordinate between zero and one.

Definition (Lean source)
parameters
V :
Type u_1
shared
v :
V → ℝ
def
clampCube V v :
V → ℝ
given by
fun i ↦ max 0 (min 1 (v i))
Causalean.Graph.FiniteDensity.clampCube · Causalean/Graph/FiniteDensity/Cube.lean:103
def MeasurableOnSet reviewed
Causalean.Graph.FiniteDensity

A function and a set determine the proposition that the function is measurable on that set, by testing the restriction to the set's subtype.

Definition (Lean source)
parameters
X Y :
Type*
MeasurableSpace X
MeasurableSpace Y
f :
X → Y
S :
Set X
def
MeasurableOnSet f S :
Prop
given by
Measurable (fun x : S ↦ f x)
Causalean.Graph.FiniteDensity.MeasurableOnSet · Causalean/Graph/FiniteDensity/Cube.lean:207
def CubeDependsOn reviewed
Causalean.Graph.FiniteDensity

A node set and an extended-nonnegative function determine cube-local dependence, by requiring agreement on those coordinates to determine the function value at any two cube points.

Definition (Lean source)
parameters
V :
Type u_1
shared
A :
Finset V
f :
(V → ℝ) → ℝ≥0∞
v w :
V → ℝ
v ∈ unitCube V
w ∈ unitCube V
(∀ i ∈ A, v i = w i)
def
CubeDependsOn A f :
Prop
given by
f v = f w
Causalean.Graph.FiniteDensity.CubeDependsOn · Causalean/Graph/FiniteDensity/Cube.lean:213
def clampedFactor reviewed
Causalean.Graph.FiniteDensity

A cube-local extended-nonnegative function determines its globally defined clamped extension, by evaluating it after coordinatewise clamping.

Definition (Lean source)
parameters
V :
Type u_1
shared
p :
(V → ℝ) → ℝ≥0∞
def
clampedFactor p :
(V → ℝ) → ℝ≥0∞
given by
fun v ↦ p (clampCube V v)
Causalean.Graph.FiniteDensity.clampedFactor · Causalean/Graph/FiniteDensity/Cube.lean:222
def clampedOfRealFactor reviewed
Causalean.Graph.FiniteDensity

A cube-local real function determines its globally defined nonnegative clamped extension, by applying the nonnegative-real conversion after coordinatewise clamping.

Definition (Lean source)
parameters
V :
Type u_1
shared
p :
(V → ℝ) → ℝ
def
clampedOfRealFactor p :
(V → ℝ) → ℝ≥0∞
given by
fun v ↦ ofReal (p (clampCube V v))
Causalean.Graph.FiniteDensity.clampedOfRealFactor · Causalean/Graph/FiniteDensity/Cube.lean:227
def unitCubeFactorizationOfCubeFactors reviewed
Causalean.Graph.FiniteDensity

Cube-local extended-nonnegative factors that are measurable on the cube, local to each node and its parents on the cube, and normalized in their own coordinates on the cube determine a global unit-cube DAG factorization, by using their clamped extensions as factors.

Definition (Lean source)
parameters
V :
Type u_1
DAG V
shared
p :
∀ i : V
if
(V → ℝ)
then
ℝ≥0∞
hmeas :
∀ i : V, MeasurableOnSet (p i) (unitCube V)
hlocal :
∀ i : V, CubeDependsOn (insert i (G.parents i)) (p i)
hnorm :
∀ i : V,
∀ v : V → ℝ,
v ∈ unitCube V → ∫⁻ x in Icc (0 : ℝ) 1, p i (update v i x) ∂volume
= 1
def
unitCubeFactorizationOfCubeFactors p hmeas hlocal hnorm :
UnitCubeFactorization V G
given by
by refine { factor := fun i ↦ clampedFactor (p i) measurable_factor := fun i ↦ measurable_clampedFactor (hmeas i) local_factor := ?_ normalized_factor := ?_ } · intro i v w hvw apply hlocal i (clampCube_mem V v) (clampCube_mem V w) intro k hk simp only [clampCube] rw [hvw k hk] · intro i v unfold unitIntervalReference change ∫⁻ x in Icc (0 : ℝ) 1, p i (clampCube V (update v i x)) ∂volume
= 1 rw [setLIntegral_congr_fun measurableSet_Icc (fun x hx ↦ congrArg (p i) (clampCube_update_of_mem V v i hx))] exact hnorm i (clampCube V v) (clampCube_mem V v)
Causalean.Graph.FiniteDensity.unitCubeFactorizationOfCubeFactors · Causalean/Graph/FiniteDensity/Cube.lean:253 · uses DAG , parents , CubeDependsOn , MeasurableOnSet , UnitCubeFactorization , unitCube
def cubeProductDensityMeasure reviewed
Causalean.Graph.FiniteDensity

Cube-local extended-nonnegative factors determine the corresponding cube-restricted observational product-density measure, by weighting restricted Lebesgue volume with their joint product.

Definition (Lean source)
parameters
V :
Type u_1
shared
p :
∀ i : V
if
(V → ℝ)
then
ℝ≥0∞
def
cubeProductDensityMeasure p :
Measure (V → ℝ)
given by
(volume.restrict (unitCube V)).withDensity (fun v ↦ ∏ i, p i v)
Causalean.Graph.FiniteDensity.cubeProductDensityMeasure · Causalean/Graph/FiniteDensity/Cube.lean:301
def cubeInterventionDensityMeasure reviewed
Causalean.Graph.FiniteDensity

Cube-local extended-nonnegative factors, a target coordinate, and a replacement density determine the corresponding cube-restricted single-target product-density measure, by replacing that coordinate's factor in the joint product.

Definition (Lean source)
parameters
V :
Type u_1
shared
p :
∀ i : V
if
(V → ℝ)
then
ℝ≥0∞
j :
V
q :
ℝ → ℝ≥0∞
def
cubeInterventionDensityMeasure p j q :
Measure (V → ℝ)
given by
(volume.restrict (unitCube V)).withDensity (fun v ↦ q (v j) * ∏ i ∈ Finset.univ.erase j, p i v)
Causalean.Graph.FiniteDensity.cubeInterventionDensityMeasure · Causalean/Graph/FiniteDensity/Cube.lean:308
theorem observationalMeasure_unitCubeFactorizationOfCubeFactors reviewed
Causalean.Graph.FiniteDensity

Cube-local factors with cube measurability, node-and-parent locality, and coordinate-wise normalization give an observational law of the clamped factorization equal to the cube-restricted product-density measure.

Formal statement
hypotheses
V :
Type u_1
DAG V
shared
p :
∀ i : V
if
(V → ℝ)
then
ℝ≥0∞
hmeas :
∀ i : V, MeasurableOnSet (p i) (unitCube V)
hlocal :
∀ i : V, CubeDependsOn (insert i (G.parents i)) (p i)
hnorm :
∀ i : V,
∀ v : V → ℝ,
v ∈ unitCube V → ∫⁻ x in Icc (0 : ℝ) 1, p i (update v i x) ∂volume
= 1
conclusion
(unitCubeFactorizationOfCubeFactors p hmeas hlocal hnorm).observationalMeasure
= cubeProductDensityMeasure p
Proof (Lean source)
theorem observationalMeasure_unitCubeFactorizationOfCubeFactors {G : DAG V} (p : ∀ i : V, (V → ℝ) → ℝ≥0∞) (hmeas : ∀ i : V, MeasurableOnSet (p i) (unitCube V)) (hlocal : ∀ i : V, CubeDependsOn (insert i (G.parents i)) (p i)) (hnorm : ∀ i : V, ∀ v : V → ℝ, v ∈ unitCube V → ∫⁻ x in Icc (0 : ℝ) 1, p i (update v i x) ∂volume = 1) : (unitCubeFactorizationOfCubeFactors p hmeas hlocal hnorm).observationalMeasure = cubeProductDensityMeasure p := by -- Rewrite the reference measure with `unitCubeReference_eq_volume_restrict`; then apply -- `Measure.withDensity_congr_ae`, using the factor-on-cube lemma under the restricted measure. rw [observationalMeasure] change (unitCubeReference V).withDensity _ = _ rw [unitCubeReference_eq_volume_restrict] unfold cubeProductDensityMeasure apply withDensity_congr_ae filter_upwards [ae_restrict_mem measurableSet_unitCube] with v hv unfold observationalDensity partialDensity apply Finset.prod_congr rfl intro i hi exact unitCubeFactorizationOfCubeFactors_factor_eq p hmeas hlocal hnorm i hv
Causalean.Graph.FiniteDensity.observationalMeasure_unitCubeFactorizationOfCubeFactors · Causalean/Graph/FiniteDensity/Cube.lean:316 · uses DAG , parents , CubeDependsOn , observationalMeasure , MeasurableOnSet , cubeProductDensityMeasure , unitCube , unitCubeFactorizationOfCubeFactors , unitIntervalReference
def interventionDensityOfCube reviewed
Causalean.Graph.FiniteDensity

A target coordinate and a cube-local replacement density that is measurable on the interval and normalized there determine a global intervention density, by scalar clamping.

Definition (Lean source)
parameters
V :
Type u_1
shared
j :
V
q :
ℝ → ℝ≥0∞
hqmeas :
MeasurableOnSet q (Icc (0 : ℝ) 1)
hqnorm :
∫⁻ x in Icc (0 : ℝ) 1, q x ∂volume = 1
def
interventionDensityOfCube j q hqmeas hqnorm :
InterventionDensity j (fun _ : V ↦ ℝ) (fun _ : V ↦ unitIntervalReference)
given by
by refine { density := fun x ↦ q (max 0 (min 1 x)) measurable_density := ?_ normalized_density := ?_ } · exact hqmeas.comp ((measurable_const.max (measurable_const.min measurable_id)).subtype_mk (h := fun x ↦ by exact ⟨le_max_left _ _, max_le zero_le_one (min_le_left _ _)⟩)) · unfold unitIntervalReference change ∫⁻ x in Icc (0 : ℝ) 1, q (max 0 (min 1 x)) ∂volume
= 1 rw [setLIntegral_congr_fun measurableSet_Icc] · exact hqnorm · intro x hx simp [min_eq_right hx.2, max_eq_right hx.1]
Causalean.Graph.FiniteDensity.interventionDensityOfCube · Causalean/Graph/FiniteDensity/Cube.lean:342 · uses InterventionDensity , MeasurableOnSet , unitIntervalReference
def unitCubeFactorizationOfRealCubeFactors reviewed
Causalean.Graph.FiniteDensity

Real-valued cube factors that are measurable on the cube, nonnegative there, local to each node and its parents, and normalized by Lebesgue integration in their own coordinate determine a global unit-cube DAG factorization, by conversion to extended nonnegative factors.

Definition (Lean source)
parameters
V :
Type u_1
DAG V
shared
p :
∀ i : V
if
(V → ℝ)
then
ℝ
hmeas :
∀ i : V, MeasurableOnSet (p i) (unitCube V)
hnonneg :
∀ i : V, ∀ v, v ∈ unitCube V → 0 ≤ p i v
hlocal :
∀ i : V,
∀ {v w : V → ℝ},
v ∈ unitCube V → w ∈ unitCube V → (∀ k ∈ insert i (G.parents i), v k = w k) → p i v
= p i w
hnorm :
∀ i : V,
∀ v : V → ℝ,
v ∈ unitCube V → ∫ x in Icc (0 : ℝ) 1, p i (update v i x) ∂volume
= 1
def
unitCubeFactorizationOfRealCubeFactors p hmeas hnonneg hlocal hnorm :
UnitCubeFactorization V G
given by
by apply unitCubeFactorizationOfCubeFactors (fun i v ↦ ofReal (p i v)) · intro i exact ENNReal.measurable_ofReal.comp (hmeas i) · intro i v w hv hw hvw exact congrArg ofReal (hlocal i hv hw hvw) · intro i v hv have hvi : ∀ x ∈ Icc (0 : ℝ) 1, update v i x ∈ unitCube V := by intro x hx k hk by_cases hki : k
= i · subst k simpa using hx · simpa [update, hki] using hv k hk have hnn : 0 ≤ᵐ[volume.restrict (Icc (0 : ℝ) 1)] (fun x ↦ p i (update v i x)) := ae_restrict_of_forall_mem measurableSet_Icc fun x hx ↦ hnonneg i _ (hvi x hx) have hint : Integrable (fun x ↦ p i (update v i x)) (volume.restrict (Icc (0 : ℝ) 1)) := integrable_of_integral_eq_one (hnorm i v hv) rw [← ofReal_integral_eq_lintegral_ofReal hint hnn, hnorm i v hv, ENNReal.ofReal_one]
Causalean.Graph.FiniteDensity.unitCubeFactorizationOfRealCubeFactors · Causalean/Graph/FiniteDensity/Cube.lean:402 · uses DAG , parents , MeasurableOnSet , UnitCubeFactorization , unitCube
def realCubeProductDensityMeasure reviewed
Causalean.Graph.FiniteDensity

Real-valued cube factors, with no sign restriction, determine their cube-restricted observational product-density measure: Lebesgue measure restricted to the unit cube, weighted by the joint product of the factors, where a negative product is truncated to zero.

Definition (Lean source)
parameters
V :
Type u_1
shared
p :
∀ i : V
if
(V → ℝ)
then
ℝ
def
realCubeProductDensityMeasure p :
Measure (V → ℝ)
given by
(volume.restrict (unitCube V)).withDensity (fun v ↦ ofReal (∏ i, p i v))
Causalean.Graph.FiniteDensity.realCubeProductDensityMeasure · Causalean/Graph/FiniteDensity/Cube.lean:464
def realCubeInterventionDensityMeasure reviewed
Causalean.Graph.FiniteDensity

Real-valued cube factors, a target coordinate, and a real-valued replacement function for that coordinate, none sign-restricted, determine their cube-restricted single-target product-density measure: Lebesgue measure restricted to the unit cube, weighted by the product in which the target factor is replaced by the replacement evaluated at the target coordinate, with a negative product truncated to zero.

Definition (Lean source)
parameters
V :
Type u_1
shared
p :
∀ i : V
if
(V → ℝ)
then
ℝ
j :
V
q :
ℝ → ℝ
def
realCubeInterventionDensityMeasure p j q :
Measure (V → ℝ)
given by
(volume.restrict (unitCube V)).withDensity (fun v ↦ ofReal (q (v j) * ∏ i ∈ Finset.univ.erase j, p i v))
Causalean.Graph.FiniteDensity.realCubeInterventionDensityMeasure · Causalean/Graph/FiniteDensity/Cube.lean:471
def interventionDensityOfRealCube reviewed
Causalean.Graph.FiniteDensity

A target coordinate and a real replacement density that is measurable on the unit interval, nonnegative there, and Lebesgue-normalized determine a global intervention density, by nonnegative-real conversion followed by scalar clamping.

Definition (Lean source)
parameters
V :
Type u_1
shared
j :
V
q :
ℝ → ℝ
hqmeas :
MeasurableOnSet q (Icc (0 : ℝ) 1)
hqnonneg :
∀ x ∈ Icc (0 : ℝ) 1, 0 ≤ q x
hqnorm :
∫ x in Icc (0 : ℝ) 1, q x ∂volume = 1
def
interventionDensityOfRealCube j q hqmeas hqnonneg hqnorm :
InterventionDensity j (fun _ : V ↦ ℝ) (fun _ : V ↦ unitIntervalReference)
given by
by apply interventionDensityOfCube j (fun x ↦ ofReal (q x)) · exact ENNReal.measurable_ofReal.comp hqmeas · have hnn : 0
≤ᵐ[volume.restrict (Icc (0 : ℝ) 1)] q := ae_restrict_of_forall_mem measurableSet_Icc hqnonneg have hint : Integrable q (volume.restrict (Icc (0 : ℝ) 1)) := integrable_of_integral_eq_one hqnorm rw [← ofReal_integral_eq_lintegral_ofReal hint hnn, hqnorm, ENNReal.ofReal_one]
Causalean.Graph.FiniteDensity.interventionDensityOfRealCube · Causalean/Graph/FiniteDensity/Cube.lean:513 · uses InterventionDensity , MeasurableOnSet , unitIntervalReference
15 supporting declarations (lemmas, instances)