Formalization: Minimax Response Recovery under Global Overlap Tails
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. Note: this index was generated at a different commit than the paper's audited pin (d07574d) — statements may have moved since the audit.
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.DornScope 12 declarations The printed pointwise lower clause is obstructed by a known-regression singleton family.
Scope of Dorn's Theorem 1
The printed pointwise lower clause is obstructed by a known-regression singleton family. The source upper clause is kept as a cited, explicit gate.
A fixed, known-regression Gaussian experiment on Dorn's cube. For the stated inputs and conditions, the dornCanonicalLaw object being defined.
Definition (Lean source)
The canonical experiment has the stated uniform covariate law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The independent half-treated arm has constant selected propensity. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Both conditional response arms of the canonical experiment are standard Gaussian. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Pointwise miss probability, as an extended nonnegative risk. For the stated inputs and conditions, the dornPointwiseMissRisk object being defined.
Definition (Lean source)
If the regression curve is known across a family, its pointwise minimax miss probability vanishes for every positive threshold. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A constant half propensity has the global polynomial tail with coefficient 2 ^ (γ - 1) under any probability design. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A Euclidean ball centered in Dorn's closed cube has positive volume in the cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The known zero regression has zero spatial variance under the canonical design. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The zero regression belongs to every positive-radius Dorn seminorm class. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A known-regression family has zero pointwise minimax error. In particular, the explicit uniform-design, half-treated, centered Gaussian singleton obeys Dorn's per-law conditions and common A3, yet has zero minimax error. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Dorn's Theorem 1(ii) gives a no-log L∞(P_X) upper rate after the source family, all common constants including gamma, and the selected propensity representatives have been fixed. The source comparison is supplied by the cited gate, including measurability of every displayed L∞(P_X) exceedance event and hence its ordinary probability. The second conclusion gives the known-regression obstruction to the printed lower clause, including its Gaussian witness. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.HolderCompletion 1 declarations The source class supplies only an intrinsic top-order seminorm.
Fixed-cube completion of Dorn's Hölder seminorm
The source class supplies only an intrinsic top-order seminorm. The completion and affine transport are performed on the closed cubes using within-cube jets.
A response sup bound and Dorn's top-derivative seminorm control the full intrinsic Hölder radius after affine scaling. The constant depends on dimension and smoothness alone. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.Identification 6 declarations Identification of the Hölder treated response
Identification of the Hölder treated response
A global lower-tail bound excludes a zero propensity set. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The global tail condition makes the propensity strictly positive almost everywhere under the covariate law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A positive density lower bound gives the reverse absolute continuity needed to transfer almost-everywhere identification to volume on the cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Observing a causal completion preserves its covariate marginal. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
An almost-everywhere property under a composition product holds at a fixed fiber value whenever that value has positive conditional mass almost everywhere. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Consistency, exchangeability, and global positivity identify the treated conditional regression almost everywhere; continuity and the density lower bound fix its representative at all cube points. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.LowerPair 60 declarations Bounded radial Bernoulli two-point experiment
Bounded radial Bernoulli two-point experiment
One coordinate factor of the explicit bump is Mathlib's standard smooth flat function composed with 1 - x². For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The explicit finite product bump is infinitely differentiable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The product bump is a valid unit-scale Bernoulli perturbation. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A perturbation below the baseline keeps both response kernels Bernoulli. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The radial CDF formula gives a valid treatment probability at every point. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The truncated radial CDF is bounded by the volume of a full cube of radius r, including when the centre is on the boundary. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The radial propensity is at most the full-cube radius power. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A uniform propensity bound on a radius-h neighbourhood of the bump. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Restricted volume on the unit cube is a probability measure. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The uniform-cube mass of a sup-norm ball is the displayed truncated radial CDF. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Applying the radial CDF to its own radius variable is stochastically no smaller than a uniform variable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Fixed positive choices of the bump amplitude and mesh multiplier satisfy all Bernoulli parameter constraints in the lower-pair construction. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Both testing responses retain the positive baseline success probability. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The perturbed testing response remains within twice its baseline. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Both Bernoulli response parameters stay strictly inside the unit interval, so their two-point response laws have common support. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The product bump has unit height at its centre. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every nonzero bump value lies inside the unit box in each coordinate. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A scaled nonzero bump is confined to the radius-h test cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A nonzero scaled bump lies in the closed sup-norm radius-h cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On the perturbation support, the treated-design weight has the small radius factor used in the lower-pair entropy estimate. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The two treated Bernoulli parameters differ by the full bump amplitude at the designated test point. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The treated Bernoulli perturbation is nonnegative and bounded by its nominal amplitude at every covariate point. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The observed Bernoulli kernels differ only inside the bump cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Scaling the bump by the oracle mesh yields the oracle separation scale. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Fixed positive construction constants give an admissible Bernoulli pair and the oracle-scale response-parameter gap at every sample size. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The oracle bandwidth cancels the sample-size factor in the pair's KL bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A fixed bandwidth multiplier makes any finite oracle-scale KL coefficient small, uniformly in the sample size. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Choose admissible testing parameters once, with both the oracle-scale KL budget and a positive response separation constant. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The binary relative entropy is bounded by the Pearson quadratic at the second Bernoulli parameter. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A common positive Bernoulli baseline makes the KL constant uniform over the testing pair. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The Bernoulli response kernels in the lower pair satisfy the quadratic KL estimate uniformly in location and bandwidth. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The treated KL integrand has the small propensity factor on the bump support, and vanishes away from that support. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Both potential outcomes of every admissible testing law lie in {0, B}. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The paper's explicit bump is the promoted normalized product bump. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The treated response perturbation belongs to the paper Hölder ball when the promoted uniform bump radius fits inside L. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A Hölder representative B p₁ identifies the conditional mean of the treated potential outcome in the explicit completion. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Endpoint-supported potential outcomes give the required treated mean and sub-Gaussian residual bound whenever treatment is positive almost everywhere. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A valid explicit completion over the uniform cube is a global-tail model once its response representative and sharp propensity tail are supplied. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The localized common-statistic Bernoulli KL estimate over an arbitrary measurable base space. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At a fixed covariate, the observed completion is the disjoint sum of its control and treated scaled-Bernoulli cells. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The fixed-covariate observed law is a measurable embedding of a treatment Bernoulli followed by the selected arm's scaled Bernoulli response. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A localized common-statistic KL bound from any supplied pointwise quadratic Bernoulli estimate. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The observed fixed-covariate KL has the treatment-propensity weight. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Integrating the fixed-covariate bound over the bump support gives the raw one-observation KL rate. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Identification makes the noncomputably selected response representative agree on the cube with any displayed model witness for the same observed law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The exact completion witnesses underlying the two observed lower-pair laws. For the stated inputs and conditions, the LowerPairExactModelWitness object being defined.
Definition (Lean source)
Fixed admissible pair constants work at every positive sample size. The KL and separation conditions are stated in the single-observation form used by the Le Cam substrate; both laws have bounded potential outcomes. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The compatibility wrapper retaining the original lower-pair API for the stated inputs and conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.Model 43 declarations The causal completion and the observed data law use explicit product spaces.
Weak-overlap response model
The causal completion and the observed data law use explicit product spaces. This
is a bypass-justified use of product measures: POSystem is regime-indexed,
whereas the present result concerns a random-design regression experiment.
BackdoorEstimationSystem assumes strict overlap. The local Hölder conditions
use intrinsic coordinate jets on the closed cube. Ambient representatives arise
only through the separate extension theorem.
Stated parameter spaces for a fixed model class. For the stated inputs and conditions, the ModelParameterDomain object being defined.
Definition (Lean source)
Stated compact range of overlap exponents. For the stated inputs and conditions, the AdaptationParameterDomain object being defined.
Definition (Lean source)
Covariate cube. For the stated inputs and conditions, the cube object being defined.
Fixed compact adaptation range. For the stated inputs and conditions, the adaptationRange object being defined.
Definition (Lean source)
Local polynomial degree. For the stated inputs and conditions, the polynomialDegree object being defined.
Definition (Lean source)
Effective covariate dimension. For the stated inputs and conditions, the effectiveDimension object being defined.
Definition (Lean source)
Oracle mesh width. For the stated inputs and conditions, the oracleMesh object being defined.
Definition (Lean source)
Oracle risk scale. For the stated inputs and conditions, the oracleRate object being defined.
Definition (Lean source)
The oracle mesh is interpreted on the model's parameter domain. For the stated inputs and conditions, the OracleMeshDomain object being defined.
Definition (Lean source)
The formula for the oracle mesh has the stated range on its parameter domain. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
One observation (X,A,Y). For the stated inputs and conditions, the Obs object being defined.
Completion (X,A,Y(0),Y(1),Y). For the stated inputs and conditions, the Completion object being defined.
Observable projection of the causal completion. For the stated inputs and conditions, the observed object being defined.
Definition (Lean source)
Covariate marginal of an observed law. For the stated inputs and conditions, the covariateLaw object being defined.
Covariate density, using the Radon–Nikodym derivative. For the stated inputs and conditions, the covariateDensity object being defined.
Definition (Lean source)
A propensity version obtained from the conditional treatment kernel. For the stated inputs and conditions, the propensity object being defined.
Definition (Lean source)
Density of the treated covariate distribution, normalized by the probability of treatment when that probability is positive. For the stated inputs and conditions, the treatedCovariateDensity object being defined.
Definition (Lean source)
Conditional treated response distribution. For the stated inputs and conditions, the treatedKernel object being defined.
Definition (Lean source)
Treated conditional regression. For the stated inputs and conditions, the treatedRegression object being defined.
Definition (Lean source)
Bounds on within-set coordinate jets on an arbitrary covariate domain. For the stated inputs and conditions, the HolderDerivBoundOn object being defined.
Definition (Lean source)
Top-order within-set coordinate-jet modulus on a covariate domain. For the stated inputs and conditions, the HolderTopModulusOn object being defined.
Definition (Lean source)
Maximum over coordinate partial derivatives through degree ceil β - 1. For the stated inputs and conditions, the HolderDerivBound object being defined.
Definition (Lean source)
Maximum over top-order coordinate partial Hölder moduli. For the stated inputs and conditions, the HolderTopModulus object being defined.
Definition (Lean source)
Intrinsic Hölder class on a specified cube, including Dorn's original cube. For the stated inputs and conditions, the HolderBallOn object being defined.
Definition (Lean source)
The response itself belongs to the intrinsic Hölder ball on the closed covariate cube; no outside extension is selected as a model member.
Definition (Lean source)
The paper's intrinsic ball is exactly the within-cube ball of the cube-extension library. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The sample law is the iid product of the observed law. For the stated inputs and conditions, the IIDSampleLaw object being defined.
Covariate density bounded below relative to volume on the cube. For the stated inputs and conditions, the CovariateDensityLowerBound object being defined.
Definition (Lean source)
Observed outcome equals the selected potential outcome. For the stated inputs and conditions, the OutcomeConsistency object being defined.
Definition (Lean source)
Potential outcomes and treatment are conditionally independent given X. For the stated inputs and conditions, the CondExchangeable object being defined.
Definition (Lean source)
Polynomial lower-propensity tail under the covariate law. For the stated inputs and conditions, the GlobalPropensityTail object being defined.
Definition (Lean source)
Bounded treated mean and conditionally sub-Gaussian treated residual. For the stated inputs and conditions, the BoundedMeanSubGaussianResidual object being defined.
Definition (Lean source)
The potential-outcome response has the designated Hölder representative. For the stated inputs and conditions, the HolderResponse object being defined.
Definition (Lean source)
Global-tail causal model with sub-Gaussian treated residuals.
Definition (Lean source)
@realizes X(covariate law supported on the cube)
@realizes f(covariate law absolutely continuous with respect to cube volume)
Observed laws admitting a causal completion in the model. For the stated inputs and conditions, the ModelClass object being defined.
Definition (Lean source)
A chosen Hölder representative for a law in the model class. For the stated inputs and conditions, the responseOf object being defined.
Definition (Lean source)
Euclidean closed ball, distinct from the sup-norm covariate cube. For the stated inputs and conditions, the ball2 object being defined.
A source-law tuple carries the observed law and the selected treated mean, control mean, and pointwise propensity representative. For the stated inputs and conditions, the DornSourceLaw object being defined.
Dorn's original covariate cube. For the stated inputs and conditions, the dornCube object being defined.
A selected propensity version for a probability law on a specified cube. For the stated inputs and conditions, the DornSelectedPropensity object being defined.
Definition (Lean source)
Dorn's A3 is a property of a nonempty family and its selected pointwise propensity versions. Its constants are common to every family member. For the stated inputs and conditions, the DornA3 object being defined.
Definition (Lean source)
Singleton abbreviation for the displayed law and selected propensity on the paper's unit cube. For the stated inputs and conditions, the DornA3OnCube object being defined.
Definition (Lean source)
The numerical local anti-concentration clause of Dorn's A3 for one displayed propensity on the paper's cube. This clause deliberately does not impose the separate selected-propensity requirement that e < 1 almost surely. For the stated inputs and conditions, the DornA3AntiConcentrationOnCube object being defined.
Definition (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.OrderedMass 3 declarations Uniform ordered treated-mass bound
Uniform ordered treated-mass bound
Rewrite the nonnegative geometric microcell volume as an ordinary real power. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Separate the cell volume and rank powers after division by the rank. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
One constant works uniformly over the compact range of overlap exponents. The first inequality is the layer-cake setwise bound; the second is the ordered weakest-cell profile. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.OrderedMass.Density 6 declarations Density lower bounds for covariate mass
Density lower bounds for covariate mass
An almost-everywhere lower density bound controls the mass of every measurable set. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The model's density condition gives a setwise lower covariate mass bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Each scaled microcell has covariate mass at least its volume times the model's density floor. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Treated mass adds over one selected microcell in each distinct macro-cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The same disjointness gives additivity of covariate mass over selected cells. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A set of distinct selected cells carries at least its cardinality times the single-cell density lower bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.OrderedMass.Geometry 8 declarations Geometry of treated microcells
Geometry of treated microcells
Reference microcubes are measurable, including at the template boundary. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every scaled microcell is measurable at every dyadic mesh. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Under the template width cap, every coordinate of a reference microcube lies strictly between zero and one. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A dyadic mesh width multiplied by the number of cells is one. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every scaled microcell lies inside its indexed macro-cube, including at the boundary of the ambient cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A point in a scaled microcell lies strictly between the corresponding macro-cube faces in every coordinate. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Microcells in different macro-cubes are disjoint, even if the microcell labels differ. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every scaled microcell has the same Euclidean volume, independently of its tensor node and macro-cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.OrderedMass.Ranking 14 declarations Ordered weakest-cell mass combinatorics
Ordered weakest-cell mass combinatorics
The minimum mass in a macro-cube is below each of its microcell masses. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A finite family of microcells contains one attaining the macro-cube minimum. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The setwise tail estimate gives a treated-mass bound for any measurable microcell once its covariate mass has a lower bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The sharp setwise tail estimate applies to any finite union of selected microcells, with covariate mass growing linearly in the number selected. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Sorting the finite macro-cube masses retains exactly one entry per cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The ordered masses are monotone in their list indices. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every in-range ordered mass is the minimum mass of a macro-cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every earlier ordered mass is no larger than the mass at rank k. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The total mass of the first k ordered macro-cubes is at most k times the mass at rank k. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At least k macro-cubes have weakest-microcell mass at most the mass at rank k, counting ties with their multiplicity. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A finite union of selected treated microcells has mass at most the sum of its component treated masses. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Selecting a minimizing microcell in each cube bounds the mass of their union by the number of cubes times any common upper bound on the minima. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Choose exactly the first k weakest macro-cubes (breaking ties arbitrarily) and one mass-minimizing microcell in each of them. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The treated mass of k selected weakest microcells is at most k times the kth weakest macro-cube mass. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.OrderedMass.Setwise 16 declarations Setwise and ordered treated-mass bounds
Setwise and ordered treated-mass bounds
The conditional treatment kernel disintegrates treated mass over any measurable covariate set. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The propensity version from the model gives the same setwise treated mass. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The setwise treatment probability is the real integral of the propensity. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A propensity version is almost everywhere between zero and one. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The propensity version is integrable on every measurable covariate set. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Layer cake expresses treated propensity mass through upper-level sets. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The global tail bound also controls the part of an arbitrary set lying in the low-propensity region. This is the setwise estimate used by layer cake. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Each set retains at least its mass minus the global lower tail above a propensity threshold. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On a bounded threshold interval, the layer-cake integrand dominates the set mass minus the global lower-tail envelope. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The exact integral in the setwise treated-mass argument. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Substituting the tail threshold into the layer-cake integral. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The proposed threshold balances the set mass against the tail envelope. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The layer-cake cutoff lies in the unit interval for a probability mass. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The analytic value of the layer-cake lower bound at its balancing threshold. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The global propensity tail yields the sharp setwise treated-mass bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The ordered-cell coefficient has a positive lower bound over a compact range of overlap exponents. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.SelectedMesh 19 declarations Selected-mesh coefficient envelope
Selected-mesh coefficient envelope
A positive selected width comes from a feasible dyadic index. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On the nonempty feasible event, the selected width is the width of the selected dyadic index. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Intersect a measurable count event with an almost-sure conditional coefficient assertion without increasing its failure probability. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The selected count event and the actual conditional coefficient MGF hold simultaneously on one measurable event with the count-event failure budget. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Convert the actual conditional coefficient MGF to the ordered variance proxy. The finite template factor and the uniform mass coefficient are absorbed into one constant. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Normalize the conditional MGF at its own cube-mass rank before reindexing cubes for the maximal inequality. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
One event controls the selected counts and the actual conditional coefficient MGF with a uniform rank proxy. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The logarithmic exponent has a fixed upper bound over the adaptation range; its apparent reciprocal dependence on the overlap exponent cancels. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The ordered maximal exponent stays in a fixed positive interval. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Apply the vector maximal inequality to cubes whose coefficient proxy is expressed through their mass rank. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The selected mesh obeys the count event, ordered conditional coefficient variance proxies, and a logarithm-free expected coefficient envelope under the stated inputs and conditions.
Formal statement
Proof (Lean source)
A design-saturated event has conditional probability one on the entire conditional sample fibre whenever the conditioning sample belongs to it. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The explicit design-saturated count event supports the ranked coefficient MGF bounds almost everywhere. Auxiliary fibre facts remain in the ambient almost-everywhere filter rather than being added to the event. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On the explicit design-saturated event, the conditional expected maximal coefficient fluctuation has the oracle-rate bound almost everywhere. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The saturated conditional bound integrates to the desired uniform risk bound for every displayed model witness. This version keeps the response representative explicit, so it is usable below the responseOf choice layer. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.SelectedMesh.Bias 19 declarations Deterministic selected-cell bias bounds
Deterministic selected-cell bias bounds
The identified Hölder representative agrees with the treated regression at every coordinate of an IID sample, outside one design-null set. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Rescaling any point of a dyadic macro-cell by its lower corner and width lands in the unit covariate cube, including the global right boundary. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The capped floor index assigns every cube point to its corresponding half-open dyadic macro-cell. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The normalized coordinates selected by cubeIndex lie in the unit cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Replacing treated outcomes by the identified regression preserves a local polynomial approximation and hence controls every fitted coefficient. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Almost surely over an IID sample, the conditional coefficient centre inherits any pointwise local-polynomial approximation of the selected design. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The local Hölder Taylor constant can be chosen before the centre and domain. This is the centre-uniform form needed by the selected mesh. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
One approximation constant works for every response in the intrinsic Holder ball. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Intrinsic [0,1]^d Hölder regularity supplies a fixed-cell polynomial in the exact MonoIndex basis. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every dyadic mesh width lies in (0,1]. For the stated inputs and conditions, the asserted conclusion holds.
Proof (Lean source)
The cell-bias constant is uniform over every model completion and response in the stated Holder ball. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Uniformly over cells, the conditional coefficient centre is close to a Taylor polynomial which approximates the Hölder representative throughout the whole dyadic cell. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The continuous Hölder representative inherits the treated-mean bound at every cube point, rather than only almost everywhere. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A cellwise conditional-centre bias bound and the realized coefficient envelope give a uniform pointwise bound for the clipped selected estimator. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The deterministic estimator bound can use the conditional centre and cell-bias witnesses at any representative of the same complete-design fibre. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A uniform real loss bound on the cube lifts directly to the ENNReal cube supremum used by the minimax risk. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Clipping bounds every estimator error by twice the outcome envelope. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.SelectedMesh.Coefficients 31 declarations Design-fixed coefficient differences
Design-fixed coefficient differences
The treated-cell count depends only on covariates and treatment arms. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Equal designs give the same equal-cell Gram matrix. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The change in a response moment is the design-weighted sum of the observation-wise changes in treated outcomes. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At a fixed design, a coefficient difference is the inverse Gram matrix applied to the difference of response moments. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At a fixed design, each coefficient difference is a finite linear combination of the treated outcome changes. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Replacing each outcome by its design-conditional mean isolates the treated residual in every coefficient coordinate. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The fixed-design weight of one response in a coefficient coordinate. For the stated inputs and conditions, the coefResidualWeight object being defined.
Definition (Lean source)
A coefficient residual weight vanishes for an untreated observation. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Residual weights are fixed on each fibre of the covariate and arm design. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A centered coefficient is one observation-wise weighted residual sum. The weights depend only on the covariates and treatment arms. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On a design fibre, every residual coefficient uses the weights from the conditioning design, even when the outcomes vary. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Squared observation weights in one treated microcell cost one inverse count. This is the counting step in the conditional variance proxy. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Collect the fixed-design coefficient weight by template cell. The matrix row and monomial vector form one scalar coefficient per observation. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A fixed finite number of template cells converts the cellwise inverse-count estimate into a bound for their combined observation weight. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A bounded inverse-Gram row evaluation gives the coefficient coordinate the inverse-count variance scale. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Equal-cell response moments exactly reproduce a polynomial in the local monomial basis. For the stated inputs and conditions, the asserted conclusion holds.
Proof (Lean source)
On an occupied equal-cell design, fitting polynomial responses recovers their coefficient vector exactly. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Feasibility forces every treated template cell to be occupied. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A coordinate of a matrix-vector product is controlled by the finite Euclidean operator norm. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A uniform coordinate bound controls the Euclidean norm of a finite vector by the square root of its dimension. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
If every treated response perturbation entering a template cell is at most r, then every coordinate of the equal-cell response moment changes by at most r. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On an occupied equal-cell design, a coordinatewise response-moment perturbation is stable under inversion of the empirical Gram matrix. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Pointwise treated-response approximation on every occupied microcell implies a dimension-explicit bound for each fitted coefficient. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
An occupied equal-cell fit is stable around any local polynomial whose values uniformly approximate the treated responses entering its microcells. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Conditioning of the equal-cell Gram matrix bounds each evaluation of an inverse-Gram row at a normalized covariate. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On the unit cube, every monomial coordinate has magnitude at most one, so the whole template vector has norm at most the square root of its size. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Clipping to the outcome range cannot increase error relative to a target already in that range. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A uniform coordinate error in local polynomial coefficients yields a uniform evaluation error on the normalized unit cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Combining coefficient control with clipping leaves only the deterministic local-polynomial approximation error. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At a positive selected mesh, coefficient control plus a local polynomial approximation controls the actual clipped estimator at a fixed point. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every occupied template cell has the same dimension-only inverse-Gram row bound. This supplies the row premise of the squared-weight estimate. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.SelectedMesh.Counts 28 declarations Oracle witness and simultaneous selected-count event
Oracle witness and simultaneous selected-count event
A single event controls treated counts over every candidate dyadic mesh and every template cell. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The all-candidate count deviation event can be retained together with its saturation under equality of covariates and treatment arms. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The simultaneous deviation event gives the selected-mesh count envelope once an oracle-scale candidate satisfies the deterministic mass and budget bounds. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The oracle selected-count event can be chosen design-saturated. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Once the oracle candidate meets its deterministic mass and budget conditions, the logarithmic finite-family budget gives the desired event. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Log-budget specialization retaining design saturation. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At the oracle scale, expected counts at the effective dimension balance the inverse-squared smoothness threshold. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Oracle-scale lower mass and a dyadic width comparison imply the feasibility count threshold. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A candidate whose width is above a fixed multiple of the oracle width has enough expected treated observations in every template microcell. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A positive lower bound for the model's mass coefficient is enough for the oracle-candidate count lower bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The model mass inequality discharges the oracle witness mass premise in the finite-family count event. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The common conclusion of the design-saturated selected-count wrappers. For the stated inputs and conditions, the SaturatedSelectedCountEvent object being defined.
Definition (Lean source)
Oracle-candidate specialization retaining the saturated event. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The oracle-candidate event accepts any positive uniform lower bound for the model's overlap-mass coefficient. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Positive-coefficient oracle specialization retaining saturation. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Feasibility and the selected count event give both variance scales for a single treated microcell. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The selected-count event controls the sum of inverse counts in a cube. This is the design-dependent factor in every coefficient variance proxy. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Insert an ordered-mass lower bound into the inverse-count variance factor. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The finest dyadic candidate width eventually lies below any fixed multiple of the oracle width when the effective dimension is strictly larger. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Effective dimension decreases as the overlap-tail exponent increases. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Over a compact overlap range, every oracle width lies between the two endpoint oracle widths. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
One selected-count constant and one sample-size threshold work uniformly over the compact overlap-exponent range. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Uniform selected-count control with an explicitly design-saturated event. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Fixed-overlap selected-count control with an explicitly design-saturated event. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.SelectedMesh.Counts.Asymptotics 7 declarations Elementary asymptotic budgets for selected counts
Elementary asymptotic budgets for selected counts
Every positive power eventually pays for a fixed multiple of the logarithmic simultaneous-count budget. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A power also pays for an affine logarithmic union-bound budget. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A faster decaying power eventually lies below any fixed multiple of a slower decaying one. This places the oracle width above the finest candidate width when the effective dimension exceeds the ordinary dimension. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A fixed multiple of a negative power is eventually at most one. This places a fixed enlargement of the oracle width below the coarsest mesh. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A positive fixed fraction of a power eventually pays for an affine logarithmic budget. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Choose a single oracle enlargement large enough for the effective dimension mass inequality. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At an oracle-order width, the inverse-squared smoothness threshold eventually dominates any affine logarithmic count budget. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.SelectedMesh.Counts.Base 17 declarations Simultaneous treated-count event for the selected mesh
Simultaneous treated-count event for the selected mesh
A full-sample event depends only on the covariates and treatment arms. For the stated inputs and conditions, the CountDesignSaturated object being defined.
The treated microcell count is the sum of its Bernoulli indicators. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The treated microcell indicator is measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Each treated microcell count is measurable on the finite product sample. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Bernstein deviation for a Bernoulli count on the finite product law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The one-observation treated microcell indicator has the population cell mass as mean. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Bernstein deviation for one treated microcell count. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A deviation threshold linear in the mean and the logarithmic budget. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
One design-measurable event controls any finite collection of treated microcell counts, including cells taken from different candidate meshes. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The explicit simultaneous count event can be chosen saturated with respect to the complete covariate-and-treatment design. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A feasible count that exceeds the uniform deviation threshold also controls its population mean from below. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On a feasible mesh, a uniform count deviation yields the selected-cell population lower bound once the feasibility threshold dominates the tail budget. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
An oracle-scale candidate is feasible when every expected treated count dominates its feasibility threshold and the simultaneous deviation budget. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A feasible oracle-scale witness and simultaneous count deviations imply the selected mesh and selected-cell count bounds. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The density floor and global propensity tail give a quantitative lower bound for each treated template microcell. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every template microcell has positive treated mass under the model's density floor and global propensity-tail condition. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Express the model's treated microcell lower bound as a coefficient times the effective-dimension power of the dyadic width. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.SelectedMesh.Counts.Budget 6 declarations Finite-family count budget for selected meshes
Finite-family count budget for selected meshes
The number of candidate treated microcells is the geometric count of dyadic cubes times the fixed number of template cells. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A finite candidate-family bound for setting the simultaneous deviation budget. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A logarithmic budget pays for the full finite family of candidate cells and leaves an inverse-square failure probability. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The largest candidate dyadic denominator is at most the sample size. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The simultaneous-count family has a polynomial size bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The logarithm of the count family grows at most as an affine log sample size. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.SelectedMesh.Fibre 20 declarations Conditional selected-mesh coefficient fibres
Conditional selected-mesh coefficient fibres
Treatment and covariate coordinates of a sample. For the stated inputs and conditions, the sampleDesign object being defined.
The treated outcome residual on a fixed complete-design fibre, extended by zero on untreated coordinates. For the stated inputs and conditions, the conditionalTreatedResidual object being defined.
Definition (Lean source)
Replace each response by its treated conditional mean, with an arbitrary zero value on untreated coordinates. For the stated inputs and conditions, the conditionalMeanSample object being defined.
Definition (Lean source)
For the stated dimensions, the complete vector of covariates and treatment arms is measurable.
Formal statement
Proof (Lean source)
The treated residual condition holds at every coordinate of an IID sample. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The iid observation law disintegrates over the complete treatment and covariate design as a product of one-observation outcome kernels. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Given the complete design, the outcome vector has the product of the one-observation conditional outcome laws. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The conditional complete-sample law sends its response vector to the product of the one-observation response kernels. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Under the complete-design conditional law, each response coordinate has the corresponding one-observation conditional response law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On almost every fixed-design fibre, every treated response residual has the one-observation exponential integrability and MGF bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Conditional on the design, the response coordinates are independent. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Almost every complete-design fibre carries independent residual coordinates with the original uniform exponential-moment bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every fixed-design residual coordinate is integrable and has mean zero under almost every conditional sample law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Conditional on the observed design, the complete sample has that design almost surely. This supplies the fibre hypothesis for the coefficient identity below. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A fibre of the design map has a fixed Gram matrix; its coefficient variation is exactly the inverse Gram applied to the response variation. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On a fixed design fibre, one coefficient coordinate is a finite weighted sum of the treated response residuals. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On a design fibre, the coefficient difference is the weighted sum of outcome differences, with all weights fixed by the conditioning design. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On a complete-design fibre, subtracting the fitted coefficient at the conditional-mean sample leaves exactly the weighted residual sum. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Conditional centre of one fitted coefficient given all designs and arms. For the stated inputs and conditions, the conditionalCoefCentre object being defined.
The conditional coefficient centre is the fitted coefficient obtained by replacing treated responses with their conditional means. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.SelectedMesh.MGF 3 declarations Finite conditional sub-Gaussian sums
Finite conditional sub-Gaussian sums
Independent centred residuals with coordinatewise Gaussian MGF bounds retain the sum of their variance proxies under a finite weighted sum. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Fixed design weights turn a common residual proxy into the squared-weight proxy used by the selected coefficient bounds. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Exponential integrability is preserved under the same finite weighted sum, so the maximal inequality can use the coefficient MGF bounds. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.SelectedMesh.Maximal 24 declarations Ordered sub-Gaussian maximal inequality
Ordered sub-Gaussian maximal inequality
The logarithmic correction is absorbed by a positive power on the unit interval. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A fixed upper scale gives a uniform bound for the oracle logarithmic factor. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Convert a selected-width bound into the oracle-rate logarithmic envelope. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The final deterministic term in the selected-mesh envelope. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The stochastic coefficient scale is the oracle mesh raised to the smoothness plus half the effective dimension. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Dividing the stochastic scale by the bias scale leaves only the ratio between oracle and selected mesh widths. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A positive power in the maximal bound changes only the constant in its logarithmic factor. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A mass rank at least the ordered position gives the ordered variance proxy. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A uniform lower bound on the mass coefficient absorbs its reciprocal inside the two competing variance scales. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Normalize the ordered inverse-count proxy after bounding its mass coefficient uniformly on the adaptation interval. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The raw selected-mesh variance proxy has one constant for every ordered cube, including ties in the cube masses. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Convert a raw mass-rank MGF estimate into the common ordered proxy used by the scalar maximal inequality. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
One maximal constant works over a fixed compact exponent interval. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The maximum of the coefficient sup norms is bounded by the sum of the coordinatewise maxima. This lets a scalar maximal inequality handle the finite monomial index without changing its logarithmic scale. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Integrate the finite-coordinate reduction once the scalar maxima are integrable, as they are under the conditional sub-Gaussian bounds. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Exponential moments on both sides make a scalar coefficient integrable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The maximum of finitely many integrable scalar absolute values is integrable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
An integrable finite family has an integrable maximum absolute value. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Finite scalar maxima are integrable when all coordinates have two-sided exponential moments. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Coordinate exponential moments give the integrability conditions for a finite maximum of coefficient sup norms. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Apply the scalar ordered maximal theorem to every coefficient coordinate, then sum over the fixed finite monomial index. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The uniform vector maximal inequality with its integrability hypotheses deduced from the coordinate exponential moments. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Reindex the vector maximal inequality by a mass-ordered enumeration of a finite cube family. The maximum over cubes is unchanged by the enumeration. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The weak-overlap rank exponent stays in a fixed positive interval when the overlap exponent ranges over a compact interval. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.SelectedMesh.Measurability 24 declarations Measurability of the selected equal-cell estimator
Measurability of the selected equal-cell estimator
For a sample size, smoothness exponent, outcome bound, regression function, and realized sample, the real-valued equal-cell cube loss is the supremum, over cube points, of the estimator's absolute error.
Feasibility of a fixed mesh index is a measurable sample event. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Membership of a fixed index in the data-selected feasible set is measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The finite feasible-index set is a measurable function of the sample. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The selected mesh width is a measurable function of the finite sample. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A fixed sample coordinate falling in a fixed treated microcell is measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every coordinate of the equal-cell response moment is sample measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every coordinate of the equal-cell Gram matrix is sample measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A finite real matrix with measurable entries has measurable determinant. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every entry of the inverse of a finite measurable real matrix is measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every coordinate of the equal-cell fitted coefficient vector is measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
With the dyadic index fixed, the clipped equal-cell estimate is measurable in the sample. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At every fixed covariate point, the selected equal-cell estimate is measurable in the sample. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The supremum of pointwise measurable continuous ENNReal sections over a second-countable space is measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Polynomial estimator formula with its dyadic index and cube fixed. For the stated inputs and conditions, the equalCellEstimatorAtCell object being defined.
Definition (Lean source)
At a fixed point and cell, the polynomial estimator formula is sample measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For a fixed sample and cell, the polynomial estimator formula is continuous in x. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Against a continuous target on the cube, the cube-supremum loss of the selected equal-cell estimator is sample measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A Holder representative supplies the continuity premise required by the sample-measurability theorem for the cube-supremum loss. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The selected-estimator cube loss against a model Holder response is almost-everywhere measurable under any sample law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Integrate fibrewise good-event and global bounds without changing the event used for conditioning. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.SelectedMesh.Rank 13 declarations Selected-mesh mass ranks and coefficient proxies
Selected-mesh mass ranks and coefficient proxies
Rank by weakest-cell mass; ties receive their largest available rank. For the stated inputs and conditions, the cubeMassRank object being defined.
Mass ranks respect the order of cube masses, including tied masses. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Each cube contributes itself to its mass rank. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
An injective list of cubes in increasing mass order has at least its position in the mass rank. This is the index conversion for the ordered maximal inequality. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Enumerate all cubes in nondecreasing weakest-cell mass, breaking ties by an arbitrary fixed finite index. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The rank counting all cubes with mass no larger than a given cube gives that cube the same ordered lower bound, including when masses tie. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The concrete mass-rank profile for any observed law in the model class. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Feasibility and the selected event give the ordered inverse-count factor with the model's explicit mass constant. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On the selected count event, the coefficient weights have both the feasibility and ordered-mass variance scales. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The equal-cell conditioning theorem supplies the uniform row constant in the ordered squared-weight bound; no separate row assumption is needed. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Once the outcome residuals are independent under the fixed-design law, the selected count event gives both ordered coefficient MGF proxies. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On almost every complete-design fibre, a coefficient centred by its conditional integral obeys the selected ordered mass-rank MGF bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The centered coefficient has every exponential moment on almost every complete-design fibre. This supplies the integrability premise of the ordered maximal inequality separately from its MGF upper bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.Template 35 declarations This file defines the empirical equal-cell Gram matrix and estimator, then derives deterministic conditioning from the tensor-template geometry.
Count-adaptive equal-cell estimator
This file defines the empirical equal-cell Gram matrix and estimator, then derives deterministic conditioning from the tensor-template geometry.
Largest dyadic index permitted by the sample size. For the stated inputs and conditions, the maxMeshIndex object being defined.
Finite set of candidate dyadic mesh indices. For the stated inputs and conditions, the meshIndices object being defined.
Definition (Lean source)
Width at dyadic index j. For the stated inputs and conditions, the meshWidth object being defined.
Definition (Lean source)
Dyadic cube index of a point, capped at the last cube. For the stated inputs and conditions, the cubeIndex object being defined.
Lower-left corner of a dyadic cube. For the stated inputs and conditions, the cubeCorner object being defined.
Half-open dyadic cube with the global right boundary included. For the stated inputs and conditions, the dyadicCube object being defined.
Definition (Lean source)
Scaled microcell in a macro-cube. For the stated inputs and conditions, the scaledMicroCell object being defined.
Treated observations in one microcell. For the stated inputs and conditions, the treatedCount object being defined.
Total inverse-count weight assigned to one template cell. For the stated inputs and conditions, the treatedCellWeightSum object being defined.
Definition (Lean source)
When a template cell is occupied, its inverse-count observation weights sum to one. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Mesh passes every cell-count threshold. For the stated inputs and conditions, the meshFeasible object being defined.
Feasible dyadic indices. For the stated inputs and conditions, the feasibleIndices object being defined.
Definition (Lean source)
Numerically smallest feasible width, or zero when no mesh is feasible. For the stated inputs and conditions, the countSelectedMesh object being defined.
Definition (Lean source)
Equal-cell empirical Gram matrix. For the stated inputs and conditions, the gramHat object being defined.
Definition (Lean source)
Equal-cell weighting preserves symmetry of the empirical Gram matrix. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Equal-cell average of squared polynomial evaluations. For the stated inputs and conditions, the gramHatSquareAvg object being defined.
Definition (Lean source)
The empirical equal-cell Gram quadratic form is an average of squares. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every equal-cell empirical Gram matrix has a nonnegative quadratic form. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Equal-cell weighting preserves any lower bound that holds at every treated observation in each occupied template cell. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A uniform pointwise squared-evaluation error transfers through equal-cell weighting to a Gram quadratic-form error. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Within a template microcube, the squared polynomial evaluation differs from its node value by at most the template Lipschitz radius times the squared coefficient norm. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Equal-cell empirical response moment. For the stated inputs and conditions, the responseMoment object being defined.
Definition (Lean source)
Local polynomial coefficient vector. For the stated inputs and conditions, the coefHat object being defined.
Count-adaptive, clipped equal-cell local polynomial estimator. For the stated inputs and conditions, the equalCellEstimator object being defined.
Definition (Lean source)
Population treated microcell mass. For the stated inputs and conditions, the microcellMass object being defined.
Definition (Lean source)
Minimum microcell mass in a macro-cube. For the stated inputs and conditions, the cubeMass object being defined.
Definition (Lean source)
Sorted weakest-cell masses. For the stated inputs and conditions, the orderedCubeMass object being defined.
Expected pointwise loss for a measurable estimator and one model law. For the stated inputs and conditions, the pointwiseLossRisk object being defined.
Definition (Lean source)
Pointwise minimax risk with extended nonnegative loss. For the stated inputs and conditions, the pointwiseRisk object being defined.
Definition (Lean source)
Expected spatial-supremum loss for one model law. For the stated inputs and conditions, the supLossRisk object being defined.
Definition (Lean source)
Expected supremum minimax risk with extended nonnegative loss. For the stated inputs and conditions, the supremumRisk object being defined.
Definition (Lean source)
A strictly positive quadratic lower bound makes a finite Gram matrix invertible. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A positive quadratic lower bound controls the Euclidean norm of the inverse. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Unisolvence and distribution-free equal-cell Gram conditioning. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A feasible candidate mesh has the uniform equal-cell Gram conditioning asserted in the paper. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.TemplateAlgebra 21 declarations Causalean.Stat.Nonparametric.designMatrix is univariate and designMatrix_inv_concentration concerns random Gram concentration.
Tensor-template algebra and finite Euclidean norms
Causalean.Stat.Nonparametric.designMatrix is univariate and
designMatrix_inv_concentration concerns random Gram concentration. This file
constructs the explicit multivariate tensor template, proves unisolvence, and
develops the finite Euclidean norm bounds used for Gram perturbations.
Total-degree multiindices. For the stated inputs and conditions, the monoIdx object being defined.
For the dimension and degree bound, the monomial-index type collects precisely the multiindices whose total degree does not exceed that bound.
Vector of all total-degree monomials. For the stated inputs and conditions, the monoVec object being defined.
Number of tensor nodes. For the stated inputs and conditions, the tensorCount object being defined.
Definition (Lean source)
Tensor interpolation node. For the stated inputs and conditions, the tensorNode object being defined.
A polynomial of coordinatewise degree at most m that vanishes on every template node is zero. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Equal-weight monomial Gram matrix. For the stated inputs and conditions, the templateGram object being defined.
Definition (Lean source)
The deterministic tensor template Gram matrix is symmetric. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The tensor Gram quadratic form is the mean of squared polynomial evaluations. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The tensor Gram matrix is positive semidefinite. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
One nonzero tensor-node evaluation makes the Gram quadratic form positive. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Euclidean norm of a finite real vector. For the stated inputs and conditions, the finiteL2Norm object being defined.
The square of the finite Euclidean norm is the sum of coordinate squares. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A finite vector has positive Euclidean norm exactly when it is nonzero. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A unit finite vector has a nonzero coordinate. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Tensor-grid unisolvence makes the Gram quadratic form positive on unit vectors. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Euclidean operator norm of a finite real matrix. For the stated inputs and conditions, the finiteL2OpNorm object being defined.
The finite Euclidean operator norm is nonnegative. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The custom finite Euclidean operator norm is bounded by Mathlib's matrix ℓ² operator norm. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The custom finite operator norm bounds its action on every vector. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A real square-matrix quadratic form is bounded above by its finite Euclidean operator norm times the squared coefficient norm. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.TemplateGeometry 16 declarations This file proves the spectral gap and Lipschitz control for the deterministic tensor template and defines the contained template microcubes.
Template spectral and microcube geometry
This file proves the spectral gap and Lipschitz control for the deterministic tensor template and defines the contained template microcubes.
Rayleigh-quotient least eigenvalue. For the stated inputs and conditions, the templateLambda object being defined.
Definition (Lean source)
Compactness of the finite unit sphere makes strict Gram positivity uniform. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The template Rayleigh infimum bounds every unit-vector quadratic form. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The least template Rayleigh quotient controls every coefficient vector. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Lipschitz quotient of the matrix-valued polynomial basis on the cube. For the stated inputs and conditions, the templateLip object being defined.
Definition (Lean source)
The polynomial outer-product difference quotients on the compact cube are bounded above. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
templateLip bounds each nontrivial outer-product difference quotient on the cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every matrix difference quotient in the template Lipschitz radius is nonnegative. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Template microcell width. For the stated inputs and conditions, the templateEta object being defined.
Definition (Lean source)
The fixed template cells have strictly positive width. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The chosen microcell radius fits inside half the template spectral gap. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Closed microcube around a tensor node. For the stated inputs and conditions, the microCube object being defined.
Definition (Lean source)
Membership in a template microcube gives the norm bound used by Gram perturbation. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every tensor interpolation node lies in the unit cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every template microcube is contained in the unit cube. For the stated inputs and conditions, the asserted conclusion holds.
Proof (Lean source)
The fixed finite family of unisolvent template microcubes. For the stated inputs and conditions, the EqualCellTemplate object being defined.
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.Helpers.Witnesses 48 declarations The three cited logical claims are explicit proposition-valued inputs.
Thin-strip and radial testing constructions, and cited gates
The three cited logical claims are explicit proposition-valued inputs. Dorn,
Minimax Rates Under Global Overlap Bounds (2026), Assumptions 1–2, fixes the
remaining model recorded by DornRemainingClassSpec; Assumption 3 and
Theorem 1 are recorded separately by DornSourceRateTranscription. Gaïffas,
Convergence Rates for Pointwise Curve Estimation with a Degenerate Design
(2005), arXiv:math/0410354, Eq. (2.1), Definition 2, Assumption M and
Theorem 1, is the scope of
GaiffasDegenerateDesignRate.
A Bernoulli law, extended definitionally to all real parameters. For the stated inputs and conditions, the realBernoulli object being defined.
A valid Bernoulli parameter gives a probability measure. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The law of B times a Bernoulli draw. For the stated inputs and conditions, the scaledBernoulli object being defined.
Definition (Lean source)
Scaling a Bernoulli outcome preserves its total probability. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every scaled Bernoulli outcome lies at one of its two endpoints. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Cube-centre radial coordinate. For the stated inputs and conditions, the centreRadius object being defined.
Definition (Lean source)
CDF of the centre radius on the unit cube. For the stated inputs and conditions, the centreRadiusCDF object being defined.
Definition (Lean source)
The thin strip through the cube centre. For the stated inputs and conditions, the thinStrip object being defined.
Thin-strip propensity. For the stated inputs and conditions, the stripPropensity object being defined.
Definition (Lean source)
Kernel giving (A,Y0,Y1,Y) at fixed covariate x. For the stated inputs and conditions, the completionAt object being defined.
Definition (Lean source)
Valid treatment and outcome probabilities give a causal probability kernel. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The fixed-covariate completion records the selected potential outcome. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The fixed-covariate completion retains its input covariate. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Integrating valid fixed-covariate completions preserves the base law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Mixing fixed-covariate completions preserves outcome consistency. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Both potential outcomes in a Bernoulli completion lie at its two endpoints. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Mixing valid Bernoulli completions retains the endpoint support of both potential outcomes. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Common bounded Bernoulli response success probability. For the stated inputs and conditions, the baselineSuccess object being defined.
Definition (Lean source)
Causal completion of the thin-strip law. For the stated inputs and conditions, the thinStripCompletion object being defined.
Definition (Lean source)
Observed thin-strip law on its stated exponent domain. For the stated inputs and conditions, the thinStripLaw object being defined.
Definition (Lean source)
Cube-truncated radial CDF around any point, including boundary points. For the stated inputs and conditions, the radialCDF object being defined.
Radial propensity for the Bernoulli testing experiment. For the stated inputs and conditions, the radialPropensity object being defined.
The radial treatment probability is a measurable covariate function. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Explicit smooth product bump supported on the closed sup-norm unit box. For the stated inputs and conditions, the smoothBump object being defined.
Treated Bernoulli success parameter for one testing law. For the stated inputs and conditions, the pairSuccess object being defined.
Definition (Lean source)
Both Bernoulli response probabilities are measurable, including at the boundary of the bump support. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The positive pair constants for which every Bernoulli parameter is in [0,1] on the cube at every positive sample size. The measure construction below remains total even outside this probability-law domain. For the stated inputs and conditions, the boundedLowerPairAdmissible object being defined.
Definition (Lean source)
Completion for one law in the bounded radial testing pair. For the stated inputs and conditions, the lowerPairCompletion object being defined.
Definition (Lean source)
Totalized observed bounded Bernoulli testing pair for every positive a,c. On boundedLowerPairAdmissible, all three Bernoulli parameters lie in [0,1] for every n ≥ 1 and every covariate in the cube. For the stated inputs and conditions, the boundedLowerPair object being defined.
Definition (Lean source)
Descriptive, nonassertive adaptation proposal. It defines no estimator, comparison rule, envelope functional, existence claim, or risk theorem. the jointAdaptationHandle object being defined.
Definition (Lean source)
Open question, recorded as a nonassertive text carrier. the jointAdaptationQuestion object being defined.
Definition (Lean source)
Regular variation at zero from the right, on the positive-radius domain. For the stated inputs and conditions, the RegularlyVaryingAtZero object being defined.
Definition (Lean source)
Slow variation at zero from the right is regular variation of index zero. For the stated inputs and conditions, the SlowlyVaryingAtZero object being defined.
Definition (Lean source)
Gaussian random-design regression law with density on the real line. For the stated inputs and conditions, the gaiffasObservedLaw object being defined.
Local approximation class at the sample-size-dependent bandwidth. For the stated inputs and conditions, the gaiffasLocalClass object being defined.
Definition (Lean source)
Gaïffas's class Sigma_n = F_(h_n)(x₀,ω) ∩ U(α_n), on the measurable regression functions defining the Gaussian experiment. For the stated inputs and conditions, the gaiffasSigma object being defined.
Definition (Lean source)
Rooted pointwise L^p minimax risk in the fixed-design Gaussian experiment. For the stated inputs and conditions, the gaiffasPointwiseRisk object being defined.
Definition (Lean source)
Gaïffas (2005), Convergence Rates for Pointwise Curve Estimation with a Degenerate Design, arXiv:math/0410354, Eq. (2.1), Definition 2, Assumption M and Theorem 1 (2.4)–(2.5), with the positive, divergent approximation radii used by Proposition 6 for the lower bound. Radial density continuity is required only at positive radii, so a singularity at the target point is allowed. This is the rooted L^p risk on the sample-size-dependent local approximation class in the univariate Gaussian experiment. Both the slowly varying rate and ω (hₙ n) have eventual two-sided risk bounds, with comparison constants depending only on s,b,p, not on σ. the GaiffasDegenerateDesignRate object being defined.
Definition (Lean source)
Conditional observed outcome distribution in arm a. For the stated inputs and conditions, the armKernel object being defined.
Definition (Lean source)
Dorn's Σ(β,L₀) controls only the highest coordinate derivatives on the closed source cube, using intrinsic traces. It imposes no bound on the function or its lower derivatives and selects no outside extension. For the stated inputs and conditions, the DornTopDerivativeSeminorm object being defined.
Definition (Lean source)
A measurable selected conditional propensity, strictly between zero and one almost surely. Assumptions 1–2 impose no pointwise range at null points. For the stated inputs and conditions, the DornA12SelectedPropensity object being defined.
Definition (Lean source)
An A3 selected version also meets the almost-sure A1/A2 requirements. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Dorn's Assumptions 1–2 without Assumption 3. Assumption 1(a)'s common conditional q-moment bound implies |μ₁| ≤ M; it is derived in the transfer, not imposed here. Assumption 1(b) is the variance bound, while the fixed Gaussian variance in Assumption 2 supplies Assumption 1(c). The Hölder condition is only Dorn's top-derivative seminorm, with no lower-derivative bound. The selected propensity is measurable and almost surely the conditional propensity in (0,1). For the stated inputs and conditions, the DornRemainingModel object being defined.
Definition (Lean source)
The exact remaining class in Dorn's Section 2 after Assumption 3 is deleted. Membership includes a probability law and every clause of Assumptions 1–2, with only the top-derivative Hölder seminorm. For the stated inputs and conditions, the DornRemainingClass object being defined.
Definition (Lean source)
For the dimension, regularity, moment, variance, tail constants, and candidate family, the Dorn Assumptions 1--2 family consists of laws satisfying nonemptiness and the per-law model conditions.
Definition (Lean source)
Dorn (2026), Minimax Rates Under Global Overlap Bounds, Section 2 Setting and Notation, Assumptions 1–2, author PDF pp. 3–7. The concrete DornA12Family records the source's fixed-constant family assumptions. The equivalence says that such a family is precisely an arbitrary nonempty subfamily of the maximal remaining-class envelope; it does not require the family itself to equal that envelope. For the stated inputs and conditions, the DornRemainingClassSpec object being defined.
Definition (Lean source)
Dorn's Assumption 3 with constants shared by the whole source family. For the stated inputs and conditions, the DornA3OnOriginalClass object being defined.
Definition (Lean source)
Dorn (2026), Minimax Rates Under Global Overlap Bounds, Section 2 Notation and Setting, Assumptions 1–3, Theorem 1(ii) (author PDF pp. 3–7, 12), Lemma 11 (p. 23), Lemma 13 (p. 24), and the proof (pp. 27–28). This source-scoped gate fixes one source family, its common constants including gamma, and its selected propensity representatives before selecting a measurable estimator and rate constants. Each displayed L∞(P_X) exceedance event is required to be measurable, so the upper probability comparison uses ordinary probability on the original Gaussian cube and the source's L∞(P_X) norm. The printed lower clause (i) is bibliographic attribution only: arbitrary singleton families obstruct it. The no-gamma sentence and count thresholds are construction provenance only. the DornSourceRateTranscription object being defined.
Definition (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.TAdaptiveMinimax 15 declarations Logarithm-free adaptive weak-overlap minimax rate
Logarithm-free adaptive weak-overlap minimax rate
Expected supremum risk of the concrete estimator at one law. For the stated inputs and conditions, the estimatorSupRisk object being defined.
Definition (Lean source)
The bounded-potential-outcome subclass used in the minimax converse. For the stated inputs and conditions, the boundedOutcomeClass object being defined.
Definition (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The exact completion payload exported by the lower-pair construction places either observed arm in the bounded-outcome subclass. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The selected-cell estimator has one expected supremum-risk constant over the entire compact overlap range. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A uniform bound for the concrete selected-cell estimator bounds the corresponding supremum minimax risk. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Clipping the selected-cell estimator gives a sample-size-independent upper bound for the supremum minimax risk. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Pointwise loss on the bounded-potential-outcome subclass. For the stated inputs and conditions, the boundedPointwiseLossRisk object being defined.
Definition (Lean source)
Pointwise minimax risk restricted to bounded potential outcomes. For the stated inputs and conditions, the boundedPointwiseRisk object being defined.
Definition (Lean source)
Restricting the model class to bounded potential outcomes can only reduce the pointwise minimax risk. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Evaluating a curve estimator at a point in the cube yields an admissible scalar estimator whose loss is bounded by its spatial supremum loss. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A pair in the bounded-outcome class with the standard KL budget gives an ENNReal pointwise minimax lower bound. Clipping arbitrary estimators makes the finite-L¹ Le Cam lemma applicable without an integrability assumption. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The explicit bounded Bernoulli pair gives the oracle-rate pointwise converse at every positive sample size. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
One count-selected estimator, whose type takes n,d,β,B and the data but no overlap exponent or class constants, achieves logarithm-free expected supremum risk uniformly on a compact overlap range. A bounded Bernoulli pair provides the pointwise minimax converse. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.TDornA3FreeCorollary 103 declarations Assumption-3-free upper bound on Dorn's remaining Gaussian model
Assumption-3-free upper bound on Dorn's remaining Gaussian model
Coordinatewise affine transformation from [-1,1]^d to [0,1]^d. For the stated inputs and conditions, the affineToCube object being defined.
Push an observed law from Dorn's cube to the unit cube. For the stated inputs and conditions, the transformedDornLaw object being defined.
Definition (Lean source)
Corresponding transformed treated-response curve. For the stated inputs and conditions, the transformedResponse object being defined.
The coordinate change used to transport Dorn's source cube is measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The displayed inverse coordinate change cancels affineToCube globally. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The inverse coordinate change from the unit cube to Dorn's cube is measurable on the whole ambient space. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The inverse coordinate change is also a right inverse of affineToCube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
An invertible measurable affine change of covariates generates exactly the same conditioning sigma algebra. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The global affine coordinate change as a measurable equivalence. For the stated inputs and conditions, the affineToCubeMeasurableEquiv object being defined.
Definition (Lean source)
Conditional independence is insensitive to replacing the conditioning measurable space by an equal one. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Conditional expectation is unchanged when its conditioning measurable space is replaced by an equal one. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Pulling a response to the unit cube and evaluating at the transported point recovers the original response exactly. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The affine coordinate change identifies Dorn's source cube with the unit cube used by the causal model. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The covariate marginal of the transported observed law is the pushforward of the original marginal by the affine coordinate change. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The coordinatewise affine map has Jacobian factor 2⁻ᵈ and hence its pushforward multiplies ambient volume by 2ᵈ. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Normalized volume on Dorn's cube pushes forward exactly to unit-cube volume under the coordinatewise affine map. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A Dorn law with normalized uniform covariates transports to exact uniform volume on the unit cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Exact transported uniform covariates supply cube support, absolute continuity, and density lower bound one. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Affine transport reindexes the conditional treatment kernel by the covariate equivalence. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Affine transport reindexes both coordinates of the conditional outcome kernel and leaves its response law unchanged. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The global propensity tail is invariant under the affine covariate equivalence when the displayed propensity is pulled back by its inverse. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every observed law factors into its covariate marginal and the regular conditional treatment kernel. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Disintegrating an observed law over (X,A) and mapping the resulting product back through tuple reassociation recovers the original law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Any almost-everywhere versions of the treatment and response kernels may be substituted into the two-stage observed-law disintegration. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A probability law on Bool is determined by the real value of its mass at true. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A selected propensity in (0,1) identifies the entire Bool-valued conditional treatment law, rather than only its mass at true. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Gaussian arm-kernel identities holding for almost every covariate lift to the joint (X,A) law used by observed-law disintegration. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A positive selected propensity lets the joint affine outcome-kernel transport be specialized to the treated Gaussian arm. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A Gaussian with standard deviation bounded by B satisfies the model's centered MGF envelope with scale B. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Transported Gaussian treated kernels give the bounded-mean and sub-Gaussian residual field once their means and standard deviation are bounded by the model scale. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Affine transport preserves the probability-law instance. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Gaussian specialization of the two-stage recomposition theorem. The two almost-everywhere hypotheses are exactly the propensity and arm-kernel identifications supplied by a Dorn remaining-model witness. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The displayed selected propensity and Dorn's two Gaussian arm identities jointly determine the full observed law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Gaussian completion at covariate x with independent potential outcomes. For the stated inputs and conditions, the gaussianCompletionAt object being defined.
Definition (Lean source)
Gaussian completion is a measurable measure-valued map whenever its propensity and the two arm means are measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The measurable Gaussian completion family, packaged as a kernel. For the stated inputs and conditions, the gaussianCompletionKernel object being defined.
Definition (Lean source)
Every fixed Gaussian product fibre records the selected potential outcome. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Mixing measurable Gaussian product fibres preserves outcome consistency. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A pair of Gaussian laws with measurable means is measure-valued measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At fixed covariates, Gaussian potential outcomes and treatment factor. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Mixing the fixed Gaussian factorization preserves its conditional product. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Covariate almost-everywhere propensity validity suffices for a Gaussian completion bind to retain its base covariate law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The Bernoulli parameter used by a Gaussian completion is a propensity version of its observed law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A globally valid representative of a real-valued propensity. For the stated inputs and conditions, the gaussianPropensityClamp object being defined.
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
If a real number and its unit-interval certificate are given, clamping that number to the unit interval leaves it unchanged.
Formal statement
Proof (Lean source)
If a propensity is valid on the base law almost everywhere, clamping it globally does not change the Gaussian completion bind. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Independent Gaussian potential-outcome fibres make treatment conditionally independent of the potential outcomes given covariates. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Translating a centred Gaussian bounds its first absolute moment by the absolute mean plus the centred first absolute moment. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
An integrable Gaussian mean over a finite base law makes the treated potential outcome integrable under the completion bind. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Once integrability is supplied, the Gaussian treated-arm mean is the conditional treated-potential response of the product completion. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Practical Gaussian Holder-response assembly from an integrable mean. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The conditional-mean component of the Gaussian completion, separated from any regularity property of its representative. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Changing only the covariate coordinate preserves consistency. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
An invertible measurable affine change of the covariate coordinate preserves conditional exchangeability. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Affine covariate transport preserves the treated-potential conditional mean identity, independently of the chosen regularity representative. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
An affine covariate pushforward transports a potential-outcome conditional mean once the transformed representative has the requested Holder bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated dimension, Gaussian scale, response functions, measurability certificates, and covariate, the Gaussian completion kernel evaluates to the corresponding pointwise completion.
Formal statement
Proof (Lean source)
At fixed covariates, observing the independent Gaussian completion selects the Gaussian response belonging to the realized treatment arm. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Fixed-covariate Gaussian completion agrees with a treatment Bernoulli followed by the selected Gaussian arm kernel. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Binding the Gaussian completion over a covariate law produces the usual two-stage treatment and selected-arm Gaussian observed law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The observed response kernel of a Gaussian completion is the selected Gaussian arm kernel. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The Gaussian completion reconstructed from a selected propensity and the two Gaussian arm kernels has exactly the original observed law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Affinely transporting the covariate coordinate of the reconstructed Gaussian completion gives exactly the transported observed law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Gaussianized thin-strip completion, rescaled to Dorn's cube. For the stated inputs and conditions, the gaussianThinStripOriginal object being defined.
Definition (Lean source)
Original-cube version of the capped thin-strip propensity. For the stated inputs and conditions, the gaussianStripPropensity object being defined.
Definition (Lean source)
The inverse affine map sends unit-cube volume to normalized volume on Dorn's cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Affine normalization cancels the inverse affine map in the definition of the original-cube Gaussian strip law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The capped inverse-affine strip is a valid selected propensity on Dorn's cube, including strict almost-sure overlap. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
An almost-sure Bernoulli property holds at false when the failure mass is positive. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Both conditional response arms of the inverse-affine Gaussian strip law are the centred Gaussian used in its completion. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Capping the strip propensity at 3/4 preserves a polynomial lower-tail bound, with the fixed loss contributed only by levels above the cap. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The inverse-affine capped strip has the same global propensity tail as its unit-cube representative. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every centred real Gaussian has a finite q moment; enlarging its moment integral produces the exact positive radius required by Dorn's model. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The inverse cube affine map scales Euclidean balls by exactly two. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Dorn's local ratio condition is invariant under the coordinatewise affine similarity between the source cube and the unit cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Capping the thin-strip propensity at 3/4 does not repair A3. On the shrinking balls used in the obstruction the uncapped propensity is already strictly below the cap. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The capped Gaussian strip violates Dorn A3 on the original source cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The full coordinatewise Hölder radius of a response on the unit cube. For the stated inputs and conditions, the holderFullNorm object being defined.
One radius for every transformed member of Dorn's seminorm class with the common response bound obtained from Assumption 1. For the stated inputs and conditions, the dornCommonRadius object being defined.
Definition (Lean source)
Fixed-cube interpolation constant: its inputs are only dimension and smoothness, with all admissible amplitude and seminorm pairs normalized out. For the stated inputs and conditions, the dornInterpolationConstant object being defined.
Definition (Lean source)
The infimum defining holderFullNorm is attained. Each defining inequality is closed in its radius, so it may be passed to the infimum pointwise. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Increasing the common radius preserves the intrinsic Holder ball. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A Holder response may be replaced by a representative agreeing on the cube when the completion covariate is supported there. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every admissible Hölder radius bounds the value at a point of the cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Constant responses satisfy Dorn's top-order seminorm condition. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Under Dorn's normalized cube design, the stated pulled-back L∞ loss is bounded by the pointwise cube supremum used in dornTransformedSupRisk. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Markov's inequality converts an expected ENNReal loss bound into the corresponding real probability bound at the rescaled rate. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Enlarging the numerical tail constant preserves membership in the causal model class. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Expected supremum loss of the transformed estimator against Dorn's designated Gaussian response, with no model-membership premise. For the stated inputs and conditions, the dornTransformedSupRisk object being defined.
Definition (Lean source)
Once affine transport has supplied a causal-model witness with the transported response, the Dorn risk is exactly the model-class estimator risk. This isolates the chosen-representative issue from the Gaussian construction. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The Gaussian arm clause identifies its conditional mean with the designated response. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Conditional on the disclosed Dorn remaining-class scope, every law in the remaining uniform Gaussian Hölder model transfers to the global-tail causal class and inherits the expected-supremum rate; Markov gives the published uniform-probability criterion. The strict Gaussian strip uses witness constants selected separately for each γ, independent of the fixed upper-rate tuple. The common response bound comes from Dorn's conditional moment clause, and the full Hölder radius comes from fixed-cube interpolation of his top-derivative seminorm. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_WeakoverlapUnisolventRate_Research.TStrictEnlargement 104 declarations The global-tail class strictly contains laws excluded by Dorn A3
The global-tail class strictly contains laws excluded by Dorn A3
The common Bernoulli response is admissible for both the outcome and Hölder-radius envelopes. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The strip used in the treatment kernel is Borel measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The displayed propensity is a measurable function of the covariates. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A pointwise-valid Bernoulli completion is a measurable measure-valued kernel when its three success probabilities are measurable. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At a fixed covariate, a treated covariate event has Bernoulli mass e x. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At fixed covariate x, the (X,A) marginal is the product of the point mass at x and the displayed Bernoulli treatment law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The joint (X,A) law of a completion bind is the covariate law composed with its explicit Bernoulli treatment kernel. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The displayed Bernoulli parameter is a version of the propensity of the observed completion law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
When the two response arms have the same Bernoulli law, selecting the observed response leaves that law independent of the treatment draw. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Mixing the equal-arm fixed-covariate identity gives the joint observed law as the composition-product of the (X,A) law and its response kernel. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The conditional observed-response kernel in the equal-arm completion is the displayed scaled Bernoulli kernel. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
An almost-sure Bernoulli property holds at true when its success mass is positive. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Positive treatment mass promotes the equal-arm response-kernel identity to the treated fibre over almost every covariate. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The mean of the scaled Bernoulli law is its scale times its success probability. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The treated regression of the equal-arm completion is B * p. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A [0,B]-valued scaled Bernoulli variable satisfies the model's looser B² centered MGF envelope. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Equal bounded Bernoulli arms satisfy the model's treated mean and sub-Gaussian residual condition. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At fixed covariates, the potential-outcome pair and treatment factor as the product used by the completion construction. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Mixing the fixed-covariate factorization preserves the conditional product of the potential-outcome pair and treatment. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The product completion makes its treatment conditionally independent of the potential-outcome pair given the covariates. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Integrating a nonnegative covariate function over treated observations of a completion bind weights the base covariate law by the displayed propensity. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Bochner-integral form of completionBind_observed_treated_setLIntegral. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The thin-strip treatment probability is a valid Bernoulli parameter. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The strip component supplies a fixed positive treated mass. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The strip bump raises propensity by at most one quarter. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The strip adjustment only increases the radial propensity. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every low-propensity event lies inside the corresponding radial event. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A propensity sublevel is contained in the corresponding radial CDF sublevel. This is the event inclusion behind the exact global tail bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The thin strip carries a fixed treatment probability at its centre. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Outside the strip, the propensity is exactly its radial component. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The radial treatment probability on a small cube is bounded by its outer radius. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At a sufficiently small radius, a propensity level above a quarter-scale threshold can occur only inside the thin strip. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Every ball centered at the strip center has propensity supremum at least one quarter. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The centre also witnesses the quarter lower bound when the local ball is restricted to the covariate cube, as in Dorn's A3. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A sufficiently small radial bound confines Dorn's local superlevel event to the thin strip, for every proposed A3 level ρ. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A vanishing local fraction of the strip defeats every proposed numerical anti-concentration triple. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Dorn's full A3 property implies its numerical anti-concentration clause. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Failure of the numerical anti-concentration clause rules out full Dorn A3. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The off-strip radial propensity bound vanishes as the neighborhood shrinks. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A neighborhood can be chosen below both a proposed A3 radius and its superlevel threshold. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
In a centered cube, the strip's transverse coordinate has width h ^ a. This is the geometric bound used for its vanishing local mass and second moment. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The same transverse-width bound holds in a centered Euclidean ball. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A one-sided product box inside the thin strip. Its first coordinate is kept away from the centre so the transverse width has a uniform lower scale. For the stated inputs and conditions, the thinStripCoreBox object being defined.
For a small positive radius, the core box lies in both the strip and the centered Euclidean ball. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The core box has one transverse side of length 2 r^a and d-1 ordinary sides of length r, where r = h/(4d). For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The strip bump supplies treated mass of the sharp order h^a h^(d-1) on a centered ball. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A centered ball cuts the strip into a box with transverse half-width h ^ a. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The box estimate has one transverse factor 2 h^a and d-1 ordinary factors 2 h. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The normalized transverse second moment is uniformly small on the strip. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The radial treatment part contributes its small radius bound; the strip part contributes only its vanishing transverse width. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Pointwise split retaining the small strip volume for the transverse term. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Integrated numerator split, before inserting the two geometric volume bounds. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A centered Euclidean ball is contained in its coordinate box. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The numerator has the two sharp powers needed after division by treated mass. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The deterministic strip contribution to the normalized second moment vanishes. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The pointwise envelope for the normalized treated second moment vanishes. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A closed cube of radius r around the design centre has volume (2*r)^d. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A coordinate box of half-width h / d gives a quantitative lower bound for the uniform-cube mass of a centered Euclidean ball. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Under uniform cube volume, the strip occupies at most a constant times h^(a-1) of a sufficiently small centered ball. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The transverse exponent a > 1 makes the strip's fraction of centered balls vanish under uniform cube volume. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The sup-norm radius sublevel set is the centred coordinate cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The centred radial CDF has the stated elementary volume formula. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The thin strip inside a sup-norm ball has one side of width 2 h^a and d-1 sides of width 2 h. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The integrated pointwise split on the sup-norm event used by stripSecondMoment. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Quantitative numerator bound on the actual sup-norm event. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The core-box treated-mass lower bound transfers to the sup-norm event. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A centred radius at most one half stays in the covariate cube. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The uniform design assigns the centred radius sublevel its cube volume. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
On the support of the uniform cube design, the radial CDF has its unsaturated polynomial form. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The radius CDF evaluated at an interior radius has precisely its stated probability under the uniform covariate design. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The centre-radius CDF is uniform under the cube design, in the sublevel form needed for the thin-strip global tail argument. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The displayed thin-strip propensity obeys the sharp global tail bound under the uniform covariate design. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The causal thin-strip completion retains the uniform cube covariate law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The explicit completion is a probability measure. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The observed outcome coordinate is definitionally selected from the two potential outcomes in the explicit completion. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The observed thin-strip witness has the uniform cube covariate marginal. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The observed thin-strip witness is a probability law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Disintegration of the frozen treated second-moment numerator onto the uniform covariate law. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Disintegration of the denominator of stripSecondMoment. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The uniform thin-strip witness violates Dorn's numerical local mass condition. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The uniform thin-strip witness violates full Dorn A3 because it violates the numerical local mass condition. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Transfer the sharp strip tail bound from uniform cube volume to any observed law with that covariate marginal. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The selected strip propensity satisfies the numerical tail inequality for every admissible model coefficient. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Under the uniform design, the displayed propensity vanishes only on a null set, as follows from its sharp lower-tail bound. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
The sharp tail bound gives almost-everywhere positivity under uniform design. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
At fixed covariates, the covariate and treated potential outcome have the product law determined by the treated Bernoulli arm. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Mixing the fixed-covariate identity identifies the joint covariate and treated-potential-outcome law as a kernel product. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A constant response whose magnitude is at most the radius belongs to the paper's intrinsic Hölder ball. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
In an equal-arm completion with a constant Bernoulli success probability, the constant scaled mean is a Hölder representative of the treated potential outcome conditional mean. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
All fields of the thin-strip global-tail model other than the explicitly supplied Hölder response follow from the completion construction. For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
Treated-design second moment in the normalized second direction. For the stated inputs and conditions, the stripSecondMoment object being defined.
Definition (Lean source)
For the stated inputs and conditions, the asserted conclusion holds.
Formal statement
Proof (Lean source)
A centred thin-strip propensity satisfies the global tail bound, yet it fails Dorn's numerical anti-concentration clause even when propensity one is allowed. Its normalized treated design also loses its second direction. For the stated inputs and conditions, the asserted conclusion holds.