SCM.Factored

Factorization of an SCM's observational law into prefix kernels: parent lookup, step kernels, and the correspondence with deterministic evaluation.

Prefix­State 5 core · 2 supporting This file builds the finite prefix state spaces used to construct a structural causal model's joint kernel sequentially along a topological ordering. ★ measurable_extendOrderedLatentPrefix

Prefix States for Factored Kernels

This file builds the finite prefix state spaces used to construct a structural causal model's joint kernel sequentially along a topological ordering. The definitions package latent values together with already generated observed values, with measurability facts for the downstream factored-kernel construction.

def ObservedPrefixValues reviewed
Causalean.SCM

For a finite collection of distinguishable node labels with measurable value spaces, a structural causal model, a natural number nn no greater than its number of observed nodes, the observed-prefix value space is the one-point space of the empty assignment when n=0n=0, and the product of the preceding prefix space and the value space of the nn-th observed node when nn is positive.

Definition (Lean source)
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
n :
ℕ
n ≤ M.observed.card
ObservedPrefixValues M n :
Type _
fun n hn
=> match n with | 0 => PUnit.{uΩ + 1} | k
+ 1
=> ObservedPrefixValues M k (le_of_succ_le hn) × swigΩ Ω (M.observedAt ⟨k, hn⟩).val
Causalean.SCM.ObservedPrefixValues · Causalean/SCM/Factored/PrefixState.lean:38 · uses SWIGNode , SCM
abbrev OrderedLatentPrefixValues reviewed
Causalean.SCM

Random values consisting of the latent tuple paired with an observed prefix. This is the state-space of the kernel at step n in the factored construction.

Definition (Lean source)
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
n :
ℕ
hn :
n ≤ M.observed.card
OrderedLatentPrefixValues M n hn :
Type (max (max uΩ uN) uΩ)
Causalean.SCM.OrderedLatentPrefixValues · Causalean/SCM/Factored/PrefixState.lean:65 · uses SWIGNode , SCM
def observedPrefixValue reviewed
Causalean.SCM

For a finite collection of distinguishable node labels with measurable value spaces, a structural causal model, a prefix length no greater than the number of its observed nodes, an assignment on that prefix, and a position within the prefix, the observed-prefix coordinate reader has no value when the prefix is empty, and otherwise returns the assigned value at that position, reading recursively from the preceding prefix or directly from its final coordinate.

Definition (Lean source)
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
n :
ℕ
hn :
n ≤ M.observed.card
M.ObservedPrefixValues n hn
i :
Fin n
observedPrefixValue M hn i :
swigΩ Ω (M.observedAt ⟨i.1, lt_of_lt_of_le i.2 hn⟩).val
clause 1
| 0, _, _, i => elim0 i
clause 2
| k + 1, hn, ξ, i
=> Fin.lastCases (by simpa using ξ.2) (fun j => by simpa using M.observedPrefixValue (le_of_succ_le hn) ξ.1 j) i
def extendOrderedLatentPrefix reviewed
Causalean.SCM

For a finite collection of distinguishable node labels with measurable value spaces, a structural causal model, a natural number nn, and evidence that the model has at least n+1n+1 observed nodes, the ordered-latent prefix extension map takes a latent assignment, an assignment to the first nn observed nodes, and the value of the next observed node, and returns the same latent assignment paired with the resulting length-n+1n+1 observed prefix.

Definition (Lean source)
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
n :
ℕ
hn :
n + 1 ≤ M.observed.card
extendOrderedLatentPrefix M hn :
(M.OrderedLatentPrefixValues n (le_of_succ_le hn) × swigΩ Ω (M.observedAt ⟨n, hn⟩).val) → M.OrderedLatentPrefixValues (n + 1) hn
| ((ℓ, ξ), y) => (ℓ, (ξ, y))
theorem measurable_extendOrderedLatentPrefix reviewed
Causalean.SCM

Fix a structural causal model M and a step index n such that there are at least n + 1 observed nodes, so n names the next node to be appended in the canonical topological order of observed nodes. Then the map that appends the freshly generated value of that node to a length-n prefix of previously observed values, together with the latent assignment, producing a length-(n + 1) prefix, is measurable.

Formal statement
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
n :
ℕ
hn :
n + 1 ≤ M.observed.card
Measurable (M.extendOrderedLatentPrefix hn)
Proof (Lean source)
@[fun_prop] theorem measurable_extendOrderedLatentPrefix (M : SCM N Ω) {n : ℕ} (hn : n + 1 ≤ M.observed.card) : Measurable (M.extendOrderedLatentPrefix hn) := prodMk (measurable_fst.comp measurable_fst) (prodMk (measurable_snd.comp measurable_fst) measurable_snd)
2 supporting declarations (lemmas, instances)
  • instMeasurableSpaceObservedPrefixValues instance — For a finite, distinguishable node population with measurable node-value spaces, a structural causal model, and any natural number no greater than the number of its observed nodes, the measurable-space structure on the corresponding observed-prefix value space is provided by the one-point measurable space for a zero-length prefix and by the product measurable space for a positive-length prefix.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n ≤ M.observed.card
    instMeasurableSpaceObservedPrefixValues M hn :
    MeasurableSpace (M.ObservedPrefixValues n hn)
    clause 1
    | 0, _ => by dsimp [ObservedPrefixValues] infer_instance
    clause 2
    | k + 1, hn
    => by dsimp [ObservedPrefixValues] letI := instMeasurableSpaceObservedPrefixValues (M := M) (hn := le_of_succ_le hn) infer_instance
    Causalean.SCM.instMeasurableSpaceObservedPrefixValues · Causalean/SCM/Factored/PrefixState.lean:52
  • measurable_observedPrefixValue theorem — observedPrefixValue is measurable in its prefix-state argument.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n ≤ M.observed.card
    i :
    Fin n
    Measurable (fun ξ : M.ObservedPrefixValues n hn => M.observedPrefixValue hn ξ i) | 0, _, i
    => elim0 i | k
    + 1, hn, i
    => Fin.lastCases (by have h : Measurable (fun ξ : M.ObservedPrefixValues k (le_of_succ_le hn) × swigΩ Ω (M.observedAt ⟨k, hn⟩).val => ξ.2) := measurable_snd simp only [SCM.observedPrefixValue, Fin.lastCases_last] exact h) (fun j => by have h : Measurable (fun ξ : M.ObservedPrefixValues k (le_of_succ_le hn) × swigΩ Ω (M.observedAt ⟨k, hn⟩).val => M.observedPrefixValue (le_of_succ_le hn) ξ.1 j) := (M.measurable_observedPrefixValue (le_of_succ_le hn) j).comp measurable_fst simp only [SCM.observedPrefixValue, Fin.lastCases_castSucc] exact h) i
    Proof (Lean source)
    @[fun_prop] theorem measurable_observedPrefixValue (M : SCM N Ω) : ∀ {n : ℕ} (hn : n ≤ M.observed.card) (i : Fin n), Measurable (fun ξ : M.ObservedPrefixValues n hn => M.observedPrefixValue hn ξ i) | 0, _, i => elim0 i | k + 1, hn, i => Fin.lastCases (by have h : Measurable (fun ξ : M.ObservedPrefixValues k (le_of_succ_le hn) × swigΩ Ω (M.observedAt ⟨k, hn⟩).val => ξ.2) := measurable_snd simp only [SCM.observedPrefixValue, Fin.lastCases_last] exact h) (fun j => by have h : Measurable (fun ξ : M.ObservedPrefixValues k (le_of_succ_le hn) × swigΩ Ω (M.observedAt ⟨k, hn⟩).val => M.observedPrefixValue (le_of_succ_le hn) ξ.1 j) := (M.measurable_observedPrefixValue (le_of_succ_le hn) j).comp measurable_fst simp only [SCM.observedPrefixValue, Fin.lastCases_castSucc] exact h) i
    Causalean.SCM.measurable_observedPrefixValue · Causalean/SCM/Factored/PrefixState.lean:95
Prefix­Kernel 3 core · 3 supporting This file constructs the prefix kernels that generate latent variables and then observed variables sequentially along a topological order.

Prefix Kernels for Sequential Factorization

This file constructs the prefix kernels that generate latent variables and then observed variables sequentially along a topological order. These kernels are the recursive components used to express the structural-model joint kernel as a Markov factorization, with Markov-kernel instances for the base and recursive cases.

def latentKernelOnFixed reviewed
Causalean.SCM

For a finite collection of nodes with a measurable outcome space for each node and a structural causal model, the kernel giving the distribution of the latent-node values conditional on the fixed-node values assigns the same latent product distribution to every fixed-node assignment.

Definition (Lean source)
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
latentKernelOnFixed M :
Kernel M.FixedValues M.LatentValues
const _ M.latentProduct
def jointKernelPrefixZero reviewed
Causalean.SCM

For a finite collection of nodes with a measurable outcome space for each node and a structural causal model, the zero-step prefix kernel maps every fixed-node assignment to the joint distribution of all latent-node values and the unique empty observed-node prefix at prefix length zero.

Definition (Lean source)
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
jointKernelPrefixZero M :
Kernel M.FixedValues (M.OrderedLatentPrefixValues 0 (zero_le _))
M.latentKernelOnFixed.map (fun ℓ => (ℓ, (PUnit.unit : PUnit.{uΩ + 1})))
def jointKernelPrefix reviewed
Causalean.SCM

For a finite collection of nodes with a measurable outcome space for each node, a structural causal model, a nonnegative integer, and proof that this integer does not exceed the number of observed nodes, the prefix kernel maps each fixed-node assignment to the joint distribution of all latent-node values and the values of the first specified number of observed nodes. At zero observed nodes it is the zero-step prefix kernel; at each positive prefix length it extends the preceding prefix distribution by the next observed node's deterministic structural equation.

Definition (Lean source)
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
n :
ℕ
hn :
n ≤ M.observed.card
jointKernelPrefix M n hn :
Kernel M.FixedValues (M.OrderedLatentPrefixValues n hn)
clause 1
| 0, _ => M.jointKernelPrefixZero
clause 2
| k + 1, hn
=> ((M.jointKernelPrefix k (le_of_succ_le hn)) ⊗ₖ (M.stepKernel hn)).map (M.extendOrderedLatentPrefix hn)
3 supporting declarations (lemmas, instances)
  • isMarkov_latentKernelOnFixed instance — For a finite collection of nodes with measurable value spaces and a structural causal model, the Markov-kernel structure for the constant latent-value kernel asserts that the kernel assigning the latent product distribution to every fixed-value assignment is a Markov kernel.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    isMarkov_latentKernelOnFixed M :
    IsMarkovKernel M.latentKernelOnFixed
    by unfold latentKernelOnFixed; infer_instance
    Causalean.SCM.isMarkov_latentKernelOnFixed · Causalean/SCM/Factored/PrefixKernel.lean:65
  • isMarkov_jointKernelPrefixZero instance — For a finite collection of nodes with measurable value spaces and a structural causal model, the Markov-kernel structure for the zero-step prefix kernel asserts that the kernel generating the latent values and the empty observed prefix is a Markov kernel.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    isMarkov_jointKernelPrefixZero M :
    IsMarkovKernel M.jointKernelPrefixZero
    by unfold jointKernelPrefixZero exact ProbabilityTheory.Kernel.IsMarkovKernel.map M.latentKernelOnFixed (by fun_prop)
    Causalean.SCM.isMarkov_jointKernelPrefixZero · Causalean/SCM/Factored/PrefixKernel.lean:92
  • isMarkov_jointKernelPrefix instance — For a finite collection of nodes with measurable value spaces, a structural causal model, a nonnegative integer, and proof that this integer does not exceed the number of observed nodes, the Markov-kernel structure for the corresponding prefix kernel asserts that the kernel generating all latent values and the first specified observed values is a Markov kernel.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n ≤ M.observed.card
    isMarkov_jointKernelPrefix M n hn :
    IsMarkovKernel (M.jointKernelPrefix n hn)
    clause 1
    | 0, _ => M.isMarkov_jointKernelPrefixZero
    clause 2
    | k + 1, hn
    => by letI := M.isMarkov_jointKernelPrefix k (le_of_succ_le hn) letI := M.isMarkov_stepKernel hn change IsMarkovKernel (((M.jointKernelPrefix k (le_of_succ_le hn)) ⊗ₖ (M.stepKernel hn)).map (M.extendOrderedLatentPrefix hn)) exact ProbabilityTheory.Kernel.IsMarkovKernel.map ((M.jointKernelPrefix k (le_of_succ_le hn)) ⊗ₖ (M.stepKernel hn)) (M.measurable_extendOrderedLatentPrefix hn)
    Causalean.SCM.isMarkov_jointKernelPrefix · Causalean/SCM/Factored/PrefixKernel.lean:128
Step­Kernel 3 core · 1 supporting This file constructs the deterministic kernel that generates the next observed coordinate from its fixed, latent, and previously generated observed parents. ★ measurable_stepFun

Step Kernels for Observed Nodes

This file constructs the deterministic kernel that generates the next observed coordinate from its fixed, latent, and previously generated observed parents. The step kernels are the local transition pieces in the sequential factorization of the joint kernel, and their measurability follows from the parent-lookup map and the SCM structural-function measurability field.

def stepFun reviewed
Causalean.SCM

For a structural causal model and an index nn for which at least n+1n+1 observed vertices exist, the deterministic step function maps a fixed-value assignment together with the latent and already generated observed-prefix values to the value of the nn-th observed vertex in the model's canonical topological order, by applying that vertex's structural function to the values of its parents.

Definition (Lean source)
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
n :
ℕ
hn :
n + 1 ≤ M.observed.card
stepFun M hn :
(M.FixedValues × M.OrderedLatentPrefixValues n (le_of_succ_le hn)) → swigΩ Ω (M.observedAt ⟨n, hn⟩).val
fun sℓξ => M.structFun (M.observedAt ⟨n, hn⟩) (M.parentValuesFromPrefix hn sℓξ)
theorem measurable_stepFun reviewed
Causalean.SCM

Fix a structural causal model M and a step index n such that there are at least n + 1 observed nodes, so n names a valid position in the canonical topological order of observed nodes. Then the deterministic map stepFun, which produces the value of the n-th observed node by assembling its parent tuple from the fixed values, latent values, and previously generated observed prefix and applying the node's structural equation, is measurable.

Formal statement
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
n :
ℕ
hn :
n + 1 ≤ M.observed.card
Measurable (M.stepFun hn)
Proof (Lean source)
@[fun_prop] theorem measurable_stepFun (M : SCM N Ω) {n : ℕ} (hn : n + 1 ≤ M.observed.card) : Measurable (M.stepFun hn) := (M.structFun_measurable (M.observedAt ⟨n, hn⟩)).comp (M.measurable_parentValuesFromPrefix hn)
def stepKernel reviewed
Causalean.SCM

For a structural causal model and an index nn for which at least n+1n+1 observed vertices exist, the step kernel is the probability kernel that assigns unit mass to the value of the nn-th observed vertex produced by its structural function from the fixed values, latent values, and already generated observed-prefix values.

Definition (Lean source)
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
n :
ℕ
hn :
n + 1 ≤ M.observed.card
stepKernel M hn :
Kernel (M.FixedValues × M.OrderedLatentPrefixValues n (le_of_succ_le hn)) (swigΩ Ω (M.observedAt ⟨n, hn⟩).val)
deterministic (M.stepFun hn) (M.measurable_stepFun hn)
1 supporting declaration (lemmas, instances)
  • isMarkov_stepKernel instance — For a finite node population with measurable value spaces, a structural causal model, a nonnegative integer, and proof that adding one to this integer does not exceed the number of observed nodes, the Markov-kernel structure for the corresponding deterministic step kernel asserts that the kernel assigning the next observed value from its structural equation is a Markov kernel.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n + 1 ≤ M.observed.card
    isMarkov_stepKernel M hn :
    IsMarkovKernel (M.stepKernel hn)
    by unfold stepKernel; infer_instance
    Causalean.SCM.isMarkov_stepKernel · Causalean/SCM/Factored/StepKernel.lean:101
Eval­Map­Correspond 2 core · 7 supporting This file relates the recursive prefix-kernel construction to the deterministic evaluation map of a structural causal model. ★ jointKernelPrefix_apply_eq

Correspondence Between Prefix Kernels and Evaluation

This file relates the recursive prefix-kernel construction to the deterministic evaluation map of a structural causal model. It defines the deterministic prefix state produced by fixed and latent assignments, proves its measurability and latent projection facts, proves coordinate agreement with evalObservedAux, and identifies each prefix kernel as the pushforward of the latent product through that deterministic prefix map.

def partialEvalMap reviewed
Causalean.SCM

For a finite collection of nodes with a measurable outcome space for each node, a structural causal model, a nonnegative integer, and proof that this integer does not exceed the number of observed nodes, the deterministic prefix-state map takes fixed-node values and latent-node values and returns the latent-node values together with the values generated for the first specified number of observed nodes. At zero observed nodes it returns the latent-node values and the unique empty prefix; at each positive prefix length it first forms the preceding prefix and then appends the value given by the next node's structural equation.

Definition (Lean source)
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
n :
ℕ
hn :
n ≤ M.observed.card
partialEvalMap M n hn :
clause 1
| 0, _, _, ℓ => (ℓ, (PUnit.unit : PUnit.{uΩ + 1}))
clause 2
| k + 1, hn, s, ℓ
=> let prev := M.partialEvalMap k (le_of_succ_le hn) s ℓ M.extendOrderedLatentPrefix hn (prev, M.stepFun hn (s, prev))
theorem jointKernelPrefix_apply_eq reviewed
Causalean.SCM

Main correspondence. For a structural causal model M, its length-n prefix kernel evaluated at a fixed assignment s equals the pushforward of the latent-value product measure through the deterministic partial evaluation map at s.

Formal statement
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
s :
n :
ℕ
hn :
n ≤ M.observed.card
(M.jointKernelPrefix n hn) s
= M.latentProduct.map (fun ℓ => M.partialEvalMap n hn s ℓ) | 0, _ => by have hpair0 : Measurable (fun ℓ : LatentValues M => (ℓ, (PUnit.unit : PUnit.{uΩ + 1})))
Proof (Lean source)
theorem jointKernelPrefix_apply_eq (M : SCM N Ω) (s : FixedValues M) : ∀ (n : ℕ) (hn : n ≤ M.observed.card), (M.jointKernelPrefix n hn) s = M.latentProduct.map (fun ℓ => M.partialEvalMap n hn s ℓ) | 0, _ => by -- Base: jointKernelPrefixZero at `s` is `latentProduct.map (fun ℓ => (ℓ, PUnit.unit))`, -- which matches `partialEvalMap 0 _ s ℓ = (ℓ, PUnit.unit)` by definition. -- `partialEvalMap 0 _ s ℓ = (ℓ, PUnit.unit)`, matching the def of -- `jointKernelPrefixZero` after unfolding `Kernel.map_apply` + `const_apply`. have hpair0 : Measurable (fun ℓ : LatentValues M => (ℓ, (PUnit.unit : PUnit.{uΩ + 1}))) := by fun_prop change (M.latentKernelOnFixed.map (fun ℓ => (ℓ, (PUnit.unit : PUnit.{uΩ + 1})))) s = _ rw [ProbabilityTheory.Kernel.map_apply _ hpair0] unfold latentKernelOnFixed rw [ProbabilityTheory.Kernel.const_apply] rfl | k + 1, hn => by have ih := M.jointKernelPrefix_apply_eq s k (le_of_succ_le hn) -- Measurability helpers. have hext := M.measurable_extendOrderedLatentPrefix hn have hstep := M.measurable_stepFun hn have hpair : Measurable (fun ξ : M.OrderedLatentPrefixValues k (le_of_succ_le hn) => (ξ, M.stepFun hn (s, ξ))) := by fun_prop have hpem : Measurable (fun ℓ : LatentValues M => M.partialEvalMap k (le_of_succ_le hn) s ℓ) := by fun_prop -- Unfold `jointKernelPrefix (k+1)` to `(compProd k ⊗ stepKernel).map extend`. change (((M.jointKernelPrefix k (le_of_succ_le hn)) ⊗ₖ (M.stepKernel hn)).map (M.extendOrderedLatentPrefix hn)) s = _ rw [ProbabilityTheory.Kernel.map_apply _ hext] -- Collapse the compProd with deterministic stepKernel via 3b helper. unfold stepKernel rw [compProd_deterministic_apply (M.jointKernelPrefix k (le_of_succ_le hn)) hstep s] -- LHS: `((κ s).map pair).map extend`. Compose via `Measure.map_map`. rw [MeasureTheory.Measure.map_map hext hpair] -- Apply IH to replace `κ s` with `latentProduct.map (partialEvalMap k _ s ·)`. rw [ih] -- LHS: `(latentProduct.map (partialEvalMap k _ s)).map (extend ∘ pair)`. -- Collapse via `Measure.map_map` once more. rw [MeasureTheory.Measure.map_map (hext.comp hpair) hpem] -- Match composition with `partialEvalMap (k+1) hn s ·` by definitional unfolding. rfl
7 supporting declarations (lemmas, instances)
  • partialEvalMap_latent theorem — The first component of partialEvalMap is always the input latent tuple: the recursion only writes to the ObservedPrefixValues factor.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    s :
    ℓ :
    n :
    ℕ
    hn :
    n ≤ M.observed.card
    (M.partialEvalMap n hn s ℓ).1 = ℓ | 0, _ => rfl | k + 1, hn => by have ih
    Proof (Lean source)
    theorem partialEvalMap_latent (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) : ∀ (n : ℕ) (hn : n ≤ M.observed.card), (M.partialEvalMap n hn s ℓ).1 = ℓ | 0, _ => rfl | k + 1, hn => by -- Unfold one step and reduce `extendOrderedLatentPrefix`. have ih := M.partialEvalMap_latent s ℓ k (le_of_succ_le hn) -- `partialEvalMap (k+1) hn s ℓ = extendOrderedLatentPrefix hn (prev, stepFun hn (s, prev))`. -- `extendOrderedLatentPrefix hn ((ℓ', ξ), y) = (ℓ', (ξ, y))`, so `.1 = prev.1 = ℓ` by IH. change (M.extendOrderedLatentPrefix hn (M.partialEvalMap k (le_of_succ_le hn) s ℓ, M.stepFun hn (s, M.partialEvalMap k (le_of_succ_le hn) s ℓ))).1 = ℓ -- By definition of `extendOrderedLatentPrefix` on `((ℓ', ξ), y)`. set prev := M.partialEvalMap k (le_of_succ_le hn) s ℓ with hprev rcases hprev_eq : prev with ⟨ℓ', ξ⟩ have : ℓ' = ℓ := by have : prev.1 = ℓ := ih rw [hprev_eq] at this exact this subst this rfl
    Causalean.SCM.partialEvalMap_latent · Causalean/SCM/Factored/EvalMapCorrespond.lean:99
  • measurable_partialEvalMap theorem — partialEvalMap is jointly measurable in (s, ℓ). Proved by induction on n: the base case is a product of projections, and the step case composes the measurable stepFun, extendOrderedLatentPrefix, and the inductive hypothesis.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n ≤ M.observed.card
    Measurable (fun sℓ : FixedValues M × LatentValues M => M.partialEvalMap n hn sℓ.1 sℓ.2) | 0, _
    => by change Measurable (fun sℓ : FixedValues M × LatentValues M => (sℓ.2, (PUnit.unit : PUnit.{uΩ + 1}))) exact prodMk measurable_snd measurable_const | k
    + 1, hn => by have ih
    Proof (Lean source)
    @[fun_prop] theorem measurable_partialEvalMap (M : SCM N Ω) : ∀ (n : ℕ) (hn : n ≤ M.observed.card), Measurable (fun sℓ : FixedValues M × LatentValues M => M.partialEvalMap n hn sℓ.1 sℓ.2) | 0, _ => by -- `partialEvalMap 0 _ s ℓ = (ℓ, PUnit.unit)`. change Measurable (fun sℓ : FixedValues M × LatentValues M => (sℓ.2, (PUnit.unit : PUnit.{uΩ + 1}))) exact prodMk measurable_snd measurable_const | k + 1, hn => by have ih := M.measurable_partialEvalMap k (le_of_succ_le hn) -- Build the pair `(prev, stepFun hn (s, prev))`, then apply -- `extendOrderedLatentPrefix hn`. have hpair : Measurable (fun sℓ : FixedValues M × LatentValues M => (M.partialEvalMap k (le_of_succ_le hn) sℓ.1 sℓ.2, M.stepFun hn (sℓ.1, M.partialEvalMap k (le_of_succ_le hn) sℓ.1 sℓ.2))) := by refine prodMk ih ?_ refine (M.measurable_stepFun hn).comp ?_ exact prodMk measurable_fst ih exact (M.measurable_extendOrderedLatentPrefix hn).comp hpair
    Causalean.SCM.measurable_partialEvalMap · Causalean/SCM/Factored/EvalMapCorrespond.lean:128
  • observedPrefixValue_succ_last lemma — Appending an observed coordinate to a prefix makes the final coordinate of the expanded prefix equal to the appended value.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    k :
    ℕ
    hn :
    k + 1 ≤ M.observed.card
    ξ :
    M.ObservedPrefixValues k (le_of_succ_le hn)
    y :
    swigΩ Ω (M.observedAt ⟨k, hn⟩).val
    M.observedPrefixValue hn ((ξ, y) : M.ObservedPrefixValues (k + 1) hn) (last k) = y
    Proof (Lean source)
    lemma observedPrefixValue_succ_last (M : SCM N Ω) {k : ℕ} (hn : k + 1 ≤ M.observed.card) (ξ : M.ObservedPrefixValues k (le_of_succ_le hn)) (y : swigΩ Ω (M.observedAt ⟨k, hn⟩).val) : M.observedPrefixValue hn ((ξ, y) : M.ObservedPrefixValues (k + 1) hn) (last k) = y := by simp [observedPrefixValue, Fin.lastCases_last]
    Causalean.SCM.observedPrefixValue_succ_last · Causalean/SCM/Factored/EvalMapCorrespond.lean:165
  • observedPrefixValue_succ_castSucc lemma — Appending an observed coordinate to a prefix leaves every earlier coordinate of the prefix unchanged.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    k :
    ℕ
    hn :
    k + 1 ≤ M.observed.card
    ξ :
    M.ObservedPrefixValues k (le_of_succ_le hn)
    y :
    swigΩ Ω (M.observedAt ⟨k, hn⟩).val
    j :
    Fin k
    M.observedPrefixValue hn ((ξ, y) : M.ObservedPrefixValues (k + 1) hn) j.castSucc
    = M.observedPrefixValue (le_of_succ_le hn) ξ j
    Proof (Lean source)
    lemma observedPrefixValue_succ_castSucc (M : SCM N Ω) {k : ℕ} (hn : k + 1 ≤ M.observed.card) (ξ : M.ObservedPrefixValues k (le_of_succ_le hn)) (y : swigΩ Ω (M.observedAt ⟨k, hn⟩).val) (j : Fin k) : M.observedPrefixValue hn ((ξ, y) : M.ObservedPrefixValues (k + 1) hn) j.castSucc = M.observedPrefixValue (le_of_succ_le hn) ξ j := by simp [observedPrefixValue, Fin.lastCases_castSucc]
    Causalean.SCM.observedPrefixValue_succ_castSucc · Causalean/SCM/Factored/EvalMapCorrespond.lean:175
  • partialEvalMap_succ_snd_fst lemma — Extending a deterministic evaluation prefix by one observed variable leaves the previously computed observed prefix unchanged.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    s :
    ℓ :
    k :
    ℕ
    hn :
    k + 1 ≤ M.observed.card
    ((M.partialEvalMap (k + 1) hn s ℓ).2 : M.ObservedPrefixValues (k + 1) hn).1
    = (M.partialEvalMap k (le_of_succ_le hn) s ℓ).2
    Proof (Lean source)
    lemma partialEvalMap_succ_snd_fst (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) {k : ℕ} (hn : k + 1 ≤ M.observed.card) : ((M.partialEvalMap (k + 1) hn s ℓ).2 : M.ObservedPrefixValues (k + 1) hn).1 = (M.partialEvalMap k (le_of_succ_le hn) s ℓ).2 := by rfl
    Causalean.SCM.partialEvalMap_succ_snd_fst · Causalean/SCM/Factored/EvalMapCorrespond.lean:186
  • partialEvalMap_succ_snd_snd lemma — Extending a deterministic evaluation prefix appends the value determined for the newly added observed variable.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    s :
    ℓ :
    k :
    ℕ
    hn :
    k + 1 ≤ M.observed.card
    ((M.partialEvalMap (k + 1) hn s ℓ).2 : M.ObservedPrefixValues (k + 1) hn).2
    = M.stepFun hn (s, M.partialEvalMap k (le_of_succ_le hn) s ℓ)
    Proof (Lean source)
    lemma partialEvalMap_succ_snd_snd (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) {k : ℕ} (hn : k + 1 ≤ M.observed.card) : ((M.partialEvalMap (k + 1) hn s ℓ).2 : M.ObservedPrefixValues (k + 1) hn).2 = M.stepFun hn (s, M.partialEvalMap k (le_of_succ_le hn) s ℓ) := by rfl
    Causalean.SCM.partialEvalMap_succ_snd_snd · Causalean/SCM/Factored/EvalMapCorrespond.lean:196
  • partialEvalMap_observedPrefixValue theorem — Bridges partialEvalMap (kernel-side) to evalObservedAux (existing evaluator). Proven by induction on n mirroring the definitions: at each step, the newly-appended coordinate (index n) is stepFun hn (s, prev) = structFun v_n (parentValuesFromPrefix hn (s, prev)), which equals evalObservedAux M s ℓ n _ once one shows the parent lookups agree. Earlier indices are handled by the inductive hypothesis through observedPrefixValue of the extension.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    s :
    ℓ :
    n :
    ℕ
    hn :
    n ≤ M.observed.card
    i :
    Fin n
    M.observedPrefixValue hn (M.partialEvalMap n hn s ℓ).2 i
    = M.evalObservedAux s ℓ i.val (lt_of_lt_of_le i.isLt hn) | 0, _, i => elim0 i | k
    + 1, hn, i
    => by refine Fin.lastCases ?_ ?_ i · change M.observedPrefixValue hn ((M.partialEvalMap k (le_of_succ_le hn) s ℓ).2, M.stepFun hn (s, M.partialEvalMap k (le_of_succ_le hn) s ℓ)) (last k) = _ rw [observedPrefixValue_succ_last] unfold stepFun rw [evalObservedAux_eq] congr 1 funext w have hfix_disj_unobs : ∀ u : SWIGNode N, u ∈ M.unobserved → u ∉ M.fixed
    Proof (Lean source)
    theorem partialEvalMap_observedPrefixValue (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) : ∀ (n : ℕ) (hn : n ≤ M.observed.card) (i : Fin n), M.observedPrefixValue hn (M.partialEvalMap n hn s ℓ).2 i = M.evalObservedAux s ℓ i.val (lt_of_lt_of_le i.isLt hn) | 0, _, i => elim0 i | k + 1, hn, i => by refine Fin.lastCases ?_ ?_ i · -- Last slot: i = last k. LHS reduces to stepFun; RHS is evalObservedAux at k. -- Step 1: unfold `(partialEvalMap (k+1) hn s ℓ).2` as a pair. change M.observedPrefixValue hn ((M.partialEvalMap k (le_of_succ_le hn) s ℓ).2, M.stepFun hn (s, M.partialEvalMap k (le_of_succ_le hn) s ℓ)) (last k) = _ -- Step 2: pick the `y` slot. rw [observedPrefixValue_succ_last] -- Step 3: unfold `stepFun` and `evalObservedAux_eq` on the RHS. unfold stepFun rw [evalObservedAux_eq] -- Step 4: the `structFun` head matches (both at `⟨k, hn⟩`); reduce to parent-arg eq. congr 1 funext w -- Step 5: split by the parent class (fixed / unobserved / observed) on both sides. have hfix_disj_unobs : ∀ u : SWIGNode N, u ∈ M.unobserved → u ∉ M.fixed := by intro u hu hf obtain ⟨m, hm⟩ := M.fixed_is_fixed u hf obtain ⟨j, hj⟩ := M.unobserved_is_random u hu rw [hm] at hj; cases hj simp only [parentValuesFromPrefix] by_cases hfix : w.val ∈ M.fixed · -- Fixed parent branch. simp only [dif_pos hfix] have huo : w.val ∉ M.unobserved := fun hu => hfix_disj_unobs _ hu hfix exact (parentMap_fixed M s ℓ _ _ w hfix).symm · simp only [dif_neg hfix] by_cases hobs : w.val ∈ M.observed · -- Observed parent branch: use IH on smaller prefix index. simp only [dif_pos hobs] have huo : w.val ∉ M.unobserved := not_unobs_of_obs M.toSWIGGraph hobs -- IH at (k, iobs) where iobs points to the parent's observed index. have hedge : M.dag.edge w.val (M.observedAt ⟨k, hn⟩).val := M.dag.mem_parents.mp w.property have hlt : M.observedIndex ⟨w.val, hobs⟩ < (⟨k, hn⟩ : Fin M.observed.card) := M.observed_parent_index_lt hn hedge hobs have hlt' : (M.observedIndex ⟨w.val, hobs⟩).val < k := hlt have ih := partialEvalMap_observedPrefixValue M s ℓ k (le_of_succ_le hn) ⟨(M.observedIndex ⟨w.val, hobs⟩).val, hlt'⟩ -- Rewrite `observedPrefixValue` via IH, so both sides become -- `castEq ▸ evalObservedAux s ℓ idx _` for the same equality. rw [ih] refine Eq.trans ?_ (parentMap_observed M s ℓ _ _ w hobs).symm -- Both sides transport the evaluator result along the same node -- equality. have hNode : (M.observedAt (M.observedIndex ⟨w.val, hobs⟩)).val = w.val := M.observedAt_observedIndex ⟨w.val, hobs⟩ simp [eqRec_eq_cast] · -- Unobserved parent branch. have hunobs : w.val ∈ M.unobserved := by have hedge : M.dag.edge w.val (M.observedAt ⟨k, hn⟩).val := M.dag.mem_parents.mp w.property have hclass : w.val ∈ M.fixed ∪ M.observed ∪ M.unobserved := (M.dag_edges_classified _ _ hedge).1 rcases Finset.mem_union.mp hclass with h | h · rcases Finset.mem_union.mp h with h | h · exact (hfix h).elim · exact (hobs h).elim · exact h simp only [dif_neg hobs] -- LHS: `sℓξ.2.1 ⟨w.val, hunobs⟩` where `sℓξ = (s, partialEvalMap k _ s ℓ)`, -- so `.2.1 = (partialEvalMap k _ s ℓ).1 = ℓ`. rw [partialEvalMap_latent] exact (parentMap_unobserved M s ℓ _ _ w hunobs).symm · -- Earlier slots: i = j.castSucc. Apply IH on (k, j). intro j have ih := partialEvalMap_observedPrefixValue M s ℓ k (le_of_succ_le hn) j -- Unfold `(partialEvalMap (k+1) hn s ℓ).2` as the pair `(prev.2, stepFun _)`, -- then use `observedPrefixValue_succ_castSucc` to recurse into `prev.2`. change M.observedPrefixValue hn ((M.partialEvalMap k (le_of_succ_le hn) s ℓ).2, M.stepFun hn (s, M.partialEvalMap k (le_of_succ_le hn) s ℓ)) j.castSucc = _ rw [observedPrefixValue_succ_castSucc] simpa using ih
    Causalean.SCM.partialEvalMap_observedPrefixValue · Causalean/SCM/Factored/EvalMapCorrespond.lean:210
Factorization 3 core · 2 supporting This file assembles the prefix-kernel correspondence into the final factorization theorem for the joint kernel of a structural causal model. ★ jointKernel_factored★ jointKernel_eq_factored_kernel

Factorization of the Joint Kernel

This file assembles the prefix-kernel correspondence into the final factorization theorem for the joint kernel of a structural causal model. It identifies the full prefix state with all random coordinates, proves the reindexing map is measurable, relates the full deterministic prefix map to evalMap, and states both pointwise and kernel-level factorization theorems.

def orderedLatentPrefixFullToRandom reviewed
Causalean.SCM

For a finite collection of nodes with a measurable outcome space for each node and a structural causal model, the map from a completed latent-and-observed prefix state to an assignment of all random nodes assigns each observed node its completed prefix value and each unobserved node its latent value.

Definition (Lean source)
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
orderedLatentPrefixFullToRandom M :
M.OrderedLatentPrefixValues M.observed.card (le_refl _) → M.RandomValues
fun p v
=> by by_cases hobs : v.val ∈ M.observed · have hEq : swigΩ Ω (M.observedAt (M.observedIndex ⟨v.val, hobs⟩)).val = swigΩ Ω v.val := by simpa using congrArg (swigΩ Ω) (M.observedAt_observedIndex ⟨v.val, hobs⟩) exact cast hEq (M.observedPrefixValue (le_refl _) p.2 (M.observedIndex ⟨v.val, hobs⟩)) · have hunobs : v.val ∈ M.unobserved := by rcases Finset.mem_union.mp v.property with hobs' | hunobs · exact False.elim (hobs hobs') · exact hunobs exact p.1 ⟨v.val, hunobs⟩
theorem jointKernel_factored reviewed
Causalean.SCM

Main factorization theorem (pointwise). For a structural causal model M, at each fixed assignment s, the joint kernel equals the pushforward of the full-length prefix kernel through the reindexing map identifying the full prefix state with the random coordinates.

Formal statement
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
s :
M.jointKernel s
= ((M.jointKernelPrefix M.observed.card (le_refl _)) s).map M.orderedLatentPrefixFullToRandom
Proof (Lean source)
theorem jointKernel_factored (M : SCM N Ω) (s : FixedValues M) : M.jointKernel s = ((M.jointKernelPrefix M.observed.card (le_refl _)) s).map M.orderedLatentPrefixFullToRandom := by -- Step 1: unfold `jointKernel` at `s`. rw [M.jointKernel_apply_eq s] -- Step 2: rewrite `evalMap s` as `orderedLatentPrefixFullToRandom ∘ partialEvalMap _ _ s`. have hfun : (fun ℓ => M.evalMap s ℓ) = M.orderedLatentPrefixFullToRandom ∘ (fun ℓ => M.partialEvalMap M.observed.card (le_refl _) s ℓ) := by funext ℓ exact (M.partialEvalMap_full_eq s ℓ).symm rw [hfun] -- Step 3: use `Measure.map_map` to commute `.map` with composition. have hmeas_reindex := M.measurable_orderedLatentPrefixFullToRandom have hmeas_partial : Measurable (fun ℓ : LatentValues M => M.partialEvalMap M.observed.card (le_refl _) s ℓ) := by have := M.measurable_partialEvalMap M.observed.card (le_refl _) exact this.comp (prodMk measurable_const measurable_id) rw [← MeasureTheory.Measure.map_map hmeas_reindex hmeas_partial] -- Step 4: rewrite the inner `.map` using `jointKernelPrefix_apply_eq`. rw [← M.jointKernelPrefix_apply_eq s M.observed.card (le_refl _)]
theorem jointKernel_eq_factored_kernel reviewed
Causalean.SCM

Kernel-level factorization. For a structural causal model M, its joint kernel equals the prefix kernel at full length, pushed through the reindexing map identifying the full prefix state with the random coordinates. Follows from the pointwise form via kernel extensionality.

Formal statement
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
M.jointKernel
= (M.jointKernelPrefix M.observed.card (le_refl _)).map M.orderedLatentPrefixFullToRandom
Proof (Lean source)
theorem jointKernel_eq_factored_kernel (M : SCM N Ω) : M.jointKernel = (M.jointKernelPrefix M.observed.card (le_refl _)).map M.orderedLatentPrefixFullToRandom := by refine ProbabilityTheory.Kernel.ext fun s => ?_ rw [ProbabilityTheory.Kernel.map_apply _ M.measurable_orderedLatentPrefixFullToRandom] exact M.jointKernel_factored s
2 supporting declarations (lemmas, instances)
  • measurable_orderedLatentPrefixFullToRandom theorem — orderedLatentPrefixFullToRandom is measurable. Case-split mirrors the definition; the observed branch composes observedPrefixValue with a cast.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    Measurable M.orderedLatentPrefixFullToRandom
    Proof (Lean source)
    @[fun_prop] theorem measurable_orderedLatentPrefixFullToRandom (M : SCM N Ω) : Measurable M.orderedLatentPrefixFullToRandom := by classical refine measurable_pi_lambda _ ?_ intro ⟨n, hn⟩ simp only [orderedLatentPrefixFullToRandom] by_cases hobs : n ∈ M.observed · simp [hobs] have hNode : (M.observedAt (M.observedIndex ⟨n, hobs⟩)).val = n := M.observedAt_observedIndex ⟨n, hobs⟩ have hmeas : Measurable fun p : M.OrderedLatentPrefixValues M.observed.card (le_refl _) => M.observedPrefixValue (le_refl _) p.2 (M.observedIndex ⟨n, hobs⟩) := (M.measurable_observedPrefixValue (le_refl _) (M.observedIndex ⟨n, hobs⟩)).comp (measurable_snd : Measurable snd) exact (measurable_cast_family hNode).comp hmeas · have hunobs : n ∈ M.unobserved := by rcases Finset.mem_union.mp hn with hobs' | hunobs · exact False.elim (hobs hobs') · exact hunobs simp [hobs] exact ((measurable_pi_apply (⟨n, hunobs⟩ : {x // x ∈ M.unobserved})).comp (measurable_fst : Measurable fst))
    Causalean.SCM.measurable_orderedLatentPrefixFullToRandom · Causalean/SCM/Factored/Factorization.lean:90
  • partialEvalMap_full_eq theorem — Bridge lemma: reindexing the deterministic full-prefix value built from partialEvalMap at length observed.card yields exactly evalMap s ℓ.
    N :
    Type uN
    N → Type uΩ
    shared
    M :
    SCM N Ω
    s :
    ℓ :
    M.orderedLatentPrefixFullToRandom (M.partialEvalMap M.observed.card (le_refl _) s ℓ)
    = M.evalMap s ℓ
    Proof (Lean source)
    theorem partialEvalMap_full_eq (M : SCM N Ω) (s : FixedValues M) (ℓ : LatentValues M) : M.orderedLatentPrefixFullToRandom (M.partialEvalMap M.observed.card (le_refl _) s ℓ) = M.evalMap s ℓ := by funext v unfold orderedLatentPrefixFullToRandom by_cases hobs : v.val ∈ M.observed · -- Observed branch: both sides are (cast) of `evalObservedAux` at -- `observedIndex v`. simp only [hobs, dif_pos] -- LHS: cast hEq (observedPrefixValue ((partialEvalMap ...).2) (observedIndex v)) rw [M.partialEvalMap_observedPrefixValue s ℓ M.observed.card (le_refl _) (M.observedIndex ⟨v.val, hobs⟩)] -- RHS: evalMap_observed form rw [M.evalMap_observed s ℓ v hobs] -- Both sides transport the same `evalObservedAux` along the identity -- `(M.observedAt (observedIndex v)).val = v.val`. LHS uses `cast -- (congrArg (swigΩ Ω) h)`, RHS uses `h ▸ _`; they agree by the generic -- identity `cast (congrArg f h) x = h ▸ x` (both `Eq.mpr`/`Eq.mp` when -- `h` is used as a motive transport). -/ have hNode : (M.observedAt (M.observedIndex ⟨v.val, hobs⟩)).val = v.val := M.observedAt_observedIndex ⟨v.val, hobs⟩ -- Abstract the transported value as `aux` with the exact shape expected -- on the RHS: the `▸` motive transports along `hNode : (observedAt idx).val = v.val`, -- so `aux` must have type `swigΩ Ω (observedAt (observedIndex v)).val`. let aux0 : swigΩ Ω (M.observedAt (M.observedIndex ⟨v.val, hobs⟩)).val := M.evalObservedAux s ℓ (M.observedIndex ⟨v.val, hobs⟩).val (lt_of_lt_of_le (M.observedIndex ⟨v.val, hobs⟩).isLt (le_refl _)) -- Goal: cast hEq aux0 = hNode ▸ aux0; both transports use the same node -- equality, so they're equal via `eqRec_eq_cast`. change cast _ aux0 = hNode ▸ aux0 exact (eqRec_eq_cast (motive := fun x _ => swigΩ Ω x) aux0 hNode).symm · -- Unobserved branch: LHS reads `p.1 ⟨v.val, huo⟩ = ℓ ⟨v.val, huo⟩` by -- `partialEvalMap_latent`; RHS is `ℓ ⟨v.val, huo⟩` by `evalMap_unobserved`. simp only [hobs, dif_neg, not_false_eq_true] have hunobs : v.val ∈ M.unobserved := by rcases Finset.mem_union.mp v.property with hobs' | hunobs · exact False.elim (hobs hobs') · exact hunobs rw [M.evalMap_unobserved s ℓ v hunobs] -- LHS: `(partialEvalMap M.observed.card _ s ℓ).1 ⟨v.val, hunobs⟩` -- By `partialEvalMap_latent`, `.1 = ℓ`. have := M.partialEvalMap_latent s ℓ M.observed.card (le_refl _) rw [this]
    Causalean.SCM.partialEvalMap_full_eq · Causalean/SCM/Factored/Factorization.lean:122
Obs­Chain­Kernel 9 core · 21 supporting The observational kernel factors along the topological order of observed nodes as the iterated product of one-node conditional kernels given the full observed history. ★ obsKernel_eq_qFactorProduct

Observational Chain-Rule Kernel

The observational kernel factors along the topological order of observed nodes as the iterated product of one-node conditional kernels given the full observed history. This is the ordinary chain rule for kernels, formulated with Mathlib's continuous-safe condKernel.

This file builds the prefix node sets, the one-step observational conditional kernel, the recursive chain kernel, and the full-length product kernel qFactorProduct. Despite its historical name, qFactorProduct is the ordinary per-node observational chain-rule product, not a c-component factor product. The final equality with obsKernel is proved by standard disintegration induction.

def observedPredecessors reviewed
Causalean.Graph.SWIGGraph

For a finite collection of distinguishable base-variable labels, a SWIG graph, and a graph node, the observed-predecessor set consists exactly of the observed nodes that occur strictly before that node in the graph's topological order.

Definition (Lean source)
N :
Type u_1
shared
G :
shared
v :
observedPredecessors G v :
G.observed.filter (fun w => G.dag.topoOrder w < G.dag.topoOrder v)
Causalean.Graph.SWIGGraph.observedPredecessors · Causalean/SCM/Factored/ObsChainKernel.lean:44 · uses SWIGGraph , SWIGNode
def prefixNodes reviewed
Causalean.SCM

For a finite collection of distinguishable base-variable labels with a measurable value space attached to each label, a structural causal model, and a nonnegative integer, the prefix node set consists of precisely the first nn observed nodes in its canonical topological order; if nn is at least the number of observed nodes, it is the full observed-node set.

Definition (Lean source)
N :
Type u_1
N → Type u_2
shared
M :
SCM N Ω
n :
ℕ
prefixNodes M n :
M.observed.filter (fun v => if h : v ∈ M.observed then (M.observedIndex ⟨v, h⟩).val < n else False)
def obsStepCondKernel reviewed
Causalean.SCM

For a structural causal model, an index strictly below its number of observed nodes, a standard Borel and nonempty value space for the observed node at that index, and a countably generated conditioning σ-algebra for the fixed values and preceding observed values, the one-step observational conditional kernel gives the conditional distribution of that node's value given the fixed values and all earlier observed values.

Definition (Lean source)
N :
Type u_1
N → Type u_2
shared
M :
SCM N Ω
n :
ℕ
hn :
n < M.observed.card
StandardBorelSpace (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
Nonempty (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes n) (swigΩ Ω))
obsStepCondKernel M hn :
Kernel (M.FixedValues × ValuesOn (M.prefixNodes n) (swigΩ Ω)) (swigΩ Ω (M.observedAt ⟨n, hn⟩).val)
(M.obsCondKernel ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (M.prefixNodes n) (by intro v hv have hv_eq : v = (M.observedAt ⟨n, hn⟩).val := by simpa using hv simp [hv_eq, (M.observedAt ⟨n, hn⟩).property]) (M.prefixNodes_subset_observed n)).map (singletonValue (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val))
def emptyPrefixValues reviewed
Causalean.SCM

For a structural causal model, the empty-prefix assignment is the unique assignment of values to its empty initial observed-node set.

Definition (Lean source)
N :
Type u_1
N → Type u_2
shared
M :
SCM N Ω
emptyPrefixValues M :
ValuesOn (M.prefixNodes 0) (swigΩ Ω)
fun ⟨v, hv⟩
=> by have : v ∈ (∅ : Finset (SWIGNode N)) := by simp [M.prefixNodes_zero] at hv simp at this
def obsChainKernelZero reviewed
Causalean.SCM

For a structural causal model, the zero-step observational chain kernel assigns, at every fixed-value setting, unit probability to the unique assignment on the empty observed prefix.

Definition (Lean source)
N :
Type u_1
N → Type u_2
shared
M :
SCM N Ω
obsChainKernelZero M :
Kernel M.FixedValues (ValuesOn (M.prefixNodes 0) (swigΩ Ω))
const _ (dirac M.emptyPrefixValues)
def extendObsPrefix reviewed
Causalean.SCM

For a structural causal model and an index strictly below its number of observed nodes, the extended prefix assignment maps an assignment on the first nn observed nodes together with a value for the next node to the assignment on the first n+1n+1 observed nodes that retains the prefix values and appends that value.

Definition (Lean source)
N :
Type u_1
N → Type u_2
shared
M :
SCM N Ω
n :
ℕ
hn :
n < M.observed.card
extendObsPrefix M hn :
ValuesOn (M.prefixNodes n) (swigΩ Ω) × swigΩ Ω (M.observedAt ⟨n, hn⟩).val → ValuesOn (M.prefixNodes (n + 1)) (swigΩ Ω)
fun p
=> (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hn).symm) (valuesUnionMk p.1 (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val) p.2))
def obsChainKernel reviewed
Causalean.SCM

For a structural causal model, standard Borel and nonempty value spaces for every observed node, and countably generated conditioning σ-algebras for every observed prefix, the observational chain kernel assigns to every nonnegative integer not exceeding the number of observed nodes the kernel obtained at zero by the point mass on the empty prefix and at each positive index by composing the preceding chain kernel with the next one-node conditional kernel and extending the prefix.

Definition (Lean source)
N :
Type u_1
N → Type u_2
shared
M :
SCM N Ω
∀ (k : ℕ) (hk : k < M.observed.card),
StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
∀ (k : ℕ) (hk : k < M.observed.card),
Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
∀ k : Fin M.observed.card,
CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes k.val) (swigΩ Ω))
n :
ℕ
hn :
n ≤ M.observed.card
obsChainKernel M n hn :
Kernel M.FixedValues (ValuesOn (M.prefixNodes n) (swigΩ Ω))
clause 1
| 0, _ => M.obsChainKernelZero
clause 2
| k + 1, hn
=> by have hk : k < M.observed.card := Nat.lt_of_succ_le hn letI : StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω)) := inferInstance letI : Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω)) := inferInstance letI : CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes k) (swigΩ Ω)) := (inferInstance : CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes (⟨k, hk⟩ : Fin M.observed.card).val) (swigΩ Ω))) exact ((M.obsChainKernel k (le_of_succ_le hn)) ⊗ₖ (M.obsStepCondKernel hk)).map (M.extendObsPrefix hk)
def qFactorProduct reviewed
Causalean.SCM

For a structural causal model, standard Borel and nonempty value spaces for every observed node, and countably generated conditioning σ-algebras for every observed prefix, the full observational chain-rule product is the full-length observational chain kernel transported from the complete prefix to the observed-value space. Despite its historical name, it is not a c-component factor product.

Definition (Lean source)
N :
Type u_1
N → Type u_2
shared
M :
SCM N Ω
∀ (k : ℕ) (hk : k < M.observed.card),
StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
∀ (k : ℕ) (hk : k < M.observed.card),
Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
∀ k : Fin M.observed.card,
CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes k.val) (swigΩ Ω))
qFactorProduct M :
Kernel M.FixedValues M.ObservedValues
(M.obsChainKernel M.observed.card (le_refl _)).map (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _)))
theorem obsKernel_eq_qFactorProduct reviewed
Causalean.SCM

For a structural causal model M, at a fixed assignment s, its observational kernel equals the full chain-rule product of one-node conditional kernels along the observed topological order.

Formal statement
N :
Type u_1
N → Type u_2
shared
M :
SCM N Ω
s :
M.FixedValues
∀ (k : ℕ) (hk : k < M.observed.card),
StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
∀ (k : ℕ) (hk : k < M.observed.card),
Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
∀ k : Fin M.observed.card,
CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes k.val) (swigΩ Ω))
M.obsKernel s = M.qFactorProduct s
Proof (Lean source)
theorem obsKernel_eq_qFactorProduct (M : SCM N Ω) (s : M.FixedValues) [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : Fin M.observed.card, CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes k.val) (swigΩ Ω))] : M.obsKernel s = M.qFactorProduct s := by unfold qFactorProduct rw [ProbabilityTheory.Kernel.map_apply _ (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))).measurable] have hprefix := M.obsKernel_map_prefixNodes s M.observed.card (le_refl _) rw [← hprefix] rw [MeasureTheory.Measure.map_map (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))).measurable (measurable_valuesProjection (M.prefixNodes_subset_observed M.observed.card))] have hcomp : (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_card M.observed.card (le_refl _))) ∘ valuesProjection (M.prefixNodes_subset_observed M.observed.card) = (id : M.ObservedValues → M.ObservedValues) := by funext ω rfl rw [hcomp, MeasureTheory.Measure.map_id]
21 supporting declarations (lemmas, instances)
  • observedPredecessors_subset_observed lemma — Observed predecessors are observed by construction.
    N :
    Type u_1
    shared
    G :
    shared
    v :
    G.observedPredecessors v ⊆ G.observed
    Proof (Lean source)
    lemma observedPredecessors_subset_observed (v : SWIGNode N) : G.observedPredecessors v ⊆ G.observed := by intro w hw exact (Finset.mem_filter.mp hw).1
    Causalean.Graph.SWIGGraph.observedPredecessors_subset_observed · Causalean/SCM/Factored/ObsChainKernel.lean:50
  • mem_prefixNodes_iff lemma — Membership in prefixNodes is exactly having observed index below n.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    v :
    v ∈ M.prefixNodes n ↔ ∃ h : v ∈ M.observed, (M.observedIndex ⟨v, h⟩).val < n
    Proof (Lean source)
    lemma mem_prefixNodes_iff (M : SCM N Ω) (n : ℕ) (v : SWIGNode N) : v ∈ M.prefixNodes n ↔ ∃ h : v ∈ M.observed, (M.observedIndex ⟨v, h⟩).val < n := by unfold prefixNodes constructor · intro hv rcases Finset.mem_filter.mp hv with ⟨hobs, hltif⟩ exact ⟨hobs, by simpa [hobs] using hltif⟩ · rintro ⟨hobs, hlt⟩ exact Finset.mem_filter.mpr ⟨hobs, by simpa [hobs] using hlt⟩
    Causalean.SCM.mem_prefixNodes_iff · Causalean/SCM/Factored/ObsChainKernel.lean:74
  • prefixNodes_subset_observed lemma — Prefix nodes are observed nodes.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    M.prefixNodes n ⊆ M.observed
    Proof (Lean source)
    lemma prefixNodes_subset_observed (M : SCM N Ω) (n : ℕ) : M.prefixNodes n ⊆ M.observed := by intro v hv exact (M.mem_prefixNodes_iff n v).mp hv |>.1
    Causalean.SCM.prefixNodes_subset_observed · Causalean/SCM/Factored/ObsChainKernel.lean:86
  • prefixNodes_zero lemma — The empty prefix has no nodes.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    M.prefixNodes 0 = ∅
    Proof (Lean source)
    lemma prefixNodes_zero (M : SCM N Ω) : M.prefixNodes 0 = ∅ := by ext v constructor · intro hv rcases (M.mem_prefixNodes_iff 0 v).mp hv with ⟨_, hlt⟩ omega · simp
    Causalean.SCM.prefixNodes_zero · Causalean/SCM/Factored/ObsChainKernel.lean:92
  • observedAt_mem_prefixNodes_iff lemma — An observed node at index i belongs to the first n nodes iff i < n.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    i :
    Fin M.observed.card
    (M.observedAt i).val ∈ M.prefixNodes n ↔ i.val < n
    Proof (Lean source)
    lemma observedAt_mem_prefixNodes_iff (M : SCM N Ω) (n : ℕ) (i : Fin M.observed.card) : (M.observedAt i).val ∈ M.prefixNodes n ↔ i.val < n := by rw [M.mem_prefixNodes_iff] constructor · rintro ⟨hobs, hlt⟩ have hidx : M.observedIndex ⟨(M.observedAt i).val, hobs⟩ = i := by have hsub : (⟨(M.observedAt i).val, hobs⟩ : {v // v ∈ M.observed}) = M.observedAt i := Subtype.ext rfl rw [hsub] exact M.observedIndex_observedAt i rwa [hidx] at hlt · intro hlt exact ⟨(M.observedAt i).property, by simpa [M.observedIndex_observedAt i] using hlt⟩
    Causalean.SCM.observedAt_mem_prefixNodes_iff · Causalean/SCM/Factored/ObsChainKernel.lean:102
  • prefixNodes_card lemma — Every prefix at least as long as the observed-node list is the full observed node set.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    M.observed.card ≤ n
    M.prefixNodes n = M.observed
    Proof (Lean source)
    lemma prefixNodes_card (M : SCM N Ω) (n : ℕ) (hn : M.observed.card ≤ n) : M.prefixNodes n = M.observed := by ext v constructor · exact fun hv => M.prefixNodes_subset_observed _ hv · intro hv exact (M.mem_prefixNodes_iff n v).mpr ⟨hv, lt_of_lt_of_le (M.observedIndex ⟨v, hv⟩).isLt hn⟩
    Causalean.SCM.prefixNodes_card · Causalean/SCM/Factored/ObsChainKernel.lean:120
  • observedAt_not_mem_prefixNodes lemma — The next observed node is not in the previous prefix.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n < M.observed.card
    (M.observedAt ⟨n, hn⟩).val ∉ M.prefixNodes n
    Proof (Lean source)
    lemma observedAt_not_mem_prefixNodes (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) : (M.observedAt ⟨n, hn⟩).val ∉ M.prefixNodes n := by rw [M.observedAt_mem_prefixNodes_iff n ⟨n, hn⟩] exact Nat.lt_irrefl n
    Causalean.SCM.observedAt_not_mem_prefixNodes · Causalean/SCM/Factored/ObsChainKernel.lean:131
  • prefixNodes_succ lemma — The prefix successor is obtained by adjoining the next observed node.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n < M.observed.card
    M.prefixNodes (n + 1) = M.prefixNodes n ∪ {(M.observedAt ⟨n, hn⟩).val}
    Proof (Lean source)
    lemma prefixNodes_succ (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) : M.prefixNodes (n + 1) = M.prefixNodes n ∪ {(M.observedAt ⟨n, hn⟩).val} := by ext v constructor · intro hv rcases (M.mem_prefixNodes_iff (n + 1) v).mp hv with ⟨hobs, hlt⟩ by_cases hlt_n : (M.observedIndex ⟨v, hobs⟩).val < n · exact mem_union_left _ ((M.mem_prefixNodes_iff n v).mpr ⟨hobs, hlt_n⟩) · have hidx_val : (M.observedIndex ⟨v, hobs⟩).val = n := by omega have hidx : M.observedIndex ⟨v, hobs⟩ = ⟨n, hn⟩ := Fin.ext hidx_val have hv_eq : v = (M.observedAt ⟨n, hn⟩).val := by have hround := M.observedAt_observedIndex ⟨v, hobs⟩ rw [hidx] at hround exact hround.symm exact mem_union_right _ (by simp [hv_eq]) · intro hv rcases Finset.mem_union.mp hv with hvpre | hvlast · rcases (M.mem_prefixNodes_iff n v).mp hvpre with ⟨hobs, hlt⟩ exact (M.mem_prefixNodes_iff (n + 1) v).mpr ⟨hobs, by omega⟩ · have hv_eq : v = (M.observedAt ⟨n, hn⟩).val := by simpa using hvlast subst hv_eq rw [M.observedAt_mem_prefixNodes_iff (n + 1) ⟨n, hn⟩] exact lt_succ_self n
    Causalean.SCM.prefixNodes_succ · Causalean/SCM/Factored/ObsChainKernel.lean:138
  • prefixNodes_disjoint_singleton_next lemma — The previous prefix is disjoint from the singleton next node.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n < M.observed.card
    Disjoint (M.prefixNodes n) ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N))
    Proof (Lean source)
    lemma prefixNodes_disjoint_singleton_next (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) : Disjoint (M.prefixNodes n) ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) := by rw [Finset.disjoint_singleton_right] exact M.observedAt_not_mem_prefixNodes hn
    Causalean.SCM.prefixNodes_disjoint_singleton_next · Causalean/SCM/Factored/ObsChainKernel.lean:165
  • observedPredecessors_observedAt lemma — For the node at index n, Tian's full-history predecessor set is exactly the first n observed nodes.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n < M.observed.card
    M.toSWIGGraph.observedPredecessors (M.observedAt ⟨n, hn⟩).val = M.prefixNodes n
    Proof (Lean source)
    lemma observedPredecessors_observedAt (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) : M.toSWIGGraph.observedPredecessors (M.observedAt ⟨n, hn⟩).val = M.prefixNodes n := by classical letI := M.topoLinearOrder ext w constructor · intro hw rcases Finset.mem_filter.mp hw with ⟨hwobs, htopo⟩ have hw_lt : (⟨w, hwobs⟩ : {v // v ∈ M.observed}) < M.observedAt ⟨n, hn⟩ := by change w < (M.observedAt ⟨n, hn⟩).val exact htopo have hidx : M.observedIndex ⟨w, hwobs⟩ < M.observedIndex (M.observedAt ⟨n, hn⟩) := (M.observed.orderIsoOfFin rfl).symm.strictMono hw_lt rw [M.observedIndex_observedAt] at hidx exact (M.mem_prefixNodes_iff n w).mpr ⟨hwobs, hidx⟩ · intro hw rcases (M.mem_prefixNodes_iff n w).mp hw with ⟨hwobs, hidx_lt⟩ refine Finset.mem_filter.mpr ⟨hwobs, ?_⟩ have hfin : M.observedIndex ⟨w, hwobs⟩ < ⟨n, hn⟩ := by exact Fin.mk_lt_mk.mpr hidx_lt have hw_lt : (⟨w, hwobs⟩ : {v // v ∈ M.observed}) < M.observedAt ⟨n, hn⟩ := by have hmono := (M.observed.orderIsoOfFin rfl).strictMono (show (M.observed.orderIsoOfFin rfl).symm ⟨w, hwobs⟩ < (⟨n, hn⟩ : Fin M.observed.card) from hfin) rw [OrderIso.apply_symm_apply] at hmono exact hmono change w < (M.observedAt ⟨n, hn⟩).val at hw_lt exact hw_lt
    Causalean.SCM.observedPredecessors_observedAt · Causalean/SCM/Factored/ObsChainKernel.lean:172
  • isMarkov_obsStepCondKernel instance — For a finite node population with measurable value spaces, a structural causal model, an index strictly below its number of observed nodes, a standard Borel and nonempty value space for the observed node at that index, and a countably generated conditioning σ-algebra for the fixed values and preceding observed values, the Markov-kernel structure for the one-step observational conditional kernel asserts that this conditional distribution is a Markov kernel.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n < M.observed.card
    StandardBorelSpace (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
    Nonempty (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
    CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes n) (swigΩ Ω))
    isMarkov_obsStepCondKernel M hn :
    IsMarkovKernel (M.obsStepCondKernel hn)
    by have hY : ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) ⊆ M.observed := by intro v hv have hv_eq : v
    = (M.observedAt ⟨n, hn⟩).val := by simpa using hv simp [hv_eq, (M.observedAt ⟨n, hn⟩).property] have hCC : M.prefixNodes n ⊆ M.observed := M.prefixNodes_subset_observed n haveI : IsMarkovKernel (M.obsCondPairKernel ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (M.prefixNodes n) hY hCC) := by unfold SCM.obsCondPairKernel exact ProbabilityTheory.Kernel.IsMarkovKernel.map _ (prodMk (measurable_valuesProjection hCC) (measurable_valuesProjection hY)) haveI : IsFiniteKernel (M.obsCondPairKernel ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (M.prefixNodes n) hY hCC) := by infer_instance unfold obsStepCondKernel SCM.obsCondKernel exact ProbabilityTheory.Kernel.IsMarkovKernel.map _ (measurable_singletonValue (α := swigΩ Ω))
    Causalean.SCM.isMarkov_obsStepCondKernel · Causalean/SCM/Factored/ObsChainKernel.lean:236
  • obsStepCondKernel_map_singletonValues lemma — Mapping the scalar step kernel back to the singleton tuple recovers the conditional kernel it was built from.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n < M.observed.card
    StandardBorelSpace (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
    Nonempty (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
    CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes n) (swigΩ Ω))
    (M.obsStepCondKernel hn).map (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val))
    = M.obsCondKernel ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (M.prefixNodes n) (by intro v hv have hv_eq : v = (M.observedAt ⟨n, hn⟩).val := by simpa using hv simp [hv_eq, (M.observedAt ⟨n, hn⟩).property]) (M.prefixNodes_subset_observed n)
    Proof (Lean source)
    lemma obsStepCondKernel_map_singletonValues (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) [StandardBorelSpace (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [Nonempty (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes n) (swigΩ Ω))] : (M.obsStepCondKernel hn).map (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val)) = M.obsCondKernel ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (M.prefixNodes n) (by intro v hv have hv_eq : v = (M.observedAt ⟨n, hn⟩).val := by simpa using hv simp [hv_eq, (M.observedAt ⟨n, hn⟩).property]) (M.prefixNodes_subset_observed n) := by refine ProbabilityTheory.Kernel.ext fun sc => ?_ unfold obsStepCondKernel rw [ProbabilityTheory.Kernel.map_apply _ (measurable_singletonValues (α := swigΩ Ω))] rw [ProbabilityTheory.Kernel.map_apply _ (measurable_singletonValue (α := swigΩ Ω))] rw [MeasureTheory.Measure.map_map (measurable_singletonValues (α := swigΩ Ω)) (measurable_singletonValue (α := swigΩ Ω))] have hcomp : (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val) ∘ singletonValue (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val)) = (id : ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω) → ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω)) := by funext x exact singletonValues_singletonValue (α := swigΩ Ω) x rw [hcomp, MeasureTheory.Measure.map_id]
    Causalean.SCM.obsStepCondKernel_map_singletonValues · Causalean/SCM/Factored/ObsChainKernel.lean:273
  • obsStepCondKernel_sectR_map_singletonValues lemma — Slice form of obsStepCondKernel_map_singletonValues.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n < M.observed.card
    StandardBorelSpace (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
    Nonempty (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
    CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes n) (swigΩ Ω))
    s :
    M.FixedValues
    ((M.obsStepCondKernel hn).sectR s).map (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val))
    = (M.obsCondKernel ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (M.prefixNodes n) (by intro v hv have hv_eq : v = (M.observedAt ⟨n, hn⟩).val := by simpa using hv simp [hv_eq, (M.observedAt ⟨n, hn⟩).property]) (M.prefixNodes_subset_observed n)).sectR s
    Proof (Lean source)
    lemma obsStepCondKernel_sectR_map_singletonValues (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) [StandardBorelSpace (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [Nonempty (ValuesOn ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes n) (swigΩ Ω))] (s : M.FixedValues) : ((M.obsStepCondKernel hn).sectR s).map (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val)) = (M.obsCondKernel ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (M.prefixNodes n) (by intro v hv have hv_eq : v = (M.observedAt ⟨n, hn⟩).val := by simpa using hv simp [hv_eq, (M.observedAt ⟨n, hn⟩).property]) (M.prefixNodes_subset_observed n)).sectR s := by refine ProbabilityTheory.Kernel.ext fun c => ?_ unfold sectR rw [ProbabilityTheory.Kernel.map_apply _ (measurable_singletonValues (α := swigΩ Ω))] rw [ProbabilityTheory.Kernel.comap_apply] rw [ProbabilityTheory.Kernel.comap_apply] have h := congrArg (fun k => k (s, c)) (M.obsStepCondKernel_map_singletonValues hn) change ((M.obsStepCondKernel hn).map (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val))) (s, c) = M.obsCondKernel ({(M.observedAt ⟨n, hn⟩).val} : Finset (SWIGNode N)) (M.prefixNodes n) (by intro v hv have hv_eq : v = (M.observedAt ⟨n, hn⟩).val := by simpa using hv simp [hv_eq, (M.observedAt ⟨n, hn⟩).property]) (M.prefixNodes_subset_observed n) (s, c) at h rw [ProbabilityTheory.Kernel.map_apply _ (measurable_singletonValues (α := swigΩ Ω))] at h exact h
    Causalean.SCM.obsStepCondKernel_sectR_map_singletonValues · Causalean/SCM/Factored/ObsChainKernel.lean:311
  • isMarkov_obsChainKernelZero instance — For a finite node population with measurable value spaces and a structural causal model, the Markov-kernel structure for the zero-step observational chain kernel asserts that the kernel assigning unit probability to the unique empty-prefix assignment is a Markov kernel.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    isMarkov_obsChainKernelZero M :
    IsMarkovKernel M.obsChainKernelZero
    by unfold obsChainKernelZero infer_instance
    Causalean.SCM.isMarkov_obsChainKernelZero · Causalean/SCM/Factored/ObsChainKernel.lean:367
  • measurable_extendObsPrefix lemma — Prefix extension is measurable.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n < M.observed.card
    Measurable (M.extendObsPrefix hn)
    Proof (Lean source)
    @[fun_prop] lemma measurable_extendObsPrefix (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) : Measurable (M.extendObsPrefix hn) := by unfold extendObsPrefix exact (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hn).symm).measurable.comp ((measurable_valuesUnionMk (Ω := swigΩ Ω)).comp (prodMk measurable_fst ((measurable_singletonValues (α := swigΩ Ω)).comp measurable_snd)))
    Causalean.SCM.measurable_extendObsPrefix · Causalean/SCM/Factored/ObsChainKernel.lean:387
  • prefixSucc_projection_pair lemma — Projecting the successor prefix through the union equivalence gives the previous-prefix block and the singleton next-node block.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n < M.observed.card
    (fun ω : M.ObservedValues => valuesUnionEquiv (Ω := Ω) (M.prefixNodes_disjoint_singleton_next hn) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hn)) (valuesProjection (M.prefixNodes_subset_observed (n + 1)) ω)))
    = (fun ω : M.ObservedValues => (valuesProjection (M.prefixNodes_subset_observed n) ω, valuesProjection (by intro w hw have hw_eq : w = (M.observedAt ⟨n, hn⟩).val := by simpa using hw simp [hw_eq, (M.observedAt ⟨n, hn⟩).property]) ω))
    Proof (Lean source)
    lemma prefixSucc_projection_pair (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) : (fun ω : M.ObservedValues => valuesUnionEquiv (Ω := Ω) (M.prefixNodes_disjoint_singleton_next hn) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hn)) (valuesProjection (M.prefixNodes_subset_observed (n + 1)) ω))) = (fun ω : M.ObservedValues => (valuesProjection (M.prefixNodes_subset_observed n) ω, valuesProjection (by intro w hw have hw_eq : w = (M.observedAt ⟨n, hn⟩).val := by simpa using hw simp [hw_eq, (M.observedAt ⟨n, hn⟩).property]) ω)) := by funext ω ext i · rfl · rfl
    Causalean.SCM.prefixSucc_projection_pair · Causalean/SCM/Factored/ObsChainKernel.lean:398
  • valuesUnionEquiv_valuesEquivOfEq_symm_valuesUnionMk lemma — Transporting a combined assignment to an equal index set and back, then splitting the disjoint union, recovers the original pair of assignments.
    N :
    Type u_1
    N → Type u_2
    shared
    hDisj :
    hUnion :
    C = A ∪ B
    p :
    ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω)
    valuesUnionEquiv (Ω := Ω) hDisj ((valuesEquivOfEq (Ω := swigΩ Ω) hUnion) ((valuesEquivOfEq (Ω := swigΩ Ω) hUnion).symm (valuesUnionMk p.1 p.2)))
    = p
    Proof (Lean source)
    lemma valuesUnionEquiv_valuesEquivOfEq_symm_valuesUnionMk {A B C : Finset (SWIGNode N)} (hDisj : Disjoint A B) (hUnion : C = A ∪ B) (p : ValuesOn A (swigΩ Ω) × ValuesOn B (swigΩ Ω)) : valuesUnionEquiv (Ω := Ω) hDisj ((valuesEquivOfEq (Ω := swigΩ Ω) hUnion) ((valuesEquivOfEq (Ω := swigΩ Ω) hUnion).symm (valuesUnionMk p.1 p.2))) = p := by rw [(valuesEquivOfEq (Ω := swigΩ Ω) hUnion).apply_symm_apply] exact (valuesUnionEquiv (Ω := Ω) hDisj).right_inv p
    Causalean.SCM.valuesUnionEquiv_valuesEquivOfEq_symm_valuesUnionMk · Causalean/SCM/Factored/ObsChainKernel.lean:422
  • valuesUnionEquiv_extendObsPrefix lemma — The successor-prefix extension is inverse to the union-equivalence view of the successor prefix.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    n :
    ℕ
    hn :
    n < M.observed.card
    p :
    ValuesOn (M.prefixNodes n) (swigΩ Ω) × swigΩ Ω (M.observedAt ⟨n, hn⟩).val
    valuesUnionEquiv (Ω := Ω) (M.prefixNodes_disjoint_singleton_next hn) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hn)) (M.extendObsPrefix hn p))
    = (p.1, singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val) p.2)
    Proof (Lean source)
    lemma valuesUnionEquiv_extendObsPrefix (M : SCM N Ω) {n : ℕ} (hn : n < M.observed.card) (p : ValuesOn (M.prefixNodes n) (swigΩ Ω) × swigΩ Ω (M.observedAt ⟨n, hn⟩).val) : valuesUnionEquiv (Ω := Ω) (M.prefixNodes_disjoint_singleton_next hn) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hn)) (M.extendObsPrefix hn p)) = (p.1, singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hn⟩).val) p.2) := by unfold extendObsPrefix exact valuesUnionEquiv_valuesEquivOfEq_symm_valuesUnionMk (M.prefixNodes_disjoint_singleton_next hn) (M.prefixNodes_succ hn) (p.1, singletonValues p.2)
    Causalean.SCM.valuesUnionEquiv_extendObsPrefix · Causalean/SCM/Factored/ObsChainKernel.lean:434
  • obsCondPairKernel_apply_eq_compProd lemma — Slice-level disintegration for the pair kernel defining obsCondKernel.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    Y CC :
    hY :
    Y ⊆ M.observed
    hCC :
    CC ⊆ M.observed
    Nonempty (ValuesOn Y (swigΩ Ω))
    s :
    M.FixedValues
    M.obsCondPairKernel Y CC hY hCC s
    = ((M.obsKernel s).map (valuesProjection hCC)) ⊗ₘ (M.obsCondKernel Y CC hY hCC).sectR s
    Proof (Lean source)
    lemma obsCondPairKernel_apply_eq_compProd (M : SCM N Ω) (Y CC : Finset (SWIGNode N)) (hY : Y ⊆ M.observed) (hCC : CC ⊆ M.observed) [StandardBorelSpace (ValuesOn Y (swigΩ Ω))] [Nonempty (ValuesOn Y (swigΩ Ω))] [CountableOrCountablyGenerated M.FixedValues (ValuesOn CC (swigΩ Ω))] (s : M.FixedValues) : M.obsCondPairKernel Y CC hY hCC s = ((M.obsKernel s).map (valuesProjection hCC)) ⊗ₘ (M.obsCondKernel Y CC hY hCC).sectR s := by classical have hπCC : Measurable (valuesProjection (Ω := swigΩ Ω) hCC) := measurable_valuesProjection _ have hπY : Measurable (valuesProjection (Ω := swigΩ Ω) hY) := measurable_valuesProjection _ set κ : Kernel M.FixedValues (ValuesOn CC (swigΩ Ω) × ValuesOn Y (swigΩ Ω)) := M.obsCondPairKernel Y CC hY hCC with hκ_def haveI : IsMarkovKernel κ := by rw [hκ_def] unfold obsCondPairKernel exact ProbabilityTheory.Kernel.IsMarkovKernel.map _ (hπCC.prodMk hπY) have hDisint : κ.fst ⊗ₖ M.obsCondKernel Y CC hY hCC = κ := by change κ.fst ⊗ₖ κ.condKernel = κ exact ProbabilityTheory.Kernel.disintegrate _ _ haveI : IsMarkovKernel (M.obsCondKernel Y CC hY hCC) := by unfold obsCondKernel infer_instance have hAt : (κ.fst s) ⊗ₘ (M.obsCondKernel Y CC hY hCC).sectR s = κ s := by have h := congrArg (fun k => k s) hDisint change (κ.fst ⊗ₖ M.obsCondKernel Y CC hY hCC) s = κ s at h rw [ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR] at h exact h have hFst : κ.fst s = (M.obsKernel s).map (valuesProjection hCC) := by rw [hκ_def] unfold obsCondPairKernel rw [ProbabilityTheory.Kernel.fst_map_prod _ hπY, ProbabilityTheory.Kernel.map_apply _ hπCC] rw [hκ_def, ← hAt, hFst]
    Causalean.SCM.obsCondPairKernel_apply_eq_compProd · Causalean/SCM/Factored/ObsChainKernel.lean:451
  • isMarkov_obsChainKernel instance — For a finite node population with measurable value spaces, a structural causal model, standard Borel and nonempty value spaces for every observed node, and countably generated conditioning σ-algebras for every observed prefix, a nonnegative integer, and proof that this integer does not exceed the number of observed nodes, the Markov-kernel structure for the corresponding observational chain kernel asserts that the sequential conditional distribution of the first specified observed values is a Markov kernel.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    ∀ (k : ℕ) (hk : k < M.observed.card),
    StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
    ∀ (k : ℕ) (hk : k < M.observed.card),
    Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
    ∀ k : Fin M.observed.card,
    CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes k.val) (swigΩ Ω))
    n :
    ℕ
    hn :
    n ≤ M.observed.card
    isMarkov_obsChainKernel M n hn :
    IsMarkovKernel (M.obsChainKernel n hn)
    clause 1
    | 0, _ => M.isMarkov_obsChainKernelZero
    clause 2
    | k + 1, hn
    => by have hk : k < M.observed.card := Nat.lt_of_succ_le hn letI := M.isMarkov_obsChainKernel k (le_of_succ_le hn) letI : StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω)) := inferInstance letI : Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω)) := inferInstance letI : CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes k) (swigΩ Ω)) := (inferInstance : CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes (⟨k, hk⟩ : Fin M.observed.card).val) (swigΩ Ω))) change IsMarkovKernel (((M.obsChainKernel k (le_of_succ_le hn)) ⊗ₖ (M.obsStepCondKernel hk)).map (M.extendObsPrefix hk)) exact ProbabilityTheory.Kernel.IsMarkovKernel.map _ (M.measurable_extendObsPrefix hk)
    Causalean.SCM.isMarkov_obsChainKernel · Causalean/SCM/Factored/ObsChainKernel.lean:526
  • obsKernel_map_prefixNodes theorem — Prefix form of the observational chain rule.
    N :
    Type u_1
    N → Type u_2
    shared
    M :
    SCM N Ω
    s :
    M.FixedValues
    ∀ (k : ℕ) (hk : k < M.observed.card),
    StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
    ∀ (k : ℕ) (hk : k < M.observed.card),
    Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))
    ∀ k : Fin M.observed.card,
    CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes k.val) (swigΩ Ω))
    n :
    ℕ
    hn :
    n ≤ M.observed.card
    (M.obsKernel s).map (valuesProjection (M.prefixNodes_subset_observed n))
    = M.obsChainKernel n hn s
    Proof (Lean source)
    theorem obsKernel_map_prefixNodes (M : SCM N Ω) (s : M.FixedValues) [∀ (k : ℕ) (hk : k < M.observed.card), StandardBorelSpace (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ (k : ℕ) (hk : k < M.observed.card), Nonempty (ValuesOn ({(M.observedAt ⟨k, hk⟩).val} : Finset (SWIGNode N)) (swigΩ Ω))] [∀ k : Fin M.observed.card, CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes k.val) (swigΩ Ω))] : ∀ (n : ℕ) (hn : n ≤ M.observed.card), (M.obsKernel s).map (valuesProjection (M.prefixNodes_subset_observed n)) = M.obsChainKernel n hn s := by intro n induction n with | zero => intro hn change (M.obsKernel s).map (valuesProjection (M.prefixNodes_subset_observed 0)) = M.obsChainKernelZero s unfold obsChainKernelZero rw [ProbabilityTheory.Kernel.const_apply] refine MeasureTheory.Measure.ext fun A hA => ?_ have hsub : Subsingleton (ValuesOn (M.prefixNodes 0) (swigΩ Ω)) := by refine ⟨fun f g => ?_⟩ funext ⟨w, hw⟩ have : w ∈ (∅ : Finset (SWIGNode N)) := by rw [M.prefixNodes_zero] at hw exact hw exact absurd this (notMem_empty _) by_cases hmem : M.emptyPrefixValues ∈ A · have hAuniv : A = univ := by ext x constructor · intro _; trivial · intro _ have hx : x = M.emptyPrefixValues := Subsingleton.elim _ _ simpa [hx] using hmem rw [hAuniv] rw [MeasureTheory.Measure.map_apply (measurable_valuesProjection (M.prefixNodes_subset_observed 0)) MeasurableSet.univ] simp [M.obsKernel_apply_univ s] · have hAempty : A = ∅ := by ext x constructor · intro hx have hx0 : x = M.emptyPrefixValues := Subsingleton.elim _ _ exact (hmem (by simpa [hx0] using hx)).elim · intro hx exact False.elim hx rw [hAempty] simp | succ n ih => intro hn classical have hk : n < M.observed.card := Nat.lt_of_succ_le hn letI : CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes n) (swigΩ Ω)) := inferInstanceAs (CountableOrCountablyGenerated (M.FixedValues) (ValuesOn (M.prefixNodes (⟨n, hk⟩ : Fin _).val) (swigΩ Ω))) let Y : Finset (SWIGNode N) := {(M.observedAt ⟨n, hk⟩).val} let hY : Y ⊆ M.observed := by intro v hv have hv_eq : v = (M.observedAt ⟨n, hk⟩).val := by simpa [Y] using hv simp [hv_eq, (M.observedAt ⟨n, hk⟩).property] let hCC : M.prefixNodes n ⊆ M.observed := M.prefixNodes_subset_observed n let e : ValuesOn (M.prefixNodes (n + 1)) (swigΩ Ω) ≃ᵐ ValuesOn (M.prefixNodes n) (swigΩ Ω) × ValuesOn Y (swigΩ Ω) := (valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hk)).trans (valuesUnionEquiv (Ω := Ω) (M.prefixNodes_disjoint_singleton_next hk)) refine e.map_measurableEquiv_injective ?_ have hIH := ih (le_of_succ_le hn) change map e (map (valuesProjection (M.prefixNodes_subset_observed (n + 1))) (M.obsKernel s)) = map e ((((M.obsChainKernel n (le_of_succ_le hn)) ⊗ₖ (M.obsStepCondKernel hk)).map (M.extendObsPrefix hk)) s) rw [ProbabilityTheory.Kernel.map_apply _ (M.measurable_extendObsPrefix hk)] rw [ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR] rw [← hIH] rw [MeasureTheory.Measure.map_map e.measurable (measurable_valuesProjection (M.prefixNodes_subset_observed (n + 1)))] rw [MeasureTheory.Measure.map_map e.measurable (M.measurable_extendObsPrefix hk)] have hleft_fun : e ∘ valuesProjection (M.prefixNodes_subset_observed (n + 1)) = (fun ω : M.ObservedValues => (valuesProjection (M.prefixNodes_subset_observed n) ω, valuesProjection hY ω)) := by change (fun ω : M.ObservedValues => valuesUnionEquiv (Ω := Ω) (M.prefixNodes_disjoint_singleton_next hk) ((valuesEquivOfEq (Ω := swigΩ Ω) (M.prefixNodes_succ hk)) (valuesProjection (M.prefixNodes_subset_observed (n + 1)) ω))) = (fun ω : M.ObservedValues => (valuesProjection (M.prefixNodes_subset_observed n) ω, valuesProjection hY ω)) exact M.prefixSucc_projection_pair hk rw [hleft_fun] have hright_fun : e ∘ M.extendObsPrefix hk = (fun p : ValuesOn (M.prefixNodes n) (swigΩ Ω) × swigΩ Ω (M.observedAt ⟨n, hk⟩).val => (p.1, singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hk⟩).val) p.2)) := by funext p exact M.valuesUnionEquiv_extendObsPrefix hk p rw [hright_fun] change map (fun ω : M.ObservedValues => (valuesProjection hCC ω, valuesProjection hY ω)) (M.obsKernel s) = map (map id (singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hk⟩).val))) (((M.obsKernel s).map (valuesProjection hCC)) ⊗ₘ (M.obsStepCondKernel hk).sectR s) rw [← MeasureTheory.Measure.compProd_map (μ := (M.obsKernel s).map (valuesProjection hCC)) (κ := (M.obsStepCondKernel hk).sectR s) (f := singletonValues (α := swigΩ Ω) (v := (M.observedAt ⟨n, hk⟩).val)) (measurable_singletonValues (α := swigΩ Ω))] rw [M.obsStepCondKernel_sectR_map_singletonValues hk s] rw [← M.obsCondPairKernel_apply_eq_compProd Y (M.prefixNodes n) hY hCC s] unfold obsCondPairKernel rw [ProbabilityTheory.Kernel.map_apply _ ((measurable_valuesProjection hCC).prodMk (measurable_valuesProjection hY))]
    Causalean.SCM.obsKernel_map_prefixNodes · Causalean/SCM/Factored/ObsChainKernel.lean:585
Parent­Lookup 2 core · 1 supporting This file builds the map that reads the parent values of the next observed node from a fixed assignment, a latent assignment, and an observed prefix. ★ measurable_parentValuesFromPrefix

Parent Lookup from Prefix States

This file builds the map that reads the parent values of the next observed node from a fixed assignment, a latent assignment, and an observed prefix. The lookup classifies each parent as fixed, observed, or unobserved, then proves the joint measurability needed by the deterministic step kernels in the factored construction of the joint kernel.

def parentValuesFromPrefix reviewed
Causalean.SCM

For a finite collection of nodes with a measurable outcome space for each node, a structural causal model, a nonnegative integer, and proof that the next position exists among the observed nodes, the map producing the values of all parents of the next observed node takes fixed-node values, latent-node values, and a prefix of the preceding observed-node values, and returns the corresponding value for every parent of that next observed node.

Definition (Lean source)
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
n :
ℕ
hn :
n + 1 ≤ M.observed.card
parentValuesFromPrefix M hn :
(M.FixedValues × M.OrderedLatentPrefixValues n (le_of_succ_le hn)) → (∀ w : {w // w ∈ M.dag.parents (M.observedAt ⟨n, hn⟩).val}, swigΩ Ω w.val)
fun sℓξ w
=> by by_cases hfix : w.val ∈ M.fixed · exact sℓξ.1 ⟨w.val, hfix⟩ · by_cases hobs : w.val ∈ M.observed · have hlt : M.observedIndex ⟨w.val, hobs⟩ < ⟨n, hn⟩ := M.observed_parent_index_lt hn (M.dag.mem_parents.mp w.property) hobs let iobs : Fin n := ⟨(M.observedIndex ⟨w.val, hobs⟩ : ℕ), hlt⟩ have hEq : swigΩ Ω (M.observedAt (M.observedIndex ⟨w.val, hobs⟩)).val = swigΩ Ω w.val := by simpa using congrArg (swigΩ Ω) (M.observedAt_observedIndex ⟨w.val, hobs⟩) exact cast hEq <| by simpa [iobs] using M.observedPrefixValue (le_of_succ_le hn) sℓξ.2.2 iobs · have hunobs : w.val ∈ M.unobserved := parent_unobserved_of_not_fixed_not_observed M.toSWIGGraph (M.dag.mem_parents.mp w.property) hfix hobs exact sℓξ.2.1 ⟨w.val, hunobs⟩
theorem measurable_parentValuesFromPrefix reviewed
Causalean.SCM

Fix a structural causal model M and a step index n such that there are at least n + 1 observed nodes, so n names a valid position in the canonical topological order of observed nodes. Then the map parentValuesFromPrefix that reads off the parent values of the n-th observed node from a fixed-value assignment, a latent assignment, and the already-generated length-n prefix of observed values is jointly measurable in these three arguments.

Formal statement
N :
Type uN
N → Type uΩ
shared
M :
SCM N Ω
n :
ℕ
hn :
n + 1 ≤ M.observed.card
Measurable (M.parentValuesFromPrefix hn)
Proof (Lean source)
@[fun_prop] theorem measurable_parentValuesFromPrefix (M : SCM N Ω) {n : ℕ} (hn : n + 1 ≤ M.observed.card) : Measurable (M.parentValuesFromPrefix hn) := by classical refine measurable_pi_lambda _ ?_ intro w by_cases hfix : w.val ∈ M.fixed · -- Fixed case: projection `sℓξ ↦ sℓξ.1 ⟨w.val, hfix⟩`. have h0 : Measurable fun x : M.FixedValues => x (⟨w.val, hfix⟩ : {x // x ∈ M.fixed}) := measurable_pi_apply _ have h : Measurable fun c : M.FixedValues × M.OrderedLatentPrefixValues n (le_of_succ_le hn) => c.1 (⟨w.val, hfix⟩ : {x // x ∈ M.fixed}) := h0.comp measurable_fst simpa [SCM.parentValuesFromPrefix, hfix] using h · by_cases hobs : w.val ∈ M.observed · -- Observed case: `cast ∘ observedPrefixValue ∘ snd ∘ snd`. have hlt : M.observedIndex ⟨w.val, hobs⟩ < ⟨n, hn⟩ := M.observed_parent_index_lt hn (M.dag.mem_parents.mp w.property) hobs let iobs : Fin n := ⟨(M.observedIndex ⟨w.val, hobs⟩ : ℕ), hlt⟩ have hNode : (M.observedAt (M.observedIndex ⟨w.val, hobs⟩)).val = w.val := by simpa using M.observedAt_observedIndex ⟨w.val, hobs⟩ have hEq : swigΩ Ω (M.observedAt (M.observedIndex ⟨w.val, hobs⟩)).val = swigΩ Ω w.val := by simpa using congrArg (swigΩ Ω) hNode -- Measurability of reading slot `iobs` from the prefix, as a function -- of the full product input. have hmeas : Measurable fun c : M.FixedValues × M.OrderedLatentPrefixValues n (le_of_succ_le hn) => M.observedPrefixValue (le_of_succ_le hn) c.2.2 iobs := (M.measurable_observedPrefixValue (le_of_succ_le hn) iobs).comp ((measurable_snd : Measurable snd).comp (measurable_snd : Measurable snd)) have hcast : Measurable (fun y : swigΩ Ω (M.observedAt (M.observedIndex ⟨w.val, hobs⟩)).val => cast hEq y) := measurable_cast_family hNode have hmeasCast : Measurable fun c : M.FixedValues × M.OrderedLatentPrefixValues n (le_of_succ_le hn) => cast hEq (M.observedPrefixValue (le_of_succ_le hn) c.2.2 iobs) := hcast.comp hmeas simpa [SCM.parentValuesFromPrefix, hfix, hobs, iobs] using hmeasCast · -- Unobserved case: projection `sℓξ ↦ sℓξ.2.1 ⟨w.val, hunobs⟩`. have hunobs : w.val ∈ M.unobserved := parent_unobserved_of_not_fixed_not_observed M.toSWIGGraph (M.dag.mem_parents.mp w.property) hfix hobs have h0 : Measurable fun x : M.LatentValues => x (⟨w.val, hunobs⟩ : {x // x ∈ M.unobserved}) := measurable_pi_apply _ have h : Measurable fun c : M.FixedValues × M.OrderedLatentPrefixValues n (le_of_succ_le hn) => c.2.1 (⟨w.val, hunobs⟩ : {x // x ∈ M.unobserved}) := h0.comp (measurable_fst.comp measurable_snd) simpa [SCM.parentValuesFromPrefix, hfix, hobs, hunobs] using h
1 supporting declaration (lemmas, instances)
  • parent_unobserved_of_not_fixed_not_observed theorem — A parent that is neither fixed nor observed must be an unobserved node. This lets an evaluator classify a parent's value source without depending on where the target appears in an observation order.
    N :
    Type uN
    shared
    G :
    u v :
    hedge :
    G.dag.edge u v
    hfix :
    u ∉ G.fixed
    hobs :
    u ∉ G.observed
    u ∈ G.unobserved
    Proof (Lean source)
    theorem parent_unobserved_of_not_fixed_not_observed (G : SWIGGraph N) {u v : SWIGNode N} (hedge : G.dag.edge u v) (hfix : u ∉ G.fixed) (hobs : u ∉ G.observed) : u ∈ G.unobserved := by have hclass : u ∈ G.fixed ∪ G.observed ∪ G.unobserved := (G.dag_edges_classified _ _ hedge).1 rcases Finset.mem_union.mp hclass with h | h · rcases Finset.mem_union.mp h with h | h · exact (hfix h).elim · exact (hobs h).elim · exact h
    Causalean.SCM.parent_unobserved_of_not_fixed_not_observed · Causalean/SCM/Factored/ParentLookup.lean:64