Formalization: A Minimax Bracket for Average Treatment Effect Estimation with Discrete Adjustment and Bounded Heterogeneity
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 51 declarations
One observed record (X,A,Y) in the real-outcome experiment.
Observed records carry the measurable structure generated by their covariate, treatment, and outcome coordinates.
Definition (Lean source)
One full-data record (X,A,Y(0),Y(1),Y).
Full-data records carry the measurable structure generated by the covariate, treatment, both potential outcomes, and the observed outcome.
Definition (Lean source)
Projection from full data to the observed record.
Definition (Lean source)
Real mass of an event under a measure.
Definition (Lean source)
A real-outcome finite-cell law, including the primitive cell parametrization and a full-data coupling. The identities below pin every auxiliary to the law.
Definition (Lean source)
Cell treatment effect tau_k = mu_1k - mu_0k.
Definition (Lean source)
The finite-cell g-formula attached to an arbitrary real law. This auxiliary is used while the identified model classes are being assembled.
Definition (Lean source)
The causal full-data average E[Y(1)-Y(0)].
Definition (Lean source)
Cell deviation from the average treatment effect.
Definition (Lean source)
Standing range condition for the known outcome scale.
Definition (Lean source)
Y = Y(A) almost surely under the full-data law.
Definition (Lean source)
Atomic-cell formulation of (Y(0),Y(1)) conditionally independent of A given X, valid for arbitrary measurable potential-outcome events.
Definition (Lean source)
Positive-mass cells have propensity in [epsilon,1-epsilon].
Conditional means lie in [-M/2,M/2] on positive-mass cells.
Definition (Lean source)
The conditional second central moment is bounded by M^2; outcomes themselves need not be bounded.
Definition (Lean source)
If conditional second moments are finite and bounded and the stated condition on the cell holds, a finite conditional second central moment implies the first-moment integrability needed by the finite-cell g-formula.
Formal statement
Proof (Lean source)
Every supported cell effect is within sigma*M of the ATE.
Definition (Lean source)
The causal-identification domain for the finite-cell functional. It records exactly consistency, conditional exchangeability, overlap, and the supported-cell first-moment integrability presupposed by the g-formula.
Definition (Lean source)
The identified ATE functional on the causal model domain. Its value is the finite-cell g-formula; ate_identification proves that this equals the causal expectation E[Y(1)-Y(0)].
Definition (Lean source)
The approximately homogeneous real-outcome model class.
Definition (Lean source)
The corresponding model without a heterogeneity-radius restriction.
Definition (Lean source)
The identified-law view carried by every approximately homogeneous model.
Formal statement
Proof (Lean source)
The identified-law view carried by every unrestricted model.
Formal statement
Proof (Lean source)
The n-fold observed product law generated by a one-unit real law.
Every finite product of the observed-data law is a probability measure.
Definition (Lean source)
The induced experiment of all observed n-sample laws from the model class.
Definition (Lean source)
Total estimators with measurable output clipped to [-M,M].
Definition (Lean source)
Mean-squared error under the model's product sample law.
Definition (Lean source)
Worst-case risk of an estimator over the specified model class.
Definition (Lean source)
Minimax MSE over all total measurable [-M,M]-valued estimators.
Definition (Lean source)
The logarithmic scale log(e n).
Polynomial-estimator component d^2/(n^2 log(en)^2).
Definition (Lean source)
Collision-estimator component sigma^2+d/n^2.
Definition (Lean source)
The paper's upper frontier rate.
Definition (Lean source)
If the sample is nonempty, on its declared positive-sample domain, the frontier rate is positive.
Formal statement
Proof (Lean source)
The proved capped converse benchmark.
Definition (Lean source)
Number of observations in arm a and cell k.
Total number of observations in cell k.
Pairwise collision-denominator kernel: the two records share a cell and belong to opposite treatment arms.
Definition (Lean source)
Whether both treatment arms occur in a cell.
Total occupancy among cells containing both treatment arms.
Definition (Lean source)
Sum of observed outcomes in arm a and cell k.
Indicator-totalized empirical arm mean.
Population collision weight for cell k.
Definition (Lean source)
Total collision weight on the positive-overlap model.
Definition (Lean source)
The finite collection of cell masses partitions the observed probability law.
Proof (Lean source)
If the alphabet is nonempty, a nonempty positive-overlap model has strictly positive collision weight.
Formal statement
Proof (Lean source)
The primitive cell masses of a real law sum to at most one.
Proof (Lean source)
Mean normalization bounds every cell effect and the ATE, so radius 2 is equivalent to the unrestricted class.
Formal statement
Proof (Lean source)
Helpers.AffineEmbedding 21 declarations
A binary full-data record used to state law-level source couplings.
Definition (Lean source)
Equality of binary full-data records is decidable.
Definition (Lean source)
The space of binary full-data records is finite.
Definition (Lean source)
Binary full-data records carry the discrete measurable structure.
Definition (Lean source)
The observed binary record selected from a binary full-data record.
Definition (Lean source)
Deterministic affine scaling of both binary potential outcomes.
Definition (Lean source)
A binary potential-outcome coupling has the prescribed observed source law.
Definition (Lean source)
Lift an observed binary record to consistent binary full data by using a fixed value for the unobserved potential outcome.
Definition (Lean source)
Observing the canonical full-data lift recovers the source record.
Formal statement
Proof (Lean source)
The pushforward of a binary observation law by the canonical lift is a probability coupling with exactly the prescribed observed margin.
Definition (Lean source)
The canonical lifted law satisfies the binary coupling interface.
Formal statement
Proof (Lean source)
The deterministic affine pushforward on an observed binary record.
Definition (Lean source)
Observing an affinely scaled full-data record is the same as affinely scaling its observed binary record.
Formal statement
Proof (Lean source)
The affine image of the canonical binary full-data coupling has the expected affinely transformed observed margin.
Formal statement
Proof (Lean source)
The totalized binary conditional outcome law in one arm and cell.
Definition (Lean source)
One law-level affine binary-to-real pushforward. The same M-indexed map pins the observed law, every positive arm-cell conditional outcome law, and a full-data potential-outcome coupling.
Definition (Lean source)
The one-record affine binary-to-real observation map is measurable.
Formal statement
Proof (Lean source)
An affine embedding transports the whole finite sample coordinatewise.
Formal statement
Proof (Lean source)
The real-outcome g-formula of an affine binary embedding is the binary weighted regression contrast multiplied by the affine slope.
Formal statement
Proof (Lean source)
If the source law satisfies overlap, under binary overlap, the preceding scaling identity is exactly scaling of the source ATE functional.
Formal statement
Proof (Lean source)
If the outcome scale is nonnegative and the outcome scale satisfies its stated bound and the source parameter set has the stated form and the affine embedding identity holds and the source law satisfies overlap and the transported family belongs to the target model class, a genuinely hard binary family transfers to the ambient minimax problem through any affine embedding whose images have model-class witnesses.
Formal statement
Proof (Lean source)
Helpers.AffineMembership 7 declarations
If the source law satisfies the stated model condition, affine outcome scaling preserves the binary source law's overlap condition.
Formal statement
Proof (Lean source)
If the outcome scale satisfies its stated bound, the affine binary real-outcome law has conditional means bounded in absolute value by half the outcome scale.
Formal statement
Proof (Lean source)
If the outcome scale satisfies its stated bound, the affine binary real-outcome law has conditional second central moments bounded by the squared outcome scale.
Formal statement
Proof (Lean source)
This packages an affine binary source law as a member of the unrestricted real-outcome class.
Definition (Lean source)
If the source law satisfies the stated model condition, an exactly homogeneous binary source remains exactly homogeneous after affine embedding into real outcomes.
Formal statement
Proof (Lean source)
This packages an exactly homogeneous affine binary law as a zero-radius member of the model class.
Definition (Lean source)
If the overlap constant is positive and the overlap constant is below one half and the outcome scale satisfies its stated bound and the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, a model whose control outcome is identically zero is outside the affine binary image, since a nonzero affine scale only takes the values ±M/2.
Formal statement
Proof (Lean source)
Helpers.AffineRealLaw 15 declarations
This is the two-point outcome distribution with the specified success probability and affine outcome scale.
Definition (Lean source)
the binary outcome distribution assigns real probability p to the upper affine endpoint.
Formal statement
Proof (Lean source)
the binary outcome distribution assigns real probability one minus p to the lower affine endpoint.
Formal statement
Proof (Lean source)
This augments an observed binary record with an independently drawn missing potential outcome.
Definition (Lean source)
This is the full-data probability mass function obtained by independently imputing the missing binary potential outcome.
Definition (Lean source)
projecting the independent full-data lift recovers the original observed binary record.
Formal statement
Proof (Lean source)
projecting the independent full-data distribution gives the original observed-data law.
Formal statement
Proof (Lean source)
If the specified event is measurable, the affine image of the binary outcome distribution assigns each endpoint its binary probability.
Formal statement
Proof (Lean source)
If the specified event is measurable, the affine observed-data pushforward assigns each arm-cell-outcome event the corresponding binary joint probability.
Formal statement
Proof (Lean source)
This construction embeds a binary-outcome observational law into a real-outcome law by affine outcome scaling and an independent full-data coupling.
Definition (Lean source)
If the stated pos condition holds, the measure induced by the binary outcome distribution equals the corresponding conditional outcome law.
Formal statement
Proof (Lean source)
the affine real-outcome construction satisfies the binary embedding identities for cell probabilities, propensities, and conditional means.
Formal statement
Proof (Lean source)
the real probability assigned to a full-data atom factors into its observed-atom probability and the independent missing-potential probability.
Formal statement
Proof (Lean source)
the affine binary real law satisfies consistency.
Formal statement
Proof (Lean source)
The independent missing-potential-outcome augmentation makes the affine full-data law conditionally exchangeable.
Formal statement
Proof (Lean source)
Helpers.BinaryPadding 17 declarations
If the scalar satisfies the stated range condition, above one, the natural floor retains at least half of a nonnegative real.
Formal statement
Proof (Lean source)
Include a binary observation on the first m cells into an alphabet of size d.
Definition (Lean source)
If the source alphabet embeds in the target alphabet, the zero-padding map from the source observation alphabet into the larger alphabet is injective.
Formal statement
Proof (Lean source)
Push a binary law into the first m cells of a larger alphabet, assigning zero probability to all unused cells.
Definition (Lean source)
If the source alphabet embeds in the target alphabet, the observed-data law after padding is the pushforward of the source law under the padding map.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet, padding preserves joint probabilities on embedded source cells.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet and the stated condition on the cell holds, padding assigns zero joint probability to every cell outside the embedded source alphabet.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet, padding preserves cell probabilities on embedded source cells.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet and the stated condition on the cell holds, padding assigns zero cell probability outside the embedded source alphabet.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet, padding preserves arm-specific cell probabilities on embedded source cells.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet, padding preserves propensities on embedded source cells.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet, padding preserves conditional outcome means on embedded source cells.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet and the source law satisfies the stated model condition, the binary pad law preserves the overlap condition.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet and the source law satisfies the stated model condition, zero-mass padding preserves the binary average-treatment-effect functional.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet and the stated condition on the source size or matching order holds and the source law satisfies the stated model condition, padding by zero-mass cells preserves exact treatment-effect homogeneity in the support-qualified real-outcome model.
Formal statement
Proof (Lean source)
The padded affine image of an exact binary source law belongs to every nonnegative-radius ambient class.
Definition (Lean source)
If the source alphabet embeds in the target alphabet and the stated condition on the source size or matching order holds and the overlap constant is positive and the overlap constant is below one half and the outcome scale satisfies its stated bound and the heterogeneity radius is nonnegative and the heterogeneity radius is at most two and the source parameter set has the stated form, a hard exact binary family on m cells transfers to the real-outcome problem on any larger alphabet by zero-mass padding followed by affine scaling.
Formal statement
Proof (Lean source)
Helpers.CitedGates 8 declarations
The uniform-mass, exactly homogeneous binary source class.
Definition (Lean source)
Binary laws in the cited exact-homogeneity source experiment.
Definition (Lean source)
Exact-homogeneity source minimax risk.
Definition (Lean source)
Cited gate (Zeng, Balakrishnan, Han, and Kennedy, 2024, revised 2026). Source: arXiv:2405.00118v3, Theorem 4 and Appendix C.8. The fixed-sample uniform-mass exactly homogeneous binary experiment has minimax risk at least a constant times 1/n+d/n^2 throughout its source range.
Definition (Lean source)
Re-export of the cited fixed-sample one-arm lower-bound interface from the binary source development (Zeng et al., arXiv:2405.00118v3, Theorem 2, Appendix C.5, Lemma 4, and Appendix D.2).
Definition (Lean source)
Cited gate (Zeng, Balakrishnan, Han, and Kennedy, 2024, revised 2026). Source: arXiv:2405.00118v3, Lemma 1 and Appendix C.7, equation (26) and the reciprocal-occupancy display. The constants are quantified before the model parameters and hence depend only on epsilon.
Definition (Lean source)
sigma_bin is the actual maximal binary treatment-effect heterogeneity, not merely an arbitrary envelope.
Definition (Lean source)
Cited gate (Zeng, Balakrishnan, Han, and Kennedy, 2024, revised 2026). Source: arXiv:2405.00118v3, Theorem 3 on page 11 and Appendix C.7. This is the published bias/variance guarantee for their equation-(13) estimator.
Definition (Lean source)
Helpers.ConcreteExactHandle 10 declarations This module packages the canonical full-data coupling and the deterministic zero-padding identities used by the exact half of the least-favorable handle.
Concrete exact-family handle facts
This module packages the canonical full-data coupling and the deterministic zero-padding identities used by the exact half of the least-favorable handle.
Include a binary full-data record on the first m cells into an ambient alphabet of size d.
Definition (Lean source)
If the source alphabet embeds in the target alphabet, padding a binary law leaves its conditional outcome PMFs unchanged on the embedded coordinates.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet, padding commutes with the independent full-data lift of an observation.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet, the canonical independent binary full-data coupling commutes with zero-mass cell padding.
Formal statement
Proof (Lean source)
The independent-potential-outcome lift used by affineBinaryRealLaw is a full-data coupling of its binary observed law.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet, the full-data law of the padded affine embedding is exactly the affine pushforward of the canonical independent binary coupling.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet, the observed law of a padded affine source is the deterministic coordinatewise padding-and-scaling pushforward of the source observation.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet, padding and affine outcome scaling preserve every source cell mass on the embedded coordinates.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet and the stated condition on the cell holds, every ambient coordinate outside the padded source image has zero mass.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet and the source law satisfies the stated model condition, the exact padded affine embedding multiplies the binary ATE by M.
Formal statement
Proof (Lean source)
Helpers.ConcreteHandleCertificates 4 declarations This module packages ambient membership and coupling certificates for handles whose fields are the canonical padded binary constructions.
Concrete least-favorable handle certificates
This module packages ambient membership and coupling certificates for handles whose fields are the canonical padded binary constructions.
If the cap satisfies the exact-embedding bound and the padded dimension satisfies the cap bound and the overlap constant is positive and the overlap constant is below one half and the outcome scale satisfies its stated bound and the specified embedding certificate holds, a handle using the canonical padded affine exact embedding has the required radius-zero ambient membership certificate.
Formal statement
Proof (Lean source)
If the padded dimension satisfies the cap bound and the overlap constant is positive and the overlap constant is below one half and the outcome scale satisfies its stated bound and the heterogeneity radius is nonnegative and the heterogeneity radius is at most two and the specified embedding certificate holds, a handle using the padded Bernoulli-contracted affine embedding has the required radius-indexed ambient membership certificate.
Formal statement
Proof (Lean source)
If the specified full-data coupling is available, the canonical independent full-data lift packages the exact coupling certificate of a concrete handle.
Formal statement
Proof (Lean source)
If the specified full-data coupling is available, the same canonical independent full-data lift packages the radial source coupling certificate of a concrete handle.
Formal statement
Proof (Lean source)
Helpers.ConcreteRadialHandle 3 declarations This module identifies the observed experiment generated by the padded Bernoulli contraction and records the mass identities needed by the concrete least-favorable handle.
Concrete radial-family handle facts
This module identifies the observed experiment generated by the padded Bernoulli contraction and records the mass identities needed by the concrete least-favorable handle.
If the source alphabet embeds in the target alphabet and the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, padding, Bernoulli contraction, and affine outcome scaling agree exactly with applying the common observed-data Markov kernel to the source law.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet and the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, the concrete radial embedding preserves every positive source coordinate's cell mass.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet and the heterogeneity radius is nonnegative and the heterogeneity radius is at most two and the stated condition on the cell holds, every ambient coordinate outside the radial padding image has zero mass.
Formal statement
Proof (Lean source)
Helpers.Estimators 25 declarations
Clipping to a closed real interval.
The occupancy-weighted arm-mean estimator, with every empirical ratio indicator-totalized and with a zero fallback when no usable cell exists.
Definition (Lean source)
Whether an index belongs to the pilot half of the sample.
Pilot occupancy of one cell.
Definition (Lean source)
Size of the estimation block I_1.
Definition (Lean source)
Estimation-block arm/cell count.
Definition (Lean source)
Estimation-block cell count.
Definition (Lean source)
Estimation-block outcome sum.
Indicator-totalized estimation-block arm mean.
Definition (Lean source)
Fixed shifted-Chebyshev coefficient from the paper.
Definition (Lean source)
Ordered distinct-index falling-factorial statistic with exactly one real mark.
Definition (Lean source)
The light-cell polynomial contribution.
Definition (Lean source)
Calibrated constant multiplying log(en) in the polynomial degree.
Actual shifted-Chebyshev degree used by the polynomial program.
Definition (Lean source)
Heavy-cell empirical contribution, normalized by the outcome scale.
Definition (Lean source)
The uncalibrated split-sample heavy/light signed one-mark program. This companion is exposed only so the polynomial-upper lemma can certify its cutoff parameters before the public handle is formed.
Definition (Lean source)
Dependent calibration data for the polynomial estimator: a cutoff, a positive active-range multiplier, and the active-branch degree certificate.
Definition (Lean source)
The handle-indexed pilot-split heavy/light signed one-mark estimator. Its body is definitionally the complete raw program, including clipping and the exact zero fallback outside the calibrated range.
Definition (Lean source)
A light-cell signed polynomial contribution is measurable.
Formal statement
Proof (Lean source)
A heavy-cell empirical contribution is measurable.
Formal statement
Proof (Lean source)
If the outcome scale satisfies its stated bound, the collision construction is measurable and lies in the estimator range.
Formal statement
Proof (Lean source)
If the outcome scale satisfies its stated bound, the polynomial construction is measurable and lies in the estimator range.
Formal statement
Proof (Lean source)
The collision construction packaged as a member of the estimator space.
Definition (Lean source)
The polynomial handle packaged as an admissible estimator.
Definition (Lean source)
Deterministic three-branch known-radius selector on two admissible estimators. The result itself remains in the same measurable [-M,M]-valued space.
Definition (Lean source)
Helpers.ExactHardFamily 1 declarations
If the sample is nonempty and the alphabet is nonempty and the overlap constant is positive and the overlap constant is below one half and the logarithmic scale satisfies its stated bound, any level strictly below the exact binary minimax risk is attained as a lower bound against every measurable estimator by some exact source law.
Formal statement
Proof (Lean source)
Helpers.ExactHomogeneityLower 4 declarations This module discharges the fixed-sample exact-homogeneity source interface used by the heterogeneity-frontier lower transfer.
Exact-homogeneity binary lower bound
This module discharges the fixed-sample exact-homogeneity source interface used by the heterogeneity-frontier lower transfer. The parametric part is obtained from the accepted endpoint two-point experiment. The collision part uses the symmetric finite Rademacher mixture from Zeng--Balakrishnan--Han--Kennedy, Theorem 4 and Appendix C.8.
If the alphabet is nonempty and the overlap constant is positive and the overlap constant is below one half, the null endpoint distribution belongs to the exact homogeneous binary model.
Formal statement
Proof (Lean source)
If the sample is nonempty and the alphabet is nonempty and the overlap constant is positive and the overlap constant is below one half, the exact-homogeneity binary source class contains the standard randomized Bernoulli two-point experiment, hence retains the parametric 1/n lower term.
Formal statement
Proof (Lean source)
If the sample is nonempty and the alphabet is nonempty and the overlap constant is positive and the overlap constant is below one half and the stated dn condition holds, the exact-homogeneity binary minimax risk obeys the collision-regime lower bound.
Formal statement
Proof (Lean source)
Zeng--Balakrishnan--Han--Kennedy's exact-homogeneity lower bound, in the fixed finite-sample interface used by the frontier theorem.
Formal statement
Proof (Lean source)
Helpers.FactorialCovariance 32 declarations
The paper's unsplit all-block statistic: all m observations participate, and normalization is by (m)_{j+2} rather than the estimation-half factorial.
Definition (Lean source)
One all-block light-cell polynomial contribution.
Definition (Lean source)
Sum of the unsplit all-block statistics over deterministic light cells.
Definition (Lean source)
Coordinate factors whose ordered product is one all-block marked factorial kernel: the zeroth coordinate carries the outcome mark, the first only selects the cell, and all later coordinates select the arm and cell.
Definition (Lean source)
Multiplying the coordinate factors recovers the paper's displayed marked kernel, including its redundant later-coordinate product.
Formal statement
Proof (Lean source)
Every coordinate of the marked factorial kernel is measurable. This is the regularity input needed by the generic mixed-order covariance expansion.
Formal statement
Proof (Lean source)
The full coordinate product defining one marked factorial kernel is measurable under the finite product measurable space.
Formal statement
Proof (Lean source)
Every partial-matching merge of two marked factorial kernels is measurable, including the possible collision of their two real-valued marks.
Formal statement
Proof (Lean source)
If the observation belongs to a different cell, every coordinate factor vanishes away from its designated cell.
Formal statement
Proof (Lean source)
If the sampling budget satisfies the stated lower bound and the two cells are distinct, a positive-size matching between statistics from different cells has zero merged kernel: a matched observation cannot satisfy both cell selectors.
Formal statement
Proof (Lean source)
If the sampling budget satisfies the stated lower bound and the two cells are distinct, consequently every positive-overlap merged moment from two different cells is exactly zero.
Formal statement
Proof (Lean source)
The paper's all-block marked factorial statistic is exactly the generic normalized ordered-product statistic evaluated on the finite sample prefix.
Formal statement
Proof (Lean source)
If the stated condition on the cell holds, a zero-mass cell makes each of its observed arm-cell events null. This discharges the unsupported-cell branch of the marked moment audit without requesting conditional moments where the model deliberately supplies none.
Formal statement
Proof (Lean source)
Restricting the observed law to one arm and cell and then projecting the outcome gives its conditional outcome law scaled by the arm-cell mass.
Formal statement
Proof (Lean source)
If the stated condition on the cell holds, on every positive-mass arm and cell, the central-moment and mean envelopes imply integrability of the raw squared outcome and the bound E[Y²] ≤ 5M²/4. This is the paper's moment audit before normalizing the unique real mark.
Formal statement
Proof (Lean source)
If the stated condition on the cell holds, dividing by the model scale turns the raw outcome-moment audit into the dimensionless bound E[(Y/M)²] ≤ 5/4 used for a collision of two marks.
Formal statement
Proof (Lean source)
The normalized squared outcome is integrable under the full observed law. This packages the finite arm-cell partition needed whenever two marked coordinates collide in a partial matching.
Formal statement
Proof (Lean source)
The normalized observed outcome itself is square-integrable.
Formal statement
Proof (Lean source)
Selector coordinates have norm at most one, while the unique marked coordinate has norm at most the normalized outcome magnitude.
Formal statement
Proof (Lean source)
If the stated condition on the cell holds, the normalized outcome mark is integrable in each supported arm-cell law, and its conditional mean has absolute value at most one half.
Formal statement
Proof (Lean source)
Every individual marked-factorial coordinate is integrable under the observed law; the unique outcome coordinate uses the arm-cell transport.
Formal statement
Proof (Lean source)
Every marked coordinate is square-integrable. The marked position uses the observed normalized second-moment audit; every selector-only position is uniformly bounded by one.
Formal statement
Proof (Lean source)
A whole marked factorial kernel is integrable under the corresponding finite product law.
Formal statement
Proof (Lean source)
Every partial-matching merge is integrable. After bounded selectors are discarded, the only possible unbounded factor is the product of the two marked coordinates; distinct marks factor across product coordinates, while a collision is controlled by the observed second moment.
Formal statement
Proof (Lean source)
The ordered marked kernel is square-integrable under its finite product law, obtained by factoring its square coordinatewise.
Formal statement
Proof (Lean source)
If the second factorial order is admissible and the stated size condition holds, if both coordinate families have order at most K, the number of size-h partial matchings is at most K^(2h) / h!. This is the matching-count factor used when the covariance expansion is summed by overlap size.
Formal statement
Proof (Lean source)
If the first factorial order is admissible and the second factorial order is admissible and the stated condition on the source size or matching order holds and the sampling budget satisfies the stated lower bound, the generic mixed-order normalization bound specialized to the marked factorial orders occurring in the paper.
Formal statement
Proof (Lean source)
If the first factorial order is admissible and the second factorial order is admissible and the stated condition on the source size or matching order holds, the disjoint-tuple correction for two marked factorial orders is at most 2(K+2)²/m, uniformly over the polynomial degrees.
Formal statement
Proof (Lean source)
If the first factorial order is admissible and the second factorial order is admissible and the stated condition on the source size or matching order holds, summing the normalization over all size-h overlaps costs at most the paper's K^(2h)/h! matching count times the generic exp(1)/m^h ratio.
Formal statement
Proof (Lean source)
The all-block version of each marked factorial statistic is measurable on the finite product sample space.
Formal statement
Proof (Lean source)
Finite summation preserves measurability of the complete deterministic light-cell statistic.
Formal statement
Proof (Lean source)
The variance under the finite product law can be evaluated on the canonical infinite-product IID realization by restricting it to the first m coordinates.
Formal statement
Proof (Lean source)
Helpers.FactorialCovarianceAssembly 6 declarations
If the two cells are distinct and the first factorial order is admissible and the second factorial order is admissible and the stated condition on the source size or matching order holds, for different cells every positive partial matching is incompatible, so only the disjoint-tuple normalization correction remains.
Formal statement
Proof (Lean source)
If the two cells are distinct and the polynomial or elbow parameter satisfies its stated bound and the outcome bound is positive and the stated condition on the cell holds and the stated l condition holds and the stated condition on the source size or matching order holds, summing the different-cell correction over both arms and all polynomial degrees gives the required K²/m cross-cell scale.
Formal statement
Proof (Lean source)
every all-block ordered marked factorial statistic has a finite second moment.
Formal statement
Proof (Lean source)
every all-block light polynomial term has a finite second moment.
Formal statement
Proof (Lean source)
the absolute covariance between two all-block light polynomial terms satisfies the stated bound.
Formal statement
Proof (Lean source)
Under only the conditional second-moment envelope, a deterministic collection of signed one-mark ordered factorial statistics has the covariance bound used by the heavy/light estimator.
Formal statement
Proof (Lean source)
Helpers.FactorialCovarianceCoefficients 6 declarations
The signed coefficient in the real-outcome estimator is the same shifted Chebyshev coefficient used by the binary factorial construction.
Formal statement
Proof (Lean source)
Absolute shifted-coefficient series evaluated at a nonnegative intensity.
Definition (Lean source)
The marked-statistic coefficient envelope is the previously audited shifted-Chebyshev absolute series.
Formal statement
Proof (Lean source)
If the polynomial or elbow parameter satisfies its stated bound and the scalar satisfies the stated range condition, for nonnegative intensity, the absolute coefficient sum has the paper's 6^K max(1,x^(K-2)) envelope.
Formal statement
Proof (Lean source)
If the polynomial or elbow parameter satisfies its stated bound and the scalar is nonnegative and the scalar is at most one, on the unit intensity range, the absolute coefficient sum is at most 6^K.
Formal statement
Proof (Lean source)
If the polynomial or elbow parameter satisfies its stated bound and the outcome bound is positive and the cell probability is nonnegative and the scaled cell probability satisfies the budget bound, on a light cell, the coefficient-weighted factorial mean series is at most B * 6^K. This is the one-dimensional factor in the cross-cell sum.
Formal statement
Proof (Lean source)
Helpers.FactorialCovarianceExpansion 1 declarations
If the first factorial order is admissible and the second factorial order is admissible and the stated condition on the source size or matching order holds, the centered product of two paper-local all-block marked factorials is exactly the generic mixed-order partial-matching expansion.
Formal statement
Proof (Lean source)
Helpers.FactorialCovarianceMoments 8 declarations Paper-local moment bounds for marked factorial coordinates
Paper-local moment bounds for marked factorial coordinates
The squared normalized mark restricted to one arm-cell has mass-weighted second moment at most 5/4 times the cell mass.
Formal statement
Proof (Lean source)
The unique marked coordinate has mean bounded by one half of its cell mass; this is the normalized conditional-mean audit.
Formal statement
Proof (Lean source)
Every coordinate mean is bounded by the cell mass. The marked coordinate uses the preceding mean audit; selector-only coordinates are event masses.
Formal statement
Proof (Lean source)
Every coordinate has second moment at most 5/4 times its cell mass. The marked coordinate uses the outcome envelope, while every other coordinate is an idempotent selector.
Formal statement
Proof (Lean source)
When two coordinate factors are assigned to the same observation in a partial matching, their product moment is still bounded by 5/4 times the cell mass. This uniformly covers a collision of the two real marks.
Formal statement
Proof (Lean source)
The factors assigned to one merged observation by a partial matching. Each fiber contains at most one coordinate from either ordered kernel.
Definition (Lean source)
The merged marked kernel factors over its genuinely distinct observation indices, grouping the possible left/right coordinate collision in one fiber.
Formal statement
Proof (Lean source)
Independence across the ordered kernel coordinates bounds its population mean by the corresponding power of the cell mass.
Formal statement
Proof (Lean source)
Helpers.FactorialCovarianceSameCell 5 declarations
the absolute integral of a merged marked-coordinate factor satisfies the stated cell-probability bound.
Formal statement
Proof (Lean source)
If the sampling budget satisfies the stated lower bound, the same-cell merged product moment of marked factorial coordinates satisfies the stated bound.
Formal statement
Proof (Lean source)
If the first factorial order is admissible and the second factorial order is admissible and the stated condition on the source size or matching order holds, the centered cross-moment of two marked factorial statistics from the same cell satisfies the stated bound.
Formal statement
Proof (Lean source)
If the polynomial or elbow parameter satisfies its stated bound and the outcome bound is positive and the cell probability is nonnegative and the scaled cell probability satisfies the budget bound, a pointwise coefficient bound implies the corresponding weighted-sum bound.
Formal statement
Proof (Lean source)
If the polynomial or elbow parameter satisfies its stated bound and the outcome bound is positive and the stated condition on the cell holds and the stated condition on the source size or matching order holds and the stated shift condition holds, the weighted sum of same-cell centered cross-moments satisfies the stated bound.
Formal statement
Proof (Lean source)
Helpers.FactorialCovarianceSummation 2 declarations
If the first order satisfies its stated bound and the second order satisfies its stated bound and the stated condition on the source size or matching order holds, the size-h normalization sum retains one binomial coefficient instead of replacing both by powers. This is the form that sums to a shifted intensity.
Formal statement
Proof (Lean source)
If the first order satisfies its stated bound and the second order satisfies its stated bound and the stated condition on the source size or matching order holds and the probability lies in the stated range, after weighting a size-h overlap by the remaining cell-mass power, all positive overlap sizes are bounded by the binomially shifted intensity p + v / m.
Formal statement
Proof (Lean source)
Helpers.LowerTransfer 25 declarations
Apply the same Bernoulli contraction to both potential responses, then scale the contracted bits. The formula is a law-level Markov pushforward and is hypothesis-independent: only the common success function is used.
Definition (Lean source)
Concrete data carried by the two padded, embedded least-favorable families.
Definition (Lean source)
The selected control-zero source family retains a genuine fixed-sample minimax lower bound; in particular, it cannot be an arbitrary nonempty set.
Definition (Lean source)
The selected uniform exactly-homogeneous source family retains the cited fixed-sample lower bound.
Definition (Lean source)
The chosen full-data couplings have the prescribed radial source margins.
Definition (Lean source)
The chosen full-data couplings have the prescribed exact source margins.
Definition (Lean source)
Pointwise realization of the two padded source families for fixed model parameters.
Definition (Lean source)
A global least-favorable family. The two cap constants are selected from epsilon before every sample size, alphabet size, scale, and radius; hence they cannot vary with model parameters.
Definition (Lean source)
Every radial embedding belongs to the radius-indexed ambient class. This is deliberately downstream of the construction handle.
Definition (Lean source)
Every exact-homogeneity embedding belongs to the radius-zero ambient class. This is deliberately downstream of the construction handle.
Definition (Lean source)
Every embedded realization obeys the stated heterogeneity radius.
Definition (Lean source)
The channel and affine embedding scale the source targets by their declared factors.
Definition (Lean source)
Product-sample total variation cannot increase under the radial channel.
Definition (Lean source)
A source set, independently of the two-family construction handle, retains the fixed-sample one-arm lower bound.
Definition (Lean source)
The common data asserted for one realization of the radial Bernoulli channel. Factoring it out keeps the construction and its lower-transfer certificate tied to the same source, padding, embedding, and coupling.
Definition (Lean source)
The radial family and its Bernoulli channel, including capping, ambient membership, realization-wise radius, and product-sample data processing.
Definition (Lean source)
The same realized radial channel carries both its exact target scaling and an estimator-wise lower-risk witness on the channel image.
Definition (Lean source)
If the specified least-favorable family is available and the transported family belongs to the target model class and the radial source lower bound holds and the channel satisfies data processing, project the radial construction asserted by the two-family internal handle to the radial-only public construction statement.
Formal statement
Proof (Lean source)
After the finite-sample cutoffs, both capped alphabets lie in the respective source theorem ranges.
Definition (Lean source)
Each admissible ambient estimator is defeated by a member of each selected source family at the corresponding transferred lower-bound scale.
Definition (Lean source)
If the specified least-favorable family is available and the transported family belongs to the target model class and the radial source lower bound holds and the channel satisfies data processing and the target separation certificate holds and the risk-transfer certificate holds, package one realized least-favorable handle as a radial certificate whose target scaling and estimator-wise risk transfer use those same witnesses.
Formal statement
Proof (Lean source)
If the transported family belongs to the target model class, ambient membership already contains the realization-wise homogeneity bound, so it immediately supplies the handle's radius certificate.
Formal statement
Proof (Lean source)
A one-cell two-point experiment gives the uniform parametric minimax term.
Formal statement
Proof (Lean source)
The cited exact-homogeneity binary converse transfers through the affine outcome embedding and capped-alphabet restriction.
Formal statement
Proof (Lean source)
Restricted-range corollary of the exact-homogeneity transfer.
Formal statement
Proof (Lean source)
Helpers.OccupancyDischarge 1 declarations This file combines independent-Poisson usable-occupancy bounds with monotone half-intensity de-Poissonization and transports the result back to the original fixed-size real-outcome sample.
Discharge of the usable-occupancy citation
This file combines independent-Poisson usable-occupancy bounds with monotone half-intensity de-Poissonization and transports the result back to the original fixed-size real-outcome sample.
The cited usable-occupancy reciprocal interface follows from the formal Poissonization and de-Poissonization argument.
Formal statement
Proof (Lean source)
Helpers.OccupancyTransport 33 declarations This file forgets real outcomes while retaining the finite cell-and-arm marks that determine usable occupancy.
Occupancy transport and monotone de-Poissonization
This file forgets real outcomes while retaining the finite cell-and-arm marks that determine usable occupancy. It also supplies deterministic prefix monotonicity and a paper-independent transfer from an i.i.d. stream stopped at an independent Poisson count to a fixed prefix.
The finite cell-and-arm mark obtained by forgetting an observation's outcome.
Definition (Lean source)
Forgetting the outcome is measurable.
Formal statement
Proof (Lean source)
The one-observation law of the finite cell-and-arm mark.
Definition (Lean source)
The finite product law of observed binary marks is a probability measure.
Definition (Lean source)
The factorization field of a real law gives the exact mass of every cell-and-arm atom after outcomes are forgotten.
Formal statement
Proof (Lean source)
Mapping every coordinate of a real-outcome product sample to its finite cell-and-arm mark gives the product of the corresponding mark law.
Formal statement
Proof (Lean source)
Number of occurrences of one arm and cell in the first n marks of a stream.
Total number of marks in a cell in the first n stream positions.
Definition (Lean source)
Usable occupancy in the first n positions of a cell-and-arm stream.
Definition (Lean source)
If the shorter prefix is contained in the longer prefix, arm counts cannot decrease when a stream prefix is enlarged.
Formal statement
Proof (Lean source)
If the shorter prefix is contained in the longer prefix, usable occupancy cannot decrease when a stream prefix is enlarged.
Formal statement
Proof (Lean source)
If the specified object and the specified function or embedding and the stream functional is measurable and the stream functional decreases with sample size, a reusable monotone de-Poissonization inequality. If a nonnegative stream statistic decreases with the prefix length, then its fixed-n expectation, multiplied by the probability that the independent Poisson count does not exceed n, is bounded by the statistic evaluated at that random count.
Formal statement
Proof (Lean source)
If the specified object, the first moment of a Poisson count is its intensity, in lintegral form.
Formal statement
Proof (Lean source)
A Poisson count with mean n/2 is at most n with probability at least one half.
Formal statement
Proof (Lean source)
The zero-occupancy indicator on a stream prefix.
Definition (Lean source)
The combined zero-event and reciprocal penalty used for monotone de-Poissonization.
Definition (Lean source)
Usable occupancy computed directly on a finite tuple of cell-and-arm marks.
Definition (Lean source)
Range-based stream occupancy equals direct occupancy of the finite prefix.
Formal statement
Proof (Lean source)
Fixed-prefix usable occupancy is measurable as a function of the stream.
Formal statement
Proof (Lean source)
If the shorter prefix is contained in the longer prefix, the zero-occupancy indicator decreases along stream prefixes.
Formal statement
Proof (Lean source)
If the shorter prefix is contained in the longer prefix, the combined zero-event/reciprocal penalty decreases along stream prefixes.
Formal statement
Proof (Lean source)
The identity partition of the finite cell-and-arm mark space.
Definition (Lean source)
Counts of every arm-cell atom in a finite marked sample.
Definition (Lean source)
The arm-cell count vector is measurable.
Formal statement
Proof (Lean source)
If the specified object, under the marked Poisson construction, all arm-cell counts are jointly independent Poisson variables with their atom-specific intensities.
Formal statement
Proof (Lean source)
Regroup an arm-cell count vector into false/true counts within each cell.
Usable occupancy computed from a regrouped pair of arm counts.
Definition (Lean source)
If the specified object, the regrouped arm-count vector is the pushforward of the independent atom-count product law.
Formal statement
Proof (Lean source)
Regrouping the atom counts preserves the stream usable-total formula.
Formal statement
Proof (Lean source)
The marked finite-sample usable total is exactly the deterministic regrouping of its arm-cell count vector.
Definition (Lean source)
Restricting a retained marked prefix to an arm-cell and counting it agrees with the corresponding range count in the underlying stream.
Formal statement
Proof (Lean source)
Marked-sample usable occupancy is exactly usable occupancy of the retained random prefix after the auxiliary real marks are forgotten.
Formal statement
Proof (Lean source)
If the specified object, the marked Poisson law is the random-prefix iid-stream law on observation-mark pairs.
Formal statement
Proof (Lean source)
Helpers.OccupancyUpper 13 declarations
The conditional-on-design center of the unclipped occupancy estimator, totalized by zero when no cell contains both treatment arms.
Definition (Lean source)
If the cell is usable, on the usable event, subtracting the ATE from the conditional design center is exactly the occupancy-weighted average of the cell deviations.
Formal statement
Proof (Lean source)
If the cell is usable and the stated support-size bound holds, if every empirically usable cell is in the population support, approximate homogeneity bounds the conditional design bias by sigma * M.
Formal statement
Proof (Lean source)
Mean normalization bounds the ATE of every radius-indexed model by the outcome scale.
Formal statement
Proof (Lean source)
If the stated support-size bound holds, the conditional-design squared bias is bounded by the homogeneity radius, plus the indicator of the zero-usable-occupancy fallback.
Formal statement
Proof (Lean source)
Empirically usable cells have positive population mass almost surely under the product experiment.
Formal statement
Proof (Lean source)
The conditional design center is measurable because it factors through the finite cell-and-treatment design.
Formal statement
Proof (Lean source)
The usable total is a measurable finite-design statistic.
Formal statement
Proof (Lean source)
Integrating the conditional-design squared bias introduces exactly the zero-usable-occupancy probability and no unsupported-cell contribution.
Formal statement
Proof (Lean source)
If the sample is nonempty, the de-Poissonization occupancy scale is bounded by the advertised parametric-plus-alphabet rate.
Formal statement
Proof (Lean source)
If the radial cap satisfies its stated bound and the scalar satisfies the stated range condition, an inverse-scale exponential tail is absorbed by a constant multiple of the scale, uniformly over every positive scale.
Formal statement
Proof (Lean source)
Within one supported arm and cell, the observed centered outcome has zero integral. The statement is totalized over zero-mass cells, where the arm-cell event is null.
Formal statement
Proof (Lean source)
The observed centered second moment on an arm-cell event is bounded by its arm-cell probability times M², including the null-cell boundary.
Formal statement
Proof (Lean source)
Helpers.OccupancyUpperAssembly 11 declarations
the test sample's arm-cell count agrees with the generic grouped count.
Formal statement
Proof (Lean source)
the sum of arm-specific group counts equals the total count for the cell.
Formal statement
Proof (Lean source)
summing the test sample's cell counts gives the sample size.
Formal statement
Proof (Lean source)
This is the untruncated occupancy estimator before final clipping.
Definition (Lean source)
If the stated count condition holds, the arm-specific residual contribution has mean zero.
Formal statement
Proof (Lean source)
the untruncated occupancy estimator minus its design center equals the sum of its arm-specific residual contributions.
Formal statement
Proof (Lean source)
the integral of an arm indicator equals its treatment-arm probability.
Formal statement
Proof (Lean source)
the untruncated occupancy estimator has a finite second moment.
Formal statement
Proof (Lean source)
the centered occupancy estimator has a finite second moment.
Formal statement
Proof (Lean source)
for every alphabet size, the collision estimator achieves the stated continuous-outcome risk upper bound.
Formal statement
Proof (Lean source)
Restricted-range form of the occupancy estimator upper bound.
Formal statement
Proof (Lean source)
Helpers.OneArmLowerDischarge 1 declarations This module exposes the proved binary one-arm lower bound in the local heterogeneity-frontier namespace.
One-arm lower-bound discharge
This module exposes the proved binary one-arm lower bound in the local heterogeneity-frontier namespace.
The proved binary one-arm minimax result discharges the local cited interface.
Formal statement
Proof (Lean source)
Helpers.ParametricLower 42 declarations
This is the full-data atom used in the parametric two-point lower-bound experiment.
Definition (Lean source)
the parametric full-data atom is measurable as a function of its outcome.
Formal statement
Proof (Lean source)
the projection from full data to observed data is measurable.
Formal statement
Proof (Lean source)
the full-data covariate coordinate is measurable.
Formal statement
Proof (Lean source)
the full-data treatment coordinate is measurable.
Formal statement
Proof (Lean source)
the control potential-outcome coordinate is measurable.
Formal statement
Proof (Lean source)
the treated potential-outcome coordinate is measurable.
Formal statement
Proof (Lean source)
the observed-outcome coordinate on full data is measurable.
Formal statement
Proof (Lean source)
This is the full-data law of the parametric two-point experiment.
Definition (Lean source)
If the outcome bound is positive and the local mean lies within the outcome bound, the test full law is a probability measure.
Formal statement
Proof (Lean source)
This is the observed-data atom associated with the parametric full-data atom.
Definition (Lean source)
the parametric observed-data atom is measurable as a function of its outcome.
Formal statement
Proof (Lean source)
the observed covariate coordinate is measurable.
Formal statement
Proof (Lean source)
the observed treatment coordinate is measurable.
Formal statement
Proof (Lean source)
the observed outcome coordinate is measurable.
Formal statement
Proof (Lean source)
This is the observed-data margin of the parametric two-point experiment.
Definition (Lean source)
If the outcome bound is positive and the local mean lies within the outcome bound, the test observed law is a probability measure.
Formal statement
Proof (Lean source)
If the outcome bound is positive and the local mean lies within the outcome bound, the observed margin of the parametric full-data law equals the constructed observed-data law.
Formal statement
Proof (Lean source)
This is the conditional outcome distribution in the parametric test model.
Definition (Lean source)
If the outcome bound is positive and the local mean lies within the outcome bound, the test outcome law is a probability measure.
Formal statement
Proof (Lean source)
If the outcome bound is positive and the local mean lies within the outcome bound, the test law assigns unit cell probability to the designated cell and zero to every other cell.
Formal statement
Proof (Lean source)
If the outcome bound is positive and the local mean lies within the outcome bound, the test outcome mean is the local mean in the treated arm and zero in the control arm.
Formal statement
Proof (Lean source)
If the outcome bound is positive and the local mean lies within the outcome bound, the conditional outcome law has an integrable squared centered outcome with second moment at most the squared outcome bound.
Formal statement
Proof (Lean source)
This assembles the real-outcome law for the parametric two-point experiment.
Definition (Lean source)
If the outcome bound is positive and the local mean lies within the outcome bound, the raw average-treatment-effect formula of the parametric test law equals its local mean parameter.
Formal statement
Proof (Lean source)
If the outcome bound is positive and the local mean lies within the outcome bound, the test real law satisfies consistency.
Formal statement
Proof (Lean source)
If the control-potential event is measurable and the treated-potential event is measurable, the joint covariate-treatment-potential-outcome probability under the test law has the stated two-point formula.
Formal statement
Proof (Lean source)
If the outcome bound is positive and the local mean lies within the outcome bound, the covariate marginal of the parametric full-data law is concentrated on the designated cell.
Formal statement
Proof (Lean source)
If the outcome bound is positive and the local mean lies within the outcome bound, the treatment-arm marginal of the parametric full-data law is one half.
Formal statement
Proof (Lean source)
If the control-potential event is measurable and the treated-potential event is measurable, the potential-outcome marginal of the parametric full-data law has the stated formula.
Formal statement
Proof (Lean source)
If the outcome bound is positive and the local mean lies within the outcome bound, the parametric test law satisfies conditional exchangeability.
Formal statement
Proof (Lean source)
This packages the parametric test law as a member of the heterogeneous model class.
Definition (Lean source)
This rescales a binary test observation into the real-outcome observation space.
Definition (Lean source)
the affine map from binary test observations to real observations is measurable.
Formal statement
Proof (Lean source)
If the outcome scale satisfies its stated bound and the second order satisfies its stated bound, at the null endpoint, affine rescaling maps the test observed law to the binary null law.
Formal statement
Proof (Lean source)
If the outcome scale satisfies its stated bound and the second order satisfies its stated bound, at the perturbed endpoint, affine rescaling maps the test observed law to the binary alternative law.
Formal statement
Proof (Lean source)
If the outcome scale satisfies its stated bound and the second order satisfies its stated bound and the first order satisfies its stated bound, coordinatewise affine rescaling maps the null test-sample law to the binary null product law.
Formal statement
Proof (Lean source)
If the outcome scale satisfies its stated bound and the second order satisfies its stated bound and the first order satisfies its stated bound, coordinatewise affine rescaling maps the perturbed test-sample law to the binary alternative product law.
Formal statement
Proof (Lean source)
risk on the parametric test model is bounded by the ambient minimax risk.
Formal statement
Proof (Lean source)
finite ambient risk makes the squared error on the parametric test model integrable.
Formal statement
Proof (Lean source)
If the outcome scale satisfies its stated bound and the bad-event probability is bounded as stated and the stated tau0 condition holds and the stated tau1 condition holds and the stated tv condition holds, the two parametric test laws give the stated two-point minimax lower bound.
Formal statement
Proof (Lean source)
the parametric two-point experiment yields the stated inverse-sample-size minimax lower bound.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.AggregateBridge 30 declarations
This bijection decomposes a marked tuple into its distinguished coordinate and the remaining coordinates.
Definition (Lean source)
If the specified marked tuple, the inverse marked-tuple decomposition recovers the distinguished coordinate at position zero.
Formal statement
Proof (Lean source)
If the specified marked tuple, the inverse marked-tuple decomposition recovers each tail coordinate at its successor position.
Formal statement
Proof (Lean source)
removing the distinguished coordinate rewrites the weighted matching count in terms of its tail pattern.
Formal statement
Proof (Lean source)
If the stated i condition holds, the complement fiber of a finite Boolean pattern has cardinality equal to the total size minus the selected fiber size.
Formal statement
Proof (Lean source)
This Boolean tail pattern records whether each remaining coordinate matches a designated arm.
Definition (Lean source)
This Boolean marked pattern adds the distinguished arm to the tail pattern.
Definition (Lean source)
every coordinate of the same-arm Boolean tail pattern equals the designated arm.
Formal statement
Proof (Lean source)
If the stated i condition holds, the same-arm Boolean tail pattern has the full matching count.
Formal statement
Proof (Lean source)
for the opposite-arm tail pattern, the fiber over the designated arm has cardinality zero.
Formal statement
Proof (Lean source)
for the opposite-arm tail pattern, the fiber over the other arm has full tail cardinality.
Formal statement
Proof (Lean source)
If the stated i condition holds, the opposite-arm Boolean tail pattern has the stated complementary matching count.
Formal statement
Proof (Lean source)
the same-arm Boolean pattern has the stated weighted matching value.
Formal statement
Proof (Lean source)
the opposite-arm Boolean pattern has the stated weighted matching value.
Formal statement
Proof (Lean source)
the two Boolean fibers of a marked pattern have cardinalities that sum to the pattern length.
Formal statement
Proof (Lean source)
a property holds for every marked Boolean pattern exactly when it holds for the two possible marked arms and every tail pattern.
Formal statement
Proof (Lean source)
the unrestricted weighted marked sum reduces to the sum of the two Boolean arm cases.
Formal statement
Proof (Lean source)
An injective embedding identifies its domain with the subtype of points in its range.
Definition (Lean source)
summing a range-indicator over the target of an embedding recovers the sum over the source.
Formal statement
Proof (Lean source)
for an injective function, summing its range-indicator over the codomain recovers the domain sum.
Formal statement
Proof (Lean source)
the marked kernel equals its explicit conditional product formula.
Formal statement
Proof (Lean source)
a property holds for every finite index at least two exactly when it holds for every index after removing the first two positions.
Formal statement
Proof (Lean source)
the subtype of sample indices in a given arm and cell has cardinality equal to the corresponding arm-cell count.
Formal statement
Proof (Lean source)
the subtype of sample indices in a given cell has cardinality equal to the corresponding cell count.
Formal statement
Proof (Lean source)
the normalized mark sum over a cell subtype equals the corresponding grouped mark sum divided by the outcome scale.
Formal statement
Proof (Lean source)
the marked-kernel matching condition is equivalent to the stated arm-and-cell coordinate conditions.
Formal statement
Proof (Lean source)
the all-block ordered marked factorial statistic equals its closed-form expression in the arm mark sum and descending factorial counts.
Formal statement
Proof (Lean source)
The concrete estimation-block factorial is exactly the all-block statistic on the canonically reindexed estimation fold.
Formal statement
Proof (Lean source)
Each concrete light-cell polynomial is the finite-product all-block polynomial on the canonically reindexed estimation fold.
Formal statement
Proof (Lean source)
Summing over a deterministic light set preserves the exact fold identification.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.Assembly 2 declarations
The explicit heavy/light signed one-mark estimator is total and has the capped all-alphabet polynomial risk bound under conditional second moments.
Formal statement
Proof (Lean source)
Restricted-range form of the polynomial upper bound.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.Bias 6 declarations
The coefficients used by the real-outcome estimator are exactly the shifted-Chebyshev reciprocal polynomial from the binary construction.
Formal statement
Proof (Lean source)
If the polynomial or elbow parameter satisfies its stated bound and the outcome bound is positive and the overlap constant is positive and the probability lies in the stated range and the scaled probability satisfies the budget bound and the shifted probability satisfies the stated range and the shifted scaled probability satisfies the budget bound and the approximation argument lies in its stated range and the evaluation point lies in its stated range, on a genuinely light cell, the shifted-Chebyshev arm polynomial has the paper's deterministic B /(2 ε K²) bias bound.
Formal statement
Proof (Lean source)
Treated-minus-control population polynomial for one fixed light cell.
Definition (Lean source)
If the polynomial or elbow parameter satisfies its stated bound and the outcome bound is positive and the cell is classified as light, on a genuinely light supported cell, the signed population polynomial approximates its normalized cell contribution with bias at most B /(ε K²).
Formal statement
Proof (Lean source)
Deterministic bias of the population polynomial over a fixed genuinely light set.
Definition (Lean source)
If the polynomial or elbow parameter satisfies its stated bound and the outcome bound is positive and the cell is classified as light, summing the cellwise Chebyshev approximation bound costs only the number of genuinely light cells.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.Calibration 24 declarations
The explicit shifted-Chebyshev degree constant is strictly positive.
Formal statement
the polynomial calibration constant is at most one.
Formal statement
Proof (Lean source)
The declared degree constant fits the coefficient-growth budget used by the shifted-Chebyshev variance bound.
Formal statement
Proof (Lean source)
The same degree constant fits the stronger covariance calibration budget.
Formal statement
Proof (Lean source)
Removing the floor can only increase the calibrated real-valued degree.
Formal statement
Proof (Lean source)
the effective logarithmic sample size is nonnegative.
Formal statement
Proof (Lean source)
If the sample is nonempty, the effective logarithmic sample size is at least one.
Formal statement
Proof (Lean source)
If the sample is nonempty, the polynomial degree is at most the effective logarithmic sample size.
Formal statement
Proof (Lean source)
If the polynomial or elbow parameter satisfies its stated bound, the polynomial degree satisfies its stated lower bound in terms of the effective logarithmic sample size.
Formal statement
Proof (Lean source)
The squared coefficient-growth factor is dominated by a small exponential power of the effective logarithmic sample size.
Formal statement
Proof (Lean source)
The fourth-power coefficient factor obeys the matching doubled exponent budget.
Formal statement
Proof (Lean source)
If the sample is nonempty, the polynomial estimation block is nonempty.
Formal statement
Proof (Lean source)
If the sample is nonempty, the polynomial light-cell scale is positive.
Formal statement
Proof (Lean source)
If the sample is nonempty, the polynomial light-cell scale satisfies its stated upper bound.
Formal statement
Proof (Lean source)
If the sample size satisfies the stated lower bound and the overlap constant is positive, the pilot denominator satisfies the stated lower bound.
Formal statement
Proof (Lean source)
If the sample is nonempty, the calibrated polynomial shift satisfies the required approximation condition.
Formal statement
Proof (Lean source)
If the sample is nonempty and the stated llarge condition holds, the fourth-power logarithmic growth term satisfies the stated sample-size bound.
Formal statement
Proof (Lean source)
If the sample is nonempty and the stated llarge condition holds, the squared logarithmic growth term satisfies the stated sample-size bound.
Formal statement
Proof (Lean source)
If the sample is nonempty and the stated llarge condition holds, the calibrated fixed branch satisfies the required degree-versus-block-size condition.
Formal statement
Proof (Lean source)
the effective logarithmic sample size is eventually at least 240.
Formal statement
Proof (Lean source)
If the sample is nonempty and the stated llarge condition holds and the alphabet size satisfies the stated condition, the pilot bad-event term is absorbed by the target polynomial rate.
Formal statement
Proof (Lean source)
Beyond an explicit finite cutoff, the calibrated polynomial degree is at least two.
Formal statement
Proof (Lean source)
If the outcome scale satisfies its stated bound, for every cutoff choice, the concrete estimator is measurable, uses its declared zero fallback, and is clipped to the required range.
Formal statement
Proof (Lean source)
One finite cutoff simultaneously supplies the degree side condition and, for every alphabet and scale, the total clipped estimator certificate used in the all-alphabet assembly.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.ClippingAssembly 4 declarations
The normalized heavy/light sum before the estimator's final clipping.
Definition (Lean source)
If the indicated calibration branch applies, on the calibrated branch, the concrete estimator is exactly the outcome scale times the clipped normalized heavy/light sum.
Formal statement
Proof (Lean source)
The model's ATE divided by its positive outcome scale lies in the clipping interval.
Formal statement
Proof (Lean source)
If the indicated calibration branch applies and the specified random quantity is integrable and the raw normalized-error bound holds, a normalized pre-clipping mean-square bound transfers to the scaled, clipped estimator whenever the normalized target lies in [-1,1].
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.Complexity 13 declarations
This straight-line program computes an empirical treatment-arm mean.
Definition (Lean source)
This straight-line program computes the heavy-cell contribution to the polynomial estimator.
Definition (Lean source)
This straight-line program computes a marked polynomial term.
Definition (Lean source)
This straight-line program computes the light-cell polynomial contribution.
Definition (Lean source)
This straight-line program assembles the calibrated polynomial estimator.
Definition (Lean source)
Each marked syntax node evaluates to the aggregate falling-factorial statistic.
Formal statement
Proof (Lean source)
Each light-cell syntax subtree evaluates to the declared polynomial term.
Formal statement
Proof (Lean source)
Evaluation of the explicit aggregate syntax is the calibrated estimator branch.
Formal statement
Proof (Lean source)
The explicit syntax fits the fixed quadratic-in-degree per-cell budget.
Formal statement
Proof (Lean source)
If the indicated calibration branch applies, the calibrated branch has a concrete aggregate program with the advertised budget.
Formal statement
Proof (Lean source)
If the indicated calibration branch applies, on either declared fallback branch, the constant-zero aggregate program computes the estimator and has zero arithmetic cost.
Formal statement
Proof (Lean source)
If the calibration handle is available, every branch of the total polynomial estimator has an executable certificate.
Formal statement
Proof (Lean source)
If the calibration handle is available, the fixed 128 proof-local certificate implies the public family-level O(d K²) arithmetic statement.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.Expectation 5 declarations
The marked coordinate has mean p_k q_{ak} μ_{ak}/M, the cell-only coordinate has mean p_k, and every later arm-cell coordinate has mean p_k q_{ak}. This is the exact coordinate audit behind the marked-factorial expectation formula.
Formal statement
Proof (Lean source)
Independence across the ordered coordinates gives exactly one normalized outcome mark, one cell selector, and j additional arm-cell selectors.
Formal statement
Proof (Lean source)
If the factorial order fits in the estimation block, an all-block marked factorial is exactly unbiased for its coordinatewise product-law moment whenever its order fits in the estimation block.
Formal statement
Proof (Lean source)
If the factorial order fits in the estimation block, the same exact marked-factorial expectation identity holds directly under the finite product experiment used by the estimator.
Formal statement
Proof (Lean source)
If the factorial order fits in the estimation block, the all-block statistic has the paper's exact marked-factorial expectation: one normalized marked arm-cell moment, one cell mass, and j further arm-cell masses.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.Fallback 3 declarations
If the indicated calibration branch applies, outside the calibrated sample-size/alphabet branch, the declared zero fallback has squared risk at most M².
Formal statement
Proof (Lean source)
If the tuning radius satisfies the stated restriction, for fixed positive alphabet cutoff, the zero fallback already satisfies the paper's capped polynomial rate on every uncalibrated branch.
Formal statement
Proof (Lean source)
If the target lies in the clipping interval, clipping a normalized estimate to [-1,1] cannot increase squared loss against a normalized target already in that interval.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.FixedBranchAssembly 3 declarations
The normalized error of a deterministic heavy set and its complementary light set, both evaluated on one independent block.
Definition (Lean source)
Every deterministic normalized branch has an integrable square under the finite product law.
Formal statement
Proof (Lean source)
The fixed-heavy marked-ratio bound and fixed-light factorial-moment bound combine into a single deterministic-selector risk inequality.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.FixedBranchRate 1 declarations
every fixed heavy-set branch of the polynomial estimator obeys the stated uniform normalized-risk bound.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.FixedLightRisk 6 declarations
Each finite-product marked factorial is integrable; this is the finite-law counterpart of the infinite-IID MemLp certificate used in the covariance proof.
Formal statement
Proof (Lean source)
If the outcome bound is positive and the polynomial degree fits the sample block, the exact marked-factorial expectation reconstructs the deterministic population polynomial for one light cell.
Formal statement
Proof (Lean source)
A finite-product light-cell polynomial is square-integrable.
Formal statement
Proof (Lean source)
If the outcome bound is positive and the polynomial degree fits the sample block, summing the cellwise exact expectations reconstructs the population polynomial over a deterministic light set.
Formal statement
Proof (Lean source)
The deterministic finite-product light sum is square-integrable.
Formal statement
Proof (Lean source)
The exact expectation, Chebyshev bias, and marked-factorial covariance bound combine into the fixed-light-set squared-risk inequality.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.FoldRiskBridge 10 declarations
The balanced estimation fold has the canonical finite index type of its declared cardinality.
Definition (Lean source)
Reindex an estimation-fold tuple by the canonical finite type with the same cardinality.
Definition (Lean source)
Regard an estimation-fold index as an index of the original finite sample.
Definition (Lean source)
Rebuilding a full tuple and then restricting to an estimation-fold index returns the original fold observation.
Formal statement
Proof (Lean source)
Under the infinite iid realization, the reindexed balanced estimation fold has exactly the finite product law of size n - n / 2.
Formal statement
Proof (Lean source)
Every estimation-block arm/cell count is the corresponding count on the canonically reindexed fold tuple.
Formal statement
Proof (Lean source)
Every estimation-block marked outcome sum is the corresponding supported mark sum on the canonically reindexed fold tuple.
Formal statement
Proof (Lean source)
The estimation-block cell count is the generic cell count on the reindexed fold.
Formal statement
Proof (Lean source)
The zero-safe estimation-block arm mean is the generic totalized arm mean on the reindexed fold.
Formal statement
Proof (Lean source)
The concrete heavy-cell term is exactly the normalized fixed-stratum term on the reindexed estimation fold.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.Heavy 9 declarations
The cell aggregates available after the single pass through the sample. No raw observation is retained by the post-aggregation evaluator.
The concrete aggregation pass used by the polynomial estimator.
Definition (Lean source)
A small executable arithmetic language over the aggregated cell table. Its only inputs are counts and outcome sums; loops are represented explicitly by finite sums, so their arithmetic cost is determined by syntax.
Definition (Lean source)
Operational semantics of the post-aggregation arithmetic language.
Definition (Lean source)
Structural arithmetic cost of an executable program. Input reads and constants are free; every arithmetic/comparison node and every finite-sum accumulation is charged.
Definition (Lean source)
A genuine post-aggregation program certificate: executing its syntax on the actual aggregate table computes the handle-indexed estimator for every sample.
Definition (Lean source)
The proof-local numerical budget used to certify the concrete program.
Definition (Lean source)
Internal finite-sample strengthening with the proof's explicit numerical constant. This is not the public complexity claim.
Definition (Lean source)
The estimator family has post-aggregation arithmetic complexity O(d K²), with one constant uniform in the sample size, alphabet size, and outcome scale.
Definition (Lean source)
Helpers.PolynomialUpper.HeavyRisk 8 declarations
The arm-cell center agrees with the model mean on supported cells and is zero on null cells, making the fixed-stratum center envelope total.
Definition (Lean source)
The support-totalized center obeys the model's half-scale envelope on every cell, including null cells.
Formal statement
Proof (Lean source)
Supported residuals about the totalized centers are square-integrable under the observed law.
Formal statement
Proof (Lean source)
Each support-totalized arm-cell residual has zero integral.
Formal statement
Proof (Lean source)
Each support-totalized arm-cell residual obeys the conditional second-moment envelope with the exact observed arm-cell mass.
Formal statement
Proof (Lean source)
If the stated condition on the cell holds, on every supported cell, the generic fixed-stratum population arm mean is exactly the model's declared conditional outcome mean.
Formal statement
Proof (Lean source)
If the selected heavy set is fixed, for a deterministic supported heavy set, the generic marked-ratio target is the corresponding cell-mass-weighted sum of model treatment effects.
Formal statement
Proof (Lean source)
If the truncation threshold satisfies its stated bound, for every deterministic heavy set whose cells have mass at least B, the fixed-heavy marked-ratio score satisfies the generic boundary-safe parametric and missing-arm risk bound under the real-outcome model assumptions.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.Pilot 10 declarations
Population-mass lower band certified for cells selected as heavy.
Definition (Lean source)
Population-mass upper band certified for cells selected as light.
Definition (Lean source)
If the sample size satisfies the stated lower bound, from sample size two onward, the pilot light-band lies below one quarter of the polynomial scale used on the independent estimation half.
Formal statement
Proof (Lean source)
The estimator's pilot count is exactly the generic finite-category count on the first half of the infinite iid realization.
Formal statement
Proof (Lean source)
Simultaneous pilot event: every selected-heavy cell has the stated lower mass and every selected-light cell has the stated upper mass.
Definition (Lean source)
The paper-local simultaneous pilot event is measurable.
Formal statement
Proof (Lean source)
If the pilot event is good and the stated condition on the cell holds, on the simultaneous pilot event, every cell selected by the concrete heavy threshold has population mass at least the declared lower band.
Formal statement
Proof (Lean source)
If the pilot event is good and the stated condition on the cell holds, on the simultaneous pilot event, every cell rejected by the concrete heavy threshold has population mass at most the declared upper band.
Formal statement
Proof (Lean source)
If the sample is nonempty, the generic logarithmic two-sided pilot bound specialized to the exact threshold and balanced first block used by rawPolyEstimator.
Formal statement
Proof (Lean source)
If the sample size satisfies the stated lower bound, at the declared pilot bands, the two Chernoff exponents both dominate 32 * log(en), giving a directly usable bad-selector probability bound.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.RateAlgebra 2 declarations
If the sample is nonempty and the logarithmic scale satisfies its stated bound and the stated growth condition holds, the first coefficient-growth term is absorbed by the parametric and quadratic-alphabet rates once its scalar logarithmic factor is at most the square-root sample scale.
Formal statement
Proof (Lean source)
If the sample is nonempty and the logarithmic scale satisfies its stated bound and the stated growth condition holds, the second coefficient-growth term is absorbed directly by the quadratic-alphabet rate under the corresponding logarithmic growth bound.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.RateClosure 5 declarations
If the sample size satisfies the stated lower bound and the overlap constant is positive, the missing-mass term is bounded by the polynomial rate component.
Formal statement
Proof (Lean source)
If the sample is nonempty and the overlap constant is positive and the polynomial or elbow parameter satisfies its stated bound, the polynomial approximation bias term is bounded by the polynomial rate component.
Formal statement
Proof (Lean source)
If the sample is nonempty and the stated llarge condition holds, the linear light-cell variance term is bounded by the target polynomial rate.
Formal statement
Proof (Lean source)
If the sample is nonempty and the stated llarge condition holds, the quadratic light-cell variance term is bounded by the polynomial rate component.
Formal statement
Proof (Lean source)
If the sample size satisfies the stated lower bound and the overlap constant is positive and the stated c condition holds and the polynomial or elbow parameter satisfies its stated bound and the stated llarge condition holds, the complete uniform branchwise error expression is bounded by the target polynomial rate.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.SelectionDecomposition 4 declarations The pilot selector partitions the normalized pre-clipping error into a heavy marked-ratio error and a light polynomial error.
The pilot selector partitions the normalized pre-clipping error into a heavy marked-ratio error and a light polynomial error. Keeping this identity separate lets the two fixed-set moment bounds be assembled independently.
The normalized estimation error contributed by cells selected as heavy.
Definition (Lean source)
The normalized estimation error contributed by cells selected as light.
Definition (Lean source)
The pre-clipping normalized error is exactly the sum of the selected heavy and selected light errors; no probability or moment assumption enters this partition identity.
Formal statement
Proof (Lean source)
The exact selector partition yields the standard two-term squared-error bound used to combine the heavy and light risk estimates.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.SelectorBridge 3 declarations
If the selected heavy set is fixed, the selector's fixed heavy error equals the heavy component of the corresponding fixed branch.
Formal statement
Proof (Lean source)
the selector's fixed light error equals the light component of the corresponding fixed branch.
Formal statement
Proof (Lean source)
If the selected heavy set is fixed, the selector's fixed total error equals the error of the corresponding fixed branch.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.SelectorRisk 5 declarations
If the target lies in the clipping interval, the squared clipped normalized error is at most four.
Formal statement
Proof (Lean source)
the clipped normalized error for a selected polynomial branch is measurable.
Formal statement
Proof (Lean source)
If the bad-event contribution is bounded as stated, the probability that a pilot fold is bad satisfies the stated exponential bound.
Formal statement
Proof (Lean source)
If the stated lower bound holds and the branchwise risk is bounded as stated and the bad-event probability is bounded as stated and each fixed branch has the stated risk bound and the bad-event contribution is bounded as stated, a uniform deterministic fixed-branch bound transfers through the measurable pilot selector. Clipping supplies the global envelope on the bad pilot event.
Formal statement
Proof (Lean source)
If the indicated calibration branch applies and the stated stream condition holds, the polynomial estimator's mean squared error is bounded by the corresponding clipped-stream normalized risk after rescaling.
Formal statement
Proof (Lean source)
Helpers.PolynomialUpper.SplitBridge 26 declarations
The deterministic half-split used by the concrete polynomial estimator, packaged as a generic one-shot split of the infinite iid realization.
Definition (Lean source)
Rebuild a full sample from its pilot fold, filling the unused estimation positions by an arbitrary fixed observation.
Definition (Lean source)
Rebuild a full sample from its estimation fold, filling the unused pilot positions by an arbitrary fixed observation.
Definition (Lean source)
Rebuilding the full tuple from the estimation fold is measurable.
Formal statement
Proof (Lean source)
Rebuilding from the pilot fold preserves every concrete pilot count.
Formal statement
Proof (Lean source)
Rebuilding from the estimation fold preserves every arm-cell count.
Formal statement
Proof (Lean source)
Rebuilding from the estimation fold preserves every marked outcome sum.
Formal statement
Proof (Lean source)
The aggregate one-mark factorial is a function of the estimation fold alone.
Formal statement
Proof (Lean source)
Every fixed light-cell polynomial contribution depends only on the estimation fold.
Formal statement
Proof (Lean source)
Every fixed heavy-cell marked-ratio contribution depends only on the estimation fold.
Formal statement
Proof (Lean source)
The finite heavy-set branch selected by a rebuilt pilot fold.
Definition (Lean source)
The finite heavy-set selector is measurable as a function of the pilot fold. Its value depends only on the finite cell labels, not on outcomes.
Formal statement
Proof (Lean source)
A deterministic selector value is eligible when every selected-heavy cell lies above the lower pilot band and every complementary light cell lies below the upper pilot band.
Definition (Lean source)
The fold-level good event is the measurable preimage of the eligible finite selector values.
Definition (Lean source)
Eligibility of the pilot-selected heavy set is a measurable event on the finite pilot fold.
Formal statement
Proof (Lean source)
Normalized heavy error for a deterministic pilot-selected set, evaluated only on the independent estimation fold.
Definition (Lean source)
Normalized light error for the complementary deterministic set, evaluated only on the independent estimation fold.
Definition (Lean source)
Every deterministic heavy-branch error is measurable on the independent estimation fold.
Formal statement
Proof (Lean source)
Every deterministic complementary light-branch error is measurable on the independent estimation fold.
Formal statement
Proof (Lean source)
The fixed-selector branch error combines the heavy score on the selected set with the polynomial score on its complement.
Definition (Lean source)
Every fixed-selector total error is measurable on the estimation fold.
Formal statement
Proof (Lean source)
On the iid realization, the fold-valued selector is exactly the heavy set appearing in the concrete full-sample estimator.
Formal statement
Proof (Lean source)
If the pilot event is good, the simultaneous pilot sandwich event from the probability bound implies eligibility of the concrete finite selector on the pilot fold.
Formal statement
Proof (Lean source)
Selecting the fixed-heavy branch with the pilot fold recovers the concrete selected-heavy error on the iid prefix.
Formal statement
Proof (Lean source)
Selecting the complementary fixed-light branch with the pilot fold recovers the concrete selected-light error on the iid prefix.
Formal statement
Proof (Lean source)
Selecting a fixed total branch with the pilot fold recovers the complete normalized pre-clipping error on the iid prefix.
Formal statement
Proof (Lean source)
Helpers.RadialChannelKernel 4 declarations This file constructs the hypothesis-independent one-record channel used by the radial converse and proves that it is a Markov kernel throughout the declared radius range.
The observed Bernoulli contraction kernel
This file constructs the hypothesis-independent one-record channel used by the radial converse and proves that it is a Markov kernel throughout the declared radius range.
The success probability of the paper's binary contraction channel.
Definition (Lean source)
If the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, for a radius parameter between zero and two, both conditional success probabilities are valid Bernoulli parameters.
Formal statement
Proof (Lean source)
The one-record radial channel preserves the padded cell and treatment, draws the contracted Bernoulli response, and sends its atoms to ±M/2.
Definition (Lean source)
If the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, the observed Bernoulli contraction is a Markov kernel for every declared radius 0 ≤ sigma ≤ 2.
Formal statement
Proof (Lean source)
Helpers.RadialContractedBinary 9 declarations This file constructs the binary observation law obtained by passing the source response through the paper's hypothesis-independent Bernoulli contraction.
Contracted binary source law for the radial converse
This file constructs the binary observation law obtained by passing the source response through the paper's hypothesis-independent Bernoulli contraction.
Conditional law of the contracted response bit given the source bit.
Definition (Lean source)
If the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, the success atom of the contraction PMF has the declared channel mass.
Formal statement
Proof (Lean source)
If the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, the failure atom of the contraction PMF has the complementary mass.
Formal statement
Proof (Lean source)
The source observation law after retaining (X,A) and independently drawing the contracted response bit conditional on the source response.
Definition (Lean source)
If the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, the contraction leaves the joint (X,A) margin exactly unchanged.
Formal statement
Proof (Lean source)
If the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, each output atom is the source-bit mixture prescribed by the common Bernoulli contraction channel.
Formal statement
Proof (Lean source)
If the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, summing over the contracted response shows that the channel preserves each cell-treatment mass exactly.
Formal statement
Proof (Lean source)
If the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, the Bernoulli contraction preserves every source cell mass.
Formal statement
Proof (Lean source)
If the heterogeneity radius is nonnegative and the heterogeneity radius is at most two and the source law satisfies the stated model condition, because both cell and cell-treatment masses are preserved, contraction preserves the strong-overlap certificate.
Formal statement
Proof (Lean source)
Helpers.RadialFiniteSampleScale 1 declarations Finite-sample radial transport scale
Finite-sample radial transport scale
If the sample is nonempty and the sampling budget satisfies the stated lower bound, below a fixed sample-size cutoff, the one-arm parametric source bound dominates the capped radial term after Bernoulli-channel scaling.
Formal statement
Proof (Lean source)
Helpers.RadialFullCoupling 4 declarations This module proves the finite PMF identity behind the full-data radial-channel certificate, including the zero-mass-cell boundary case.
Full-data coupling under the radial Bernoulli channel
This module proves the finite PMF identity behind the full-data radial-channel certificate, including the zero-mass-cell boundary case.
This is the full-data probability mass function obtained after radial Bernoulli contraction.
Definition (Lean source)
If the heterogeneity radius is nonnegative and the heterogeneity radius is at most two and the transport scale satisfies the stated condition, the outcome distribution of a radially contracted binary law is the corresponding Bernoulli contraction distribution.
Formal statement
Proof (Lean source)
If the overlap constant is positive and the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, the contracted full-data distribution equals the independent coupling generated from the contracted observed law.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet and the overlap constant is positive and the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, the concrete affine radial embedding is exactly the paper's common two-potential-outcome Bernoulli channel applied to the independent source coupling.
Formal statement
Proof (Lean source)
Helpers.RadialHardFamily 8 declarations
If the alphabet is nonempty and the overlap constant is positive and the overlap constant is below one half and the logarithmic scale satisfies its stated bound, any level strictly below the one-arm minimax risk is attained as a lower bound against every measurable estimator by a control-zero source law.
Formal statement
Proof (Lean source)
If the alphabet is nonempty and the overlap constant is positive and the overlap constant is below one half and the strict one-arm lower-bound constant is available and the stated lower bound holds, a strict one-arm minimax lower bound equips the full control-zero source class with the hard-family certificate carried by a radius-channel handle.
Formal statement
Proof (Lean source)
If the sample is nonempty and the alphabet is nonempty and the overlap constant is positive and the overlap constant is below one half and the transport scale satisfies the stated condition and the stated lower bound holds, a positive non-strict one-arm lower bound yields a hard full source family after halving its constant, which supplies the strict level required by the minimax hard-family extractor.
Formal statement
Proof (Lean source)
If the sample is nonempty and the alphabet is nonempty and the overlap constant is positive and the overlap constant is below one half and the transport scale satisfies the stated condition and the stated lower bound holds, a positive fixed-sample one-arm lower bound supplies exactly the uniformly bounded source-estimator hardness premise required by randomized kernel transport, after the standard strict half-constant reduction.
Formal statement
Proof (Lean source)
If the sample is nonempty and the alphabet is nonempty and the overlap constant is positive and the overlap constant is below one half, the one-arm two-point subexperiment supplies the uniformly bounded source-estimator hardness interface at every positive sample size. The strict half-constant permits extraction of an actual source law from the minimax infimum and is the fallback used below the radial asymptotic cutoff.
Formal statement
Proof (Lean source)
If the overlap constant is positive and the overlap constant is below one half, the proved Zeng one-arm theorem yields constants, a cutoff, and the estimator-wise source hardness interface consumed by the Bernoulli channel transport in the radius converse.
Formal statement
Proof (Lean source)
If the sample is nonempty and the alphabet is nonempty and the overlap constant is positive and the overlap constant is below one half, for every positive sample size and alphabet, the full control-zero source class is a genuinely hard family. The positive (instance-dependent) constant is obtained by normalizing the universal one-arm parametric lower bound by the strictly positive source rate.
Formal statement
Proof (Lean source)
If the sample is nonempty and the alphabet size satisfies the stated condition and the overlap constant is positive and the overlap constant is below one half and the source parameter set has the stated form, a least-favorable handle whose radial source is the full control-zero class inherits the unconditional hard-family certificate.
Formal statement
Proof (Lean source)
Helpers.RadialMembership 2 declarations
If the source alphabet embeds in the target alphabet and the overlap constant is positive and the outcome scale satisfies its stated bound and the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, the contracted control-zero construction has realization-wise radius at most sigma * M, including the zero-radius endpoint.
Formal statement
Proof (Lean source)
The concrete padded radial channel is an ambient model-class element.
Definition (Lean source)
Helpers.RadialProductDataProcessing 2 declarations This module lifts a one-record common Markov-kernel identity to the finite product experiments and records the resulting data-processing inequality.
Product total-variation contraction for the radial channel
This module lifts a one-record common Markov-kernel identity to the finite product experiments and records the resulting data-processing inequality.
If the first target law is produced by the channel and the second target law is produced by the channel, a common one-record Markov channel contracts total variation after taking the finite i.i.d. product experiment.
Formal statement
Proof (Lean source)
If the target law is the specified transported law, the pointwise observed-law identity for a common radial kernel packages directly as the handle's product data-processing certificate.
Formal statement
Proof (Lean source)
Helpers.RadialRateAlgebra 2 declarations
If the sample size satisfies the stated lower bound and the alphabet is nonempty and the radial cap satisfies its stated bound and the radial cap is at most one quarter and the scalar satisfies the stated range condition, capping the source alphabet at half of b n log(en) retains, up to the explicit factor b²/16, the ambient capped polynomial component.
Formal statement
Proof (Lean source)
If the sample size satisfies the stated lower bound and the alphabet is nonempty and the transport scale satisfies the stated condition and the radial cap satisfies its stated bound and the radial cap is at most one quarter and the scalar satisfies the stated range condition, after the Bernoulli channel scales the source target by M σ / 2, the capped source lower bound supplies the ambient radial term with the explicit constant a b² / 128.
Formal statement
Proof (Lean source)
Helpers.RadialTarget 4 declarations This file proves the exact conditional-mean and ATE scaling identities used by the concrete least-favorable radial handle.
Target scaling under the radial Bernoulli channel
This file proves the exact conditional-mean and ATE scaling identities used by the concrete least-favorable radial handle.
If the heterogeneity radius is nonnegative and the heterogeneity radius is at most two and the transport scale satisfies the stated condition, on every positive source arm, the common Bernoulli contraction sends the conditional response mean through its declared affine channel.
Formal statement
Proof (Lean source)
If the overlap constant is positive and the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, on the control-zero source family, contraction multiplies the binary ATE by exactly sigma / 2, including the zero-radius endpoint.
Formal statement
Proof (Lean source)
If the source alphabet embeds in the target alphabet and the overlap constant is positive and the heterogeneity radius is nonnegative and the heterogeneity radius is at most two, zero-mass padding and affine outcome scaling preserve the radial target identity, giving the exact slope used by Markov-kernel risk transport.
Formal statement
Proof (Lean source)
If the transport scale satisfies the stated condition and the radial target formula holds and the exact risk-transfer identity holds, pointwise affine target formulas for the radial and exact source families imply the pairwise separation certificate by subtraction.
Formal statement
Proof (Lean source)
Helpers.RateAlgebra 6 declarations
The parametric-plus-exact-homogeneity benchmark b.
Definition (Lean source)
If the sample is nonempty, the squared logarithmic scale is bounded by nine times the sample size.
Formal statement
Proof (Lean source)
At radii zero and two, the all-alphabet upper and lower rate expressions are uniformly comparable, radius two gives the unrestricted model class, and the radius-two frontier is exactly the unrestricted endpoint formula.
Formal statement
Proof (Lean source)
Restricted-range exact-homogeneity reduction together with the unrestricted radius-two identity and converse comparison for every positive alphabet size.
Formal statement
Proof (Lean source)
A sequence lies in the residual shrinking-radius wedge.
Definition (Lean source)
Descriptive, never-proved open question. Put L = log(en), b = n⁻¹ + d/n², and u = d²/(n²L²). In the residual wedge b ≪ u ≪ 1 and b ≪ sigma² ≪ 1, ask for either a realization-wise radius-constrained paired-cell moment-matching fuzzy experiment in the model class with ATE separation of order M * min(sigma, d/(nL)) and sample-mixture total variation bounded away from one, or an explicit total estimator with risk strictly smaller than the selector benchmark M² * (b + min(u,sigma²)). The ideal desideratum is an estimator ideally attaining the proved product benchmark M² * (b + sigma²*u). The existing hypothesis-independent channel yields only product separation M * sigma * min(1,d/(nL)) and therefore does not answer the question.
Definition (Lean source)
T_AteIdentification 19 declarations
the full-data covariate coordinate is measurable.
Formal statement
Proof (Lean source)
the full-data treatment coordinate is measurable.
Formal statement
Proof (Lean source)
the control potential-outcome coordinate is measurable.
Formal statement
Proof (Lean source)
the treated potential-outcome coordinate is measurable.
Formal statement
Proof (Lean source)
the full-data observed-outcome coordinate is measurable.
Formal statement
Proof (Lean source)
the observed covariate coordinate is measurable.
Formal statement
Proof (Lean source)
the observed treatment coordinate is measurable.
Formal statement
Proof (Lean source)
the observed outcome coordinate is measurable.
Formal statement
Proof (Lean source)
the selected potential-outcome coordinate is measurable.
Formal statement
Proof (Lean source)
the projection from full data to observed data is measurable.
Formal statement
Proof (Lean source)
the full-data probability of a covariate cell equals its observed cell probability.
Formal statement
Proof (Lean source)
the full-data probability of an arm-cell event equals the observed arm-cell probability.
Formal statement
Proof (Lean source)
the observed arm-cell outcome measure factors into cell probability, arm propensity, and the conditional outcome law.
Formal statement
Proof (Lean source)
If consistency holds, consistency implies that the observed outcome equals the treatment-selected potential outcome almost surely.
Formal statement
Proof (Lean source)
If consistency holds, under exchangeability, the full-data arm-cell potential-outcome measure factors into the arm-cell probability and conditional outcome law.
Formal statement
Proof (Lean source)
If the stated condition on the cell holds, under exchangeability and overlap, the full-data cell potential-outcome measure factors into the cell probability and conditional outcome law.
Formal statement
Proof (Lean source)
each potential outcome is integrable under the full-data law.
Formal statement
Proof (Lean source)
the full-data integral of a potential outcome within a cell equals cell probability times its conditional mean.
Formal statement
Proof (Lean source)
Consistency, conditional exchangeability, overlap, and the moment envelope identify the causal ATE from the observed margin by the finite g-formula.
Formal statement
Proof (Lean source)
T_FixedInteriorTightness 23 declarations
Selector benchmark q before saturation.
Definition (Lean source)
Product-form converse benchmark ell.
Definition (Lean source)
One of the three regimes in which the proved benchmarks match uniformly.
Definition (Lean source)
Divergence of the selector/converse benchmark ratio along a sequence.
Definition (Lean source)
Two positive sequences have the same order eventually.
Definition (Lean source)
If the heterogeneity radius is nonnegative and the heterogeneity radius is at most two and the stated lower bound holds and the stated upper bound holds, in the nonsaturated triangular regime, the selector benchmark is within a factor two of the additive benchmark using min (u, sigma²).
Formal statement
Proof (Lean source)
If the sample is nonempty, the polynomial component is below the base rate exactly at the displayed constant-free algebraic elbow.
Formal statement
Proof (Lean source)
If the sample is nonempty and the alphabet size satisfies the stated condition, the small-alphabet condition d ≤ sqrt(n) log(en) implies the polynomial component is below the base rate.
Formal statement
Proof (Lean source)
If the sample is nonempty and the alphabet size satisfies the stated condition, the regime d ≤ log(en)² is contained in the constant-free algebraic elbow.
Formal statement
Proof (Lean source)
If the sample is nonempty and the radius is bounded away from zero and the heterogeneity radius is nonnegative and the heterogeneity radius is at most two and the heterogeneity radius satisfies the stated bound, at a fixed positive radius, the selector benchmark is bounded by a constant multiple of the product-form converse benchmark, uniformly in the alphabet.
Formal statement
Proof (Lean source)
If the sample is nonempty and the polynomial or elbow parameter satisfies its stated bound and the matching-elbow condition holds, in any matching elbow, the selector benchmark is bounded by 1 + K times the converse benchmark.
Formal statement
Proof (Lean source)
If the overlap constant is positive and the overlap constant is below one half and the radius is bounded away from zero, the two-sided minimax bracket and fixed-radius benchmark comparison give uniform minimax equivalence at every radius bounded away from zero.
Formal statement
Proof (Lean source)
If the overlap constant is positive and the overlap constant is below one half and the polynomial or elbow parameter satisfies its stated bound, the two-sided minimax bracket and elbow comparison give uniform minimax equivalence in each of the three matching regimes.
Formal statement
Proof (Lean source)
The paper's logarithmic scale diverges with the sample size.
Proof (Lean source)
Every fixed natural power of log(en) is negligible relative to n.
Formal statement
Proof (Lean source)
If the sample is nonempty, on the diagonal witness, the selector and product benchmarks have the explicit reciprocal-log formulas used in the rate comparison.
Formal statement
Proof (Lean source)
The diagonal sequence d=n, sigma=log(en)^(-1/2) lies in the residual wedge.
Formal statement
Proof (Lean source)
The diagonal selector/product ratio is eventually between one third and twice the logarithmic scale.
Formal statement
Proof (Lean source)
The diagonal selector/product benchmark ratio diverges.
Formal statement
Proof (Lean source)
If the sequence is eventually in the admissible parameter range and the benchmark ratio diverges and the polynomial or elbow parameter satisfies its stated bound, a diverging benchmark ratio eventually leaves every fixed matching elbow.
Formal statement
Proof (Lean source)
If the sequence is eventually in the admissible parameter range and the benchmark ratio diverges, divergence of the all-alphabet benchmark ratio forces all four defining limits of the residual shrinking-radius wedge.
Formal statement
Proof (Lean source)
The benchmarks match at every fixed positive radius and in each stated elbow regime; any divergence is confined to the residual wedge, which is nonempty.
Formal statement
Proof (Lean source)
Restricted-range specialization of the fixed-interior and shrinking-radius phase theorem.
Formal statement
Proof (Lean source)
T_FrontierUpper 5 declarations
Asymptotic comparison with the published collision remainder.
Definition (Lean source)
The selector risk bound without the secondary published-comparison clause.
Formal statement
Proof (Lean source)
The total selector achieves the all-alphabet frontier rate.
Formal statement
Proof (Lean source)
Restricted-dimension selector upper bound.
Formal statement
Proof (Lean source)
The cited binary collision guarantee and the independent algebraic comparison to its remainder hold simultaneously.
Formal statement
Proof (Lean source)
T_RadiusChannelConverse 19 declarations
If the outcome scale satisfies its stated bound and the transport scale satisfies the stated condition and the target law is the specified transported law and the target parameter has the stated affine relation and the source parameter set has the stated form and the target separation has the stated scaling, the generic Markov-kernel comparison specializes to the radial source family: once the one-coordinate channel law and affine target identity are available, every bounded ambient estimator is defeated by a radial source member at the transported scale.
Formal statement
Proof (Lean source)
If the transport scale satisfies the stated condition and the affine observation map has the stated form and the target law is the specified transported law and the target parameter has the stated affine relation and the source parameter set has the stated form and the target separation has the stated scaling, the deterministic affine comparison specializes to the exact source family carried by a least-favorable handle. This is the exact-family analogue of radial_risk_of_kernel_transport and retains the witnessing source law, which is needed by RiskTransferCertificate.
Formal statement
Proof (Lean source)
If the transport scale satisfies the stated condition and the affine observation map has the stated form and the target law is the specified transported law and the target parameter has the stated affine relation and the source parameter set has the stated form and the target separation has the stated scaling, pointwise deterministic affine transport packages directly as the exact half of a RiskTransferCertificate.
Formal statement
Proof (Lean source)
If the outcome scale satisfies its stated bound and the transport scale satisfies the stated condition and the target law is the specified transported law and the target parameter has the stated affine relation and the source parameter set has the stated form and the target separation has the stated scaling and the exact risk-transfer identity holds, a radial Markov-kernel transport and the independently transferred exact family together discharge the two halves of RiskTransferCertificate.
Formal statement
Proof (Lean source)
If the heterogeneity radius is nonnegative, for a radius parameter in [0,2], the Bernoulli contraction probability lies in the advertised interval, including both endpoint bits.
Formal statement
Proof (Lean source)
If the specified least-favorable family is available and the heterogeneity radius is nonnegative, the channel formula stored by a least-favorable family automatically discharges the theorem's pointwise probability-range certificate.
Formal statement
Proof (Lean source)
If the base-rate constant is positive and the radius-rate constant is positive and the base lower bound holds and the radial source lower bound holds, two lower bounds against the same minimax risk combine into the displayed three-term converse rate after halving the smaller constant.
Formal statement
Proof (Lean source)
If the outcome scale satisfies its stated bound and the transported family belongs to the target model class and the risk-transfer certificate holds, the radial half of a risk-transfer certificate gives a lower bound on the ambient minimax risk once every embedded source law has a class witness.
Formal statement
Proof (Lean source)
If the outcome scale satisfies its stated bound and the base-rate constant is positive and the radius-rate constant is positive and the base lower bound holds and the transported family belongs to the target model class and the risk-transfer certificate holds, the proved all-alphabet exact transfer and a concrete radial handle assemble the full capped converse rate with the minimum of their constants.
Formal statement
Proof (Lean source)
If the alphabet is nonempty, capping a positive ambient alphabet by a cutoff forced to be at least one always leaves a nonempty source alphabet and never exceeds the ambient one.
Formal statement
Proof (Lean source)
If the radial cap satisfies its stated bound and the sample size satisfies the stated lower bound and the source range is at least one, halving the source alphabet constant absorbs the log (e n) cutoff into the cited log n source range once n ≥ 3; the explicit unit lower bound also absorbs the nonempty-alphabet max 1 guard.
Formal statement
Proof (Lean source)
If the overlap constant is positive and the overlap constant is below one half, the Zeng one-arm constants can be shrunk once so that the paper's capped radial alphabet is nonempty, remains in the source theorem's range, and has exactly the transported product-radius scale needed in the large-sample branch.
Formal statement
Proof (Lean source)
If the sample is nonempty and the alphabet is nonempty and the overlap constant is positive and the overlap constant is below one half and the transport scale satisfies the stated condition and the stated lower bound holds, a positive fixed-sample exact-homogeneity minimax lower bound supplies the estimator-wise source hardness interface used by deterministic affine transport, after the same strict half-constant reduction as in the radial family.
Formal statement
Proof (Lean source)
If the sample is nonempty and the alphabet size satisfies the stated condition and the overlap constant is positive and the overlap constant is below one half and the transport scale satisfies the stated condition and the source parameter set has the stated form and the stated lower bound holds, a handle whose exact source is the full exact binary class inherits the hard-family certificate from a positive fixed-sample exact minimax lower bound.
Formal statement
Proof (Lean source)
If the sample is nonempty and the alphabet size satisfies the stated condition and the overlap constant is positive and the overlap constant is below one half and the source parameter set has the stated form, for every positive sample size and capped alphabet, the full exact binary source class is a genuinely hard family. As in the radial source interface, the constant carried by the structural handle may depend on the concrete instance; the uniform constant used by the eventual risk-transfer certificate is supplied separately by the cited exact lower bound.
Formal statement
Proof (Lean source)
If the sample is nonempty and the alphabet is nonempty and the overlap constant is positive and the overlap constant is below one half, the exact source's two-point subexperiment gives the estimator-wise parametric risk interface at every positive sample size. The strict half-constant is what permits extraction of an actual hard source law from the minimax infimum/supremum.
Formal statement
Proof (Lean source)
If the overlap constant is positive and the overlap constant is below one half, the cited exact lower bound, its capped alphabet, and the finite-sample parametric fallback can be normalized to one estimator-wise transport scale valid for every positive sample size and ambient alphabet.
Formal statement
Proof (Lean source)
The hypothesis-independent Bernoulli contraction transfers the one-arm source bound, while the exact-homogeneity source supplies the capped d/n² term.
Formal statement
Proof (Lean source)
Restricted-range corollary of the all-alphabet radius-channel converse.
Formal statement
Proof (Lean source)
T_RobustUpperConstruction 2 declarations
The explicit polynomial and collision constructions are admissible and obey their two all-alphabet risk envelopes without an additional logarithmic factor.
Formal statement
Proof (Lean source)
Restricted-dimension form of the robust upper-construction theorem.
Formal statement
Proof (Lean source)
T_TwoSidedMinimaxBracket 3 declarations
All-alphabet two-sided minimax bracket on one and the same real-outcome model class. The two benchmarks are not asserted to be uniformly equivalent for every shrinking interior radius.
Formal statement
Proof (Lean source)
Restricted-range form of the headline minimax bracket.
Formal statement
Proof (Lean source)
The canonical affine embedding realizes the binary subclasses, with strict image inclusion and the lower- and upper-bound transfers assembled here.