PO.Assumptions

The standard identification assumptions as predicates on a potential-outcome system: unconfoundedness, overlap, and their conditional refinements.

Consistency 3 core · 0 supporting This file defines the pathwise agreement predicates and the two-clause consistency assumption for potential-outcome systems. ★ Consistency

Consistency for Potential Outcomes

This file defines the pathwise agreement predicates and the two-clause consistency assumption for potential-outcome systems. These notions connect factual agreement, sequential interventions, and equality of potential outcomes outside the intervened coordinates. The public API consists of POSystem.FactualAgrees, POSystem.IntermediateAgrees, and the POSystem.Consistency structure with its factual-consistency and composition-consistency fields.

def FactualAgrees reviewed
Causalean.PO.POSystem

For a potential-outcome system, an intervention regime, and a unit in the sample space, factual agreement means that for every variable targeted by the regime, the factual value of that variable for the unit equals the value assigned by the regime.

Definition (Lean source)
def FactualAgrees (r : Regime P.V P.X) (ω : P.Ω) : Prop := ∀ v (hv : v ∈ r.target), P.eval Regime.empty ω v = r.assign v hv
Causalean.PO.POSystem.FactualAgrees · Causalean/PO/Assumptions/Consistency.lean:25 · uses POSystem , Regime
def IntermediateAgrees reviewed
Causalean.PO.POSystem

For a potential-outcome system, two intervention regimes, and a unit in the sample space, intermediate agreement means that after applying the first regime, every variable targeted by the second regime has the value assigned to it by the second regime.

Definition (Lean source)
def IntermediateAgrees (r₁ r₂ : Regime P.V P.X) (ω : P.Ω) : Prop := ∀ v (hv : v ∈ r₂.target), P.eval r₁ ω v = r₂.assign v hv
Causalean.PO.POSystem.IntermediateAgrees · Causalean/PO/Assumptions/Consistency.lean:34 · uses POSystem , Regime
structure Consistency reviewed
Causalean.PO.POSystem

A potential-outcome system is consistent when two conditions hold. First, for every intervention regime and every finite set of variables disjoint from the regime's target, a unit's potential outcomes for that set under the regime equal its factual potential outcomes whenever it factually agrees with the regime. Second, for every pair of disjoint regimes and every finite set of variables disjoint from the union of their targets, a unit's potential outcomes for that set under the composed regime equal its potential outcomes under the first regime alone, whenever it agrees with the second regime after the first has been applied.

Definition (Lean source)
parameters
P :
POSystem
fields
Factual consistency.
factual :
∀ (r : Regime P.V P.X) (Y : Finset P.V),
_root_.Disjoint Y r.target → ∀ ω : P.Ω, P.FactualAgrees r ω → P.poVariable r Y ω
= P.poVariable Regime.empty Y ω
Composition / nested consistency.
composition :
∀ (r₁ r₂ : Regime P.V P.X) (h : r₁.Disjoint r₂) (Y : Finset P.V),
_root_.Disjoint Y (r₁.target ∪ r₂.target) → ∀ ω : P.Ω, P.IntermediateAgrees r₁ r₂ ω → P.poVariable (r₁.sqcup r₂ h) Y ω
= P.poVariable r₁ Y ω
Causalean.PO.POSystem.Consistency · Causalean/PO/Assumptions/Consistency.lean:43 · uses POSystem
Consistency­Lemmas 1 core · 8 supporting This file provides reusable pointwise consistency combinators for empty, singleton, and disjoint-union regimes, together with generic event-level rewrites for POVar counterfactual values. ★ cf_eq_factual_of_factualAgrees

Pointwise consistency lemmas for potential-outcome variables

This file provides reusable pointwise consistency combinators for empty, singleton, and disjoint-union regimes, together with generic event-level rewrites for POVar counterfactual values. These lemmas factor the consistency arguments used by LATE, frontdoor, dynamic regimes, and other multi-target PO identification files. Important results include POSystem.factualAgrees_empty, POSystem.factualAgrees_sqcup, POVar.factualAgrees_single, POVar.cf_eq_factual_on_event, and the integrated indicator rewrites POVar.factual_mul_indicator_eq_cfUnder_mul_indicator and POVar.factual_mul_indicator_eq_cf_mul_indicator.

theorem cf_eq_factual_of_factualAgrees reviewed
Causalean.PO.POVar

Multi-target consistency. Under the consistency (SUTVA) assumption on the potential-outcome system, for a regimed variable a whose index does not lie in the target of a regime r, if the outcome ω factually agrees with the regime r, then the counterfactual value of a under r at ω equals its factual value at ω.

Formal statement
hypotheses
P :
POSystem
α :
Type*
MeasurableSpace α
hC :
P.Consistency
a :
POVar P α
r :
Regime P.V P.X
h_notmem :
a.v ∉ r.target
ω :
P.Ω
hAgrees :
P.FactualAgrees r ω
conclusion
a.cf r ω = a.factual ω
Proof (Lean source)
theorem POVar.cf_eq_factual_of_factualAgrees {P : POSystem} {α : Type*} [MeasurableSpace α] (hC : P.Consistency) (a : POVar P α) (r : Regime P.V P.X) (h_notmem : a.v ∉ r.target) (ω : P.Ω) (hAgrees : P.FactualAgrees r ω) : a.cf r ω = a.factual ω := by -- Disjointness: `{a.v}` is disjoint from `r.target`. have hdisj : _root_.Disjoint ({a.v} : Finset P.V) r.target := by simpa [Finset.disjoint_singleton_left] using h_notmem -- Apply `hC.factual`. have hPoEq := hC.factual r {a.v} hdisj ω hAgrees have haEq : P.eval r ω a.v = P.eval Regime.empty ω a.v := by simpa [POSystem.poVariable] using congrFun hPoEq ⟨a.v, mem_singleton_self a.v⟩ -- Push through `a.equiv`. change a.equiv (P.eval r ω a.v) = a.equiv (P.eval Regime.empty ω a.v) exact congrArg a.equiv haEq
Causalean.PO.POVar.cf_eq_factual_of_factualAgrees · Causalean/PO/Assumptions/ConsistencyLemmas.lean:201 · uses POSystem , Consistency , FactualAgrees , POVar , cf , factual , Regime
8 supporting declarations (lemmas, instances)
  • factualAgrees_empty theorem — FactualAgrees holds vacuously for the empty regime.
    hypotheses
    ω :
    P.Ω
    conclusion
    P.FactualAgrees Regime.empty ω
    Proof (Lean source)
    theorem factualAgrees_empty (ω : P.Ω) : P.FactualAgrees Regime.empty ω := by intro v hv exact (notMem_empty v hv).elim
    Causalean.PO.POSystem.factualAgrees_empty · Causalean/PO/Assumptions/ConsistencyLemmas.lean:46
  • factualAgrees_sqcup theorem — Combinator: FactualAgrees for a disjoint union reduces to FactualAgrees for each component.
    hypotheses
    r₁ r₂ :
    Regime P.V P.X
    h :
    r₁.Disjoint r₂
    ω :
    P.Ω
    h₁ :
    P.FactualAgrees r₁ ω
    h₂ :
    P.FactualAgrees r₂ ω
    conclusion
    P.FactualAgrees (r₁.sqcup r₂ h) ω
    Proof (Lean source)
    theorem factualAgrees_sqcup {r₁ r₂ : Regime P.V P.X} (h : r₁.Disjoint r₂) {ω : P.Ω} (h₁ : P.FactualAgrees r₁ ω) (h₂ : P.FactualAgrees r₂ ω) : P.FactualAgrees (r₁.sqcup r₂ h) ω := by intro v hv -- `v ∈ r₁.target ∪ r₂.target`. have hv' : v ∈ r₁.target ∪ r₂.target := by simpa only [Regime.sqcup_target] using hv by_cases hv₁ : v ∈ r₁.target · -- `r₁.sqcup r₂` agrees with `r₁` on `r₁.target`. have hassign : (r₁.sqcup r₂ h).assign v hv = r₁.assign v hv₁ := by exact Regime.sqcup_assign_pos r₁ r₂ h v hv₁ rw [hassign] exact h₁ v hv₁ · -- Must be in `r₂.target`. have hv₂ : v ∈ r₂.target := by rcases Finset.mem_union.mp hv' with h₁ | h₂ · exact (hv₁ h₁).elim · exact h₂ have hassign : (r₁.sqcup r₂ h).assign v hv = r₂.assign v hv₂ := by exact Regime.sqcup_assign_neg r₁ r₂ h v hv₁ hv₂ rw [hassign] exact h₂ v hv₂
    Causalean.PO.POSystem.factualAgrees_sqcup · Causalean/PO/Assumptions/ConsistencyLemmas.lean:51
  • factualAgrees_single theorem — Combinator: from a factual equality a.factual ω = x, build FactualAgrees for the singleton regime {a.v ← a.equiv.symm x}.
    hypotheses
    a :
    POVar P α
    x :
    α
    ω :
    P.Ω
    h :
    a.factual ω = x
    conclusion
    P.FactualAgrees (Regime.single a.v (a.equiv.symm x)) ω
    Proof (Lean source)
    theorem factualAgrees_single (a : POVar P α) (x : α) {ω : P.Ω} (h : a.factual ω = x) : P.FactualAgrees (Regime.single a.v (a.equiv.symm x)) ω := by intro v hv -- `v ∈ {a.v}`, so `v = a.v`. have hv_eq : v = a.v := Finset.mem_singleton.mp hv subst hv_eq -- `h : a.equiv (P.eval ∅ ω a.v) = x`; apply `a.equiv.symm`. have hω : a.equiv (P.eval Regime.empty ω a.v) = x := h have := congrArg a.equiv.symm hω simpa [Regime.single] using this
    Causalean.PO.POVar.factualAgrees_single · Causalean/PO/Assumptions/ConsistencyLemmas.lean:83
  • cf_eq_factual_on_event theorem — Under consistency, changing a distinct variable to a value it already has does not change the counterfactual value of the target variable on that event.
    hypotheses
    P :
    POSystem
    α β :
    Type*
    MeasurableSpace α
    MeasurableSpace β
    hC :
    P.Consistency
    a :
    POVar P α
    w :
    POVar P β
    y :
    β
    hvw :
    a.v ≠ w.v
    ω :
    P.Ω
    hω :
    ω ∈ w.event y
    conclusion
    a.cfUnder w y ω = a.factual ω
    Proof (Lean source)
    theorem POVar.cf_eq_factual_on_event {P : POSystem} {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (hC : P.Consistency) (a : POVar P α) (w : POVar P β) (y : β) (hvw : a.v ≠ w.v) {ω : P.Ω} (hω : ω ∈ w.event y) : a.cfUnder w y ω = a.factual ω := by -- The regime: `{w.v ← w.equiv.symm y}`. set r : Regime P.V P.X := Regime.single w.v (w.equiv.symm y) with hr -- Factual agreement: `P.eval ∅ ω v = r.assign v hv` for all `v ∈ r.target`. have hAgrees : P.FactualAgrees r ω := by intro v hv have hvw_eq : v = w.v := Finset.mem_singleton.mp hv subst hvw_eq -- `hω : ω ∈ w.event y`, i.e. `w.factual ω = y`, i.e. -- `w.equiv (P.eval ∅ ω w.v) = y`. have hωeq : w.equiv (P.eval Regime.empty ω w.v) = y := hω -- Apply `w.equiv.symm` and use `symm_apply_apply`. have hsym := congrArg w.equiv.symm hωeq rw [MeasurableEquiv.symm_apply_apply] at hsym show P.eval Regime.empty ω w.v = w.equiv.symm y exact hsym -- Disjointness: `{a.v}` is disjoint from `r.target = {w.v}`. have hdisj : _root_.Disjoint ({a.v} : Finset P.V) r.target := by simp [hr, Regime.single, hvw] -- Apply `hC.factual`. have hPoEq := hC.factual r {a.v} hdisj ω hAgrees have haEq : P.eval r ω a.v = P.eval Regime.empty ω a.v := by simpa [POSystem.poVariable] using congrFun hPoEq ⟨a.v, mem_singleton_self a.v⟩ -- Push through `a.equiv`. change a.equiv (P.eval r ω a.v) = a.equiv (P.eval Regime.empty ω a.v) exact congrArg a.equiv haEq
    Causalean.PO.POVar.cf_eq_factual_on_event · Causalean/PO/Assumptions/ConsistencyLemmas.lean:99
  • factual_eq_cfUnder_self_selected theorem — Under consistency, setting a distinct variable to its realized factual value leaves the target variable at its factual value.
    hypotheses
    P :
    POSystem
    α β :
    Type*
    MeasurableSpace α
    MeasurableSpace β
    hC :
    P.Consistency
    a :
    POVar P α
    w :
    POVar P β
    hvw :
    a.v ≠ w.v
    ω :
    P.Ω
    conclusion
    a.factual ω = a.cfUnder w (w.factual ω) ω
    Proof (Lean source)
    theorem POVar.factual_eq_cfUnder_self_selected {P : POSystem} {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (hC : P.Consistency) (a : POVar P α) (w : POVar P β) (hvw : a.v ≠ w.v) (ω : P.Ω) : a.factual ω = a.cfUnder w (w.factual ω) ω := by -- The regime: `{w.v ← w.equiv.symm (w.factual ω)}`. set r : Regime P.V P.X := Regime.single w.v (w.equiv.symm (w.factual ω)) with hr -- Factual agreement is definitional: `w.equiv.symm (w.equiv x) = x`. have hAgrees : P.FactualAgrees r ω := by intro v hv have hvw_eq : v = w.v := Finset.mem_singleton.mp hv subst hvw_eq simp [hr, POVar.factual, POVar.cf, Regime.single] -- Disjointness. have hdisj : _root_.Disjoint ({a.v} : Finset P.V) r.target := by simp [hr, Regime.single, hvw] -- Apply `hC.factual`. have hPoEq := hC.factual r {a.v} hdisj ω hAgrees have haEq : P.eval r ω a.v = P.eval Regime.empty ω a.v := by simpa [POSystem.poVariable] using congrFun hPoEq ⟨a.v, mem_singleton_self a.v⟩ change a.equiv (P.eval Regime.empty ω a.v) = a.equiv (P.eval r ω a.v) exact (congrArg a.equiv haEq).symm
    Causalean.PO.POVar.factual_eq_cfUnder_self_selected · Causalean/PO/Assumptions/ConsistencyLemmas.lean:135
  • factual_mul_indicator_eq_cfUnder_mul_indicator theorem — Integrated form of consistency: Y · 1_{W=y} = Y(w=y) · 1_{W=y} pointwise, where a plays the role of Y and w the role of the treatment. Used in backdoor-style identification proofs where the factual outcome is replaced by the counterfactual on the event {W = y}.
    hypotheses
    P :
    POSystem
    β :
    Type*
    MeasurableSpace β
    hC :
    P.Consistency
    a :
    POVar P ℝ
    w :
    POVar P β
    y :
    β
    hvw :
    a.v ≠ w.v
    conclusion
    (fun ω => a.factual ω * (w.event y).indicator (fun _ => (1:ℝ)) ω)
    = fun ω => a.cfUnder w y ω * (w.event y).indicator (fun _ => (1:ℝ)) ω
    Proof (Lean source)
    theorem POVar.factual_mul_indicator_eq_cfUnder_mul_indicator {P : POSystem} {β : Type*} [MeasurableSpace β] (hC : P.Consistency) (a : POVar P ℝ) (w : POVar P β) (y : β) (hvw : a.v ≠ w.v) : (fun ω => a.factual ω * (w.event y).indicator (fun _ => (1:ℝ)) ω) = fun ω => a.cfUnder w y ω * (w.event y).indicator (fun _ => (1:ℝ)) ω := by funext ω by_cases hω : ω ∈ w.event y · have hind : (w.event y).indicator (fun _ => (1:ℝ)) ω = 1 := Set.indicator_of_mem hω _ have hcf : a.cfUnder w y ω = a.factual ω := POVar.cf_eq_factual_on_event hC a w y hvw hω simp [hind, hcf] · have hind : (w.event y).indicator (fun _ => (1:ℝ)) ω = 0 := Set.indicator_of_notMem hω _ simp [hind]
    Causalean.PO.POVar.factual_mul_indicator_eq_cfUnder_mul_indicator · Causalean/PO/Assumptions/ConsistencyLemmas.lean:163
  • factual_mul_indicator_eq_cfUnder_mul_indicator_fn theorem — Pointwise-function variant of POVar.factual_mul_indicator_eq_cfUnder_mul_indicator, phrased directly in terms of POVar.indicator (rather than Set.indicator on w.event y).
    hypotheses
    P :
    POSystem
    β :
    Type*
    MeasurableSpace β
    MeasurableSingletonClass β
    hC :
    P.Consistency
    y :
    POVar P ℝ
    w :
    POVar P β
    x :
    β
    h_ne :
    y.v ≠ w.v
    conclusion
    (fun ω => y.factual ω * w.indicator x ω) = fun ω => y.cfUnder w x ω * w.indicator x ω
    Proof (Lean source)
    theorem POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn {P : POSystem} {β : Type*} [MeasurableSpace β] [MeasurableSingletonClass β] (hC : P.Consistency) (y : POVar P ℝ) (w : POVar P β) (x : β) (h_ne : y.v ≠ w.v) : (fun ω => y.factual ω * w.indicator x ω) = fun ω => y.cfUnder w x ω * w.indicator x ω := by rw [w.indicator_eq_event_indicator x] exact POVar.factual_mul_indicator_eq_cfUnder_mul_indicator hC y w x h_ne
    Causalean.PO.POVar.factual_mul_indicator_eq_cfUnder_mul_indicator_fn · Causalean/PO/Assumptions/ConsistencyLemmas.lean:185
  • factual_mul_indicator_eq_cf_mul_indicator theorem — Multi-target integrated consistency: Y · 1_E = Y(r) · 1_E pointwise, whenever every ω ∈ E factually agrees with r and a.v ∉ r.target.
    hypotheses
    P :
    POSystem
    hC :
    P.Consistency
    a :
    POVar P ℝ
    r :
    Regime P.V P.X
    h_notmem :
    a.v ∉ r.target
    E :
    Set P.Ω
    hE :
    ∀ ω ∈ E, P.FactualAgrees r ω
    conclusion
    (fun ω => a.factual ω * E.indicator (fun _ => (1:ℝ)) ω)
    = (fun ω => a.cf r ω * E.indicator (fun _ => (1:ℝ)) ω)
    Proof (Lean source)
    theorem POVar.factual_mul_indicator_eq_cf_mul_indicator {P : POSystem} (hC : P.Consistency) (a : POVar P ℝ) (r : Regime P.V P.X) (h_notmem : a.v ∉ r.target) (E : Set P.Ω) (hE : ∀ ω ∈ E, P.FactualAgrees r ω) : (fun ω => a.factual ω * E.indicator (fun _ => (1:ℝ)) ω) = (fun ω => a.cf r ω * E.indicator (fun _ => (1:ℝ)) ω) := by funext ω by_cases hω : ω ∈ E · have hind : E.indicator (fun _ => (1:ℝ)) ω = 1 := Set.indicator_of_mem hω _ have hcf : a.cf r ω = a.factual ω := POVar.cf_eq_factual_of_factualAgrees hC a r h_notmem ω (hE ω hω) simp [hind, hcf] · have hind : E.indicator (fun _ => (1:ℝ)) ω = 0 := Set.indicator_of_notMem hω _ simp [hind]
    Causalean.PO.POVar.factual_mul_indicator_eq_cf_mul_indicator · Causalean/PO/Assumptions/ConsistencyLemmas.lean:225
Indep­CF 7 core · 9 supporting This file packages finite heterogeneous collections of regimed potential-outcome variables and defines independence or conditional independence between a single regimed variable and such a bundle. ★ POCFBundle★ IndepCF★ CondIndepCF★ project

Independence of Counterfactual Bundles

This file packages finite heterogeneous collections of regimed potential-outcome variables and defines independence or conditional independence between a single regimed variable and such a bundle. These forms provide reusable assumptions for identification theorems.

The main structure is POCFBundle, whose jointValue map turns a finite dependent tuple of regimed potential outcomes into one measurable conditioning object. POSystem.IndepCF and POSystem.CondIndepCF unfold to IndepFun and CondIndepFun, and the projection lemmas let downstream files extract independence for a measurable function or a single coordinate of the bundle.

structure POCFBundle reviewed
Causalean.PO

A finite heterogeneous bundle of n regimed potential-outcome variables indexed by Fin n: each coordinate carries its own value type equipped with a measurable-space structure, and each coordinate is itself a potential-outcome variable paired with the intervention regime under which it is evaluated.

Definition (Lean source)
parameters
P :
POSystem
fields
Length of the bundle.
n :
ℕ
Value type of each component.
type :
Fin n → Type*
Measurable-space structure on each component.
inst :
∀ i, MeasurableSpace (type i)
Component `RegimedVar`s.
vars :
∀ i, RegimedVar P (type i)
Causalean.PO.POCFBundle · Causalean/PO/Assumptions/IndepCF.lean:39 · uses POSystem
def jointValue reviewed
Causalean.PO.POCFBundle

The joint counterfactual-value map sends each sample point to the tuple of all regimed counterfactual values in the bundle.

Definition (Lean source)
def jointValue : P.Ω → (∀ i : Fin B.n, B.type i) := fun ω i => (B.vars i).value ω
Causalean.PO.POCFBundle.jointValue · Causalean/PO/Assumptions/IndepCF.lean:64 · uses POCFBundle , POSystem
def nil reviewed
Causalean.PO.POCFBundle

The empty counterfactual bundle has no coordinates.

Definition (Lean source)
def nil (P : POSystem) : POCFBundle P where n := 0 type := Fin.elim0 inst := fun i => i.elim0 vars := fun i => i.elim0
Causalean.PO.POCFBundle.nil · Causalean/PO/Assumptions/IndepCF.lean:73 · uses POCFBundle , POSystem
def cons reviewed
Causalean.PO.POCFBundle

Adding a regimed potential-outcome variable to the front of a bundle produces the corresponding extended counterfactual bundle.

Definition (Lean source)
def cons {P : POSystem} {α : Type*} [inst : MeasurableSpace α] (a : RegimedVar P α) (B : POCFBundle P) : POCFBundle P where n := B.n + 1 type := Fin.cases α B.type inst := Fin.cases inst B.inst vars := Fin.cases a B.vars
Causalean.PO.POCFBundle.cons · Causalean/PO/Assumptions/IndepCF.lean:80 · uses POCFBundle , POSystem , RegimedVar
def IndepCF reviewed
Causalean.PO.POSystem

A regimed potential-outcome variable is independent of a counterfactual bundle when its value is independent of the bundle's joint counterfactual value under the chosen measure.

Definition (Lean source)
def POSystem.IndepCF {α : Type*} [MeasurableSpace α] (P : POSystem) (a : RegimedVar P α) (B : POCFBundle P) (μ : Measure P.Ω := P.μ) : Prop := IndepFun a.value B.jointValue μ
Causalean.PO.POSystem.IndepCF · Causalean/PO/Assumptions/IndepCF.lean:91 · uses POCFBundle , POSystem , RegimedVar
def CondIndepCF reviewed
Causalean.PO.POSystem

A regimed potential-outcome variable is conditionally independent of a counterfactual bundle when its value is conditionally independent of the bundle's joint counterfactual value given the sigma-algebra generated by the conditioning variable.

Definition (Lean source)
def POSystem.CondIndepCF {α γ : Type*} [MeasurableSpace α] [MeasurableSpace γ] (P : POSystem) [StandardBorelSpace P.Ω] (a : RegimedVar P α) (B : POCFBundle P) (c : RegimedVar P γ) (μ : Measure P.Ω := P.μ) [IsFiniteMeasure μ] : Prop := CondIndepFun (comap c.value inferInstance) (c.measurable_value.comap_le) a.value B.jointValue μ
Causalean.PO.POSystem.CondIndepCF · Causalean/PO/Assumptions/IndepCF.lean:98 · uses POCFBundle , POSystem , RegimedVar
lemma project reviewed
Causalean.PO.POSystem.CondIndepCF

Fix a potential-outcome system in which a regimed variable a is conditionally independent of a counterfactual bundle B given a regimed variable c. Then for any measurable function ψ of the bundle's joint value, the value of a remains conditionally independent, given c, of ψ composed with the bundle's joint value.

Formal statement
hypotheses
α β γ :
Type*
MeasurableSpace α
MeasurableSpace β
MeasurableSpace γ
StandardBorelSpace P.Ω
a :
RegimedVar P α
B :
POCFBundle P
c :
RegimedVar P γ
μ :
Measure P.Ω
IsFiniteMeasure μ
ψ :
(∀ i, B.type i) → β
h :
P.CondIndepCF a B c μ
hψ :
Measurable ψ
conclusion
CondIndepFun (comap c.value inferInstance) (c.measurable_value.comap_le) a.value (ψ ∘ B.jointValue) μ
Proof (Lean source)
lemma CondIndepCF.project {α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [StandardBorelSpace P.Ω] {a : RegimedVar P α} {B : POCFBundle P} {c : RegimedVar P γ} {μ : Measure P.Ω} [IsFiniteMeasure μ] {ψ : (∀ i, B.type i) → β} (h : P.CondIndepCF a B c μ) (hψ : Measurable ψ) : CondIndepFun (comap c.value inferInstance) (c.measurable_value.comap_le) a.value (ψ ∘ B.jointValue) μ := h.toCondIndepFun.comp measurable_id hψ
Causalean.PO.POSystem.CondIndepCF.project · Causalean/PO/Assumptions/IndepCF.lean:169 · uses POCFBundle , instMeasurableSpaceType , jointValue , POSystem , CondIndepCF , RegimedVar , measurable_value , value
9 supporting declarations (lemmas, instances)