PO.ID.Exact.RDD
Regression discontinuity: identification of the cutoff effect from continuity of conditional regressions.
FuzzyRDD 19 core · 17 supporting This file formalizes fuzzy regression-discontinuity identification using regression-function representatives at the cutoff. ★ POFuzzyRDDSystem★ frd_identification★ tau_late_identification
Fuzzy Regression Discontinuity
This file formalizes fuzzy regression-discontinuity identification using
regression-function representatives at the cutoff. POFuzzyRDDSystem defines
the running variable, cutoff indicator, binary treatment, outcome, potential
treatment DofZ, potential outcome YofD, induced outcome YofDofZ, and the
complier-weighted outcome difference YdiffComplier.
The Assumptions bundle records consistency, deterministic cutoff eligibility,
local treatment monotonicity near the cutoff, latent and observable regression
representatives, one-sided support, observable one-sided limits, a complier
outcome-difference representative, and a nonzero first-stage jump. The main
definitions are tau_FRD and tau_LATE. Theorems nuD_right_limit_eq,
nuD_left_limit_eq, nuY_right_limit_eq, and nuY_left_limit_eq identify the
observable one-sided limits with latent regression values, and
frd_identification identifies the observable cutoff Wald ratio. The theorem
tau_late_identification gives the separate global-monotonicity bridge from
the fuzzy RDD ratio to the cutoff representative complier-effect ratio.
Fuzzy regression-discontinuity model in the potential-outcome framework. A unit has a continuous running variable X, an above-cutoff indicator Z recording whether X exceeds the cutoff c, a binary treatment D whose take-up probability jumps — but does not jump all the way from 0 to 1 — at the cutoff, and a real outcome Y, with the outcome, cutoff indicator, and treatment nodes pairwise distinct. The cutoff effect on the outcome divided by the cutoff jump in treatment identifies the cutoff-local LATE (def:po-fuzzy-rdd-system).
Definition (Lean source)
Factual running variable X.
Definition (Lean source)
Factual cutoff-eligibility instrument Z.
Definition (Lean source)
Factual treatment D.
Definition (Lean source)
Factual outcome Y.
Definition (Lean source)
Instrument-specific potential treatment D(z).
Treatment-specific potential outcome Y(d).
Definition (Lean source)
Outcome under the treatment induced by instrument value z, Y(D(z)).
Y-difference weighted by the complier indicator 1_{D(1)=1, D(0)=0}. Equals Y(D(1)) − Y(D(0)) a.e. under monotonicity; used in the LATE bridge.
Factual eligibility event {Z = z}.
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)
Cutoff-local fuzzy RDD Wald estimand in regression-representative form.
Cutoff-local complier-effect ratio in regression-representative form. It divides the complier outcome-difference representative at the cutoff by the first-stage jump; tau_late_identification connects this ratio to tau_FRD under the fuzzy-RDD assumptions.
The right-hand treatment limit is the selected limit at the cutoff of the observable treatment regression as the running variable approaches from above.
Definition (Lean source)
The left-hand treatment limit is the selected limit at the cutoff of the observable treatment regression as the running variable approaches from below.
Definition (Lean source)
The right-hand outcome limit is the selected limit at the cutoff of the observable outcome regression as the running variable approaches from above.
Definition (Lean source)
The left-hand outcome limit is the selected limit at the cutoff of the observable outcome regression as the running variable approaches from below.
Definition (Lean source)
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
Proof (Lean source)
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
17 supporting declarations (lemmas, instances)
-
measurable_factualXlemma — The factual running variable is measurable.conclusionMeasurable S.factualXProof (Lean source)
lemma measurable_factualX : Measurable S.factualX := S.Xvar.measurable_factual -
measurable_factualZlemma — The factual cutoff-eligibility instrument is measurable.conclusionMeasurable S.factualZProof (Lean source)
lemma measurable_factualZ : Measurable S.factualZ := S.Zvar.measurable_factual -
measurable_factualDlemma — The factual treatment is measurable.conclusionMeasurable S.factualDProof (Lean source)
lemma measurable_factualD : Measurable S.factualD := S.Dvar.measurable_factual -
measurable_factualYlemma — The factual outcome is measurable.conclusionMeasurable S.factualYProof (Lean source)
lemma measurable_factualY : Measurable S.factualY := S.Yvar.measurable_factual -
measurable_DofZlemma — The instrument-specific potential treatment is measurable.Proof (Lean source)
lemma measurable_DofZ (z : Bool) : Measurable (S.DofZ z) := S.Dvar.measurable_cfUnder S.Zvar z -
measurable_YofDlemma — The treatment-specific potential outcome is measurable.Proof (Lean source)
lemma measurable_YofD (d : Bool) : Measurable (S.YofD d) := S.Yvar.measurable_cfUnder S.Dvar d -
measurable_YofDofZlemma — The outcome under the instrument-induced treatment is measurable.Proof (Lean source)
lemma measurable_YofDofZ (z : Bool) : Measurable (S.YofDofZ z) := by unfold YofDofZ exact Measurable.ite (S.measurable_DofZ z (MeasurableSet.singleton true)) (S.measurable_YofD true) (S.measurable_YofD false) -
measurable_YdiffComplierlemma — The complier-weighted outcome difference is measurable.conclusionMeasurable S.YdiffComplierProof (Lean source)
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 -
measurableSet_zEventlemma — The factual eligibility event is measurable.Proof (Lean source)
lemma measurableSet_zEvent (z : Bool) : MeasurableSet (S.zEvent z) := by simpa [zEvent] using S.Zvar.measurableSet_event z -
tendsto_nuD_right_limitlemma — The chosen right-hand treatment-regression limit is a genuine right-hand limit at the cutoff.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 -
tendsto_nuD_left_limitlemma — The chosen left-hand treatment-regression limit is a genuine left-hand limit at the cutoff.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 -
tendsto_nuY_right_limitlemma — The chosen right-hand outcome-regression limit is a genuine right-hand limit at the cutoff.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 -
tendsto_nuY_left_limitlemma — The chosen left-hand outcome-regression limit is a genuine left-hand limit at the cutoff.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 -
nuD_right_limit_eqtheorem — Any right-hand observable treatment-regression limit at the cutoff equals the treated latent treatment regression there.hypothesesconclusionL = hA.muD true S.cProof (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 -
nuD_left_limit_eqtheorem — Any left-hand observable treatment-regression limit at the cutoff equals the untreated latent treatment regression there.hypothesesconclusionL = hA.muD false S.cProof (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 -
nuY_right_limit_eqtheorem — Any right-hand observable outcome-regression limit at the cutoff equals the treated latent outcome regression there.hypothesesconclusionL = hA.muY true S.cProof (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 -
nuY_left_limit_eqtheorem — Any left-hand observable outcome-regression limit at the cutoff equals the untreated latent outcome regression there.hypothesesconclusionL = hA.muY false S.cProof (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
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.
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
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
oneSidedLimit_eq_righttheorem — 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.hypothesesh_aeEq :f =ᵐ[π.restrict (Ici c)] ghg_cont :ContinuousAt g ch_support :∀ ε > (0 : ℝ), π (Ioo c (c + ε)) ≠ 0L :ℝhL :Tendsto f (𝓝[>] c) (𝓝 L)conclusionL = g cProof (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 -
value_eq_of_aeEq_righttheorem — 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.hypothesesh_aeEq :f =ᵐ[π.restrict (Ici c)] ghf_cont :ContinuousAt f chg_cont :ContinuousAt g ch_support :∀ ε > (0 : ℝ), π (Ioo c (c + ε)) ≠ 0conclusionf c = g cProof (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 -
value_eq_of_aeEq_lefttheorem — Symmetric pointwise version of value_eq_of_aeEq_right.hypothesesh_aeEq :f =ᵐ[π.restrict (Iio c)] ghf_cont :ContinuousAt f chg_cont :ContinuousAt g ch_support :∀ ε > (0 : ℝ), π (Ioo (c - ε) c) ≠ 0conclusionf c = g cProof (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
SharpRDD 11 core · 9 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.
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).
Factual running variable X.
Definition (Lean source)
Factual treatment D.
Definition (Lean source)
Factual outcome Y.
Definition (Lean source)
Treatment-specific potential outcome Y(d).
Definition (Lean source)
Factual treatment event {D = d}.
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)
Cutoff-local RDD estimand — by definition the difference of the treatment-specific regression representatives at the cutoff. In the standard reading of μ_d c = E[Y(d) | X = c], this is E[Y(1) - Y(0) | X = c].
The right-hand limit lim_{x ↓ c} ν(x) chosen from the existence witness of Assumptions.
Definition (Lean source)
The left-hand limit lim_{x ↑ c} ν(x) chosen from the existence witness of Assumptions.
Definition (Lean source)
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
Proof (Lean source)
9 supporting declarations (lemmas, instances)
-
measurable_factualXlemma — The factual running variable is measurable.conclusionMeasurable S.factualXProof (Lean source)
lemma measurable_factualX : Measurable S.factualX := S.Xvar.measurable_factual -
measurable_factualDlemma — The factual treatment is measurable.conclusionMeasurable S.factualDProof (Lean source)
lemma measurable_factualD : Measurable S.factualD := S.Dvar.measurable_factual -
measurable_factualYlemma — The factual outcome is measurable.conclusionMeasurable S.factualYProof (Lean source)
lemma measurable_factualY : Measurable S.factualY := S.Yvar.measurable_factual -
measurable_YofDlemma — The treatment-specific potential outcome is measurable.Proof (Lean source)
lemma measurable_YofD (d : Bool) : Measurable (S.YofD d) := S.Yvar.measurable_cfUnder S.Dvar d -
measurableSet_dEventlemma — The factual treatment event is measurable.Proof (Lean source)
lemma measurableSet_dEvent (d : Bool) : MeasurableSet (S.dEvent d) := by simpa [dEvent] using S.Dvar.measurableSet_event d -
tendsto_nu_right_limitlemma — The chosen right-hand observable regression limit is a genuine right-hand limit at the cutoff.Proof (Lean source)
lemma tendsto_nu_right_limit (hA : S.Assumptions) : Tendsto hA.nu (𝓝[>] S.c) (𝓝 (S.nu_right_limit hA)) := Classical.choose_spec hA.nu_right_limit_exists -
tendsto_nu_left_limitlemma — The chosen left-hand observable regression limit is a genuine left-hand limit at the cutoff.Proof (Lean source)
lemma tendsto_nu_left_limit (hA : S.Assumptions) : Tendsto hA.nu (𝓝[<] S.c) (𝓝 (S.nu_left_limit hA)) := Classical.choose_spec hA.nu_left_limit_exists -
nu_right_limit_eqtheorem — Any right-limit of ν at c coincides with μ_1 c.hypothesesconclusionL = hA.mu true S.cProof (Lean source)
theorem nu_right_limit_eq (hA : S.Assumptions) {L : ℝ} (h : Tendsto hA.nu (𝓝[>] S.c) (𝓝 L)) : L = hA.mu true S.c := RDDLimits.oneSidedLimit_eq_right (S.nu_eq_mu_true_ae_restrict_Ici hA) (hA.mu_continuousAt true) hA.support_right h -
nu_left_limit_eqtheorem — Any left-limit of ν at c coincides with μ_0 c.hypothesesconclusionL = hA.mu false S.cProof (Lean source)
theorem nu_left_limit_eq (hA : S.Assumptions) {L : ℝ} (h : Tendsto hA.nu (𝓝[<] S.c) (𝓝 L)) : L = hA.mu false S.c := RDDLimits.oneSidedLimit_eq_left (S.nu_eq_mu_false_ae_restrict_Iio hA) (hA.mu_continuousAt false) hA.support_left h