Formalization: Sharp Minimax Rates for Average Treatment Effects with Discrete Confounding under Fixed Overlap
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 48 declarations
Defines Cell, the stated quantity or construction used in the discrete average-treatment-effect estimator.
One observed unit (X,A,Y).
A probability law with arbitrary masses on the finite observation alphabet.
Definition (Lean source)
The measure associated with a finite law.
Definition (Lean source)
The measure attached to a finite observation law is a probability measure: its total mass is one.
Definition (Lean source)
The mass of one (k,a,y) atom.
Definition (Lean source)
Every atom probability of the observation law -- the chance of seeing a given category, treatment value and outcome value together -- lies between zero and one.
Formal statement
Proof (Lean source)
The four masses in category k, indexed by (A,Y).
Definition (Lean source)
Each of the four coordinates of a category's mass vector, indexed by the treatment and outcome values, lies between zero and one, so the vector lies in the unit cube.
Formal statement
Proof (Lean source)
Marginal mass P(X=k).
Definition (Lean source)
The marginal probability that the confounder takes a given category value lies between zero and one.
Formal statement
Proof (Lean source)
Joint mass P(X=k,A=a).
Propensity, with Lean's total division convention on zero-mass cells.
Definition (Lean source)
The propensity of any category lies between zero and one. This holds unconditionally: on a category of zero mass the totalizing division convention returns zero, which is still in range.
Formal statement
Proof (Lean source)
Binary outcome regression, again totalized on empty arm-cells.
Definition (Lean source)
The conditional mean of the binary outcome given a treatment arm and a category lies between zero and one. This holds unconditionally: on an empty arm-cell the totalizing division convention returns zero, which is still in range.
Formal statement
Proof (Lean source)
Canonical finite i.i.d. product law.
Definition (Lean source)
The n-fold independent product of a finite observation law is again a probability measure.
Definition (Lean source)
The ambient infinite sample pushes forward to the canonical finite product.
Formal statement
Proof (Lean source)
The observed sample law is the n-fold product of the one-unit law.
Definition (Lean source)
Positive-mass categories have propensity in [epsilon,1-epsilon].
Definition (Lean source)
Full-data atom (X,A,Y,Y(0),Y(1)).
Finite potential-outcome overlay used only by the causal witness.
The real-valued probability that a full-data law assigns to one atom of the extended alphabet, which records the category, the treatment, the observed outcome and both potential outcomes.
Definition (Lean source)
Y=Y(A) almost surely, written as zero mass on inconsistent atoms.
Definition (Lean source)
Conditional atom mass for (Y(0),Y(1),A,X).
Finite conditional-independence identity (Y(0),Y(1)) ⟂ A | X.
Membership of a sample law in the unrestricted overlap experiment class.
Definition (Lean source)
Four-cell arm mass.
Definition (Lean source)
Total four-cell mass.
Definition (Lean source)
The nonnegative four-cell cone with treatment mass in the overlap band.
Definition (Lean source)
Total arithmetic extension of the homogeneous four-cell contribution. The paper-facing functional is cellPhiOnCone below.
Definition (Lean source)
The homogeneous four-cell ATE contribution on its stated overlap-cone domain.
Definition (Lean source)
Evaluating the cell contribution functional at a point of the overlap cone returns the same number as applying the total arithmetic extension to the underlying four-vector of masses.
Formal statement
Proof (Lean source)
The observed-data ATE functional sum_k phi(q_k).
Definition (Lean source)
The equivalent weighted-regression formula under overlap.
Formal statement
Proof (Lean source)
Shows that ate Functional mem interval lies in the stated set or interval.
Formal statement
Proof (Lean source)
Mean squared error under a supplied sample law.
A law packaged with overlap-class membership.
Definition (Lean source)
Worst-case MSE of one measurable estimator over the experiment class.
Definition (Lean source)
Infimum, over measurable estimators, of their worst-case product-law MSE.
Definition (Lean source)
The minimax mean-squared-error risk over the overlap experiment class lies between zero and one. It is nonnegative because every worst-case risk is an integral of a square, and it is at most one because the estimator that always reports zero already incurs squared error at most one against an average treatment effect that is confined to the interval from minus one to one.
Formal statement
Proof (Lean source)
Observed marginal of a full-data law.
Definition (Lean source)
Unnormalized explicit witness mass.
Definition (Lean source)
The unnormalized masses of the explicit two-category confounding witness are nonnegative whenever the overlap constant lies between zero and one.
Formal statement
Proof (Lean source)
Establishes the stated summation identity or bound for two Category Mass sum.
Formal statement
Proof (Lean source)
Explicit two-category confounding witness with p=(1/2,1/2) and propensities (epsilon,1-epsilon).
Definition (Lean source)
Naive observed treated-minus-control contrast.
Definition (Lean source)
Helpers.ChebyshevCertificate 21 declarations
Shifted-Chebyshev coefficient expansion used in the paper's equation (1).
Formal statement
Proof (Lean source)
For a positive degree, the Chebyshev polynomial of the first kind evaluated at the shifted argument one minus twice the variable splits into three pieces: the constant one, a linear term with coefficient minus twice the squared degree, and a remainder equal to twice the squared degree times the variable squared times the explicit polynomial continuation. This isolates the quadratic-and-higher part of the shifted Chebyshev expansion that the light-cell approximation actually uses.
Formal statement
Proof (Lean source)
Uniform reciprocal-approximation certificate on [0,1].
Formal statement
Proof (Lean source)
Cone approximation bound for the explicit four-cell polynomial.
Formal statement
Proof (Lean source)
Establishes the stated property of env C in the discrete average-treatment-effect construction.
Formal statement
Establishes the stated property of env X in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Shows that env nonneg is nonnegative.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for env pow le.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for env sum le.
Formal statement
Proof (Lean source)
Defines gpos, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of abs g Coefficient in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of sign g Coefficient in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated equality relating gpos eq.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for chebyshev three le.
Formal statement
Proof (Lean source)
Shows that gpos nonneg is nonnegative.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for gpos bound.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for env arm le.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for env mass le.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for env eval G le.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for env mul4 le.
Formal statement
Proof (Lean source)
The numerical absolute-coefficient certificate with base A=6.
Formal statement
Proof (Lean source)
Helpers.CombinedEnvelope 2 declarations
Deterministic choice between the hybrid and centered estimators.
Definition (Lean source)
The deterministic smaller-bound selector attains the combined envelope.
Formal statement
Proof (Lean source)
Helpers.Endpoint 24 declarations
The bounded one-observation score averaged by centeredEstimator.
Definition (Lean source)
The bounded one-observation score used by the centering estimator always squares to one: it takes only the two values plus one and minus one.
Formal statement
Proof (Lean source)
The centering estimator is exactly the sample average of the bounded one-observation score.
Formal statement
Proof (Lean source)
Establishes the stated property of centered Unit Score mean in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Exact conditional-bias identity on a positive-mass category.
Formal statement
Proof (Lean source)
Establishes the stated equality relating joint Mass eq zero of cell Mass eq zero.
Formal statement
Proof (Lean source)
Establishes the stated summation identity or bound for cell Mass sum.
Formal statement
Proof (Lean source)
Establishes the stated property of centered Unit Score bias identity in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for centered Unit Score bias bound.
Formal statement
Proof (Lean source)
Establishes the stated property of centered Estimator mean in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for centered Unit Score variance le one.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for centered Estimator variance le.
Formal statement
Proof (Lean source)
Establishes the stated equality relating mse eq variance add sq bias.
Formal statement
Proof (Lean source)
All-n,d MSE bound for the centered estimator.
Formal statement
Proof (Lean source)
Defines endpoint Parametric Law, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines endpoint Parametric Pert Law, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of endpoint Parametric Law joint Mass in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of endpoint Parametric Pert Law joint Mass in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of endpoint Parametric Law overlap in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of endpoint Parametric Pert Law overlap in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of endpoint Parametric Law ate in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of endpoint Parametric Pert Law ate in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Explicit one-category Bernoulli two-point lower bound at randomization.
Formal statement
Proof (Lean source)
At exact randomization the minimax risk is parametric uniformly in d.
Formal statement
Proof (Lean source)
Helpers.Estimator 42 declarations
The balanced deterministic half-sample split.
Definition (Lean source)
The number of observations in one half of the deterministic sample split: the first half holds the floor of n over two indices, the second half the rest.
Definition (Lean source)
Count of one (k,a,y) atom in a split.
Definition (Lean source)
The number of observations in one half of the split whose category coordinate equals a given value.
Definition (Lean source)
The total degree of a four-cell exponent vector, that is, the sum of its four exponents.
Definition (Lean source)
Falling factorial, reusing Mathlib's Nat.descFactorial.
Definition (Lean source)
The logarithmic scale log(e n), equivalently one plus the natural logarithm of the sample size. Every calibration in the estimator -- polynomial degree, bandwidth and heavy-cell threshold -- is measured against this scale.
The numerical calibration constant A = 6, the base of the coefficient-envelope growth factor A raised to the polynomial degree that bounds the light-cell approximation.
Definition (Lean source)
The numerical calibration constant lambda_0 = 256 fixing the pilot heavy/light threshold: a category is declared heavy when its pilot-half count exceeds lambda_0 times log(e n).
Definition (Lean source)
The numerical calibration constant b_0 = 4096 fixing the light-cell bandwidth, which is b_0 times log(e n) divided by the size of the estimation half-sample.
Definition (Lean source)
The numerical calibration constant eight times the natural logarithm of 27/4, one of the two reciprocal caps that define the degree-calibration constant alpha_0.
Definition (Lean source)
The degree-calibration constant alpha_0: the smallest of one, the reciprocal of 32 log 6, and the reciprocal of 256 times the constant d_A = 8 log(27/4). It fixes the proportion of the logarithmic scale used as the approximation degree.
The calibrated approximation degree M(n): the larger of two and the integer part of alpha_0 times log(e n). This is the degree of the polynomial that replaces the plug-in ratio on light cells.
Definition (Lean source)
Defines bandwidth, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Defines cutoff Property, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of cutoff Property eventually in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Least numerical cutoff satisfying the three calibration inequalities.
Definition (Lean source)
Coefficient of the explicit polynomial continuation G_M.
Definition (Lean source)
Explicit closed polynomial continuation of G_M.
Definition (Lean source)
The formal linear polynomial in the four cell masses that returns the total mass of one treatment arm, namely the sum of that arm's outcome-zero and outcome-one coordinates.
The formal linear polynomial in the four cell masses that returns the total mass of a category, namely the sum of the two arm masses.
Definition (Lean source)
The multivariate polynomial P_{M,B} whose coefficients are factorial-lifted.
Definition (Lean source)
The unbiased factorial-moment estimate of one monomial in the four cell masses of a category: the product over the four cells of the falling factorial of that cell's estimation-half count at the corresponding exponent, divided by the falling factorial of the estimation-half sample size at the total degree.
Definition (Lean source)
Merged exponent vector in the sparse binomial expansion of one arm of cellApproxPolynomial.
Definition (Lean source)
Factorial-moment lift of the light-cell approximation polynomial, written in its sparse arm/binomial expansion. Keeping duplicate displayed monomials is intentional: linearity collects them to the coefficient-support form.
Definition (Lean source)
Pilot-heavy cells; below the cutoff every category uses the ratio branch.
Definition (Lean source)
Pilot-light cells; below the cutoff this is empty as stipulated in the note.
Definition (Lean source)
At or above the calibration cutoff, the heavy set is exactly the set of categories whose pilot-half count exceeds lambda_0 times log(e n).
Formal statement
Proof (Lean source)
Below the calibration cutoff every category is declared heavy, so the estimator reduces to the plug-in ratio branch on all of them.
Formal statement
Proof (Lean source)
Establishes the stated equality relating light Cells eq empty of lt cutoff.
Formal statement
Proof (Lean source)
Establishes the stated equality relating light Cells eq compl.
Formal statement
Proof (Lean source)
Defines empirical Ratio Cell, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines heavy Contribution, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines light Contribution, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Universally calibrated balanced ratio-polynomial hybrid, truncated to [-1,1]. Its type has no overlap parameter: overlap adaptation is structural.
Definition (Lean source)
Inputs available to the arithmetic realization: the eight split counts for each category. All dependence of the hybrid on the observed sample factors through this finite vector.
Definition (Lean source)
The finite vector of counts through which the hybrid estimator sees the sample: for each half of the split, each category, each treatment value and each outcome value, the number of matching observations, recorded as a real number.
Definition (Lean source)
One instruction in a straight-line real-arithmetic program. Natural numbers address previously computed registers, allowing factorials and powers to be computed once and shared across all polynomial monomials.
Definition (Lean source)
A finite instruction list paired with its designated output register.
Definition (Lean source)
Clause (i)'s computability assertion, in the real-arithmetic model used in the note. A universal operation-count constant works for every n,d; the program reads only split counts, returns the stated hybrid exactly, and has O(d M(n)^4) arithmetic/comparison operations.
Definition (Lean source)
The sample average of a bounded one-observation score obtained by centering the binary outcome at one half, doubling it, and attaching the sign of the treatment indicator -- positive for treated units and negative for controls.
Definition (Lean source)
Helpers.FactorialMoments 4 declarations
Falling-factorial product identity used for within-cell moments.
Formal statement
Proof (Lean source)
The ordered injective tuple count is the normalizing falling factorial.
Formal statement
Proof (Lean source)
Ratio estimate for two normalized ordered selections.
Formal statement
Proof (Lean source)
Sharp disjoint-selection normalization. This is the covariance factor for two monomials attached to distinct multinomial categories: the two ordered selections cannot share observations, so their joint moment differs from the product of their means only through this falling-factorial ratio.
Formal statement
Proof (Lean source)
Helpers.HeavyCell 54 declarations
The deterministic half split used by the estimator, packaged in the generic one-shot independence interface.
Definition (Lean source)
Transport a finite-sample integral to the canonical infinite IID sample. This lets the heavy branch use the same tail-count realization as the light branch while keeping the theorem stated under productLaw.
Formal statement
Proof (Lean source)
The mean squared deviation of an estimator component from its target, computed under the n-fold product law, equals the same expectation taken over the canonical infinite independent sample restricted to its first n coordinates.
Formal statement
Proof (Lean source)
Defines target Heavy, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines fixed Heavy Contribution, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines fixed Target Heavy, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines fixed Heavy Arm Contribution, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines fixed Target Arm, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines fixed Empirical Mass Arm, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
One-observation bounded score whose sample mean is the empirical category-mass centering of a fixed arm.
Definition (Lean source)
The fixed-mass score of an observation reduces to a single lookup: it returns the outcome regression of the given treatment arm at the observation's own category when that category belongs to the selected set, and zero otherwise.
Formal statement
Proof (Lean source)
Shows that fixed Mass Score mem unit Interval lies in the stated set or interval.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral fixed Mass Score eq.
Formal statement
Proof (Lean source)
Establishes the stated equality relating heavy Contribution eq fixed.
Formal statement
Proof (Lean source)
Establishes the stated equality relating target Heavy eq fixed.
Formal statement
Proof (Lean source)
Establishes the stated equality relating fixed Heavy Contribution eq arm sub.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for fixed Heavy Arm error sq le noise mass.
Formal statement
Proof (Lean source)
Above the calibration cutoff, the estimator's heavy set is exactly the pilot set controlled by the sandwich theorem at its calibrated threshold.
Formal statement
Proof (Lean source)
On the pilot-sandwich event, every selected heavy category has the deterministic mass lower bound required by the missing-arm estimates.
Formal statement
Proof (Lean source)
Within one half of the split, the number of observations falling in a single treatment-outcome cell of a category never exceeds the number of observations falling in that category.
Formal statement
Proof (Lean source)
The tuple obtained by restricting a finite sample to one deterministic split.
Definition (Lean source)
The abstract category index set is exactly the implemented split category count.
Formal statement
Proof (Lean source)
The abstract nested arm index set is exactly the sum of the two implemented outcome counts in that arm.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for missing Index Count split Tuple.
Formal statement
Proof (Lean source)
The abstract residual sum on a split tuple is the implemented arm-success count minus its conditional-mean centering.
Formal statement
Proof (Lean source)
Restricting the canonical finite product sample to either deterministic split again has the corresponding finite product law.
Formal statement
Proof (Lean source)
Integral transport from the full sample to either deterministic split.
Formal statement
Proof (Lean source)
Summing the fixed-mass score over the observations of one half of the split gives the sum, over the selected categories, of each category's count in that half times its outcome regression for the given treatment arm.
Formal statement
Proof (Lean source)
Establishes the stated equality relating fixed Empirical Mass Arm sub target eq score.
Formal statement
Proof (Lean source)
A fixed empirical category-mass arm score has variance at most one over the estimation-fold size.
Formal statement
Proof (Lean source)
Exact pointwise decomposition of the implemented arm ratio error about its empirical category-mass centering. The first term is centered ratio noise; the second is precisely the bias from an unobserved treatment arm.
Formal statement
Proof (Lean source)
Fixed-set product-law MSE of the arm ratio about its empirical mass centering. The first two terms are parametric ratio and missing-label diagonals; the final term is the aggregate exponentially damped missing-arm bias envelope.
Formal statement
Proof (Lean source)
The implemented category and arm counts satisfy the sharp aggregate inverse-count bound on either split.
Formal statement
Proof (Lean source)
Establishes the stated property of heavy Cells rebuild Pilot in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of split Category Count rebuild Estimation in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of fixed Heavy Arm Contribution rebuild Estimation in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Freezing one pilot-selected set factors its fiber probability from every fixed-set estimation-fold arm error.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral split count ratio le.
Formal statement
Proof (Lean source)
Shows that empirical arm ratio mem unit Interval lies in the stated set or interval.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for abs empirical Ratio Cell le.
Formal statement
Proof (Lean source)
Establishes the stated summation identity or bound for sum split Category Count.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for abs heavy Contribution le one.
Formal statement
Proof (Lean source)
Establishes the stated equality relating cell Phi cell Vector eq weighted.
Formal statement
Proof (Lean source)
Establishes the stated equality relating fixed Target Heavy eq arm sub.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for fixed Heavy error sq le two arms.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for abs cell Phi cell Vector le mass unconditional.
Formal statement
Proof (Lean source)
Establishes the stated equality relating sum cell Mass eq one.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for abs target Heavy le one.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for heavy component sq le four.
Formal statement
Proof (Lean source)
Pilot failure costs at most four times its probability, using the global range bound for the heavy component and its target.
Formal statement
Proof (Lean source)
The complete pilot-failure contribution is fourth-order polynomially small, uniformly over the calibrated dimension range.
Formal statement
Proof (Lean source)
Any uniform fixed-set arm bound transfers unchanged to the random pilot-selected set on the pilot-good event.
Formal statement
Proof (Lean source)
The deterministic fixed-heavy-set envelope has the target minimax rate, uniformly in the set and the underlying discrete law.
Formal statement
Proof (Lean source)
The aggregate ratio branch has the same rate on pilot-heavy categories.
Formal statement
Proof (Lean source)
Helpers.HeavyCellMoments 103 declarations Probability and finite-sample algebra used by the ratio branch.
Probability and finite-sample algebra used by the ratio branch. These lemmas are deliberately stated independently of the calibrated estimator, so that the handling of an empty empirical treatment arm can be reused.
The elementary pointwise inequality behind the inverse-binomial bound. The indicator is written explicitly to match Lean's total division convention.
Formal statement
Proof (Lean source)
Multiplying a binomial coefficient by the reciprocal count shifts the coefficient from row t to row t+1.
Formal statement
Proof (Lean source)
Exact finite-binomial reciprocal identity. This is equation (2) of the heavy-cell proof before dropping the numerator.
Formal statement
Proof (Lean source)
The inverse-binomial estimate used for conditional ratio variance.
Formal statement
Proof (Lean source)
First moment of the finite binomial weights.
Formal statement
Proof (Lean source)
Pure nested-binomial ratio bound. This is the complete analytic calculation after conditioning a category count N to equal t: the arm count is binomial with success probability rho, and the outer category count is binomial with success probability p.
Formal statement
Proof (Lean source)
Exact inverse-cardinality expectation for a Bernoulli random subset of a fixed finite set. This supplies the conditional arm-count law without any abstract regular-conditional-probability API.
Formal statement
Proof (Lean source)
Conditional inverse arm-count bound on a fixed active category set.
Formal statement
Proof (Lean source)
Elementary exponential envelope used after the exact missing-arm moments have been counted.
Formal statement
Proof (Lean source)
Exponential upper bound for the exact diagonal missing-arm second-moment formula. No asymptotics or independence approximation enters this step.
Formal statement
Proof (Lean source)
Overlap substitution in the missing-arm exponential envelope.
Formal statement
Proof (Lean source)
A quadratic envelope for exponential decay. This is the analytic step that converts the heavy-cell mass lower bound into the extra logarithm in the aggregate missing-arm term.
Formal statement
Proof (Lean source)
Aggregate exponential envelope on a set of cells whose masses are all at least B. With u of order the estimation-fold size and B of order log n / n, this is exactly the d / (n log n) term.
Formal statement
Proof (Lean source)
The observed success mass in one treatment arm factors into its arm mass and conditional outcome mean. The statement also handles a zero-mass arm, where Lean's totalized conditional mean is zero.
Formal statement
Proof (Lean source)
One-observation outcome residual for a specified category and arm.
Definition (Lean source)
The category-arm outcome residual is centered under one observation.
Formal statement
Proof (Lean source)
A multiplier depending on an observation only through its category and treatment design preserves residual centering.
Formal statement
Proof (Lean source)
Replace only the outcome coordinate of observation i.
Definition (Lean source)
Overwriting the outcome coordinate of one observation leaves that observation's category and treatment coordinates unchanged and installs the new outcome value.
Formal statement
Proof (Lean source)
Overwriting the outcome coordinate of one observation leaves every other observation of the tuple untouched.
Formal statement
Proof (Lean source)
Finite-product conditional-centering lemma. Any sample multiplier that is unchanged when only outcome i is replaced is orthogonal to the centered category-arm residual at i.
Formal statement
Proof (Lean source)
The one-observation residual second moment is bounded by the probability of its category-arm. This is the diagonal input for the ratio variance.
Formal statement
Proof (Lean source)
The one-observation event that the confounder equals the given category.
Definition (Lean source)
The nested one-observation category and treatment-arm event.
Definition (Lean source)
The arm probability inside a positive-mass category, totalized at zero.
Definition (Lean source)
The control-arm and treated-arm masses of a category add up to the total mass of that category.
Formal statement
Proof (Lean source)
The joint probability of a category together with a treatment value is nonnegative.
Formal statement
Proof (Lean source)
The joint probability of a category together with a treatment value never exceeds the total probability of that category.
Formal statement
Proof (Lean source)
Shows that arm Propensity mem unit Interval lies in the stated set or interval.
Formal statement
Proof (Lean source)
Establishes the stated equality relating arm Mass eq cell Mass mul arm Propensity.
Formal statement
Proof (Lean source)
Establishes the stated equality relating arm Propensity eq true.
Formal statement
Proof (Lean source)
Establishes the stated equality relating arm Propensity eq false.
Formal statement
Proof (Lean source)
Overlap supplies the same lower bound for either arm probability.
Formal statement
Proof (Lean source)
The category event has exactly its model cell mass.
Formal statement
Proof (Lean source)
The nested category-arm event has exactly its joint arm mass.
Formal statement
Proof (Lean source)
The one-observation event that both the category and the treatment value are as prescribed is contained in the event that only the category is as prescribed.
Formal statement
Proof (Lean source)
Establishes the stated property of obs Law category Arm diff mass in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of obs Law category Set compl mass in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
A design-only multiplier factors out of the one-observation residual second moment on its unique category-arm support.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral design Weight mul arm Indicator factor.
Proof (Lean source)
Conditional Bernoulli variance bound with an arbitrary nonnegative design-only multiplier.
Formal statement
Proof (Lean source)
Product-sample conditional variance bound at one coordinate, for any nonnegative multiplier unchanged by replacing that coordinate's outcome.
Formal statement
Proof (Lean source)
Product of three constants over a nested two-set partition.
Formal statement
Proof (Lean source)
Indices whose observations land in a measurable or nonmeasurable set.
Definition (Lean source)
Joint event fixing the index set in C and its nested sub-index-set in R.
Definition (Lean source)
Suppose one label set sits inside another and the prescribed inner index set sits inside the prescribed outer one. Then the event that pins down both index sets is a product event over the observations: each inner index observation is confined to the inner label set, each remaining outer index observation to the part of the outer set not in the inner one, and every other observation to the complement of the outer set.
Formal statement
Proof (Lean source)
Exact finite-product mass of a nested pair of index sets. This is the finite symmetry/counting bridge used in place of a conditional-law API.
Formal statement
Proof (Lean source)
Establishes the stated property of index Set mono in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Exact finite-product nested-count identity. In particular, this proves algebraically that the arm count conditional on a category count t has the binomial weights with parameter rho.
Formal statement
Proof (Lean source)
The finite-product nested-count identity, combined with the sharp inverse-binomial calculation. This is the unconditional design bound needed for the heavy-cell variance calculation.
Formal statement
Proof (Lean source)
Specialization of the nested-count theorem to one discrete-ATE category and either treatment arm. Overlap replaces the arm probability denominator by the uniform lower bound epsilon.
Formal statement
Proof (Lean source)
Ratio coefficient multiplying one category's residual sum.
Definition (Lean source)
Aggregate centered ratio residual over a fixed category set.
Definition (Lean source)
Overwriting the outcome coordinate of one observation does not change which observations belong to a given category.
Formal statement
Proof (Lean source)
Establishes the stated property of index Set replace Outcome arm in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for tuple Ratio Coeff replace Outcome.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral ratio Residual cross coordinates eq zero.
Formal statement
Proof (Lean source)
Establishes the stated equality relating arm Outcome Residual mul eq zero of ne.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral ratio Residual diagonal le.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral ratio Residual pair eq zero of ne.
Formal statement
Proof (Lean source)
All off-diagonal residual terms cancel exactly, across both observations and distinct categories.
Formal statement
Proof (Lean source)
Summing the squared ratio coefficient over observations in its arm produces exactly the nested count-ratio integrand.
Formal statement
Proof (Lean source)
Aggregate fixed-set residual variance. Cross-cell cancellation preserves the parametric order and the only overlap loss is one factor epsilon inverse.
Formal statement
Proof (Lean source)
One selected observation has label s, while every observation avoids the forbidden label r.
Definition (Lean source)
When the prescribed label differs from the forbidden one, the event that a distinguished observation carries the prescribed label while no observation carries the forbidden one is a product event: the distinguished coordinate is confined to the prescribed label and every other coordinate to the complement of the forbidden one.
Formal statement
Proof (Lean source)
Exact product probability of one selected non-forbidden label and no forbidden labels among the remaining observations.
Formal statement
Proof (Lean source)
Two distinct selected observations have prescribed labels while the whole sample avoids a third, forbidden label.
Definition (Lean source)
When two distinct distinguished observations carry two labels, each different from a third forbidden label, the event that they do so while no observation carries the forbidden label is a product event: each distinguished coordinate is confined to its own label and every remaining coordinate to the complement of the forbidden one.
Formal statement
Proof (Lean source)
Exact missing-label two-selection probability, the cross-cell term in equation (4) of the heavy-cell proof.
Formal statement
Proof (Lean source)
Set-valued version used for an entire treatment arm: the selected observation belongs to S, and every observation avoids the disjoint set R.
Definition (Lean source)
When two sets of labels are disjoint, the event that a distinguished observation falls in the first set while no observation falls in the second is a product event: the distinguished coordinate is confined to the first set and every other coordinate to the complement of the second. This is the form used when the first set is a whole treatment arm rather than a single label.
Formal statement
Proof (Lean source)
Exact one-selection/no-forbidden-set product probability.
Formal statement
Proof (Lean source)
Number of observations in a category when its specified nested arm is entirely missing.
Definition (Lean source)
A missing-arm category count is the sum of one-selected/no-forbidden-arm indicators.
Formal statement
Proof (Lean source)
Two ordered, distinct selected observations belong to S, while all observations avoid the disjoint forbidden set R.
Definition (Lean source)
When the two sets are disjoint, the event that two distinct distinguished observations both fall in the first set while no observation falls in the second is the product event confining the two distinguished coordinates to the first set and every remaining coordinate to the complement of the second.
Formal statement
Proof (Lean source)
Exact ordered-pair/no-forbidden-set probability. Summing this lemma over ordered distinct indices produces the (m)_2 s^2 (1-r)^(m-2) term in the missing-arm second moment.
Formal statement
Proof (Lean source)
Summed diagonal part of the exact missing-arm second moment.
Formal statement
Proof (Lean source)
Exact first moment of the missing-arm category count in the discrete ATE model.
Formal statement
Proof (Lean source)
Summed ordered-pair part of the exact missing-arm second moment. Together with sum_measure_oneSelectedAvoidSetEvent, this is precisely equation (4)'s m s (1-r)^(m-1) + (m)_2 s^2 (1-r)^(m-2) decomposition.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for one Selected indicator sq.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for one Selected indicator mul.
Formal statement
Proof (Lean source)
Exact pointwise diagonal/off-diagonal expansion of a squared missing-arm category count.
Formal statement
Proof (Lean source)
Exact second moment of one cell's category count on the event that a specified treatment arm is absent.
Formal statement
Proof (Lean source)
Cross-category event: the two selected observations may belong to different sets, and the full sample avoids a common forbidden set.
Definition (Lean source)
When a forbidden set of labels is disjoint from each of two prescribed sets, the event that one distinguished observation falls in the first set, a second distinct distinguished observation falls in the second set, and no observation falls in the forbidden set, is the product event confining each distinguished coordinate to its own set and every remaining coordinate to the complement of the forbidden set.
Formal statement
Proof (Lean source)
Exact cross-category ordered-pair probability. Taking R to be the union of the two treated-arm atoms gives the second line of equation (4).
Formal statement
Proof (Lean source)
Summed cross-category ordered-pair term.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for one Selected indicator mul cross.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for one Selected indicator mul zero of disjoint.
Formal statement
Proof (Lean source)
Distinct categories cannot contribute through the same observation, so their missing-arm product is an ordered-pair cross-event sum.
Formal statement
Proof (Lean source)
Establishes the stated property of category Set disjoint of ne in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Exact cross moment of the missing-arm counts in two distinct categories.
Formal statement
Proof (Lean source)
Defines fixed Missing Count, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines fixed Missing Outcome Bias, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated upper bound for abs fixed Missing Outcome Bias le.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for fixed Missing Outcome Bias sq le.
Formal statement
Proof (Lean source)
Establishes the stated property of fixed Missing Count sq expand in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Exact aggregate missing-arm second moment on a fixed category set.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for desc Factorial two cast le sq.
Formal statement
Proof (Lean source)
Establishes the stated property of missing diag envelope in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of missing cross envelope in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Aggregate second-moment bound for the missing-arm count on a fixed set of heavy categories. The diagonal contributes at most m; the off-diagonal and exponentially small part of the diagonal combine into the square of one mass-exponential sum.
Formal statement
Proof (Lean source)
Helpers.HybridProgram 74 declarations A verified tree-to-straight-line compiler
A verified tree-to-straight-line compiler
Defines hybrid Term Index, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Syntax trees over exactly the operations admitted by RealArithmeticInstruction.
Definition (Lean source)
The value of an arithmetic syntax tree under a given assignment of its inputs. Input and constant nodes return their own value; the addition, subtraction, multiplication and division nodes apply the corresponding real operation to the values of their two subtrees, division following the total convention that dividing by zero returns zero; the branch node returns the value of its second subtree when its first subtree evaluates to a nonpositive number and of its third subtree otherwise.
Definition (Lean source)
Defines node Count, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Defines operation Count, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of node Count pos in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Compile an expression after offset already occupied registers.
Definition (Lean source)
The compiled instruction list for an expression has exactly one instruction per node of its expression tree.
Formal statement
Proof (Lean source)
Defines run From, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of run From append in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated equality relating run From eq append.
Formal statement
Proof (Lean source)
Establishes the stated property of run From get D of lt in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Executing a list of instructions appends exactly one register value for each instruction, leaving the initial registers in place.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for get D append singleton length.
Proof (Lean source)
Establishes the stated property of code At correct in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Defines program, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of eval program in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of operation Count code At in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of operation Count program in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Defines expression Sum, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines expression Product, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated equality relating list range sum eq finset sum.
Formal statement
Proof (Lean source)
Evaluating the expression formed by summing a list gives the sum of the separately evaluated expressions.
Formal statement
Proof (Lean source)
Evaluating the expression formed by multiplying a list gives the product of the separately evaluated expressions.
Formal statement
Proof (Lean source)
The cost of a summed expression is the sum of the component costs plus one addition for every list entry.
Formal statement
Proof (Lean source)
The cost of a product expression is the sum of the component costs plus one multiplication for every list entry.
Formal statement
Proof (Lean source)
Real-arithmetic implementation of truncated natural subtraction, on natural-valued inputs.
Definition (Lean source)
The expression that implements truncated subtraction is correct: if a subexpression evaluates to a whole number, then guarding it by the branch node and subtracting a whole constant returns the truncated difference, which is zero whenever the constant is at least as large.
Formal statement
Proof (Lean source)
Defines falling Expression, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of eval falling Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of operation Count nat Sub Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of operation Count falling Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Defines hybrid Cell List, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Establishes the stated summation identity or bound for hybrid Cell List sum.
Proof (Lean source)
Establishes the stated property of hybrid Cell List prod in the discrete average-treatment-effect construction.
Proof (Lean source)
Establishes the stated equality relating split Category Count eq sum cell.
Formal statement
Proof (Lean source)
Defines split Count Expression, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines category Count Expression, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of eval split Count Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of eval category Count Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Defines factorial Monomial Expression, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of eval factorial Monomial Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of operation Count split Count Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of operation Count factorial Monomial Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Defines arm Factorial Expression, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines light Cell Expression, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of eval arm Factorial Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of eval light Cell Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of multi Degree hybrid Term Index in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of operation Count factorial Term in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for list sum map le length mul.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for operation Count arm Factorial Expression le.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for operation Count light Cell Expression le.
Formal statement
Proof (Lean source)
Defines heavy Cell Expression, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of eval heavy Cell Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of operation Count heavy Cell Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Defines selected Cell Expression, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated upper bound for eval selected Cell Expression.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for polynomial Degree two le.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for operation Count selected Cell Expression le.
Formal statement
Proof (Lean source)
Defines untruncated Hybrid Expression, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines clamp Expression, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines hybrid Expression, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated equality relating heavy add light eq selected sum.
Formal statement
Proof (Lean source)
Establishes the stated property of eval untruncated Hybrid Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of eval clamp Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of eval hybrid Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for operation Count untruncated Hybrid Expression le.
Formal statement
Proof (Lean source)
Establishes the stated property of operation Count clamp Expression in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for operation Count hybrid Expression le.
Formal statement
Proof (Lean source)
The requested straight-line program. The zero-alphabet branch is a zero-cost constant; otherwise it is the verified compilation of the exact count expression above.
Definition (Lean source)
The compiled straight-line program computes the hybrid estimator exactly: run on the vector of split counts of any sample, its designated output register holds the value of the hybrid estimator at that sample.
Formal statement
Proof (Lean source)
Establishes the stated property of hybrid Arithmetic Program operation Count in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Exact computability and the uniform O(d M(n)^4) operation certificate.
Formal statement
Proof (Lean source)
Helpers.LightCell 15 declarations
Defines target Light, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines component Error MSE, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines minimax Rate, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated equality relating light Cells eq pilot Heavy At compl of cutoff le.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for selected light mass le bandwidth quarter.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for selected light approximation bias.
Formal statement
Proof (Lean source)
Shows that integrable factorial Polynomial Contribution trunc is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral factorial Polynomial Contribution trunc.
Formal statement
Proof (Lean source)
Establishes the stated equality relating sparse Polynomial Mean eq cell Approx.
Formal statement
Proof (Lean source)
Defines selected Genuine Light Bias, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated upper bound for selected Genuine Light Bias abs.
Formal statement
Proof (Lean source)
Establishes the stated property of polynomial Degree lower half in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
The selected genuine-light approximation bias has the squared minimax normalization.
Formal statement
Proof (Lean source)
Establishes the stated property of light error decompose in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
The factorial-polynomial light branch attains the fixed-interior minimax rate. The constants are chosen before the law and are allowed to depend only on the fixed overlap constant.
Formal statement
Proof (Lean source)
Helpers.LightCellAssembly 41 declarations
Equips the stated space with the measurable structure used in this construction.
Definition (Lean source)
Defines iid Sample Shift, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines iid Sample Map, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines category Cell Label, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated upper bound for category Cell Label measurable.
Formal statement
Proof (Lean source)
Defines option Cell Exponent, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of exponent Degree option Cell Exponent in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of category Cell Label atom mass in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated equality relating split Size zero eq.
Formal statement
Proof (Lean source)
Establishes the stated equality relating split Size one eq.
Formal statement
Proof (Lean source)
Defines estimation Tail Index, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated equality relating split Cell Count eq tail count.
Formal statement
Proof (Lean source)
Establishes the stated property of category Cell Label fiber card in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Defines estimation Label Sample, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated upper bound for multinomial Factorial Count estimation Label Sample.
Formal statement
Proof (Lean source)
Establishes the stated equality relating factorial Monomial eq normalized multinomial Count.
Formal statement
Proof (Lean source)
Defines light Cell Estimation IID, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated equality relating factorial Monomial trunc eq iid Count.
Formal statement
Proof (Lean source)
Shows that integrable factorial Monomial trunc is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral factorial Monomial trunc.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral factorial Monomial mul trunc le.
Formal statement
Proof (Lean source)
Shows that integrable factorial Monomial mul trunc is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Defines observation Exponent, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of exponent Degree observation Exponent in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of estimation Tail fiber card in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of observation Exponent fiber count in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of multinomial Factorial Count observation Exponent in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated equality relating factorial Monomial eq normalized observation Count.
Formal statement
Proof (Lean source)
Establishes the stated equality relating factorial Monomial trunc eq observation Count.
Formal statement
Proof (Lean source)
Establishes the stated property of obs Law real cell Atom in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of observation Exponent mass prod in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral factorial Monomial cross trunc.
Formal statement
Proof (Lean source)
Establishes the stated property of vector Mass cell Vector in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of vector Arm Mass cell Vector in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for obs Law real singleton.
Formal statement
Proof (Lean source)
Establishes the stated property of obs Law real atom in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Shows that cell Vector mem overlap Cone lies in the stated set or interval.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for abs cell Phi cell Vector le mass.
Formal statement
Proof (Lean source)
Establishes the stated property of multi Degree factorial Expansion Index in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of factorial Expansion Index prod in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated summation identity or bound for factorial Expansion Index binomial sum.
Formal statement
Proof (Lean source)
Helpers.LightCellRateAsymptotic 10 declarations
The calibrated cutoff already forces the numerical log-scale used by the rate algebra. The apparently separate 240 hypothesis is therefore free once n is above calibrationCutoff.
Formal statement
Proof (Lean source)
The single elementary growth inequality used in the rate algebra: 6^(4M) L^6 ≤ n.
Formal statement
Proof (Lean source)
Establishes the stated property of eventually light rate cutoff in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Defines light Asymptotic Rate, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines genuine Light Set, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated upper bound for large calibration bounds.
Formal statement
Proof (Lean source)
Establishes the stated property of diagonal rate algebra in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of cross rate algebra in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Rate-normalized version of equation (17) for the pilot-selected genuinely light cells.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for selected False Light Error rate.
Formal statement
Proof (Lean source)
Helpers.LightCellRateDeterministic 41 declarations
A flattened index set for one arm of the sparse factorial lift.
A triple made of an outer index, an inner index and a cell belongs to the flattened sparse index set exactly when the outer index is strictly below the degree minus one and the inner index does not exceed the outer one.
Formal statement
Proof (Lean source)
Selecting, from the first M whole numbers, those that do not exceed a given number below M leaves exactly the first j+1 whole numbers.
Formal statement
Proof (Lean source)
Establishes the stated summation identity or bound for sum sparse Index Set.
Formal statement
Proof (Lean source)
Defines sparse Term, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated equality relating sparse Arm Contribution eq sum sparse Term.
Formal statement
Proof (Lean source)
Establishes the stated property of sparse Index degree in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for sparse Index inner le.
Formal statement
Proof (Lean source)
Defines sparse Term Envelope, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated equality relating sum sparse Term Envelope eq sparse Arm Envelope.
Formal statement
Proof (Lean source)
Shows that integrable sparse Term mul is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Shows that integrable sparse Term is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
The diagonal arm bound obtained by summing the joint factorial-moment certificate over the flattened sparse polynomial.
Formal statement
Proof (Lean source)
A genuinely light cell has a uniformly bounded shifted coefficient envelope. This is equation (15) followed by the exact A=6 certificate.
Formal statement
Proof (Lean source)
The absolute-coefficient envelope of one treatment arm in the sparse factorial expansion is nonnegative whenever the four cell values it is evaluated at are nonnegative.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral sparse Arm sq rate le.
Formal statement
Proof (Lean source)
Shows that integrable sparse Arm sq is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Shows that integrable sparse Arm is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Shows that integrable factorial Polynomial Contribution trunc rate is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Shows that integrable factorial Polynomial Contribution sq is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Diagonal second moment of one genuinely light polynomial cell.
Formal statement
Proof (Lean source)
Defines sparse Term Mean, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines sparse Arm Mean, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines sparse Polynomial Mean, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Shows that integrable factorial Monomial cross trunc is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Shows that integrable sparse Term cross mul is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral sparse Term eq mean.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral sparse Arm Contribution eq mean.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral factorial Polynomial Contribution eq sparse Polynomial Mean.
Formal statement
Proof (Lean source)
Establishes the stated property of sparse Term Mean abs in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated equality relating sum abs sparse Term Mean eq envelope.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for sparse Arm Mean abs le envelope.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for sparse Term cross covariance le.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for sparse Arm cross covariance le.
Formal statement
Proof (Lean source)
Shows that integrable sparse Arm cross mul is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Establishes the stated property of factorial Polynomial cross covariance decompose in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Equation (16): covariance between distinct light categories, with all normalization constants explicit.
Formal statement
Proof (Lean source)
Shows that integrable factorial Polynomial cross mul is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
The off-diagonal centered covariance estimate, packaged separately so that the pilot-selection layer need not normalize a large factorial expression.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for sparse Polynomial Mean abs le.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral factorial Polynomial centered sq le.
Formal statement
Proof (Lean source)
Helpers.LightCellRatePilot 32 declarations
The balanced split, duplicated here to keep the light-cell assembly below the final LightCell module in the import graph.
Definition (Lean source)
Reassembles a full n-observation sample out of the pilot half alone: positions below the floor of n over two take the supplied pilot observations, and every later position takes a fixed filler observation. Statistics that read only the pilot half are unaffected by the choice of filler.
Definition (Lean source)
Defines rebuild Estimation Sample, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of split Category Count rebuild Pilot in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of light Cells rebuild Pilot in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of split Cell Count rebuild Estimation in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of factorial Monomial rebuild Estimation in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of factorial Polynomial Contribution rebuild Estimation in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Defines light Indicator, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of light Indicator rebuild Pilot in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Exact pilot/estimation factorization for two selected centered cell errors. This is the formal conditioning step behind equation (25).
Formal statement
Proof (Lean source)
Shows that light Indicator nonneg is nonnegative.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for light Indicator le one.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral light Indicator pair mem Icc.
Formal statement
Proof (Lean source)
Shows that integrable centered Polynomial pair is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Shows that integrable selected centered Polynomial pair is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Defines selected Fixed Light Centered, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated upper bound for selected Fixed Light Centered second moment le.
Formal statement
Proof (Lean source)
Coefficient growth away from the genuinely-light cone. This is the quantitative content of equations (21)--(22), before inserting the pilot-tail exponent.
Formal statement
Proof (Lean source)
Establishes the stated property of sparse Arm Envelope cell growth in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral factorial Polynomial sq growth.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving light integral product Law eq infinite.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral light Indicator eq probability.
Formal statement
Proof (Lean source)
Equation (20) for the actual calibrated light indicator.
Formal statement
Proof (Lean source)
The positive polynomial growth is dominated by the calibrated pilot-tail exponent. The deliberately coarse constant 49 leaves ample slack.
Formal statement
Proof (Lean source)
Establishes the stated property of light Indicator target pair factorization in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral factorial Polynomial target sq growth.
Formal statement
Proof (Lean source)
Equations (20)--(24) combined for one falsely selected light cell.
Formal statement
Proof (Lean source)
Defines false Light Set, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines selected False Light Error, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Shows that integrable selected target pair is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Summed false-light remainder from equations (23)--(24).
Formal statement
Proof (Lean source)
Helpers.LightCellVariance 15 declarations
Absolute sparse coefficient sum for one arm of the factorial lift.
Definition (Lean source)
For a positive bandwidth and nonnegative cell values, the absolute-coefficient envelope of one treatment arm collapses to a closed form: the reciprocal bandwidth, times the total four-cell mass, times that arm's outcome-one coordinate, times the absolute-coefficient series of the polynomial continuation evaluated at the arm's own mass divided by the bandwidth.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for sparse Arm Envelope le.
Formal statement
Proof (Lean source)
Establishes the stated property of multi Monomial mono in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Shows that multi Monomial nonneg is nonnegative.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral factorial Monomial mul shift le.
Formal statement
Proof (Lean source)
Defines sparse Coefficient, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines sparse Arm Contribution, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated equality relating factorial Polynomial Contribution eq sparse Arms.
Formal statement
Proof (Lean source)
Defines shifted Cell Vector, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Shows that shifted Cell Vector nonneg is nonnegative.
Formal statement
Proof (Lean source)
Establishes the stated summation identity or bound for shifted Cell Vector sum.
Formal statement
Proof (Lean source)
Shows that factorial Monomial nonneg is nonnegative.
Formal statement
Proof (Lean source)
Evaluates or bounds the stated integral involving integral sparse terms mul shift le.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for factorial Monomial cross covariance le.
Formal statement
Proof (Lean source)
Helpers.LowerBound 10 declarations
The control-zero subclass D₀: overlap laws with mu_0k=0 in every cell.
Definition (Lean source)
A law of the control-zero subclass: an observation law together with the evidence that it belongs to the overlap experiment class and has an identically zero control-arm outcome regression in every category.
Definition (Lean source)
Treated-arm functional psi₁(P)=sum_k p_k mu_1k.
Definition (Lean source)
The worst-case mean squared error of a single estimator over the control-zero subclass, taken against the treated-arm functional -- the category-mass weighted average of the treated outcome regression.
Definition (Lean source)
The minimax risk for estimating the treated-arm functional over the control-zero subclass: the infimum, over measurable estimators, of their worst-case mean squared error on that subclass.
Definition (Lean source)
A uniform finite-alphabet bound used to justify the two class suprema.
Formal statement
Proof (Lean source)
Cited gate (Zeng, Balakrishnan, Han, Kennedy, 2026). Source handle cite:zeng-balakrishnan-han-kennedy-2024, arXiv:2405.00118v3, Theorem 2 and Appendix C.5, with the fixed-sample transfer in Lemma 4 and Appendix D.2. This is the documented fixed-sample control-zero specialization: the treated-arm minimax risk has the stated scale for every positive alphabet size in the source range.
Definition (Lean source)
On the control-zero subclass the observed-data ATE is the treated functional.
Formal statement
Proof (Lean source)
Restricting the global ATE experiment to the control-zero subclass can only decrease minimax risk. The target identity is proved law-by-law before the subclass supremum and common estimator infimum are compared.
Formal statement
Proof (Lean source)
Transfers the cited control-zero one-arm converse to the unrestricted ATE minimax problem by restriction of the law class.
Formal statement
Proof (Lean source)
Helpers.MultinomialMoments 36 declarations
Indices in the fibre of a finite labelling.
Definition (Lean source)
Ordered injective selections whose observed labels match a prescribed pattern.
Definition (Lean source)
Multinomial ordered-pattern cardinality, factored over label fibres.
Formal statement
Proof (Lean source)
Number of ordered injective selections matching a finite label pattern.
Definition (Lean source)
The weighted count of ordered injective selections whose observed labels match a prescribed pattern is simply the number of such selections.
Formal statement
Proof (Lean source)
Pointwise ordered multinomial count identity.
Formal statement
Proof (Lean source)
Indicator kernel of one labelled tuple.
Definition (Lean source)
The indicator that a labelled tuple equals a prescribed pattern is a measurable function of the tuple.
Formal statement
Proof (Lean source)
A labelled tuple under a finite product law has the product point mass.
Formal statement
Proof (Lean source)
Under an independent identically distributed sample, the probability that a prescribed finite family of distinct sample positions carries a prescribed pattern of labels is the product, over those positions, of the point masses of the required labels.
Formal statement
Proof (Lean source)
Shows that integrable pattern Kernel sample is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
Exact ordered-injective multinomial mean. This is equation (9) before normalization: the number of embeddings contributes (n)_{|I|}, and each labelled tuple contributes its product point mass.
Formal statement
Proof (Lean source)
Shows that integrable matching Count sample is integrable under the stated sampling distribution.
Formal statement
Proof (Lean source)
If two patterns have disjoint label ranges, their matching counts multiply to the matching count of the sum pattern. Observations cannot be shared by the two selections because their required labels differ.
Formal statement
Proof (Lean source)
Exact cross-category ordered-pattern moment (equation (13), raw form).
Formal statement
Proof (Lean source)
Exact cross-category moment for normalized factorial estimators, including the finite-sample falling-factorial covariance ratio in equation (13).
Formal statement
Proof (Lean source)
One distinguishable slot for each occurrence prescribed by an exponent vector.
The label prescribed at a multiindex slot.
Definition (Lean source)
Total degree of a finite exponent vector.
Definition (Lean source)
Product of falling-factorial cell counts, represented as an ordered-pattern count.
Definition (Lean source)
The number of distinguishable slots generated by an exponent vector equals the total degree of that vector, namely the sum of its exponents.
Formal statement
Proof (Lean source)
The ordered-pattern representation is exactly the product of cellwise falling factorials.
Formal statement
Proof (Lean source)
The product of the point masses prescribed at the slots of an exponent vector factors into the point mass of each label raised to that label's exponent.
Formal statement
Proof (Lean source)
Equation (9) for a cell-count multiindex.
Formal statement
Proof (Lean source)
The product of falling-factorial cell counts of the first n observations of an independent identically distributed sample is an integrable function.
Formal statement
Proof (Lean source)
Coordinatewise overlap choices in the product of two factorial monomials.
Definition (Lean source)
Exponent after identifying the selected observations prescribed by an overlap.
Definition (Lean source)
Multiplicity of one overlap pattern in the falling-factorial product identity.
Definition (Lean source)
Total number of identified observations in an overlap choice.
Definition (Lean source)
Establishes the stated upper bound for total Overlap le right.
Formal statement
Proof (Lean source)
Establishes the stated property of exponent Degree merged Exponent in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for factorial ratio overlap bound.
Formal statement
Proof (Lean source)
Exact within-category joint-count expansion underlying equation (12).
Formal statement
Proof (Lean source)
Exact within-category joint mean obtained by integrating the overlap expansion. This is the equality immediately preceding the bound in (12).
Formal statement
Proof (Lean source)
Exact normalized within-category joint moment, displaying the overlap sum and the falling-factorial ratio to which factorial_ratio_bound applies.
Formal statement
Proof (Lean source)
Proved light-cell factorial-moment inequality (equation (12)). The first factorial monomial supplies q^r; all possible overlaps with the second are absorbed by the shifted mass q + |s|/n, with the normalization loss bounded by exp 1.
Formal statement
Proof (Lean source)
Helpers.MvPolynomialEnvelope 9 declarations
Defines monomial Weight, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines coefficient Envelope, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Shows that monomial Weight nonneg is nonnegative.
Formal statement
Proof (Lean source)
Establishes the stated property of monomial Weight add in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of coefficient Envelope extend in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for coefficient Envelope add le.
Formal statement
Proof (Lean source)
Establishes the stated property of coefficient Envelope neg in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for coefficient Envelope sub le.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for coefficient Envelope mul le.
Formal statement
Proof (Lean source)
Helpers.PilotConditioning 3 declarations
Any measurable pilot statistic is independent of any measurable estimation-fold statistic. This is the reusable conditioning interface for freezing the pilot-selected light-cell set before applying factorial-moment bounds on the estimation fold.
Formal statement
Proof (Lean source)
Integral factorization after the pilot/estimation split.
Formal statement
Proof (Lean source)
Conditioning on a measurable pilot event does not alter an estimation-fold integral, except for multiplication by the pilot-event probability.
Formal statement
Proof (Lean source)
Helpers.PilotSandwich 13 declarations
Defines category Indicator, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of category Indicator mean in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated equality relating pilot count eq bernoulli Count.
Formal statement
Proof (Lean source)
Establishes the stated property of pilot Category upper tail in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of pilot Category lower tail in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Defines pilot Heavy At, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Defines pilot Bad Event, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Establishes the stated property of pilot Bad Event subset cellwise in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated property of pilot Bad Event probability in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for exp neg mul log Scale.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for pilot decay bound.
Formal statement
Proof (Lean source)
Polynomially small failure probability for the pilot heavy/light sandwich.
Formal statement
Proof (Lean source)
The paper's explicit threshold t=256 works for exponent K=4.
Formal statement
Proof (Lean source)
Helpers.ShiftedChebyshev 1 declarations
Explicit coefficient expansion of the shifted Chebyshev polynomial.
Formal statement
Proof (Lean source)
T_OverlapAdaptiveUniversalHybrid 2 declarations Clause (v) is deliberately represented by this scope note rather than a Lean proposition: every constant below is pointwise in a fixed epsilon.
Clause (v) is deliberately represented by this scope note rather than a Lean
proposition: every constant below is pointwise in a fixed epsilon. Nothing in
this theorem asserts a matching lower envelope for triangular arrays
epsilon = epsilon_n.
The statistical clauses of the universal-hybrid theorem, assembled from the fixed-interior upper bound, centered-estimator bound, endpoint bracket, and deterministic selector.
Formal statement
Proof (Lean source)
Universal fixed-class calibration, the all-sample centered bound, the exact randomization bracket, and the combined upper envelope. Clause (i) includes a finite real-arithmetic realization with the stated O(d M^4) operation bound; the hybrid's type has no epsilon argument, realizing its no-selector claim.
Formal statement
Proof (Lean source)
T_SharpMinimaxFixedInterior 6 declarations
Establishes the stated upper bound for clamp sq error le.
Formal statement
Proof (Lean source)
Establishes the stated property of target Heavy add target Light in the discrete average-treatment-effect construction.
Formal statement
Proof (Lean source)
Establishes the stated upper bound for hybrid mse le component errors.
Formal statement
Proof (Lean source)
Defines canonical Class Law, the stated quantity or construction used in the discrete average-treatment-effect estimator.
Definition (Lean source)
Certified upper half, separated from the cited lower gate for downstream use.
Formal statement
Proof (Lean source)
Matched fixed-interior minimax rate. The lower half is explicitly conditional on the cited ZengOneArmMinimaxLower interface.
Formal statement
Proof (Lean source)
T_TwoCategoryConfounding 1 declarations
The explicit full-data witness is consistent, conditionally exchangeable and overlapping, has ATE 1/2, and naive observed contrast epsilon.