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:32 · 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:51 · 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:58 · 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:64 · 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:76 · 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:82 · 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:39
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:89

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 almost-everywhere measurability of the conditioning variable, measurability of the representative, 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. The general conditional-expectation characterization for measurable preimages is in Causalean.Mathlib.MeasureTheory.CondExpPreimage; this file does not yet connect the two APIs.

structure IsRegressionFunction reviewed

Causalean.PO

A regression-function representative for the conditional mean of a response g given a conditioning variable X that is μ-almost-everywhere measurable: 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

aemeasurable_conditioner :

AEMeasurable X μ

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:49

lemma aeEq_of_aeEq_response reviewed

Causalean.PO.IsRegressionFunction

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₂ :

ℝ → ℝ

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₂ : ℝ → ℝ} (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 h₂.integrable_pushforward ?_ 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 h₁.aemeasurable_conditioner 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 h₂.aemeasurable_conditioner 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:111 · uses IsRegressionFunction

2 supporting declarations (lemmas, instances)

integrable_pushforward lemma — If f represents the conditional mean of g given X, then f is integrable under the pushforward measure μ.map X.

hypotheses

Ω :

Type u_1
Measure Ω
Ω → ℝ
Ω → ℝ
shared

f :

ℝ → ℝ
shared

h :

IsRegressionFunction μ X g f

conclusion

Integrable f (μ.map X)

Proof (Lean source)

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

Causalean.PO.IsRegressionFunction.integrable_pushforward · Causalean/PO/Analysis/Regression.lean:75
sub lemma — If f₁ represents the conditional mean of g₁ given X and f₂ represents the conditional mean of g₂ given X, then their difference represents the conditional mean of g₁ - g₂ given X.

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 aemeasurable_conditioner

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 aemeasurable_conditioner := h₁.aemeasurable_conditioner 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:85