Formalization: Honest Expected Length for Transported Complier Effects with Weak First Stages
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs.
Basic 72 declarations Explicit full-data and observed-data worlds
Explicit full-data and observed-data worlds
Full-data coordinate (S,X,D(0),D(1),Y(0),Y(1)).
Source observation (X,Z,D,Y).
The assigned source overlay (full data,Z).
Definition (Lean source)
Returns the indicator for whether a full-data unit belongs to the source population.
Returns a full-data unit's covariate value.
Returns a unit's potential treatment receipt under instrument value zero.
Returns a unit's potential treatment receipt under instrument value one.
Returns a unit's potential outcome under treatment receipt zero.
Returns a unit's potential outcome under treatment receipt one.
Converts a binary indicator to its real-valued zero-one representation.
Returns the treatment receipt a unit would have under the specified instrument assignment.
Returns the outcome a unit would have under the specified treatment receipt.
Definition (Lean source)
An array law contains only primitive laws and conditional-mean versions. The assumption atoms below pin every version to its law by integral identities.
Definition (Lean source)
Population-conditioned full-data law.
Definition (Lean source)
The covariate marginal in population s.
Definition (Lean source)
Target covariate law.
Definition (Lean source)
Assignment potential outcome Y(D(z)).
Definition (Lean source)
The observed source record derived from assigned full data.
Definition (Lean source)
Observed source law induced by the assigned full-data overlay.
Definition (Lean source)
Source covariate marginal.
Definition (Lean source)
Inverse-propensity score multiplier.
Definition (Lean source)
A measurable version of the observed source outcome ITT is characterized by its integrals over every measurable covariate set.
Definition (Lean source)
The source outcome ITT is the canonical observed-law representative, rather than an independently supplied model coordinate.
Definition (Lean source)
The source conditional outcome contrast is measurable as a function of covariates.
Formal statement
Proof (Lean source)
A measurable version of the observed source receipt ITT is characterized by its integrals over every measurable covariate set.
Definition (Lean source)
The source receipt ITT is the canonical observed-law representative, rather than an independently supplied model coordinate.
Definition (Lean source)
The source conditional treatment-receipt contrast is measurable as a function of covariates.
Formal statement
Proof (Lean source)
Radon--Nikodym transport weight, real-valued by ENNReal.toReal.
Definition (Lean source)
Kish dispersion.
Definition (Lean source)
Transported source outcome contrast.
Definition (Lean source)
The paper's transported first stage is the source-law moment of the transport weight times the identified conditional receipt contrast.
Definition (Lean source)
Effective identification strength.
Definition (Lean source)
A positive effective-strength threshold excludes the zero sample index.
Formal statement
Proof (Lean source)
Forced parameter range.
Target complier average causal effect, with Lean's total division convention.
Definition (Lean source)
Index-n source sample.
Definition (Lean source)
Index-n target covariate sample.
Definition (Lean source)
Product sample carrier.
Definition (Lean source)
The independent source/target finite-product sampling law.
Definition (Lean source)
Full-data probability law and bounded potential outcomes.
Definition (Lean source)
Both populations have strictly positive full-data mass.
Definition (Lean source)
The two sample factors are probability laws and N_n/n → c.
Definition (Lean source)
Instrument propensity is in [ε,1-ε] source-almost surely.
Definition (Lean source)
The paper's source assignment and consistency assumption. The assigned overlay is a genuine probability law with the source-population full-data marginal; mapping it through observeSource enforces D=D(Z) and Y=Y(D), while the last clause pins the assignment propensity.
Definition (Lean source)
Well-definedness and auxiliary-representation facts carried by the complete model. These pin its observed law and contrast fields to the paper-defined objects; SourceAssignmentConsistency is the paper assumption itself.
Definition (Lean source)
Conditional randomization: the assigned-full-data law factors with Bernoulli propensity given the source full-data law.
Definition (Lean source)
Exclusion pins the assignment potential outcome to Y(D(z)) in both populations.
Definition (Lean source)
No defiers in either population.
Definition (Lean source)
Conditional assignment-outcome contrasts are pinned to each population law and agree target-almost everywhere.
Definition (Lean source)
Integrated first-stage transport, with population conditional receipt contrasts pinned by integral identities.
Definition (Lean source)
The target complier share is positive.
Definition (Lean source)
Target covariate law is absolutely continuous with respect to source.
Definition (Lean source)
The transport density ratio is capped by 2 k_n.
Definition (Lean source)
Kish dispersion is at most the envelope.
Definition (Lean source)
The overlap envelope diverges sub-root-n while the first stage vanishes.
Definition (Lean source)
The uniform probability law on a row's injected finite covariate carrier. Equality with this measure is the carrier-exhaustion clause: the experiment is definitionally a pushforward of the discrete Fin m experiment, even though all rows share one arbitrary ambient measurable carrier.
Definition (Lean source)
At index n, cell realizes the paper's literal finite covariate experiment inside the common ambient carrier. The source law is exactly the uniform pushforward from Fin (k n); hence the injected image exhausts the row-law carrier and every ambient point outside it is null.
Definition (Lean source)
Main transported-IV model class at index n.
Definition (Lean source)
Derived-facing view of the complete model's observed-law well-definedness and auxiliary-field pinning facts.
Definition (Lean source)
The probability, boundedness, and identified-contrast consequences of the complete transported-IV model assumptions.
Formal statement
Proof (Lean source)
Complete model membership entails the paper's source assignment atom.
Formal statement
Proof (Lean source)
A covariate-indexed contrast representation remains valid after multiplication by an integrable measurable covariate weight.
Formal statement
Proof (Lean source)
The named transported first stage unfolds to the paper's weighted conditional receipt-contrast moment.
Formal statement
Proof (Lean source)
The paper-declared ranges of the four scalar functionals. This predicate does not add a model assumption: the companion lemma below derives it from membership in the transported-IV class.
Definition (Lean source)
Every transported-IV class member satisfies the scalar ranges declared in the paper. In particular these bounds are consequences of normalization, bounded contrasts, complier positivity, and the defining identities rather than additional hypotheses.
Formal statement
Proof (Lean source)
Uniform finite-cell subclass, flattened to the sixteen core members. Its finiteCellSource field carries the exact finite pushforward-law exhaustion condition, rather than merely requiring full mass on some subset.
Definition (Lean source)
Forget the finite-cell restriction.
Definition (Lean source)
Deterministic source/target covariate, weight, and propensity arrays.
Definition (Lean source)
Admissible deterministic geometry class.
Definition (Lean source)
Laws whose source law, target law, and propensity equal geometry g at index n, with the law-induced Radon--Nikodym weight equal to the geometry weight source-almost everywhere. The a.e. clause respects the fact that density-ratio versions are determined only up to source-null sets.
Definition (Lean source)
Regular nonuniform finite-cell subclass on a finite injected support whose image has full source mass.
Definition (Lean source)
Frontier 59 declarations Procedure objects
Procedure objects
Oracle weight inputs use a carrier whose elements are nonnegative pointwise, matching the density-ratio space.
Definition (Lean source)
The law-induced Radon--Nikodym weight as an admissible oracle input.
Definition (Lean source)
A measurable nonnegative version of a model row's transport density ratio. The paper determines w only source-law almost everywhere, so global oracle honesty and risk range over this entire nonempty fiber rather than silently selecting one Mathlib representative.
Definition (Lean source)
The canonical Radon--Nikodym representative witnesses that every version fiber is nonempty.
Definition (Lean source)
A fixed geometry's declared density-ratio version as an oracle input. Admissible geometries take the first branch, so procedures receive exactly g.weight; the zero fallback only totalizes this definition away from the admissible geometry class.
Definition (Lean source)
Inputs available to an oracle procedure.
Definition (Lean source)
Inputs available to a feasible finite-cell procedure. FiniteCellSource pins the row-n measure to the image of Fin (k n) inside the arbitrary ambient carrier.
Definition (Lean source)
The realized regular-cell support inside the fixed ambient carrier. The embedding is part of the experiment, so a procedure is never compared across an unrelated alternative support.
Definition (Lean source)
Inputs available to a regular-cell procedure: samples, the true realized support, and the known Fin (k n)-indexed cell-mass and propensity vectors, but no transport weight and no arbitrary ambient extensions of those vectors.
Definition (Lean source)
Oracle confidence-set sequence with range and sample-by-parameter graph measurability for every fixed ADMISSIBLE deterministic oracle input (w,e), i.e. every measurable pair. The source supplies the oracle the model's own density ratio and propensity, both measurable, so the measurability obligation is imposed exactly on the inputs the source quantifies over; a nonmeasurable w makes the sample-level score itself nonmeasurable, so demanding a measurable graph there would be strictly stronger than the source and in general unsatisfiable.
Definition (Lean source)
Sample-only finite-cell confidence-set sequence on the ambient carrier.
Definition (Lean source)
Finite-cell oracle procedures are global oracle procedures whose output on the realized finite-cell experiment depends on the oracle weight and propensity only through their values on the realized cells.
Definition (Lean source)
Regular-cell confidence-set sequence structurally excluding w. Its known q and e inputs are finite vectors indexed by the bundled true support, so there are no ambient off-support extensions to quotient out.
Definition (Lean source)
Lebesgue length restricted to the forced parameter interval.
Definition (Lean source)
Borel subsets of the forced parameter interval.
Definition (Lean source)
Lebesgue length on its exact paper domain and codomain.
Definition (Lean source)
Gives the confidence set produced by an oracle procedure from a two-sample dataset, the population transport weight, and the population propensity score.
Definition (Lean source)
Auxiliary oracle evaluation at a declared measurable version in the model row's density-ratio fiber. Intrinsic procedure invariance identifies this with the canonical paper-facing evaluation almost surely.
Definition (Lean source)
Gives the probability that an oracle confidence set contains the target complier average causal effect.
Definition (Lean source)
Gives the coverage probability of an oracle confidence set when evaluated with a specified admissible transport-weight version.
Definition (Lean source)
The oracle procedure's expected confidence-set length under the two-sample law.
Definition (Lean source)
The oracle procedure's expected confidence-set length when evaluated at a specified admissible transport-weight version.
Definition (Lean source)
A fixed-geometry oracle is evaluated with the geometry's chosen weight and propensity versions, rather than the canonical rnDeriv representative recovered from each law in the slice.
Definition (Lean source)
Gives the coverage probability of an oracle confidence set under a fixed geometry and its declared weight and propensity functions.
Definition (Lean source)
Gives the expected length of an oracle confidence set under a fixed geometry and its declared weight and propensity functions.
Definition (Lean source)
The finite-cell procedure's coverage probability for the target CACE under the two-sample law.
Definition (Lean source)
The finite-cell procedure's expected confidence-set length under the two-sample law.
Definition (Lean source)
The confidence set produced by a finite-cell oracle procedure using the population transport weight and propensity.
Definition (Lean source)
The probability that a finite-cell oracle confidence set contains the target CACE.
Definition (Lean source)
The expected length of a finite-cell oracle confidence set under the two-sample law.
Definition (Lean source)
The known source-cell mass function.
Definition (Lean source)
A regular-class witness packaged as the true support supplied to the procedure.
Definition (Lean source)
Extend a finite cell vector only for reuse by ambient-function estimator helpers. Procedure inputs expose the finite vector itself, never this arbitrary zero extension.
Definition (Lean source)
Constructs the regular-cell procedure input from a model in the regular finite-cell class and a two-sample dataset, including the class-supplied cell design, source-cell masses, and propensity scores.
Definition (Lean source)
The confidence set produced by a regular-cell procedure from a sample and the class-supplied cell design.
Definition (Lean source)
The probability that a regular-cell confidence set contains the target CACE over a regular finite-cell model.
Definition (Lean source)
The expected length of a regular-cell confidence set under the corresponding two-sample law.
Definition (Lean source)
The infimum of rowwise coverage, with the vacuous value one on an empty model row. Coverage takes values in [0,1], so this is the bounded paper-facing counterpart of the mathematical convention inf empty = +infinity.
Definition (Lean source)
Rowwise worst-case coverage indexed exactly by model rows. The canonical input represents the row's source-a.e. quotient, by intrinsic procedure invariance.
Definition (Lean source)
Oracle procedures have asymptotic uniform coverage over the main class; their structure makes evaluation well-defined on the law-indexed source-a.e. quotient of the declared density-ratio input.
Definition (Lean source)
Sample-only procedures have asymptotic uniform coverage over the finite-cell subclass.
Definition (Lean source)
Oracle procedures are honest over the full transported-IV class on the same carrier; the risk may subsequently be restricted to cells.
Definition (Lean source)
Oracle procedures honest uniformly over a fixed geometry slice.
Definition (Lean source)
Procedures using known source-cell masses and propensity, but not w, are honest over the regular finite-cell class.
Definition (Lean source)
Positive frontier thresholds, the exact paper domain of every tagged risk and minimax value function.
Definition (Lean source)
Rowwise global oracle risk over exactly the model rows satisfying the strength restriction. There is no additional weight-version supremum.
Definition (Lean source)
The corresponding rowwise risk restricted to the finite-cell submodel.
Definition (Lean source)
Total computational risk at an arbitrary real threshold.
Definition (Lean source)
Paper-facing risk on the declared positive threshold domain.
Definition (Lean source)
Gives the limiting worst-case expected length of an oracle procedure over finite-cell model rows whose effective strength meets the supplied threshold.
Definition (Lean source)
Gives the limiting worst-case expected length of an oracle procedure over model rows in a fixed geometry whose effective strength meets the supplied threshold.
Definition (Lean source)
The asymptotic worst-case expected length of a regular-cell procedure over regular finite-cell models whose effective strength exceeds a given threshold.
Definition (Lean source)
The asymptotic worst-case expected length of a finite-cell procedure over finite-cell models whose effective strength exceeds a given threshold.
Definition (Lean source)
Total computational helper underlying the paper-facing oracle value.
Definition (Lean source)
Oracle minimax expected-length frontier on its declared positive domain.
Definition (Lean source)
Gives the smallest limiting worst-case expected length attainable by an oracle-honest procedure over finite-cell models at the supplied strength threshold.
Definition (Lean source)
The global oracle-honest procedure class, with risk restricted to the growing finite-cell submodel, on the declared positive threshold domain.
Definition (Lean source)
Total computational helper underlying the fixed-geometry value.
Definition (Lean source)
Conditional minimax frontier at an admissible deterministic geometry, on the declared positive threshold domain.
Definition (Lean source)
Helpers.CellEstimators 6 declarations
Symmetric, generally nondegenerate collision kernel.
Definition (Lean source)
Ordered-pair collision estimate of Kish dispersion.
Definition (Lean source)
Source-cell inverse-frequency moment estimate.
Definition (Lean source)
Cross-average using target empirical cell frequencies.
Definition (Lean source)
Regular-cell inversion rule using cross-averaged outcome and receipt moments and the collision estimate of the transport scale.
Definition (Lean source)
Uniform-cell specialization with q_x=1/k and e=1/2.
Definition (Lean source)
Helpers.Divergence 1 declarations
Per-source-observation chi-square calibration for the continuum witness.
Formal statement
Proof (Lean source)
Helpers.ExpectedLength 2 declarations
Tonelli section identity for a jointly measurable random set.
Formal statement
Proof (Lean source)
Uniform coverage on an interval and a TV comparison with its center force positive expected length at the center law.
Formal statement
Proof (Lean source)
Helpers.FiniteCellBridge 6 declarations
The sample-only uniform-cell specialization of the regular-cell inversion procedure.
Definition (Lean source)
A uniform finite-cell law belongs to the regular finite-cell class with unit lower and upper cell-mass constants at any smaller overlap radius.
Formal statement
Proof (Lean source)
On a uniform finite-cell law, the regular procedure fed the law's cell masses and propensity agrees almost surely with the sample-only specialization.
Formal statement
Proof (Lean source)
On a uniform finite-cell law, the sample-only and regular specialized procedures have the same coverage.
Formal statement
Proof (Lean source)
On a uniform finite-cell law, the sample-only and regular specialized procedures have the same expected set length.
Formal statement
Proof (Lean source)
Honesty and worst-case expected length transfer from the unit-regular procedure to its sample-only uniform-cell specialization.
Formal statement
Proof (Lean source)
Helpers.FrontierOrder 9 declarations
On an inhabited row, coverageInfOrOne is the ordinary infimum.
Formal statement
Proof (Lean source)
On an empty row, coverageInfOrOne has its declared vacuous value.
Formal statement
Proof (Lean source)
The full representative-fiber coverage infimum is bounded by evaluation at the canonical representative of any particular class member.
Formal statement
Proof (Lean source)
Every rowwise full-fiber coverage infimum is nonnegative.
Formal statement
Proof (Lean source)
The full representative-fiber risk row dominates canonical evaluation at every member above the strength threshold.
Formal statement
Proof (Lean source)
Canonical evaluation at a finite-cell row is bounded by the full representative-fiber finite-cell risk row.
Formal statement
Proof (Lean source)
Full-fiber finite-cell oracle risk rows retain the diameter-two bound.
Formal statement
Proof (Lean source)
A globally honest procedure restricts to every fixed geometry because the geometry's declared weight is itself a member of each row's full version fiber.
Formal statement
Proof (Lean source)
Consequently the conditional minimax value is bounded by the risk of each globally honest procedure, without identifying a.e.-equal weight versions pointwise.
Formal statement
Proof (Lean source)
Helpers.InversionRisk 9 declarations
The model-free confidence set obtained by inverting one affine inequality.
Definition (Lean source)
Score inversion is an instance of model-free affine inversion.
Formal statement
Proof (Lean source)
On the nondegenerate target-sample branch, regular-cell inversion is model-free affine inversion.
Formal statement
Proof (Lean source)
On the degenerate target-sample branch, regular-cell inversion returns the whole parameter space.
Formal statement
Proof (Lean source)
Affine inversion has length at most twice its radius divided by its nonzero slope, as well as at most the diameter of the parameter space.
Formal statement
Proof (Lean source)
Affine inversion is always bounded by the diameter of the parameter space.
Formal statement
Proof (Lean source)
Expected affine-inversion length is controlled by the mean radius and the probability that the random slope is less than half its positive mean target.
Formal statement
Proof (Lean source)
Frontier conversion when the mean radius proxy is inflated by at most a factor two. The resulting inverse-root constant is exactly 4 * sqrt 2 * L.
Formal statement
Proof (Lean source)
Frontier conversion without radius-proxy inflation. The resulting inverse-root constant is exactly 4 * L.
Formal statement
Proof (Lean source)
Helpers.RateAlgebra 1 declarations
Converts an inverse-root plus inverse-strength bound to the compact min(1,t⁻¹/²) frontier form.
Formal statement
Proof (Lean source)
Helpers.RegularCellRisk_Part1 24 declarations Statistics and deterministic constants
Statistics and deterministic constants
The constant in the regular-cell variance calculation.
Definition (Lean source)
Empirical target mass of one ambient point.
Definition (Lean source)
The affine source score at a candidate effect.
Definition (Lean source)
The conditional score mean represented by the model's contrast versions.
Definition (Lean source)
Cross-averaged outcome score.
Definition (Lean source)
Cross-averaged receipt score.
Definition (Lean source)
Cross-averaged affine score.
Definition (Lean source)
The collision proxy used by the feasible regular-cell rule.
Definition (Lean source)
The zero-extended cell-value function returns a cell's assigned value at every point in that cell.
Formal statement
Proof (Lean source)
Extending a finite vector of cell values by zero outside the cells defines a measurable covariate function.
Formal statement
Proof (Lean source)
Cell-scoped graph measurability of regular-cell inversion.
Formal statement
Proof (Lean source)
The regular-cell procedure, which receives cell masses and propensity but not the transport weight.
Definition (Lean source)
On a regular finite-cell law, the bundled finite-vector input agrees almost surely with the ambient mass-and-propensity inversion.
Formal statement
Proof (Lean source)
A probability distribution supported on finitely many measurable cells is the sum of point masses at those cells, each weighted by its cell probability.
Formal statement
Proof (Lean source)
A property that holds almost everywhere also holds at any point assigned strictly positive probability.
Formal statement
Proof (Lean source)
Every strongly measurable real-valued function is integrable under a probability distribution supported on finitely many measurable cells.
Formal statement
Proof (Lean source)
On the class-supplied finite support the RN weight is the target/source point-mass ratio, and Kish dispersion is the corresponding finite sum.
Formal statement
Proof (Lean source)
The inverse-propensity affine score has the paper's 2 / epsilon envelope.
Formal statement
Proof (Lean source)
On every realized cell, the score conditional mean is DeltaY - theta * DeltaD; it is bounded by two, and at the target CACE its target-mass average is zero.
Formal statement
Proof (Lean source)
On every realized cell, the score conditional mean is DeltaY - theta * DeltaD; it is bounded by two, and at the target CACE its target-mass average is zero.
Formal statement
Proof (Lean source)
The cross average equals the source-sample average of the score weighted by each source observation's empirical target-cell mass divided by its cell mass.
Formal statement
Proof (Lean source)
The difference of the two cross averages is the source average weighted by empirical target masses.
Formal statement
Proof (Lean source)
The expectation of an average of independent draws equals the population expectation of the summand.
Formal statement
Proof (Lean source)
The variance of an average of positive-number independent draws equals the summand variance divided by the sample size.
Formal statement
Proof (Lean source)
Helpers.RegularCellRisk_Part2 4 declarations Statistics and deterministic constants
Statistics and deterministic constants
For the source-sample average weighted by target cell masses, this result gives its mean, an upper bound on its variance, and square integrability. The mean is the target-mass-weighted sum of the cell means.
Formal statement
Proof (Lean source)
The second moment of a cell's empirical target mass equals the squared population cell mass plus its binomial sampling correction.
Formal statement
Proof (Lean source)
Conditional on a fixed target sample, the source mean and variance have the paper's finite-cell expressions.
Formal statement
Proof (Lean source)
Conditional on a fixed target sample, the source mean and variance have the paper's finite-cell expressions.
Formal statement
Proof (Lean source)
Helpers.RegularCellRisk_Part3 6 declarations Statistics and deterministic constants
Statistics and deterministic constants
At the target CACE, randomness of the target empirical score mean contributes at most 4 / N.
Formal statement
Proof (Lean source)
At the target CACE, randomness of the target empirical score mean contributes at most 4 / N.
Formal statement
Proof (Lean source)
Exact multinomial second moment and its regular-cell upper bound.
Formal statement
Proof (Lean source)
Exact multinomial second moment and its regular-cell upper bound.
Formal statement
Proof (Lean source)
The variance of a statistic based on two independent samples equals its average conditional variance given the second sample plus the variance of its conditional mean.
Formal statement
Proof (Lean source)
The weighted cross-sample average is almost-everywhere strongly measurable under the joint two-sample distribution.
Formal statement
Proof (Lean source)
Helpers.RegularCellRisk_Part4 3 declarations Statistics and deterministic constants
Statistics and deterministic constants
For a transported-IV distribution supported on the regular cells, the Kish dispersion of the transport weights is at least one.
Formal statement
Proof (Lean source)
The weighted cross-sample average has variance bounded by its source-sampling contribution plus its target-sampling contribution, and its expectation equals the stated target mean.
Formal statement
Proof (Lean source)
For the witness construction, the empirical target receipt contrast has the stated mean and variance bound determined by the target cell distribution.
Formal statement
Proof (Lean source)
Helpers.RegularCellRisk_Part5_Part1 2 declarations Statistics and deterministic constants
Statistics and deterministic constants
Eventually and uniformly over the regular class, both cross moments obey the exact paper variance constant; the receipt moment is centered at the transported first stage.
Formal statement
Proof (Lean source)
Under the regular finite-cell witness conditions, the weighted cross-sample average of a bounded measurable source score is square-integrable.
Formal statement
Proof (Lean source)
Helpers.RegularCellRisk_Part5_Part2 3 declarations R1.8--R1.9: collision scale
R1.8--R1.9: collision scale
Under the regular finite-cell witness conditions, the target-sample collision-scale statistic is square-integrable.
Formal statement
Proof (Lean source)
The two cross moments and the collision proxy are square-integrable under the sampling law. The paper applies Chebyshev's inequality to each of these three statistics (writeup.tex:918-924 and 931-934) and so presupposes exactly this; it is pure regularity, carrying no rate or constant. Each holds because on a RegularFiniteCellClass member every ingredient is bounded: the affine score by 2 / epsilon, and the cell weights by k n / cminus on the class's finite support.
Formal statement
Proof (Lean source)
A bounded off-diagonal kernel average from an independent sample has variance at most 32 times the squared kernel bound divided by the sample size.
Formal statement
Proof (Lean source)
Helpers.RegularCellRisk_Part5_Part3 3 declarations R1.9b: measurability of the known design input, and exact centering
R1.9b: measurability of the known design input, and exact centering
The collision component is unbiased, is bounded on the realized target support, and has the paper's variance bound.
Formal statement
Proof (Lean source)
The lower-tail failure probability for Khat has the two paper branches.
Formal statement
Proof (Lean source)
Uniformly, the probability that the collision proxy undershoots half the true dispersion vanishes.
Formal statement
Proof (Lean source)
Helpers.RegularCellRisk_Part5_Part4 4 declarations R1.10: honesty in the exact liminf form
R1.10: honesty in the exact liminf form
On a regular finite-cell class member the known source-cell mass function is measurable. It vanishes off the class's finite cell support, because that support carries full source mass, and on the support it is constant on each of the class's measurable atoms; so it is a finite sum of scaled indicators.
Formal statement
Proof (Lean source)
The expected empirical target mass of a measurable cell equals its population target probability.
Formal statement
Proof (Lean source)
At the target CACE the two-sample contrast moment is exactly centered: its mean under the sampling law is zero. This is the identification identity theta_T = mu_{Y,n} / mu_n transported to the level of the cross-averaged moments, and it is what makes the paper's Chebyshev step at writeup.tex:925-930 a bound on a centered moment.
Formal statement
Proof (Lean source)
The regular-cell inversion procedure is uniformly asymptotically honest. The conclusion is deliberately the coverage component of RegularCellHonest, so the theorem assembly can use it directly.
Formal statement
Proof (Lean source)
Helpers.RegularCellRisk_Part5_Part5 2 declarations
The empirical first stage misses half its positive mean with probability at most 4 B / t, eventually and uniformly.
Formal statement
Proof (Lean source)
Khat has mean 1 + kappa, bounded by 2 kappa; the latter uses the probability-density lower bound kappa ≥ 1.
Formal statement
Proof (Lean source)
Helpers.ScoreInversion 14 declarations
Instrument multiplier formed from the declared propensity input.
Definition (Lean source)
Empirical transported outcome score.
Definition (Lean source)
Empirical transported receipt score.
Definition (Lean source)
Empirical second moment of the oracle transport weight.
Definition (Lean source)
Inversion of the affine transported score over Theta.
Definition (Lean source)
The inversion handle only inspects the weight at realized source-sample covariates.
Formal statement
Proof (Lean source)
Every density-ratio version agrees with the canonical version simultaneously at the finitely many realized source covariates.
Formal statement
Proof (Lean source)
Score inversion is unchanged almost surely throughout a density-ratio version fiber.
Formal statement
Proof (Lean source)
A score-inversion procedure gives the same random set almost surely throughout a model's density-ratio version fiber.
Formal statement
Proof (Lean source)
For a score-inversion procedure, coverage is unchanged when the canonical transport weight is replaced by any admissible version.
Formal statement
Proof (Lean source)
For a score-inversion procedure, expected confidence-set length is unchanged when the canonical transport weight is replaced by any admissible version.
Formal statement
Proof (Lean source)
For score inversion, taking the infimum over the full version fiber is exactly the canonical coverage infimum.
Formal statement
Proof (Lean source)
For score inversion, the full representative-fiber risk row equals the canonical row used by the existing score calculation.
Formal statement
Proof (Lean source)
Affine inversion has length at most the interval diameter and, away from a zero empirical first stage, at most twice radius over slope.
Formal statement
Proof (Lean source)
Helpers.ScoreRisk 25 declarations prop:compact-causal-range is stated in the source for every P in the class, with no integrability hypothesis, and its own proof (writeup.tex:382) applies the change-of-measure identity to Delta_Y as a BOUNDED measurable
S1.0: the contrast functions are bounded, hence integrable
prop:compact-causal-range is stated in the source for every P in the class,
with no integrability hypothesis, and its own proof (writeup.tex:382) applies
the change-of-measure identity to Delta_Y as a BOUNDED measurable function.
In the Lean encoding that boundedness is not a structure field: the contrast
functions are pinned only through the set-integral identities of
OutcomeTransport and ReceiptTransport. It is nevertheless forced by them,
because those identities equate a set integral of the contrast with a set
integral of an integrand bounded by one.
Atom-by-atom interface required of an abstract model predicate by the score-risk calculation. Each field is an implication schema, so a fixed geometry slice supplies the same atoms through its first component.
Definition (Lean source)
The global transported-IV class instantiates the abstract atom interface.
Definition (Lean source)
Every fixed-geometry slice instantiates the same abstract atom interface.
Definition (Lean source)
The one-observation affine oracle score.
Definition (Lean source)
The score average is the difference of the outcome and receipt averages.
Formal statement
Proof (Lean source)
S1.1: component score means imply the affine score identity, and the identifying ratio centers the score at the target effect.
Formal statement
Proof (Lean source)
S1.2: overlap and the outcome/parameter ranges give the exact 2 / epsilon envelope for the oracle affine score without the weight.
Formal statement
Proof (Lean source)
S1.2, squared form: after multiplying by a nonnegative weight, the score square is bounded by 4 w² / epsilon².
Formal statement
Proof (Lean source)
S1.3: the paper's weight envelope implies w⁴ ≤ 4 k_n² w² pointwise.
Formal statement
Proof (Lean source)
Exact mean and variance of an i.i.d. empirical average. This is the model-free sampling leaf used for both the score and empirical Kish moments.
Formal statement
Proof (Lean source)
S1.3: an i.i.d. empirical Kish average has variance at most 4 k² kappa / n under the paper's fourth-moment envelope.
Formal statement
Proof (Lean source)
S1.4: a probability density of mean one has second moment at least one.
Formal statement
Proof (Lean source)
A reusable Chebyshev leaf with a supplied exact mean and variance bound.
Formal statement
Proof (Lean source)
S1.4: the lower tail of empirical Kish is bounded by the paper's exact 16 k² / (n kappa) expression.
Formal statement
Proof (Lean source)
S1.5 order leaf: pointwise rows with a vanishing uniform error imply the paper's exact liminf honesty statement. Eventual inhabitation is essential only to bound the infimum rows from above; without it an empty real-valued indexed infimum is zero.
Formal statement
Proof (Lean source)
S1.6: the receipt mean/variance calculation gives exactly the paper's 4 / (epsilon² t) bad-slope bound.
Formal statement
Proof (Lean source)
S1.7: the empirical Kish statistic has exactly the population second moment as its expectation.
Formal statement
Proof (Lean source)
S1.8: direct uninflated affine-inversion frontier bound. The statement is law- and class-agnostic, so both oracle model classes feed it the same moment facts.
Formal statement
Proof (Lean source)
The inverse-root cap is antitone on positive strengths.
Formal statement
Proof (Lean source)
Abstract version of the paper's frontier risk, with the model class represented by a per-index predicate.
Definition (Lean source)
S1.8 order leaf: a pointwise uninflated frontier bound collapses both the class supremum and the asymptotic limsup at the threshold value. The capped min is retained, including both of its branches.
Formal statement
Proof (Lean source)
A measurable function whose set integrals are dominated by the measure of the set is almost everywhere bounded by one. Truncation to the bounded slices {m < f ≤ m + 1} is what makes this hold without assuming f integrable: on each slice f is bounded, so the set integral is genuine rather than Lean's junk value for a non-integrable integrand.
Formal statement
Proof (Lean source)
On a global class member both population contrast functions are integrable against the source covariate law. This is what lets compact_causal_range be applied on the global class without carrying its two integrability hypotheses as assumptions; every regular-cell consumer already discharges them from the finite cell support, and this is the corresponding global discharge.
Formal statement
Proof (Lean source)
The abstract atom interface reconstructs the paper's transported-IV class for each of its members.
Formal statement
Proof (Lean source)
Consequently compact_causal_range applies to every member of any abstract score-risk class, without an integrability hypothesis in the class interface.
Formal statement
Proof (Lean source)
Helpers.Witness 17 declarations The following definitions spell out the three independent coins used by the paper.
Measure-theoretic leaves for the witness
The following definitions spell out the three independent coins used by the paper. The first chooses compliance, the second chooses the common receipt type when the unit is not a complier, and the third chooses the binary treated outcome.
Geometry-side Kish dispersion.
Definition (Lean source)
First-stage value displayed by the fixed-strength construction.
Definition (Lean source)
Compliance probability supplied by the geometry handle.
Definition (Lean source)
Potential coordinates (D(0),D(1),Y(0),Y(1)) conditional on X.
Definition (Lean source)
Collects a unit's two potential treatment receipts and two potential outcomes into its potential-coordinate vector.
Definition (Lean source)
Geometry covariate marginal for the selected population.
Definition (Lean source)
The named least-favourable continuum attached to a geometry and strength. The compliance probability is clamped only to make the array globally valid; on the eventual geometry range the clamp is inactive.
Definition (Lean source)
The source-observation chi-square divergence between a geometry witness at perturbation level h and its zero-perturbation counterpart is bounded by eight times the squared perturbation, scaled by the geometry's signal and inverse Kish dispersion.
Formal statement
Proof (Lean source)
The continuum family Q_{n,h}^g. Each population has the same conditional potential-data kernel given X, integrated against g.sourceX in the source and g.targetX in the target. Compliance types have probabilities p_n, (1-p_n)/2, (1-p_n)/2; Y(0)=0; and binary Y(1) has mean 1/2+h for compliers and 1/2 otherwise.
Definition (Lean source)
Full fixed-strength geometry handle: admissibility, valid compliance probabilities, exact first-stage/strength identities, a continuum of witness laws, and the chi-square/total-variation comparisons with the center.
Definition (Lean source)
The continuum construction supplies a member of every sufficiently late fixed-geometry strength slice. In particular, lower bounds use an exhibited law and never a nonemptiness assumption on the model class.
Formal statement
Proof (Lean source)
The named geometry family is least favourable at every sufficiently late index throughout the prescribed local range.
Formal statement
Proof (Lean source)
At every sufficiently late index, the clamped construction gives the paper's full least-favourable family throughout its prescribed local range.
Formal statement
Proof (Lean source)
The named least-favourable family supplies the complete geometry handle, including its chi-square and total-variation calibration, eventually in n.
Formal statement
Proof (Lean source)
The uniform finite-cell construction is realizable on any measurable carrier admitting the required rowwise finite injections. The injected Fin (k n) image carries full mass, so growing support constrains the measure rather than identifying the ambient carrier with a finite type.
Formal statement
Proof (Lean source)
Forgetting the finite-cell field gives an inhabited main class on the same arbitrary carrier.
Formal statement
Proof (Lean source)
The same uniform witness inhabits every regular finite-cell class whose fixed constants contain the uniform mass 1 / k_n.
Formal statement
Proof (Lean source)
T_CompactCausalRange 6 declarations
The map from assigned full data to the observed source-data record is measurable.
Formal statement
Proof (Lean source)
Under the source-observation conditions, the source covariate distribution equals the source population covariate distribution.
Formal statement
Proof (Lean source)
A finite measure equals the measure obtained by weighting another measure when its mass on every measurable set is the corresponding integral of a nonnegative integrable weight.
Formal statement
Proof (Lean source)
Under IV randomization and overlap, the full-data distribution conditional on each instrument value is the source population law reweighted by that instrument's propensity probability.
Formal statement
Proof (Lean source)
Under IV randomization and overlap, the inverse-propensity-weighted contrast over a covariate set equals the source-population integral of the difference between the two full-data outcomes.
Formal statement
Proof (Lean source)
Source randomization identifies the two conditional contrasts; transport identifies their target means; their Wald ratio is the target CACE and belongs to the forced interval [-1,1].
Formal statement
Proof (Lean source)
T_FiniteCellUnknownWeightAttainment 1 declarations
The uniform finite-cell submodel's sample-only collision-scaled rule is honest and matches the oracle converse order, on the same arbitrary measurable carrier as the regular-cell and global results.
Formal statement
Proof (Lean source)
T_FixedGeometryFrontier 1 declarations
For every admissible deterministic geometry, the conditional honest expected-length frontier has order min(1,t0⁻¹/²), with constants independent of the geometry.
Formal statement
Proof (Lean source)
T_NoShiftReduction 1 declarations
If the transport weight is one, the target and source covariate laws agree, Kish dispersion is one, and effective strength reduces to n μ_n². The conditional frontier is therefore the compact single-population weak-ratio frontier.
Formal statement
Proof (Lean source)
T_OracleConverse 1 declarations
Universal lower-frontier constants apply both globally and to the finite-cell oracle submodel and are invariant to the decomposition of effective strength into first stage and Kish dispersion.
Formal statement
Proof (Lean source)
T_OracleScoreInversionAttainment 1 declarations
One oracle transported-score inversion sequence is honest and attains the frontier simultaneously at every fixed positive strength threshold.
Formal statement
Proof (Lean source)
T_RegularCellUnknownWeightAttainment 1 declarations
With known regular source-cell probabilities and known propensity, the cross-averaged rule does not use the transport weight and attains the oracle frontier order; the uniform fixed geometry supplies the matching converse.