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:62 · uses POSystem

def factualX reviewed

Causalean.PO.POFuzzyRDDSystem

The observed running variable in a fuzzy regression-discontinuity design records each unit's realized forcing score, whose position around the cutoff determines eligibility.

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:87 · uses POFuzzyRDDSystem , POSystem

def factualZ reviewed

Causalean.PO.POFuzzyRDDSystem

The observed cutoff-eligibility indicator in a fuzzy regression-discontinuity design records whether each unit lies above the cutoff, serving as the instrument for treatment take-up.

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:92 · uses POFuzzyRDDSystem , POSystem

def factualD reviewed

Causalean.PO.POFuzzyRDDSystem

The observed treatment in a fuzzy regression-discontinuity design records each unit's realized take-up, which may differ from cutoff eligibility.

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:97 · uses POFuzzyRDDSystem , POSystem

def factualY reviewed

Causalean.PO.POFuzzyRDDSystem

The observed outcome in a fuzzy regression-discontinuity design records each unit's realized real-valued response.

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:101 · uses POFuzzyRDDSystem , POSystem

def DofZ reviewed

Causalean.PO.POFuzzyRDDSystem

The eligibility-specific potential treatment in a fuzzy regression-discontinuity design records whether each unit would take treatment under the selected eligibility state, with that state indexing the first stage.

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:105 · uses POFuzzyRDDSystem , POSystem

def YofD reviewed

Causalean.PO.POFuzzyRDDSystem

The treatment-specific potential outcome in a fuzzy regression-discontinuity design records each unit's response if treatment were set to the selected level, with that level defining the causal outcome contrast.

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:112 · uses POFuzzyRDDSystem , POSystem

def YofDofZ reviewed

Causalean.PO.POFuzzyRDDSystem

The outcome induced by an eligibility state in a fuzzy regression-discontinuity design selects each unit's treated or untreated potential outcome according to the treatment that eligibility would induce, with the eligibility state indexing the reduced form.

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:119 · uses POFuzzyRDDSystem , POSystem

def YdiffComplier reviewed

Causalean.PO.POFuzzyRDDSystem

The complier-weighted potential-outcome contrast in a fuzzy regression-discontinuity design equals the individual treatment effect for compliers and zero for everyone else.

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:134 · uses POFuzzyRDDSystem , POSystem

def zEvent reviewed

Causalean.PO.POFuzzyRDDSystem

The observed eligibility group in a fuzzy regression-discontinuity design collects units with the selected cutoff-eligibility state, with that state distinguishing the two sides.

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:196 · 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:206 · uses POFuzzyRDDSystem , POSystem

def tau_FRD reviewed

Causalean.PO.POFuzzyRDDSystem

The cutoff fuzzy-RDD Wald estimand for a fuzzy regression-discontinuity design under the identifying assumptions divides the eligibility-induced outcome-regression jump by the first-stage treatment jump.

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:266 · uses POFuzzyRDDSystem , Assumptions , POSystem

def tau_LATE reviewed

Causalean.PO.POFuzzyRDDSystem

The cutoff complier-effect ratio for a fuzzy regression-discontinuity design under the identifying assumptions divides the complier-weighted outcome-difference regression by the latent first-stage 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:274 · uses POFuzzyRDDSystem , Assumptions , POSystem

def nuD_right_limit reviewed

Causalean.PO.POFuzzyRDDSystem

The right-hand treatment-regression limit for a fuzzy regression-discontinuity design under the identifying assumptions selects the take-up level approached from above the cutoff.

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:286 · uses POFuzzyRDDSystem , Assumptions , POSystem

def nuD_left_limit reviewed

Causalean.PO.POFuzzyRDDSystem

The left-hand treatment-regression limit for a fuzzy regression-discontinuity design under the identifying assumptions selects the take-up level approached from below the cutoff.

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:295 · uses POFuzzyRDDSystem , Assumptions , POSystem

def nuY_right_limit reviewed

Causalean.PO.POFuzzyRDDSystem

The right-hand outcome-regression limit for a fuzzy regression-discontinuity design under the identifying assumptions selects the outcome level approached from above the cutoff.

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:304 · uses POFuzzyRDDSystem , Assumptions , POSystem

def nuY_left_limit reviewed

Causalean.PO.POFuzzyRDDSystem

The left-hand outcome-regression limit for a fuzzy regression-discontinuity design under the identifying assumptions selects the outcome level approached from below the cutoff.

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:313 · uses POFuzzyRDDSystem , Assumptions , POSystem

theorem frd_identification reviewed

Causalean.PO.POFuzzyRDDSystem

Fuzzy RDD identification at the cutoff, in regression-representative form. For a fuzzy regression-discontinuity design, 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:663 · uses POFuzzyRDDSystem , Assumptions , nuD_left_limit , nuD_right_limit , nuY_left_limit , nuY_right_limit , tau_FRD , POSystem

theorem tau_late_identification_of_globalMonotonicity reviewed

Causalean.PO.POFuzzyRDDSystem

Fuzzy RDD identifies a cutoff representative complier ratio under an extra global monotonicity bridge. For a fuzzy regression-discontinuity design, under the fuzzy-RDD identifying bundle — consistency, deterministic cutoff eligibility, local monotonicity and exclusion, valid regression representatives, cutoff continuity and support, well-defined one-sided limits, and a nonzero first stage, 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_of_globalMonotonicity (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_of_globalMonotonicity · Causalean/PO/ID/Exact/RDD/FuzzyRDD.lean:719 · 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:126
measurable_factualX lemma — The running variable in a fuzzy regression-discontinuity design is measurable, so cutoff neighborhoods and its marginal law are valid.

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:144
measurable_factualZ lemma — The eligibility indicator in a fuzzy regression-discontinuity design is measurable, so above- and below-cutoff groups form valid events.

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:148
measurable_factualD lemma — Treatment take-up in a fuzzy regression-discontinuity design is measurable, so its discontinuity at the cutoff can be represented by a regression.

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:152
measurable_factualY lemma — The outcome in a fuzzy regression-discontinuity design is measurable, so its discontinuity at the cutoff can be represented by a regression.

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:156
measurable_DofZ lemma — In a fuzzy regression-discontinuity design, potential treatment under an eligibility state is measurable, so the latent first-stage regression is well-defined.

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:161
measurable_YofD lemma — In a fuzzy regression-discontinuity design, the potential outcome under a treatment level is measurable, so latent outcome regressions are well-defined.

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:168
measurable_YofDofZ lemma — In a fuzzy regression-discontinuity design, the outcome induced by an eligibility state is measurable, so its reduced-form regression is well-defined.

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:175
measurable_YdiffComplier lemma — The complier-weighted treatment effect in a fuzzy regression-discontinuity design is measurable, so it admits a cutoff regression representative.

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:184
measurableSet_zEvent lemma — In a fuzzy regression-discontinuity design, an observed eligibility state defines a measurable event suitable for consistency arguments.

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:201
tendsto_nuD_right_limit lemma — Under the fuzzy-RDD assumptions, the selected right-hand treatment limit for the design is attained by the observed take-up regression as the running variable approaches the cutoff from above.

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:322
tendsto_nuD_left_limit lemma — Under the fuzzy-RDD assumptions, the selected left-hand treatment limit for the design is attained by the observed take-up regression as the running variable approaches the cutoff from below.

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:329
tendsto_nuY_right_limit lemma — Under the fuzzy-RDD assumptions, the selected right-hand outcome limit for the design is attained by the observed outcome regression as the running variable approaches the cutoff from above.

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:336
tendsto_nuY_left_limit lemma — Under the fuzzy-RDD assumptions, the selected left-hand outcome limit for the design is attained by the observed outcome regression as the running variable approaches the cutoff from below.

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:343
aemeasurable_factualX lemma — The running variable in a fuzzy regression-discontinuity design is almost-everywhere measurable under the population law, allowing regression representatives to be pushed forward to its marginal distribution.

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:350
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:617
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:628
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:639
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:650

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

3 supporting declarations (lemmas, instances)

oneSidedLimit_eq_right theorem — Right-side limit identification. If the observable regression agrees almost everywhere with a reference regression to the right of the cutoff, the reference is continuous at the cutoff, and the running-variable law has positive mass arbitrarily close on the right, then any right-hand limit of the observable regression must equal the reference value at the cutoff. This turns one-sided a.e. regression agreement into an identified cutoff limit.

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:94
value_eq_of_aeEq_right theorem — Pointwise equality from right-side agreement. If two regression representatives agree almost everywhere to the right of the cutoff, the first is continuous there, the second is continuous there, and the running-variable law has positive mass arbitrarily close on the right, then their cutoff values coincide.

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:167
value_eq_of_aeEq_left theorem — Pointwise equality from left-side agreement. If two regression representatives agree almost everywhere to the left of the cutoff, the first is continuous there, the second is continuous there, and the running-variable law has positive mass arbitrarily close on the left, then their cutoff values coincide.

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

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

Data layout for sharp regression discontinuity. The system records a real-valued running variable, a binary treatment, a real outcome, and a cutoff, with distinct outcome and treatment nodes. The deterministic assignment rule and continuity and support conditions that make the design sharp are imposed separately by Assumptions; they are not properties of this bare variable bundle.

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:32 · uses POSystem

def factualX reviewed

Causalean.PO.POSharpRDDSystem

The observed running variable in a sharp regression-discontinuity design records each unit's realized forcing score, whose position around the cutoff determines treatment.

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:52 · uses POSharpRDDSystem , POSystem

def factualD reviewed

Causalean.PO.POSharpRDDSystem

The observed treatment in a sharp regression-discontinuity design records each unit's realized side-of-cutoff assignment.

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:57 · uses POSharpRDDSystem , POSystem

def factualY reviewed

Causalean.PO.POSharpRDDSystem

The observed outcome in a sharp regression-discontinuity design records each unit's realized real-valued response.

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:61 · uses POSharpRDDSystem , POSystem

def YofD reviewed

Causalean.PO.POSharpRDDSystem

The treatment-specific potential outcome in a sharp regression-discontinuity design records each unit's response if assigned the selected treatment, with that treatment level defining one side of the cutoff effect.

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:65 · uses POSharpRDDSystem , POSystem

def dEvent reviewed

Causalean.PO.POSharpRDDSystem

The observed treatment group in a sharp regression-discontinuity design collects units assigned the selected treatment level, with that level distinguishing the two cutoff sides.

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:89 · 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:99 · uses POSharpRDDSystem , POSystem

def tau_RDD reviewed

Causalean.PO.POSharpRDDSystem

The cutoff-local treatment effect for a sharp regression-discontinuity design under the sharp-RDD assumptions contrasts the treated and untreated potential-outcome regression representatives at the cutoff.

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:131 · uses POSharpRDDSystem , Assumptions , POSystem

def nu_right_limit reviewed

Causalean.PO.POSharpRDDSystem

The observable outcome regression's right-hand cutoff limit for a sharp regression-discontinuity design under the sharp-RDD assumptions selects the limiting outcome level approached from above the cutoff.

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:141 · uses POSharpRDDSystem , Assumptions , POSystem

def nu_left_limit reviewed

Causalean.PO.POSharpRDDSystem

The observable outcome regression's left-hand cutoff limit for a sharp regression-discontinuity design under the sharp-RDD assumptions selects the limiting outcome level approached from below the cutoff.

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:150 · uses POSharpRDDSystem , Assumptions , POSystem

theorem rdd_identification reviewed

Causalean.PO.POSharpRDDSystem

Sharp RDD identification at the cutoff (textbook form). For a sharp-RDD design, 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 :