PO.ID.Exact.RDD

fields

Running (forcing) variable `X`.

Xvar :

POVar P ℝ

Above-cutoff indicator `Z = 1{X ≥ c}`.

Zvar :

POVar P Bool

Binary treatment `D`.

Dvar :

POVar P Bool

Real outcome `Y`.

Yvar :

POVar P ℝ

Cutoff value of the running variable.

c :

ℝ

hYD :

Yvar.v ≠ Dvar.v

hZD :

Zvar.v ≠ Dvar.v

hDY :

Dvar.v ≠ Yvar.v

Causalean.PO.POFuzzyRDDSystem · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:55 · uses POSystem

def factualX reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system, the factual running variable assigns each unit its observed real-valued running variable.

Definition (Lean source)

parameters

P :

shared

S :

shared

def

factualX S :

P.Ω → ℝ

given by

S.Xvar.factual

Causalean.PO.POFuzzyRDDSystem.factualX · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:81 · uses POFuzzyRDDSystem , POSystem

def factualZ reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system, the factual cutoff-eligibility indicator assigns each unit its observed binary above-cutoff indicator.

Definition (Lean source)

parameters

P :

shared

S :

shared

def

factualZ S :

P.Ω → Bool

given by

S.Zvar.factual

Causalean.PO.POFuzzyRDDSystem.factualZ · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:84 · uses POFuzzyRDDSystem , POSystem

def factualD reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system, the factual treatment assigns each unit its observed binary treatment.

Definition (Lean source)

parameters

P :

shared

S :

shared

def

factualD S :

P.Ω → Bool

given by

S.Dvar.factual

Causalean.PO.POFuzzyRDDSystem.factualD · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:87 · uses POFuzzyRDDSystem , POSystem

def factualY reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system, the factual outcome assigns each unit its observed real outcome.

Definition (Lean source)

parameters

P :

shared

S :

shared

def

factualY S :

P.Ω → ℝ

given by

S.Yvar.factual

Causalean.PO.POFuzzyRDDSystem.factualY · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:90 · uses POFuzzyRDDSystem , POSystem

def DofZ reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system and an instrument value, the potential treatment assigns each unit the binary treatment it would take under that instrument value.

Definition (Lean source)

parameters

P :

shared

S :

shared

z :

def

DofZ S z :

P.Ω → Bool

given by

S.Dvar.cfUnder S.Zvar z

Causalean.PO.POFuzzyRDDSystem.DofZ · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:93 · uses POFuzzyRDDSystem , POSystem

def YofD reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system and a treatment value, the potential outcome assigns each unit the real outcome it would have under that treatment value.

Definition (Lean source)

parameters

P :

shared

S :

shared

d :

def

YofD S d :

P.Ω → ℝ

given by

S.Yvar.cfUnder S.Dvar d

Causalean.PO.POFuzzyRDDSystem.YofD · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:97 · uses POFuzzyRDDSystem , POSystem

def YofDofZ reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system and an instrument value, the instrument-induced potential outcome assigns each unit the potential outcome under the treatment that the instrument value would induce for that unit.

Definition (Lean source)

parameters

P :

shared

S :

shared

z :

def

YofDofZ S z :

P.Ω → ℝ

given by

fun ω => if S.DofZ z ω then S.YofD true ω else S.YofD false ω

Causalean.PO.POFuzzyRDDSystem.YofDofZ · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:101 · uses POFuzzyRDDSystem , POSystem

def YdiffComplier reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system, the complier-weighted outcome difference assigns each unit the difference between its treated and untreated potential outcomes when it is a complier, and zero otherwise.

Definition (Lean source)

parameters

P :

shared

S :

shared

def

YdiffComplier S :

P.Ω → ℝ

given by

fun ω => (S.YofD true ω - S.YofD false ω) * if S.DofZ true ω = true ∧

S.DofZ false ω = false then 1 else 0

Causalean.PO.POFuzzyRDDSystem.YdiffComplier · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:113 · uses POFuzzyRDDSystem , POSystem

def zEvent reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system and an instrument value, the eligibility event is the set of units whose observed above-cutoff indicator equals that value.

Definition (Lean source)

parameters

P :

shared

S :

shared

z :

def

zEvent S z :

Set P.Ω

given by

S.Zvar.event z

Causalean.PO.POFuzzyRDDSystem.zEvent · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:162 · uses POFuzzyRDDSystem , POSystem

structure Assumptions reviewed

Causalean.PO.POFuzzyRDDSystem

Fuzzy RDD assumption bundle. For a fuzzy regression-discontinuity system, this packages consistency (SUTVA), deterministic cutoff eligibility: the above-cutoff indicator agrees almost surely with whether the running variable has crossed the cutoff, and cutoff-neighborhood monotonicity: near the cutoff, a unit who would take treatment under the untreated instrument value would also take it under the treated instrument value. It supplies latent treatment and outcome regression representatives muD/muY and observable regression representatives nuD/nuY, each certified as a genuine regression function of the corresponding response on the running variable, with the latent representatives continuous at the cutoff; it also assumes the running variable has positive local probability mass on both sides of the cutoff, and that the observable treatment regression and outcome regression have well-defined one-sided limits at the cutoff. Finally, a complier outcome-difference representative mu_Ydiff_complier is likewise a regression function that is continuous at the cutoff, and the first-stage treatment-take-up jump at the cutoff is nonzero.

Definition (Lean source)

parameters

P :

shared

S :

fields

consistency :

P.Consistency

cutoffEligibility :

∀ᵐ ω ∂P.μ, S.factualZ ω ↔ S.c ≤ S.factualX ω

In a neighborhood of the cutoff, units who would take treatment below the cutoff would also take treatment above the cutoff, up to a null set.

monotonicity :

∃ ε > (0 : ℝ),

∀ᵐ ω ∂P.μ, |S.factualX ω - S.c| < ε → S.DofZ false ω = true → S.DofZ true ω = true

muD :

Bool → ℝ → ℝ

muY :

Bool → ℝ → ℝ

nuD :

ℝ → ℝ

nuY :

ℝ → ℝ

muD_isReg :

∀ z, IsRegressionFunction P.μ S.factualX (fun ω => ((S.DofZ z ω).toNat : ℝ)) (muD z)

muY_isReg :

∀ z, IsRegressionFunction P.μ S.factualX (S.YofDofZ z) (muY z)

nuD_isReg :

IsRegressionFunction P.μ S.factualX (fun ω => ((S.factualD ω).toNat : ℝ)) nuD

nuY_isReg :

IsRegressionFunction P.μ S.factualX S.factualY nuY

muD_continuousAt :

∀ z, ContinuousAt (muD z) S.c

muY_continuousAt :

∀ z, ContinuousAt (muY z) S.c

support_right :

∀ ε > (0 : ℝ), (P.μ.map S.factualX) (Ioo S.c (S.c + ε)) ≠ 0

support_left :

∀ ε > (0 : ℝ), (P.μ.map S.factualX) (Ioo (S.c - ε) S.c) ≠ 0

nuD_right_limit_exists :

∃ L : ℝ, Tendsto nuD (𝓝[>] S.c) (𝓝 L)

nuD_left_limit_exists :

∃ L : ℝ, Tendsto nuD (𝓝[<] S.c) (𝓝 L)

nuY_right_limit_exists :

∃ L : ℝ, Tendsto nuY (𝓝[>] S.c) (𝓝 L)

nuY_left_limit_exists :

∃ L : ℝ, Tendsto nuY (𝓝[<] S.c) (𝓝 L)

mu_Ydiff_complier :

ℝ → ℝ

mu_Ydiff_complier_isReg :

IsRegressionFunction P.μ S.factualX S.YdiffComplier mu_Ydiff_complier

mu_Ydiff_complier_continuousAt :

ContinuousAt mu_Ydiff_complier S.c

firstStageJump :

muD true S.c - muD false S.c ≠ 0

Causalean.PO.POFuzzyRDDSystem.Assumptions · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:169 · uses POFuzzyRDDSystem , POSystem

def tau_FRD reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system satisfying the fuzzy-RDD assumptions, the cutoff-local fuzzy-RDD Wald estimand is the difference between the treated- and untreated-instrument latent outcome regressions at the cutoff divided by the corresponding treatment-regression difference.

Definition (Lean source)

parameters

P :

shared

S :

shared

hA :

S.Assumptions

def

tau_FRD S hA :

ℝ

given by

(hA.muY true S.c - hA.muY false S.c) / (hA.muD true S.c - hA.muD false S.c)

Causalean.PO.POFuzzyRDDSystem.tau_FRD · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:229 · uses POFuzzyRDDSystem , Assumptions , POSystem

def tau_LATE reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system satisfying the fuzzy-RDD assumptions, the cutoff-local complier-effect ratio is the complier outcome-difference regression at the cutoff divided by the latent first-stage treatment-regression jump.

Definition (Lean source)

parameters

P :

shared

S :

shared

hA :

S.Assumptions

def

tau_LATE S hA :

ℝ

given by

hA.mu_Ydiff_complier S.c / (hA.muD true S.c - hA.muD false S.c)

Causalean.PO.POFuzzyRDDSystem.tau_LATE · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:234 · uses POFuzzyRDDSystem , Assumptions , POSystem

def nuD_right_limit reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system satisfying the fuzzy-RDD assumptions, the right-hand treatment-regression limit is the selected limit of the observed treatment regression as the running variable approaches the cutoff from above.

Definition (Lean source)

parameters

P :

shared

S :

shared

hA :

S.Assumptions

def

nuD_right_limit S hA :

ℝ

given by

choose hA.nuD_right_limit_exists

Causalean.PO.POFuzzyRDDSystem.nuD_right_limit · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:243 · uses POFuzzyRDDSystem , Assumptions , POSystem

def nuD_left_limit reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system satisfying the fuzzy-RDD assumptions, the left-hand treatment-regression limit is the selected limit of the observed treatment regression as the running variable approaches the cutoff from below.

Definition (Lean source)

parameters

P :

shared

S :

shared

hA :

S.Assumptions

def

nuD_left_limit S hA :

ℝ

given by

choose hA.nuD_left_limit_exists

Causalean.PO.POFuzzyRDDSystem.nuD_left_limit · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:250 · uses POFuzzyRDDSystem , Assumptions , POSystem

def nuY_right_limit reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system satisfying the fuzzy-RDD assumptions, the right-hand outcome-regression limit is the selected limit of the observed outcome regression as the running variable approaches the cutoff from above.

Definition (Lean source)

parameters

P :

shared

S :

shared

hA :

S.Assumptions

def

nuY_right_limit S hA :

ℝ

given by

choose hA.nuY_right_limit_exists

Causalean.PO.POFuzzyRDDSystem.nuY_right_limit · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:257 · uses POFuzzyRDDSystem , Assumptions , POSystem

def nuY_left_limit reviewed

Causalean.PO.POFuzzyRDDSystem

For a fuzzy regression-discontinuity system satisfying the fuzzy-RDD assumptions, the left-hand outcome-regression limit is the selected limit of the observed outcome regression as the running variable approaches the cutoff from below.

Definition (Lean source)

parameters

P :

shared

S :

shared

hA :

S.Assumptions

def

nuY_left_limit S hA :

ℝ

given by

choose hA.nuY_left_limit_exists

Causalean.PO.POFuzzyRDDSystem.nuY_left_limit · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:264 · uses POFuzzyRDDSystem , Assumptions , POSystem

theorem frd_identification reviewed

Causalean.PO.POFuzzyRDDSystem

Fuzzy RDD identification at the cutoff, in regression-representative form. Under the fuzzy-RDD identifying assumption bundle, the Wald ratio of the latent right- and left-hand representative jumps at the cutoff equals the Wald ratio of the one-sided observable outcome- and treatment-regression limits at the cutoff:

Formal statement

hypotheses

P :

shared

S :

shared

hA :

S.Assumptions

conclusion

S.tau_FRD hA

= (S.nuY_right_limit hA - S.nuY_left_limit hA) / (S.nuD_right_limit hA - S.nuD_left_limit hA)

Proof (Lean source)

theorem frd_identification (hA : S.Assumptions) : S.tau_FRD hA = (S.nuY_right_limit hA - S.nuY_left_limit hA) / (S.nuD_right_limit hA - S.nuD_left_limit hA) := by rw [show S.nuY_right_limit hA = hA.muY true S.c from S.nuY_right_limit_eq hA (S.tendsto_nuY_right_limit hA), show S.nuY_left_limit hA = hA.muY false S.c from S.nuY_left_limit_eq hA (S.tendsto_nuY_left_limit hA), show S.nuD_right_limit hA = hA.muD true S.c from S.nuD_right_limit_eq hA (S.tendsto_nuD_right_limit hA), show S.nuD_left_limit hA = hA.muD false S.c from S.nuD_left_limit_eq hA (S.tendsto_nuD_left_limit hA)] rfl

Causalean.PO.POFuzzyRDDSystem.frd_identification · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:606 · uses POFuzzyRDDSystem , Assumptions , nuD_left_limit , nuD_right_limit , nuY_left_limit , nuY_right_limit , tau_FRD , POSystem

theorem tau_late_identification reviewed

Causalean.PO.POFuzzyRDDSystem

Fuzzy RDD identifies a cutoff representative complier ratio under an extra global monotonicity bridge. Under the local fuzzy-RDD identifying assumption bundle — consistency, deterministic cutoff eligibility, and local exclusion through potential outcomes, and additionally assuming treatment is almost-surely monotone in the instrument, i.e. whenever the potential treatment under the untreated instrument value is realized as true, the potential treatment under the treated instrument value is true as well (no defiers), the complier-weighted local average treatment effect at the cutoff tau_LATE equals the fuzzy-RDD Wald-ratio functional tau_FRD, i.e. the observable Wald ratio at the cutoff equals the complier-weighted outcome-difference representative divided by the first-stage jump.

Formal statement

hypotheses

P :

shared

S :

shared

hA :

S.Assumptions

hmono :

∀ᵐ ω ∂P.μ, S.DofZ false ω = true → S.DofZ true ω = true

conclusion

S.tau_LATE hA = S.tau_FRD hA

Proof (Lean source)

theorem tau_late_identification (hA : S.Assumptions) (hmono : ∀ᵐ ω ∂P.μ, S.DofZ false ω = true → S.DofZ true ω = true) : S.tau_LATE hA = S.tau_FRD hA := by simp only [tau_LATE, tau_FRD] congr 1 exact (S.muY_diff_eq_mu_Ydiff_complier_at_cutoff hA hmono).symm

Causalean.PO.POFuzzyRDDSystem.tau_late_identification · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:662 · uses POFuzzyRDDSystem , Assumptions , DofZ , tau_FRD , tau_LATE , POSystem

19 supporting declarations (lemmas, instances)

YofDofZ_def lemma — The potential outcome under the treatment that an instrument value induces sends a unit to that unit's treated potential outcome when the induced treatment is one, and to its untreated potential outcome otherwise.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

z :

Bool

conclusion

S.YofDofZ z = fun ω => if S.DofZ z ω then S.YofD true ω else S.YofD false ω

Proof (Lean source)

@[causal_defs_simps] lemma YofDofZ_def (z : Bool) : S.YofDofZ z = fun ω => if S.DofZ z ω then S.YofD true ω else S.YofD false ω := rfl

Causalean.PO.POFuzzyRDDSystem.YofDofZ_def · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:105
measurable_factualX lemma — The factual running variable is measurable.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

conclusion

Measurable S.factualX

Proof (Lean source)

@[fun_prop] lemma measurable_factualX : Measurable S.factualX := S.Xvar.measurable_factual

Causalean.PO.POFuzzyRDDSystem.measurable_factualX · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:121
measurable_factualZ lemma — The factual cutoff-eligibility instrument is measurable.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

conclusion

Measurable S.factualZ

Proof (Lean source)

@[fun_prop] lemma measurable_factualZ : Measurable S.factualZ := S.Zvar.measurable_factual

Causalean.PO.POFuzzyRDDSystem.measurable_factualZ · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:124
measurable_factualD lemma — The factual treatment is measurable.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

conclusion

Measurable S.factualD

Proof (Lean source)

@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.Dvar.measurable_factual

Causalean.PO.POFuzzyRDDSystem.measurable_factualD · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:127
measurable_factualY lemma — The factual outcome is measurable.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

conclusion

Measurable S.factualY

Proof (Lean source)

@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.Yvar.measurable_factual

Causalean.PO.POFuzzyRDDSystem.measurable_factualY · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:130
measurable_DofZ lemma — The instrument-specific potential treatment is measurable.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

z :

Bool

conclusion

Measurable (S.DofZ z)

Proof (Lean source)

@[fun_prop] lemma measurable_DofZ (z : Bool) : Measurable (S.DofZ z) := S.Dvar.measurable_cfUnder S.Zvar z

Causalean.PO.POFuzzyRDDSystem.measurable_DofZ · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:134
measurable_YofD lemma — The treatment-specific potential outcome is measurable.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

d :

Bool

conclusion

Measurable (S.YofD d)

Proof (Lean source)

@[fun_prop] lemma measurable_YofD (d : Bool) : Measurable (S.YofD d) := S.Yvar.measurable_cfUnder S.Dvar d

Causalean.PO.POFuzzyRDDSystem.measurable_YofD · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:139
measurable_YofDofZ lemma — The outcome under the instrument-induced treatment is measurable.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

z :

Bool

conclusion

Measurable (S.YofDofZ z)

Proof (Lean source)

@[fun_prop] lemma measurable_YofDofZ (z : Bool) : Measurable (S.YofDofZ z) := by simp only [causal_defs_simps] exact Measurable.ite (S.measurable_DofZ z (MeasurableSet.singleton true)) (S.measurable_YofD true) (S.measurable_YofD false)

Causalean.PO.POFuzzyRDDSystem.measurable_YofDofZ · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:144
measurable_YdiffComplier lemma — The complier-weighted outcome difference is measurable.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

conclusion

Measurable S.YdiffComplier

Proof (Lean source)

@[fun_prop] lemma measurable_YdiffComplier : Measurable S.YdiffComplier := by unfold YdiffComplier apply mul · exact (S.measurable_YofD true).sub (S.measurable_YofD false) · exact Measurable.ite ((S.measurable_DofZ true (MeasurableSet.singleton true)).inter (S.measurable_DofZ false (MeasurableSet.singleton false))) measurable_const measurable_const

Causalean.PO.POFuzzyRDDSystem.measurable_YdiffComplier · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:151
measurableSet_zEvent lemma — The factual eligibility event is measurable.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

z :

Bool

conclusion

MeasurableSet (S.zEvent z)

Proof (Lean source)

lemma measurableSet_zEvent (z : Bool) : MeasurableSet (S.zEvent z) := by simpa [zEvent] using S.Zvar.measurableSet_event z

Causalean.PO.POFuzzyRDDSystem.measurableSet_zEvent · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:165
tendsto_nuD_right_limit lemma — The chosen right-hand treatment-regression limit is a genuine right-hand limit at the cutoff.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

hA :

S.Assumptions

conclusion

Tendsto hA.nuD (𝓝[>] S.c) (𝓝 (S.nuD_right_limit hA))

Proof (Lean source)

lemma tendsto_nuD_right_limit (hA : S.Assumptions) : Tendsto hA.nuD (𝓝[>] S.c) (𝓝 (S.nuD_right_limit hA)) := Classical.choose_spec hA.nuD_right_limit_exists

Causalean.PO.POFuzzyRDDSystem.tendsto_nuD_right_limit · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:271
tendsto_nuD_left_limit lemma — The chosen left-hand treatment-regression limit is a genuine left-hand limit at the cutoff.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

hA :

S.Assumptions

conclusion

Tendsto hA.nuD (𝓝[<] S.c) (𝓝 (S.nuD_left_limit hA))

Proof (Lean source)

lemma tendsto_nuD_left_limit (hA : S.Assumptions) : Tendsto hA.nuD (𝓝[<] S.c) (𝓝 (S.nuD_left_limit hA)) := Classical.choose_spec hA.nuD_left_limit_exists

Causalean.PO.POFuzzyRDDSystem.tendsto_nuD_left_limit · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:277
tendsto_nuY_right_limit lemma — The chosen right-hand outcome-regression limit is a genuine right-hand limit at the cutoff.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

hA :

S.Assumptions

conclusion

Tendsto hA.nuY (𝓝[>] S.c) (𝓝 (S.nuY_right_limit hA))

Proof (Lean source)

lemma tendsto_nuY_right_limit (hA : S.Assumptions) : Tendsto hA.nuY (𝓝[>] S.c) (𝓝 (S.nuY_right_limit hA)) := Classical.choose_spec hA.nuY_right_limit_exists

Causalean.PO.POFuzzyRDDSystem.tendsto_nuY_right_limit · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:283
tendsto_nuY_left_limit lemma — The chosen left-hand outcome-regression limit is a genuine left-hand limit at the cutoff.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

hA :

S.Assumptions

conclusion

Tendsto hA.nuY (𝓝[<] S.c) (𝓝 (S.nuY_left_limit hA))

Proof (Lean source)

lemma tendsto_nuY_left_limit (hA : S.Assumptions) : Tendsto hA.nuY (𝓝[<] S.c) (𝓝 (S.nuY_left_limit hA)) := Classical.choose_spec hA.nuY_left_limit_exists

Causalean.PO.POFuzzyRDDSystem.tendsto_nuY_left_limit · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:289
aemeasurable_factualX lemma — The observed running variable is almost-everywhere measurable.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P

conclusion

AEMeasurable S.factualX P.μ

Proof (Lean source)

@[fun_prop] lemma aemeasurable_factualX (S : POFuzzyRDDSystem P) : AEMeasurable S.factualX P.μ := S.measurable_factualX.aemeasurable

Causalean.PO.POFuzzyRDDSystem.aemeasurable_factualX · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:295
nuD_right_limit_eq theorem — Any right-hand observable treatment-regression limit at the cutoff equals the treated latent treatment regression there.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

hA :

S.Assumptions

L :

ℝ

h :

Tendsto hA.nuD (𝓝[>] S.c) (𝓝 L)

conclusion

L = hA.muD true S.c

Proof (Lean source)

theorem nuD_right_limit_eq (hA : S.Assumptions) {L : ℝ} (h : Tendsto hA.nuD (𝓝[>] S.c) (𝓝 L)) : L = hA.muD true S.c := RDDLimits.oneSidedLimit_eq_right (S.nuD_eq_muD_true_ae_restrict_Ici hA) (hA.muD_continuousAt true) hA.support_right h

Causalean.PO.POFuzzyRDDSystem.nuD_right_limit_eq · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:560
nuD_left_limit_eq theorem — Any left-hand observable treatment-regression limit at the cutoff equals the untreated latent treatment regression there.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

hA :

S.Assumptions

L :

ℝ

h :

Tendsto hA.nuD (𝓝[<] S.c) (𝓝 L)

conclusion

L = hA.muD false S.c

Proof (Lean source)

theorem nuD_left_limit_eq (hA : S.Assumptions) {L : ℝ} (h : Tendsto hA.nuD (𝓝[<] S.c) (𝓝 L)) : L = hA.muD false S.c := RDDLimits.oneSidedLimit_eq_left (S.nuD_eq_muD_false_ae_restrict_Iio hA) (hA.muD_continuousAt false) hA.support_left h

Causalean.PO.POFuzzyRDDSystem.nuD_left_limit_eq · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:571
nuY_right_limit_eq theorem — Any right-hand observable outcome-regression limit at the cutoff equals the treated latent outcome regression there.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

hA :

S.Assumptions

L :

ℝ

h :

Tendsto hA.nuY (𝓝[>] S.c) (𝓝 L)

conclusion

L = hA.muY true S.c

Proof (Lean source)

theorem nuY_right_limit_eq (hA : S.Assumptions) {L : ℝ} (h : Tendsto hA.nuY (𝓝[>] S.c) (𝓝 L)) : L = hA.muY true S.c := RDDLimits.oneSidedLimit_eq_right (S.nuY_eq_muY_true_ae_restrict_Ici hA) (hA.muY_continuousAt true) hA.support_right h

Causalean.PO.POFuzzyRDDSystem.nuY_right_limit_eq · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:582
nuY_left_limit_eq theorem — Any left-hand observable outcome-regression limit at the cutoff equals the untreated latent outcome regression there.

hypotheses

P :

POSystem
shared

S :

POFuzzyRDDSystem P
shared

hA :

S.Assumptions

L :

ℝ

h :

Tendsto hA.nuY (𝓝[<] S.c) (𝓝 L)

conclusion

L = hA.muY false S.c

Proof (Lean source)

theorem nuY_left_limit_eq (hA : S.Assumptions) {L : ℝ} (h : Tendsto hA.nuY (𝓝[<] S.c) (𝓝 L)) : L = hA.muY false S.c := RDDLimits.oneSidedLimit_eq_left (S.nuY_eq_muY_false_ae_restrict_Iio hA) (hA.muY_continuousAt false) hA.support_left h

Causalean.PO.POFuzzyRDDSystem.nuY_left_limit_eq · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:593

RDDLimits 1 core · 3 supporting This file provides the one-sided limit engine used by sharp and fuzzy regression-discontinuity identification. ★ oneSidedLimit_eq_left

RDD One-Sided Limits

This file provides the one-sided limit engine used by sharp and fuzzy regression-discontinuity identification. If two real-valued functions agree almost everywhere on the relevant side of a cutoff and the reference function is continuous at the cutoff, then any corresponding one-sided limit of the other function equals the reference value at the cutoff, provided the running variable law has positive mass arbitrarily close to that side.

Theorems oneSidedLimit_eq_right and oneSidedLimit_eq_left identify right- and left-hand limits from one-sided a.e. agreement. The pointwise versions value_eq_of_aeEq_right and value_eq_of_aeEq_left identify the cutoff values of two continuous representatives. These results isolate the topological and measure-theoretic argument from the causal RDD files.

theorem oneSidedLimit_eq_left reviewed

Causalean.PO.RDDLimits

Left-side limit identification. Symmetric form of oneSidedLimit_eq_right. If a real-valued function f agrees with a reference function g almost everywhere, with respect to a measure π, on the half-line to the left of the cutoff c, g is continuous at c, and every open interval immediately to the left of c has positive π-measure, then any left-hand limit L of f at c must equal g evaluated at c.

Formal statement

hypotheses

π :

Measure ℝ

shared

f :

ℝ → ℝ

shared

g :

ℝ → ℝ

shared

c :

ℝ

shared

h_aeEq :

f =ᵐ[π.restrict (Iio c)] g

hg_cont :

ContinuousAt g c

h_support :

∀ ε > (0 : ℝ), π (Ioo (c - ε) c) ≠ 0

L :

ℝ

hL :

Tendsto f (𝓝[<] c) (𝓝 L)

conclusion

L = g c

Proof (Lean source)

theorem oneSidedLimit_eq_left (h_aeEq : f =ᵐ[π.restrict (Iio c)] g) (hg_cont : ContinuousAt g c) (h_support : ∀ ε > (0 : ℝ), π (Ioo (c - ε) c) ≠ 0) {L : ℝ} (hL : Tendsto f (𝓝[<] c) (𝓝 L)) : L = g c := by haveI : (𝓝[<] c ⊓ Filter.principal {x | f x = g x}).NeBot := neBot_left h_aeEq h_support have h_f : Tendsto f (𝓝[<] c ⊓ Filter.principal {x | f x = g x}) (𝓝 L) := hL.mono_left inf_le_left have h_g_full : Tendsto g (𝓝[<] c) (𝓝 (g c)) := hg_cont.tendsto.mono_left inf_le_left have h_g : Tendsto g (𝓝[<] c ⊓ Filter.principal {x | f x = g x}) (𝓝 (g c)) := h_g_full.mono_left inf_le_left have h_eq : f =ᶠ[𝓝[<] c ⊓ Filter.principal {x | f x = g x}] g := by refine Filter.eventually_iff_exists_mem.mpr ?_ refine ⟨{x | f x = g x}, ?_, fun x hx => hx⟩ exact mem_inf_of_right (mem_principal_self _) have h_f' : Tendsto g (𝓝[<] c ⊓ Filter.principal {x | f x = g x}) (𝓝 L) := h_f.congr' h_eq exact tendsto_nhds_unique h_f' h_g

Causalean.PO.RDDLimits.oneSidedLimit_eq_left · Causalean/PO/ID/Exact/RDD/RDDLimits.lean:122

3 supporting declarations (lemmas, instances)

oneSidedLimit_eq_right theorem — Right-side limit identification. If f =ᵐ[π.restrict (Ici c)] g, g is continuous at c, every right-open neighborhood of c has positive π-mass, and f has any right-side limit L at c, then L = g c.

hypotheses

π :

Measure ℝ
shared

f :

ℝ → ℝ
shared

g :

ℝ → ℝ
shared

c :

ℝ
shared

h_aeEq :

f =ᵐ[π.restrict (Ici c)] g

hg_cont :

ContinuousAt g c

h_support :

∀ ε > (0 : ℝ), π (Ioo c (c + ε)) ≠ 0

L :

ℝ

hL :

Tendsto f (𝓝[>] c) (𝓝 L)

conclusion

L = g c

Proof (Lean source)

theorem oneSidedLimit_eq_right (h_aeEq : f =ᵐ[π.restrict (Ici c)] g) (hg_cont : ContinuousAt g c) (h_support : ∀ ε > (0 : ℝ), π (Ioo c (c + ε)) ≠ 0) {L : ℝ} (hL : Tendsto f (𝓝[>] c) (𝓝 L)) : L = g c := by haveI : (𝓝[>] c ⊓ Filter.principal {x | f x = g x}).NeBot := neBot_right h_aeEq h_support have h_f : Tendsto f (𝓝[>] c ⊓ Filter.principal {x | f x = g x}) (𝓝 L) := hL.mono_left inf_le_left have h_g_full : Tendsto g (𝓝[>] c) (𝓝 (g c)) := hg_cont.tendsto.mono_left inf_le_left have h_g : Tendsto g (𝓝[>] c ⊓ Filter.principal {x | f x = g x}) (𝓝 (g c)) := h_g_full.mono_left inf_le_left have h_eq : f =ᶠ[𝓝[>] c ⊓ Filter.principal {x | f x = g x}] g := by refine Filter.eventually_iff_exists_mem.mpr ?_ refine ⟨{x | f x = g x}, ?_, fun x hx => hx⟩ exact mem_inf_of_right (mem_principal_self _) have h_f' : Tendsto g (𝓝[>] c ⊓ Filter.principal {x | f x = g x}) (𝓝 L) := h_f.congr' h_eq exact tendsto_nhds_unique h_f' h_g

Causalean.PO.RDDLimits.oneSidedLimit_eq_right · Causalean/PO/ID/Exact/RDD/RDDLimits.lean:89
value_eq_of_aeEq_right theorem — Pointwise equality from a.e. agreement plus continuity. If f and g agree π.restrict (Ici c)-a.e., both are continuous at c, and every right-open neighborhood of c has positive π-mass, then f c = g c.

hypotheses

π :

Measure ℝ
shared

f :

ℝ → ℝ
shared

g :

ℝ → ℝ
shared

c :

ℝ
shared

h_aeEq :

f =ᵐ[π.restrict (Ici c)] g

hf_cont :

ContinuousAt f c

hg_cont :

ContinuousAt g c

h_support :

∀ ε > (0 : ℝ), π (Ioo c (c + ε)) ≠ 0

conclusion

f c = g c

Proof (Lean source)

theorem value_eq_of_aeEq_right (h_aeEq : f =ᵐ[π.restrict (Ici c)] g) (hf_cont : ContinuousAt f c) (hg_cont : ContinuousAt g c) (h_support : ∀ ε > (0 : ℝ), π (Ioo c (c + ε)) ≠ 0) : f c = g c := by have hL : Tendsto f (𝓝[>] c) (𝓝 (f c)) := hf_cont.tendsto.mono_left nhdsWithin_le_nhds exact oneSidedLimit_eq_right h_aeEq hg_cont h_support hL

Causalean.PO.RDDLimits.value_eq_of_aeEq_right · Causalean/PO/ID/Exact/RDD/RDDLimits.lean:158
value_eq_of_aeEq_left theorem — Symmetric pointwise version of value_eq_of_aeEq_right.

hypotheses

π :

Measure ℝ
shared

f :

ℝ → ℝ
shared

g :

ℝ → ℝ
shared

c :

ℝ
shared

h_aeEq :

f =ᵐ[π.restrict (Iio c)] g

hf_cont :

ContinuousAt f c

hg_cont :

ContinuousAt g c

h_support :

∀ ε > (0 : ℝ), π (Ioo (c - ε) c) ≠ 0

conclusion

f c = g c

Proof (Lean source)

theorem value_eq_of_aeEq_left (h_aeEq : f =ᵐ[π.restrict (Iio c)] g) (hf_cont : ContinuousAt f c) (hg_cont : ContinuousAt g c) (h_support : ∀ ε > (0 : ℝ), π (Ioo (c - ε) c) ≠ 0) : f c = g c := by have hL : Tendsto f (𝓝[<] c) (𝓝 (f c)) := hf_cont.tendsto.mono_left nhdsWithin_le_nhds exact oneSidedLimit_eq_left h_aeEq hg_cont h_support hL

Causalean.PO.RDDLimits.value_eq_of_aeEq_left · Causalean/PO/ID/Exact/RDD/RDDLimits.lean:170

SharpRDD 11 core · 10 supporting This file formalizes sharp regression-discontinuity identification in the potential-outcome framework. ★ POSharpRDDSystem★ rdd_identification

Sharp Regression Discontinuity

This file formalizes sharp regression-discontinuity identification in the potential-outcome framework. Under consistency, the deterministic cutoff rule, local support of the running variable on both sides of the cutoff, and continuity of the treatment-specific regressions, the cutoff effect equals the difference between the right and left limits of the observed outcome regression.

The proof reduces the sharp cutoff to half-line agreement between observable and potential-outcome regressions, then invokes the shared one-sided limit engine for regression-discontinuity designs.

structure POSharpRDDSystem reviewed

Causalean.PO

Sharp regression-discontinuity model in the potential-outcome framework. A unit has a continuous running variable X, a deterministic treatment D that switches on exactly when X crosses the cutoff c, jumping from 0 to 1 at the cutoff, and a real outcome Y, with the outcome and treatment nodes distinct. The jump in the outcome regression at the cutoff identifies the cutoff-local average treatment effect (def:po-sharp-rdd-system).

Definition (Lean source)

parameters

P :

fields

Running (forcing) variable `X`.

Xvar :

POVar P ℝ

Binary treatment `D` (deterministic given `X` at the cutoff).

Dvar :

POVar P Bool

Real outcome `Y`.

Yvar :

POVar P ℝ

Cutoff value of the running variable.

c :

ℝ

hYD :

Yvar.v ≠ Dvar.v

Causalean.PO.POSharpRDDSystem · Causalean/PO/ID/Exact/RDD/SharpRDD.lean:29 · uses POSystem

def factualX reviewed

Causalean.PO.POSharpRDDSystem

For a sharp regression-discontinuity system, the factual running variable assigns to each unit its real-valued forcing variable under the factual regime.

Definition (Lean source)

parameters

P :

shared

S :

shared

def

factualX S :

P.Ω → ℝ

given by

S.Xvar.factual

Causalean.PO.POSharpRDDSystem.factualX · Causalean/PO/ID/Exact/RDD/SharpRDD.lean:50 · uses POSharpRDDSystem , POSystem

def factualD reviewed

Causalean.PO.POSharpRDDSystem

For a sharp regression-discontinuity system, the factual treatment assigns to each unit its binary treatment under the factual regime.

Definition (Lean source)

parameters

P :

shared

S :

shared

def

factualD S :

P.Ω → Bool

given by

S.Dvar.factual

Causalean.PO.POSharpRDDSystem.factualD · Causalean/PO/ID/Exact/RDD/SharpRDD.lean:53 · uses POSharpRDDSystem , POSystem

def factualY reviewed

Causalean.PO.POSharpRDDSystem

For a sharp regression-discontinuity system, the factual outcome assigns to each unit its real-valued outcome under the factual regime.

Definition (Lean source)

parameters

P :

shared

S :

shared

def

factualY S :

P.Ω → ℝ

given by

S.Yvar.factual

Causalean.PO.POSharpRDDSystem.factualY · Causalean/PO/ID/Exact/RDD/SharpRDD.lean:56 · uses POSharpRDDSystem , POSystem

def YofD reviewed

Causalean.PO.POSharpRDDSystem

For a sharp regression-discontinuity system and a binary treatment level, the treatment-specific potential outcome assigns to each unit the outcome it would have under an intervention setting treatment to that level.

Definition (Lean source)

parameters

P :

shared

S :

shared

d :

def

YofD S d :

P.Ω → ℝ

given by

S.Yvar.cfUnder S.Dvar d

Causalean.PO.POSharpRDDSystem.YofD · Causalean/PO/ID/Exact/RDD/SharpRDD.lean:59 · uses POSharpRDDSystem , POSystem

def dEvent reviewed

Causalean.PO.POSharpRDDSystem

For a sharp regression-discontinuity system and a binary treatment level, the factual-treatment event is the set of units whose factual treatment equals that level.

Definition (Lean source)

parameters

P :

shared

S :

shared

d :

def

dEvent S d :

Set P.Ω

given by

S.Dvar.event d

Causalean.PO.POSharpRDDSystem.dEvent · Causalean/PO/ID/Exact/RDD/SharpRDD.lean:76 · uses POSharpRDDSystem , POSystem

structure Assumptions reviewed

Causalean.PO.POSharpRDDSystem

Sharp RDD assumption bundle (def:po-sharp-rdd-assumptions). For a sharp regression-discontinuity system, this packages consistency (SUTVA) and the deterministic cutoff rule: the treatment indicator agrees almost surely with whether the running variable has reached the cutoff. It supplies treatment-specific latent regression representatives mu and an observable outcome regression representative nu, each certified as a genuine regression function of the corresponding response on the running variable, with the latent representatives continuous at the cutoff; it also assumes the running variable has positive local probability mass on both sides of the cutoff and the observable outcome regression has well-defined one-sided limits at the cutoff.

Definition (Lean source)

parameters

P :

shared

S :

fields

consistency :

P.Consistency

sharpCutoff :

∀ᵐ ω ∂P.μ, S.factualD ω ↔ S.c ≤ S.factualX ω

mu :

Bool → ℝ → ℝ

nu :

ℝ → ℝ

mu_isReg :

∀ d, IsRegressionFunction P.μ S.factualX (S.YofD d) (mu d)

nu_isReg :

IsRegressionFunction P.μ S.factualX S.factualY nu

mu_continuousAt :

∀ d, ContinuousAt (mu d) S.c

support_right :

∀ ε > (0 : ℝ), (P.μ.map S.factualX) (Ioo S.c (S.c + ε)) ≠ 0

support_left :

∀ ε > (0 : ℝ), (P.μ.map S.factualX) (Ioo (S.c - ε) S.c) ≠ 0

nu_right_limit_exists :

∃ L : ℝ, Tendsto nu (𝓝[>] S.c) (𝓝 L)

nu_left_limit_exists :

∃ L : ℝ, Tendsto nu (𝓝[<] S.c) (𝓝 L)

Causalean.PO.POSharpRDDSystem.Assumptions · Causalean/PO/ID/Exact/RDD/SharpRDD.lean:83 · uses POSharpRDDSystem , POSystem

def tau_RDD reviewed

Causalean.PO.POSharpRDDSystem

For a sharp regression-discontinuity system satisfying its sharp-RDD assumptions, the cutoff-local regression-discontinuity estimand is the treated treatment-specific regression representative at the cutoff minus the untreated representative there.

Definition (Lean source)

parameters

P :

shared

S :

shared

hA :

S.Assumptions

def

tau_RDD S hA :

ℝ

given by

hA.mu true S.c - hA.mu false S.c

Causalean.PO.POSharpRDDSystem.tau_RDD · Causalean/PO/ID/Exact/RDD/SharpRDD.lean:115 · uses POSharpRDDSystem , Assumptions , POSystem

def nu_right_limit reviewed

Causalean.PO.POSharpRDDSystem

For a sharp regression-discontinuity system satisfying its sharp-RDD assumptions, the chosen right-hand limit of the observable outcome regression at the cutoff is the real number supplied by the assumption that this one-sided limit exists.

Definition (Lean source)

parameters

P :

shared

S :

shared

hA :

S.Assumptions

def

nu_right_limit S hA :

ℝ

given by

choose hA.nu_right_limit_exists

Causalean.PO.POSharpRDDSystem.nu_right_limit · Causalean/PO/ID/Exact/RDD/SharpRDD.lean:122 · uses POSharpRDDSystem , Assumptions , POSystem

def nu_left_limit reviewed

Causalean.PO.POSharpRDDSystem

For a sharp regression-discontinuity system satisfying its sharp-RDD assumptions, the chosen left-hand limit of the observable outcome regression at the cutoff is the real number supplied by the assumption that this one-sided limit exists.

Definition (Lean source)

parameters

P :

shared

S :

shared

hA :

S.Assumptions

def

nu_left_limit S hA :

ℝ

given by

choose hA.nu_left_limit_exists

Causalean.PO.POSharpRDDSystem.nu_left_limit · Causalean/PO/ID/Exact/RDD/SharpRDD.lean:129 · uses POSharpRDDSystem , Assumptions , POSystem

theorem rdd_identification reviewed

Causalean.PO.POSharpRDDSystem

Sharp RDD identification at the cutoff (textbook form). Under the sharp-RDD assumption bundle — SUTVA consistency, deterministic treatment assignment D = 1{X ≥ c} almost surely, regression-function representatives for the potential and observed outcomes, continuity of the potential-outcome regression functions at the cutoff, positive local mass of the running variable on each side of c, and existence of both one-sided limits of the observed-outcome regression function at c, the cutoff-local treatment effect equals the difference of the right- and left-hand limits of the observed-outcome regression function at the cutoff:

Formal statement

hypotheses

P :

shared

S :