PO.Analysis

Analytic readings of potential outcomes: distributional (quantile) functionals, regression-function predicates, and population residualization primitives.

Quantile 6 core · 2 supporting This file gives the distributional reading of a real-valued potential outcome: its law under a measure on the sample space, the associated cumulative distribution function, and the corresponding quantile. ★ cfCDF_eq_measureReal

Laws and Quantiles of Real Potential Outcomes

This file gives the distributional reading of a real-valued potential outcome: its law under a measure on the sample space, the associated cumulative distribution function, and the corresponding quantile. The main definitions are POVar.cfLaw, POVar.cfCDF, and POVar.cfQuantile, with the single-intervention specializations POVar.cfUnderLaw and POVar.cfUnderQuantile for treatment effects written as Y(d). The lemma POVar.cfCDF_eq_measureReal records the probability interpretation of the counterfactual cdf.

def cfLaw reviewed

Causalean.PO.POVar

For a potential-outcome system, a real-valued potential-outcome variable, an intervention regime, and a measure on the sample space, the counterfactual law is the distribution obtained by pushing the measure forward through the variable's potential-outcome function under that regime.

Definition (Lean source)

parameters

P :

POSystem

shared

a :

POVar P ℝ

shared

r :

Regime P.V P.X

μ :

Measure P.Ω

def

cfLaw a r μ :

Measure ℝ

given by

μ.map (a.cf r)

Causalean.PO.POVar.cfLaw · Causalean/PO/Analysis/Quantile.lean:29 · uses POSystem , POVar , Regime

def cfCDF reviewed

Causalean.PO.POVar

For a potential-outcome system, a real-valued potential-outcome variable, an intervention regime, and a measure on the sample space, the counterfactual cumulative distribution function is the cumulative distribution function of the variable's counterfactual law under that regime and measure.

Definition (Lean source)

parameters

P :

POSystem

shared

a :

POVar P ℝ

shared

r :

Regime P.V P.X

μ :

Measure P.Ω

def

cfCDF a r μ :

StieltjesFunction ℝ

given by

cdf (a.cfLaw r μ)

Causalean.PO.POVar.cfCDF · Causalean/PO/Analysis/Quantile.lean:48 · uses POSystem , POVar , Regime

def cfQuantile reviewed

Causalean.PO.POVar

For a potential-outcome system, a real-valued potential-outcome variable, an intervention regime, a measure on the sample space, and a real index, the counterfactual quantile is the quantile at that index of the variable's counterfactual law under the regime and measure.

Definition (Lean source)

parameters

P :

POSystem

shared

a :

POVar P ℝ

shared

r :

Regime P.V P.X

μ :

Measure P.Ω

τ :

ℝ

def

cfQuantile a r μ τ :

ℝ

given by

quantile (a.cfLaw r μ) τ

Causalean.PO.POVar.cfQuantile · Causalean/PO/Analysis/Quantile.lean:55 · uses POSystem , POVar , Regime

lemma cfCDF_eq_measureReal reviewed

Causalean.PO.POVar

For an intervention regime r and a measure μ on the sample space, the cdf of the potential outcome a(r) evaluated at y equals the μ-probability of the event a(r) ≤ y.

Formal statement

hypotheses

P :

POSystem

shared

a :

POVar P ℝ

shared

r :

Regime P.V P.X

μ :

Measure P.Ω

IsProbabilityMeasure μ

y :

ℝ

conclusion

a.cfCDF r μ y = (a.cfLaw r μ).real (Iic y)

Proof (Lean source)

lemma cfCDF_eq_measureReal (r : Regime P.V P.X) (μ : Measure P.Ω) [IsProbabilityMeasure μ] (y : ℝ) : a.cfCDF r μ y = (a.cfLaw r μ).real (Iic y) := cdf_eq_real (a.cfLaw r μ) y

Causalean.PO.POVar.cfCDF_eq_measureReal · Causalean/PO/Analysis/Quantile.lean:61 · uses POSystem , POVar , cfCDF , cfLaw , Regime

def cfUnderLaw reviewed

Causalean.PO.POVar

For a potential-outcome system, a real-valued outcome variable, a potential-outcome intervention variable on a measurable scale, a value of that intervention variable, and a measure on the sample space, the single-intervention counterfactual law is the distribution of the outcome variable's potential outcome when the intervention variable is set to that value.

Definition (Lean source)

parameters

P :

POSystem

shared

a :

POVar P ℝ

shared

β :

Type u_1

shared

w :

POVar P β

y :

μ :

Measure P.Ω

def

cfUnderLaw a w y μ :

Measure ℝ

given by

a.cfLaw (Regime.single w.v (w.equiv.symm y)) μ

Causalean.PO.POVar.cfUnderLaw · Causalean/PO/Analysis/Quantile.lean:73 · uses POSystem , POVar

def cfUnderQuantile reviewed

Causalean.PO.POVar

For a potential-outcome system, a real-valued outcome variable, a potential-outcome intervention variable on a measurable scale, a value of that intervention variable, a measure on the sample space, and a real index, the single-intervention counterfactual quantile is the quantile at that index of the outcome variable's potential outcome when the intervention variable is set to that value.

Definition (Lean source)

parameters

P :

POSystem

shared

a :

POVar P ℝ

shared

β :

Type u_1

shared

w :

POVar P β

y :

μ :

Measure P.Ω

τ :

ℝ

def

cfUnderQuantile a w y μ τ :

ℝ

given by

a.cfQuantile (Regime.single w.v (w.equiv.symm y)) μ τ

Causalean.PO.POVar.cfUnderQuantile · Causalean/PO/Analysis/Quantile.lean:79 · uses POSystem , POVar

2 supporting declarations (lemmas, instances)

instIsProbabilityMeasureCfLaw instance — For a potential-outcomes system, a real-valued potential-outcome variable in that system, an intervention regime, and a measure on the system's sample space, if that sample-space measure is a probability measure, then the distribution of the variable's potential outcome under the regime is a probability measure.

parameters

P :

POSystem
shared

a :

POVar P ℝ
shared

r :

Regime P.V P.X

μ :

Measure P.Ω
IsProbabilityMeasure μ

instance

instIsProbabilityMeasureCfLaw a r μ :
IsProbabilityMeasure (a.cfLaw r μ)

given by

Measure.isProbabilityMeasure_map (a.measurable_cf r).aemeasurable

Causalean.PO.POVar.instIsProbabilityMeasureCfLaw · Causalean/PO/Analysis/Quantile.lean:36
cfUnderQuantile_eq lemma — The single-intervention quantile is exactly the quantile computed from the corresponding single-intervention law.

hypotheses

P :

POSystem
shared

a :

POVar P ℝ
shared

β :

Type u_1
shared

w :

POVar P β

y :

β

μ :

Measure P.Ω

τ :

ℝ

conclusion

a.cfUnderQuantile w y μ τ = quantile (a.cfUnderLaw w y μ) τ

Proof (Lean source)

lemma cfUnderQuantile_eq (w : POVar P β) (y : β) (μ : Measure P.Ω) (τ : ℝ) : a.cfUnderQuantile w y μ τ = quantile (a.cfUnderLaw w y μ) τ := rfl

Causalean.PO.POVar.cfUnderQuantile_eq · Causalean/PO/Analysis/Quantile.lean:86

Regression 2 core · 2 supporting This file provides a measure-theoretic predicate saying that a real function is a concrete representative of a conditional mean of one real random variable given another. ★ aeEq_of_aeEq_response

Regression Function Representatives

This file provides a measure-theoretic predicate saying that a real function is a concrete representative of a conditional mean of one real random variable given another. The predicate is used as a lightweight interface in RDD-style potential-outcome identification statements.

The central structure is IsRegressionFunction μ X g f, which requires measurability, integrability, and equality of slice integrals over every measurable event in the range of X. The file also proves pushforward integrability of representatives, closure under subtraction, and almost-everywhere equality of two representatives when the represented responses are a.e. equal.

structure IsRegressionFunction reviewed

Causalean.PO

A regression-function representative for the conditional mean of a response g given a conditioning variable X: a candidate function f on the real line that is measurable, for which the response g is integrable and the composite f ∘ X is integrable, and such that the integral of g over every measurable event determined by X equals the integral of f ∘ X over that same event.

Definition (Lean source)

parameters

Ω :

Type*

MeasurableSpace Ω

μ :

Measure Ω

X :

Ω → ℝ

g :

Ω → ℝ

f :

ℝ → ℝ

assumes

measurable :

Measurable f

integrable_response :

Integrable g μ

integrable_compose :

Integrable (fun ω => f (X ω)) μ

integral_preimage_eq :

∀ A : Set ℝ

MeasurableSet A

then

(∫ ω in X ⁻¹' A, g ω ∂μ) = ∫ ω in X ⁻¹' A, f (X ω) ∂μ

Causalean.PO.IsRegressionFunction · Causalean/PO/Analysis/Regression.lean:40

lemma aeEq_of_aeEq_response reviewed

Causalean.PO.IsRegressionFunction

Fix a conditioning variable X that is μ-almost-everywhere measurable. If two response variables g₁ and g₂ are μ-almost- everywhere equal, and f₁ is a regression-function representative of the conditional mean of g₁ given X while f₂ is a regression-function representative of the conditional mean of g₂ given X, then f₁ and f₂ agree (μ.map X)-almost everywhere.

Formal statement

hypotheses

Ω :

Type*

MeasurableSpace Ω

Measure Ω

Ω → ℝ

f₁ f₂ :

ℝ → ℝ

hX :

AEMeasurable X μ

hg :

g₁ =ᵐ[μ] g₂

h₁ :

IsRegressionFunction μ X g₁ f₁

h₂ :

IsRegressionFunction μ X g₂ f₂

conclusion

f₁ =ᵐ[μ.map X] f₂

Proof (Lean source)

lemma IsRegressionFunction.aeEq_of_aeEq_response {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {X : Ω → ℝ} {g₁ g₂ : Ω → ℝ} {f₁ f₂ : ℝ → ℝ} (hX : AEMeasurable X μ) (hg : g₁ =ᵐ[μ] g₂) (h₁ : IsRegressionFunction μ X g₁ f₁) (h₂ : IsRegressionFunction μ X g₂ f₂) : f₁ =ᵐ[μ.map X] f₂ := by refine MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq f₁ f₂ (h₁.integrable_pushforward hX) (h₂.integrable_pushforward hX) ?_ intro A hA _ have h_pull₁ : (∫ x in A, f₁ x ∂(μ.map X)) = ∫ ω in X ⁻¹' A, f₁ (X ω) ∂μ := setIntegral_map (μ := μ) (g := X) (f := f₁) hA h₁.measurable.aestronglyMeasurable hX have h_pull₂ : (∫ x in A, f₂ x ∂(μ.map X)) = ∫ ω in X ⁻¹' A, f₂ (X ω) ∂μ := setIntegral_map (μ := μ) (g := X) (f := f₂) hA h₂.measurable.aestronglyMeasurable hX have h_eq₁ : (∫ ω in X ⁻¹' A, f₁ (X ω) ∂μ) = ∫ ω in X ⁻¹' A, g₁ ω ∂μ := (h₁.integral_preimage_eq A hA).symm have h_eq₂ : (∫ ω in X ⁻¹' A, f₂ (X ω) ∂μ) = ∫ ω in X ⁻¹' A, g₂ ω ∂μ := (h₂.integral_preimage_eq A hA).symm have h_g_eq : (∫ ω in X ⁻¹' A, g₁ ω ∂μ) = ∫ ω in X ⁻¹' A, g₂ ω ∂μ := integral_congr_ae (ae_restrict_of_ae hg) rw [h_pull₁, h_pull₂, h_eq₁, h_eq₂, h_g_eq]

Causalean.PO.IsRegressionFunction.aeEq_of_aeEq_response · Causalean/PO/Analysis/Regression.lean:98 · uses IsRegressionFunction

2 supporting declarations (lemmas, instances)

integrable_pushforward lemma — Pushforward integrability: f is integrable under μ.map X whenever X is AEMeasurable and f represents E[g|X=·].

hypotheses

Ω :

Type u_1
Measure Ω
Ω → ℝ
Ω → ℝ
shared

f :

ℝ → ℝ
shared

h :

IsRegressionFunction μ X g f

hX :

AEMeasurable X μ

conclusion

Integrable f (μ.map X)

Proof (Lean source)

lemma integrable_pushforward (h : IsRegressionFunction μ X g f) (hX : AEMeasurable X μ) : Integrable f (μ.map X) := by rw [integrable_map_measure h.measurable.aestronglyMeasurable hX] exact h.integrable_compose

Causalean.PO.IsRegressionFunction.integrable_pushforward · Causalean/PO/Analysis/Regression.lean:64
sub lemma — Linearity (subtraction) of IsRegressionFunction: difference of representatives is the representative of the difference.

hypotheses

Ω :

Type*
MeasurableSpace Ω
Measure Ω
Ω → ℝ
Ω → ℝ

f₁ f₂ :

ℝ → ℝ

h₁ :

IsRegressionFunction μ X g₁ f₁

h₂ :

IsRegressionFunction μ X g₂ f₂

conclusion

IsRegressionFunction μ X (fun ω => g₁ ω - g₂ ω) (fun x => f₁ x - f₂ x) where measurable

Proof (Lean source)

lemma IsRegressionFunction.sub {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {X : Ω → ℝ} {g₁ g₂ : Ω → ℝ} {f₁ f₂ : ℝ → ℝ} (h₁ : IsRegressionFunction μ X g₁ f₁) (h₂ : IsRegressionFunction μ X g₂ f₂) : IsRegressionFunction μ X (fun ω => g₁ ω - g₂ ω) (fun x => f₁ x - f₂ x) where measurable := h₁.measurable.sub h₂.measurable integrable_response := h₁.integrable_response.sub h₂.integrable_response integrable_compose := h₁.integrable_compose.sub h₂.integrable_compose integral_preimage_eq A hA := by have h_lhs : (∫ ω in X ⁻¹' A, g₁ ω - g₂ ω ∂μ) = (∫ ω in X ⁻¹' A, g₁ ω ∂μ) - ∫ ω in X ⁻¹' A, g₂ ω ∂μ := integral_sub h₁.integrable_response.integrableOn h₂.integrable_response.integrableOn have h_rhs : (∫ ω in X ⁻¹' A, f₁ (X ω) - f₂ (X ω) ∂μ) = (∫ ω in X ⁻¹' A, f₁ (X ω) ∂μ) - ∫ ω in X ⁻¹' A, f₂ (X ω) ∂μ := integral_sub h₁.integrable_compose.integrableOn h₂.integrable_compose.integrableOn rw [h_lhs, h_rhs, h₁.integral_preimage_eq A hA, h₂.integral_preimage_eq A hA]

Causalean.PO.IsRegressionFunction.sub · Causalean/PO/Analysis/Regression.lean:74