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 real-valued potential-outcome variable, an intervention regime, and a measure on the sample space, this is the distribution of the variable's potential outcome under the regime, obtained by pushing that measure forward through the counterfactual-value function.

Definition (Lean source)

noncomputable def cfLaw (r : Regime P.V P.X) (μ : Measure P.Ω) : Measure ℝ := μ.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 real-valued potential-outcome variable, an intervention regime, and a measure on the sample space, this is the cumulative distribution function of the variable's potential outcome under that regime with respect to that measure.

Definition (Lean source)

noncomputable def cfCDF (r : Regime P.V P.X) (μ : Measure P.Ω) : StieltjesFunction ℝ := cdf (a.cfLaw r μ)

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

def cfQuantile reviewed

Causalean.PO.POVar

For a real-valued potential-outcome variable, an intervention regime, a measure on the sample space, and a real index $\tau$ , this is the $\tau$ -quantile of the variable's potential outcome under that regime with respect to that measure.

Definition (Lean source)

noncomputable def cfQuantile (r : Regime P.V P.X) (μ : Measure P.Ω) (τ : ℝ) : ℝ := quantile (a.cfLaw r μ) τ

Causalean.PO.POVar.cfQuantile · Causalean/PO/Analysis/Quantile.lean:54 · 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

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:63 · uses POSystem , POVar , cfCDF , cfLaw , Regime

def cfUnderLaw reviewed

Causalean.PO.POVar

For a real-valued potential-outcome variable, another potential-outcome variable, a value of the second variable, and a measure on the sample space, this is the distribution of the first variable's potential outcome under the single-variable intervention that sets the second variable to that value.

Definition (Lean source)

noncomputable def cfUnderLaw (w : POVar P β) (y : β) (μ : Measure P.Ω) : Measure ℝ := a.cfLaw (Regime.single w.v (w.equiv.symm y)) μ

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

def cfUnderQuantile reviewed

Causalean.PO.POVar

For a real-valued potential-outcome variable, another potential-outcome variable, a value of the second variable, a measure on the sample space, and a real index $\tau$ , this is the $\tau$ -quantile of the first variable's potential outcome under the single-variable intervention that sets the second variable to that value.

Definition (Lean source)

noncomputable def cfUnderQuantile (w : POVar P β) (y : β) (μ : Measure P.Ω) (τ : ℝ) : ℝ := a.cfQuantile (Regime.single w.v (w.equiv.symm y)) μ τ

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

2 supporting declarations (lemmas, instances)

instIsProbabilityMeasureCfLaw instance — The law of a real-valued potential outcome is a probability measure whenever the original sample-space measure is a probability measure.

instance instIsProbabilityMeasureCfLaw (r : Regime P.V P.X) (μ : Measure P.Ω) [IsProbabilityMeasure μ] : IsProbabilityMeasure (a.cfLaw r μ) := 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

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

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 :

ℝ → ℝ

fields

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

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