Formalization: Minimax Inference for Threshold Modified Treatment Policies with Continuous Treatments
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.
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Basic 67 declarations This cold Stage-2 scaffold defines the observed and full-data experiments, the modeling assumptions, model classes, rate objects, and minimax criteria used by the threshold-clamp frontier.
Threshold-clamp minimax frontier: shared formal world
This cold Stage-2 scaffold defines the observed and full-data experiments, the modeling assumptions, model classes, rate objects, and minimax criteria used by the threshold-clamp frontier. Proof obligations are split into the theorem and helper modules named in the formalization plan.
The Causalean survey found reusable i.i.d.-sample and minimax infrastructure,
but no continuous-treatment clamp world. Causalean.PO is intentionally
bypassed because its finite-regime potential-outcome carrier is at a different
abstraction from the continuum-indexed standard-Borel response process here.
Kallenberg (2002), Foundations of Modern Probability, second edition, Theorem 6.3 (conditional distribution), doi:10.1007/978-1-4757-4015-8.
Definition (Lean source)
Hoeffding (1963), “Probability inequalities for sums of bounded random variables”, Theorem 2 specialized to unit ranges and two tails, doi:10.1080/01621459.1963.10500830.
Definition (Lean source)
One observed unit O = (X,A,Y) in a finite-stratum continuous-treatment model.
Definition (Lean source)
The observation carrier inherits the product Borel structure.
Definition (Lean source)
A law and its law-pinned finite-stratum nuisance functions.
The lower-threshold modified-treatment policy d_delta(a) = max a delta.
Definition (Lean source)
Conditional mass collapsed to the threshold by the clamp.
The retained natural-course contribution above the threshold.
The observed-data clamp target.
Definition (Lean source)
The designated i-th observation in the canonical finite sample.
The designated observations are the canonical first n coordinate maps under the n-fold product law; they are independent and each has law P.
Definition (Lean source)
The declared conditional density is nonnegative and gives every finite-stratum conditional treatment probability.
Every stratum mass is the corresponding atom of the X marginal and is bounded below by pmin.
The two-sided polynomial density envelope, with no smoothness imposed on the treatment density.
The local-polynomial order: the greatest natural number strictly below beta, including the integer-order correction.
Definition (Lean source)
Continuous bounded regression, its conditional-expectation law tie, and the stated Taylor-remainder Hölder condition.
Definition (Lean source)
The finite-stratum clamp model, with exactly the four core member atoms.
Definition (Lean source)
@realizes A(a.s. range [0,1]) @realizes O(treatment coordinate supported on [0,1])
@realizes Y(a.s. range [0,1]) @realizes O(outcome coordinate supported on [0,1])
Standing declared-space constraints for the frontier constants.
Definition (Lean source)
Admissibility of the regime constants forces the number of strata to be at least one.
Formal statement
Proof (Lean source)
Admissibility of the regime constants forces the error level to be positive.
Formal statement
Proof (Lean source)
Admissibility of the regime constants forces the error level to be less than one half.
Formal statement
Proof (Lean source)
The conditional test multiplier on its declared core domain.
A deterministic threshold sequence stays in [0,deltaBar].
Definition (Lean source)
The information-balance crossing set.
Definition (Lean source)
First information-balance crossing, with the prescribed empty-set fallback.
Definition (Lean source)
Candidate regular-plus-atom estimation frontier.
Definition (Lean source)
Critical threshold scale.
Definition (Lean source)
Boundary-design scale.
Definition (Lean source)
The canonical product law of the observed sample.
Observed-sample point estimators.
Observed-sample confidence-set procedures.
An estimator is measurable with respect to the observed sample.
Definition (Lean source)
A confidence procedure has measurable ordered endpoints and returns exactly the corresponding closed interval.
Definition (Lean source)
Length of the convex hull of a real confidence set.
Extended-real interval length, used so non-integrable expected lengths are represented by ∞ rather than the junk value of the real Bochner integral.
Definition (Lean source)
Absolute-error risk of an observed-sample estimator under one law.
Definition (Lean source)
Minimax absolute-error risk over the clamp model.
Definition (Lean source)
Uniform coverage of a confidence procedure over the clamp model.
Definition (Lean source)
Minimax worst-case expected length among uniformly honest intervals.
Definition (Lean source)
A full-data law packages its own standard-Borel latent carrier, so different members of a full-data model class need not share a carrier. The observed-model restriction is deliberately imposed by the class predicates below, rather than by this carrier.
Definition (Lean source)
the canonical inst measurable space latent carrier instance is defined for the specified J input, the specified PF input.
Definition (Lean source)
the canonical inst standard borel space latent carrier instance is defined for the specified J input, the specified PF input.
Definition (Lean source)
the canonical inst nonempty latent carrier instance is defined for the specified J input, the specified PF input.
Definition (Lean source)
Simultaneous latent-response consistency outside one common null set.
Definition (Lean source)
The actual X=x marginal mass under a full-data law. This is computed from the observed marginal measure, which FullDataLaw.margin_eq pins to the (X,A,Y) projection of the full-data measure; it deliberately does not use the auxiliary ClampLaw.px field.
Definition (Lean source)
Finite-stratum conditional independence of treatment and latent response, written as the exact stratumwise product-moment factorization using the actual X-marginal mass.
Definition (Lean source)
Full-data conditional response mean in a finite stratum.
Definition (Lean source)
Continuity of the fiberwise structural response mean on the declared threshold range.
Definition (Lean source)
The full-data clamp-policy mean.
Definition (Lean source)
The structural full-data class. Each member carries its own latent carrier; the observed margin belongs to the fixed-Hölder model, and the three causal member conditions hold on that same package.
Definition (Lean source)
Absolute risk of an observed-sample estimator for one full-data law.
Definition (Lean source)
The pair (R_{n,F}^star, L_{n,F}^star) of full-data criteria, with expected length valued in ℝ≥0∞ so infinite expectations are preserved.
Definition (Lean source)
Declared design spaces for the continuity-only model, with no Hölder exponent or radius among its parameters.
Definition (Lean source)
Declared spaces for the continuity-only inference regime.
Definition (Lean source)
The continuity-only observed model: the three shared law conditions and existence of a continuous conditional-regression version on the threshold range, with no common modulus or Hölder radius.
Definition (Lean source)
The selected continuous conditional-regression version. Its uniqueness is proved separately from positivity of the treatment density.
Definition (Lean source)
The continuity-only observed clamp functional.
Definition (Lean source)
The continuity-only regular-plus-atom frontier.
Definition (Lean source)
Continuity-only full-data membership over the same law-specific latent carrier, differing from the fixed-Hölder class only in its observed margin.
Definition (Lean source)
The common observed-law fields used by the full-data identification bridge.
Definition (Lean source)
Forget the fixed-Hölder regression field when proving the causal bridge. The result uses the hP condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Forget the qualitative regression field when proving the causal bridge. The result uses the hP condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The causal assumptions together with precisely the common observed-law fields needed by the measure-factorization argument.
Definition (Lean source)
The common bridge view of a fixed-Hölder full-data member. The result uses the hPF condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The common bridge view of a continuity-only full-data member. The result uses the hPF condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Absolute risk for the continuity-only observed functional.
Definition (Lean source)
The four continuity-only observed and causal decision criteria, ordered as observed risk, observed length, causal risk, and causal length.
Definition (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.Bandwidth 9 declarations AsympSeq records the explicit eventual two-sided constant sandwich used by the paper.
Information-balance bandwidth regimes
AsympSeq records the explicit eventual two-sided constant sandwich used by
the paper. The theorem keeps the threshold sequence arbitrary.
Two positive constants eventually sandwich one nonnegative sequence by another.
Definition (Lean source)
Eventually the infimum in infoBandwidth is the unique positive information-balance root. The result uses the hbeta condition, the hkappa condition, the hdeltaBar condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The balance equation bounds its positive root above by the interior-scale closed form. The result uses the hn condition, the hd condition, the hh condition, the hp condition, the hk condition, the heq condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
When the root lies below the threshold, it is also bounded below by a fixed multiple of the interior scale. The result uses the hn condition, the hd condition, the hh condition, the hp condition, the hk condition, the hhd condition, the heq condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Above the edge scale, the interior closed-form scale is no larger than the threshold. The result uses the hn condition, the hd condition, the hp condition, the hk condition, the hed condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Every positive balance root is at most the edge scale. The result uses the hn condition, the hd condition, the hh condition, the hp condition, the hk condition, the heq condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Under an edge-scale upper bound on the threshold, a positive balance root is bounded below by a fixed multiple of that edge scale. The result uses the hn condition, the hd condition, the hh condition, the hp condition, the hk condition, the hD condition, the heq condition, the hde condition, the hhe condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The crossing bandwidth has the stated balance, effective count, and the two regimes separated by deltaEdge. This is the stated conclusion.
Formal statement
Proof (Lean source)
If the threshold is asymptotically above the design edge, the information bandwidth has the interior closed-form order. Unlike bandwidth_phases, this purely analytic projection does not require an otherwise unused model law. The result uses the hreg condition, the hdelta condition, the hfar condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.CausalBridgeIdentification 11 declarations This file turns the normalized-stratum product law into the conditional integral identity and the pathwise decomposition used by the two causal bridge theorems.
Identification identities for the causal clamp bridge
This file turns the normalized-stratum product law into the conditional integral identity and the pathwise decomposition used by the two causal bridge theorems.
A globally measurable extension of a structural response map from its declared unit-dose domain.
Definition (Lean source)
The structural-response extension is measurable. The result uses the hcons condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
On the unit dose interval, the measurable extension equals the original structural response. The result uses the hcons condition, the ha condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The full-data stratum conditional mean satisfies the same design-cell integral identity as the observed regression. The result uses the hPF condition, the hkappa condition, the hcplus condition, the hpmin condition, the hB condition, the hBunit condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A continuous regression times the polynomially bounded treatment density is integrable on the threshold interval. The result uses the hcond condition, the hthin condition, the hkappa condition, the hcplus condition, the hdelta condition, the hmu condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equality of all density-weighted cell integrals identifies two continuous regressions pointwise on the threshold interval. The result uses the hcond condition, the hthin condition, the hkappa condition, the hcminus condition, the hcplus condition, the hdelta condition, the hdeltaOne condition, the hcont₁ condition, the hcont₂ condition, the hint₁ condition, the hint₂ condition, the hint condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Set integrals of observed-coordinate functions agree under a full-data law and its observed margin. The result uses the hS condition, the hf condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Full-data and fixed-Hölder observed regressions agree pointwise on the declared threshold interval. The result uses the hPF condition, the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Full-data and continuity-only observed regressions agree pointwise on the declared threshold interval. The result uses the hPF condition, the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Simultaneous consistency gives the pathwise lower-clamp decomposition. The result uses the hcons condition, the hsupp condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The expectation of the clamped atom contribution is the finite-stratum sum of atom masses times full-data response means. The result uses the hPF condition, the hkappa condition, the hcplus condition, the hpmin condition, the hdeltaBarOne condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.CausalBridgeMeasure 7 declarations This module derives the normalized stratum product law and continuity of the full-data response mean used by the causal clamp bridge.
Conditional full-data stratum measure helpers
This module derives the normalized stratum product law and continuity of the full-data response mean used by the causal clamp bridge.
After restriction to a positive-mass stratum and normalization, treatment and the latent response coordinate are independent. The result uses the hexch condition, the hpx condition, the hmass condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The treatment marginal of the normalized full-data stratum is the declared conditional treatment law. The result uses the hmodel condition, the hkappa condition, the hcplus condition, the hpmin condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A bounded measurable function of treatment and the latent coordinate integrates by iterated integration under the normalized stratum law. The result uses the hmodel condition, the hexch condition, the hkappa condition, the hcplus condition, the hpmin condition, the hF condition, the hM condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The latent-coordinate integral under the normalized stratum law is the full-data response mean. The result uses the hmodel condition, the hpmin condition, the hcons condition, the ha condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Conditional L1 response distance bounds the distance between full-data response means. The result uses the hmodel condition, the hpmin condition, the hcons condition, the hs condition, the ht condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The full-data mean-continuity member is exactly continuity of the structural response mean on the declared threshold interval. The result uses the hcont condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Two continuous conditional-regression versions on the threshold interval coincide there under the positive polynomial treatment-density envelope. The result uses the hP condition, the hreg condition, the hcont₁ condition, the hcont₂ condition, the hver₁ condition, the hver₂ condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.ContinuityCriteriaLift 2 declarations Concrete transport of continuity-only decision criteria
Concrete transport of continuity-only decision criteria
Identification rewrites the causal risk of every observed-sample estimator as the corresponding continuity-only observed risk. The result uses the hreg condition, the hdelta condition, the hPF condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The paper's quantile lift and identification bridge instantiate the abstract transport interface without importing the later frontier theorem. The result uses the hreg condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.ContinuityCriteriaTransport 1 declarations Abstract transport of continuity-only decision criteria
Abstract transport of continuity-only decision criteria
Surjectivity of the observed-margin map and point identification of the causal target are sufficient to identify both continuity-only causal decision criteria with their observed counterparts. The result uses the hsurj condition, the htarget condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.ContinuityExpectedLength 3 declarations This file bounds the expected length of the two-block Hoeffding interval by its deterministic root-block radii and the polynomial threshold-mass envelope.
Expected length of the continuity-only interval
This file bounds the expected length of the two-block Hoeffding interval by its deterministic root-block radii and the polynomial threshold-mass envelope.
The continuity-only interval has length at most twice its displayed radius, before intersection with the outcome range. This is the stated conclusion.
Formal statement
Proof (Lean source)
Under a continuity-only model, the real expected interval length is bounded by the two deterministic Hoeffding radii, the atom-estimation noise, and the polynomial threshold-mass envelope. The result uses the hP condition, the hreg condition, the hdelta condition, the hcard1 condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The real expected-length bound upgrades to the extended-real convention used by the continuity-only minimax criterion. The result uses the hP condition, the hreg condition, the hdelta condition, the hcard1 condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.ContinuityLengthLower 5 declarations Two-point lower bounds for continuity-only honest confidence length
Two-point lower bounds for continuity-only honest confidence length
A close pair in the continuity-only model lower-bounds minimax honest expected interval length. The result uses the hP0 condition, the hP1 condition, the hgap condition, the hsep condition, the hac condition, the hint condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A numerical upper bound on the product chi-square divergence gives a corresponding explicit honest-length lower bound. The result uses the hP0 condition, the hP1 condition, the hgap condition, the hsep condition, the hac condition, the hint condition, the hchi0 condition, the hchi condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The continuity-only minimax honest length has the regular root-sample-size lower bound, uniformly over threshold sequences. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Narrow continuous bumps give an atom-scale lower bound for continuity-only minimax honest length. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The regular and atom experiments combine into the full continuity frontier lower bound for minimax honest expected length. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.ContinuityProcedureBounds 11 declarations Finite-sample bounds for the continuity-only procedure
Finite-sample bounds for the continuity-only procedure
Hoeffding's inequality for an empirical average over a deterministic block of the canonical finite-product sample. The result uses the hf condition, the hf01 condition, the ht condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Outcome support lifts coordinatewise to the canonical finite product for a continuity-only model. The result uses the hP condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The retained-block empirical mean has root-block-size absolute risk in the continuity-only model. The result uses the hP condition, the hcard condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A stratum-threshold empirical mass has root-block-size absolute risk in the continuity-only model. The result uses the hP condition, the hcard condition, the hdelta condition, the hdelta1 condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The polynomial thinning envelope controls each population atom coefficient in the continuity-only model. The result uses the hP condition, the hreg condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The fixed one-half fallback has an explicit root-block plus threshold-mass absolute-risk bound. The result uses the hP condition, the hreg condition, the hdelta condition, the hcard0 condition, the hcard1 condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Summing the stratum indicators gives the single threshold indicator. This is the stated conclusion.
Formal statement
Proof (Lean source)
The population counterpart of the total empirical threshold mass. The result uses the hP condition, the hdelta condition, the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A deterministic deviation implication used by the two-block interval. The result uses the hP condition, the hreg condition, the hdelta condition, the h0 condition, the h1 condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The displayed square-root radius calibrates the two-sided Hoeffding tail to alpha / 2. The result uses the hm condition, the ha condition, the ha1 condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The continuity-only interval covers its model-specific target with the advertised finite-sample probability. The result uses the HoeffdingBoundedAverage_of_gate condition, the hP condition, the hreg condition, the hdelta condition, the hcard0 condition, the hcard1 condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.ContinuityRates 2 declarations Elementary rates for the continuity-only frontier
Elementary rates for the continuity-only frontier
At the continuity elbow the two summands of the frontier have root-sample size order. The result uses the hkappa condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
At threshold zero the continuity-only frontier is exactly the regular root-sample-size term. The result uses the hkappa condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.ContinuityRiskLower 4 declarations Two-point lower bounds for continuity-only risk
Two-point lower bounds for continuity-only risk
A close pair in the continuity-only model lower-bounds its observed minimax absolute risk. The result uses the hreg condition, the hdelta condition, the hP0 condition, the hP1 condition, the hgap0 condition, the hsep condition, the hac condition, the hint condition, the hchi0 condition, the hchi4 condition, the hchi condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The continuity-only minimax risk has the regular root-sample lower bound, uniformly over threshold sequences. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Arbitrarily narrow continuous bumps give an atom-scale minimax lower bound uniformly over the whole threshold range. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The regular and atom experiments combine into the full continuity frontier lower bound. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.ContinuityUpper 3 declarations Elementary upper bounds for the continuity-only procedure
Elementary upper bounds for the continuity-only procedure
The selected continuous conditional-mean version remains in the outcome range throughout the threshold interval. The result uses the hP condition, the hreg condition, the ha condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The continuity-only functional is the expectation of the observed outcome above the threshold and of the selected continuous regression below it. The result uses the hP condition, the hreg condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The continuity-only clamp functional lies in the outcome range. The result uses the hP condition, the hreg condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.ContinuityWitness 3 declarations This file places the canonical Bernoulli regression laws in the qualitative continuity model without imposing a common modulus of continuity.
Continuity-only canonical witnesses
This file places the canonical Bernoulli regression laws in the qualitative continuity model without imposing a common modulus of continuity.
A bounded continuous Bernoulli regression on the canonical design law is a member of the continuity-only model. The result uses the hJ condition, the hkappa condition, the hcminus condition, the hcplus condition, the hpmin condition, the hqmeas condition, the hqbound condition, the hcont condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Constant shifts belong to the continuity-only model. The result uses the hreg condition, the heps condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A fixed-height bump with an arbitrarily small positive width belongs to the same continuity-only class. In particular, the class membership carries no width-dependent Hölder radius. The result uses the hreg condition, the hh condition, the hamp condition, the hamp_le condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.ContinuityWitnessFunctional 5 declarations Functionals of the canonical continuity witnesses
Functionals of the canonical continuity witnesses
The selected continuous regression of a canonical Bernoulli witness is the displayed Bernoulli mean throughout the threshold range. The result uses the hreg condition, the hqmeas condition, the hqbound condition, the hcont condition, the ha condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The continuity functional of a canonical witness agrees with its explicit clamp functional on the threshold range. The result uses the hreg condition, the hdelta condition, the hqmeas condition, the hqbound condition, the hcont condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A fixed-height continuity bump changes the threshold functional by at least its atom contribution. The result uses the hJ condition, the hkappa condition, the hdelta condition, the hh condition, the hamp condition, the hamp_le condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The canonical center and a fixed-height narrow bump form an admissible continuity-only two-point experiment with an explicit product chi-square budget and atom-scale functional separation. The result uses the hreg condition, the hdelta condition, the hh condition, the hamp condition, the hamp_le condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Two constant Bernoulli regressions give the regular root-sample-size two-point experiment inside the continuity-only model. The result uses the hreg condition, the hdelta condition, the heps condition, the heps_le condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.Design 29 declarations This module gives full definitions of the paper's reference Gram, deterministic three-way split, local count and total Gram, exact intercept weights, stabilized estimator, bias-aware interval, and realized-design modulus
Realized local-polynomial design and estimators
This module gives full definitions of the paper's reference Gram, deterministic three-way split, local count and total Gram, exact intercept weights, stabilized estimator, bias-aware interval, and realized-design modulus handle.
Monomial basis (1,u,...,u^ell).
Definition (Lean source)
Normalized population reference moment matrix for (rho+u)^kappa.
Definition (Lean source)
Quadratic form of a real square matrix.
Smallest quadratic-form value on the Euclidean unit sphere.
Uniform population-Gram constant.
Definition (Lean source)
Three deterministic, pairwise-disjoint sample blocks, each of size at least floor(n/4).
Rescaled location of one observed treatment relative to the moving threshold.
Definition (Lean source)
Number of observations in stratum x and the local threshold window.
Definition (Lean source)
The zero-one localization weight on the full finite design.
Definition (Lean source)
Unnormalized total local Gram matrix, realized by Causalean's weighted monomial design matrix.
Definition (Lean source)
For sample blocks, a realized sample, a stratum, a polynomial degree, a threshold and bandwidth, and two matrix coordinates, the local Gram entry equals the active-window monomial sum.
Formal statement
Proof (Lean source)
The good-design event, encoded by its load-bearing quadratic-form lower bound.
Definition (Lean source)
Exact local-polynomial intercept weight from Causalean's equivalent kernel on the good event, and zero off it.
Definition (Lean source)
Given a good design, an observation in the regression block, the required stratum match, and local-window membership, the intercept weight is the zeroth coordinate of the inverse-Gram feature vector.
Formal statement
Proof (Lean source)
On the good-design event, the intercept weight equals the equivalent-kernel weight.
Formal statement
Proof (Lean source)
On the good-design event, if an observation is inactive, its intercept weight is zero.
Formal statement
Proof (Lean source)
Projection to the outcome range [0,1].
Empirical average over a deterministic finite block.
Retained-course empirical mean on block zero.
Definition (Lean source)
Empirical threshold mass in one stratum on block one.
Definition (Lean source)
Stabilized local regression value, with the prescribed one-half fallback.
Definition (Lean source)
Sample-split total-Gram-stabilized estimator of the clamp functional.
Definition (Lean source)
Continuity-only estimator using the retained-course block and the fixed one-half regression fallback for the total empirical atom mass.
Definition (Lean source)
Continuity-only Hoeffding interval, intersected with the outcome range.
Definition (Lean source)
The per-stratum bias-plus-noise radius, including the singular-Gram fallback.
Definition (Lean source)
Bias-aware interval intersected with [0,1].
Definition (Lean source)
Exact worst-case Hölder bias of affine weights on a realized local window. The derivatives are intrinsic to [0,1], so the value is invariant under any change to an ambient extension of the regression.
Definition (Lean source)
Conditional affine modulus for one realized design. Only observations in the local stratum-window may receive weight, and the full Hölder bias—not a coarse L h^beta sum |w_i| upper bound—is optimized.
Definition (Lean source)
The realized-design exact-modulus handle integrates the conditional sample-dependent modulus under a probability/support-pinned polynomial- thinning design law, for a positive bandwidth and a nonnegative test multiplier.
Definition (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.Divergence 2 declarations The upper inequality uses the Causalean quarter-band lemma.
Two-sided Bernoulli divergence bridges
The upper inequality uses the Causalean quarter-band lemma. The lower inequality is the missing direction needed by the one-cell calibration and follows from the exact Bernoulli formula (or Pinsker with the exact two-atom variation).
On the quarter window, Bernoulli KL from 1/2+g to 1/2 is comparable to g^2 in both directions. The result uses the hg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Integrating the scalar band against a nonnegative design density preserves both inequalities, yielding the localized one-observation KL order. The result uses the hpi_int condition, the hgamma_meas condition, the hkl_meas condition, the hpi condition, the hgamma condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.EstimatorMeasurable 11 declarations Measurability of the realized total-Gram estimator
Measurability of the realized total-Gram estimator
local count is measurable for the specified J input, the specified n input, the specified B input, the specified x input, the specified delta input, the specified h input.
Formal statement
Proof (Lean source)
local gram entry is measurable for the specified J input, the specified n input, the specified ell input, the specified B input, the specified x input, the specified r input, the specified s input, the specified delta input, the specified h input.
Formal statement
Proof (Lean source)
local gram is measurable for the specified J input, the specified n input, the specified ell input, the specified B input, the specified x input, the specified delta input, the specified h input.
Formal statement
Proof (Lean source)
the stated local gram is hermitian property holds for the specified J input, the specified n input, the specified ell input, the specified B input, the specified z input, the specified x input, the specified delta input, the specified h input.
Formal statement
Proof (Lean source)
local gram inv is measurable for the specified J input, the specified n input, the specified ell input, the specified B input, the specified x input, the specified delta input, the specified h input.
Formal statement
Proof (Lean source)
good gram event is measurable for the specified J input, the specified n input, the specified ell input, the specified B input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input.
Formal statement
Proof (Lean source)
intercept weight is measurable for the specified J input, the specified n input, the specified ell input, the specified B input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input, the specified i input.
Formal statement
Proof (Lean source)
retained estimate is measurable for the specified J input, the specified n input, the specified B input, the specified delta input.
Formal statement
Proof (Lean source)
atom estimate is measurable for the specified J input, the specified n input, the specified B input, the specified x input, the specified delta input.
Formal statement
Proof (Lean source)
local regression estimate is measurable for the specified J input, the specified n input, the specified ell input, the specified B input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input.
Formal statement
Proof (Lean source)
total gram estimator is measurable for the specified J input, the specified n input, the specified ell input, the specified B input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.FixedPositive 1 declarations This module closes the fixed-threshold branch from the moving-threshold rate lemmas.
Fixed-positive-threshold frontier
This module closes the fixed-threshold branch from the moving-threshold rate lemmas.
If the threshold converges to a positive constant, the actual frontier has the fixed-threshold nonparametric order. The result uses the hreg condition, the hdelta0 condition, the hdelta condition, the htend condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.HonestCoverage 4 declarations Finite-sample coverage of the bias-aware interval
Finite-sample coverage of the bias-aware interval
Hoeffding for a deterministic block, proved directly from the Causalean finite-product theorem and hence requiring no external theorem gate. The result uses the hf condition, the hf01 condition, the ht condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The common logarithmic radius gives each of the 2J+1 bad events ample budget under the union bound. The result uses the hJ condition, the hm condition, the ha condition, the ha1 condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
honest weighted tail satisfies the stated upper bound for the specified J input, the specified alpha input, the specified hJ input, the specified ha input, the specified ha1 input.
Formal statement
Proof (Lean source)
Every fixed model law is covered by the bias-aware interval with probability at least 1-alpha. The result uses the hmodel condition, the hJ condition, the hbeta condition, the hL condition, the ha condition, the ha1 condition, the hn condition, the hdelta condition, the hupper condition, the hh condition, the hlambda condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.HonestExpectedLength 9 declarations This module reduces the expected length of the clipped honest interval to its displayed sample-dependent radius.
Expected-length reductions for the bias-aware interval
This module reduces the expected length of the clipped honest interval to its displayed sample-dependent radius. It also records the exact mean of the atom-frequency estimate, the population input needed to bound that radius.
On a probability space, integrating the square root of a nonnegative integrable function is bounded by the square root of its integral. The result uses the hf condition, the hf0 condition, the hfInt condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Statistics computed from the atom block and local-regression block factor under the canonical product law. The result uses the hprob condition, the F condition, the G condition, the hF condition, the hG condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The displayed radius of the bias-aware interval.
Definition (Lean source)
Under the regime restrictions and nonnegative bandwidth, the displayed honest radius is nonnegative. The result uses the hreg condition, the hn condition, the hh condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Clipping the honest interval to the outcome range cannot make it longer than twice its displayed radius. The result uses the hreg condition, the hn condition, the hh condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A uniform modelwise expected-length bound passes through the real supremum convention used for the concrete honest interval. The result uses the hreg condition, the hupper condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The mean empirical atom frequency is bounded by its population thinning envelope plus the root-block fluctuation scale. The result uses the hmodel condition, the hreg condition, the hcard condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The expected square root of the stabilized local-weight energy is bounded by the square root of the existing integrated energy envelope. The result uses the hsampling condition, the hh condition, the hlambda condition, the hp condition, the hcard condition, the hmean condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Each per-stratum radius is bounded by a good-Gram bias/noise expression plus the indicator of Gram failure. The result uses the hbeta condition, the hL condition, the hh condition, the ht condition, the hb1 condition, the hlambda condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.HonestIntervalBasic 7 declarations Measurability and elementary length bounds for the honest interval
Measurability and elementary length bounds for the honest interval
The convex-hull length of a nonempty closed interval is its nonnegative endpoint difference. This is the stated conclusion.
Formal statement
Proof (Lean source)
The sample-dependent per-stratum honest radius is measurable. This is the stated conclusion.
Formal statement
Proof (Lean source)
Once the split blocks are nonempty, the displayed honest radius is nonnegative under the regime restrictions. The result uses the hreg condition, the hn condition, the hh condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The honest interval has measurable ordered endpoints for all sufficiently large sample sizes. The result uses the hreg condition, the hn condition, the hh condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Intersecting the honest interval with the outcome range bounds its length by one on every sample. This is the stated conclusion.
Formal statement
Proof (Lean source)
The displayed interval length is measurable as a function of the observed sample. This is the stated conclusion.
Formal statement
Proof (Lean source)
A real uniform expected-length upper bound upgrades to the extended-real worst-length convention. The result uses the hupper condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.HonestLengthLower 9 declarations This file isolates the low-level expected-length converse for the fixed-Hölder clamp model.
Two-point lower bounds for honest confidence length
This file isolates the low-level expected-length converse for the fixed-Hölder clamp model. It deliberately defines the worst length of one procedure here, so that the headline module can reuse the results without an import cycle.
Worst expected extended interval length of one procedure over the fixed-Hölder clamp model.
Definition (Lean source)
A close pair in the fixed-Hölder model lower-bounds the worst expected length of every interval procedure that is honest over that model. The result uses the hC condition, the hP0 condition, the hP1 condition, the hgap condition, the hsep condition, the hac condition, the hint condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The same two-point experiment lower-bounds the minimax honest expected length. The result uses the hP0 condition, the hP1 condition, the hgap condition, the hsep condition, the hac condition, the hint condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A numerical product chi-square budget can replace the exact divergence in the two-point expected-length bound. The result uses the hP0 condition, the hP1 condition, the hgap condition, the hsep condition, the hac condition, the hint condition, the hchi0 condition, the hchi condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Every honest procedure's worst length dominates the minimax honest length. The result uses the hC condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The fixed-Hölder minimax honest length has the root-sample-size lower bound, uniformly over admissible threshold sequences. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A fixed contraction of the information bandwidth gives the local fixed-Hölder lower component for minimax honest expected length. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The root and localized experiments combine into the full fixed-Hölder frontier lower bound for minimax honest expected length. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The same eventual frontier lower bound holds for the worst expected length of every uniformly honest procedure. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.HonestLengthUpper 3 declarations Eventual expected-length upper bound for the honest interval
Eventual expected-length upper bound for the honest interval
Exponential decay along the smallest effective-sample polynomial implied by the balance equation dominates the root-sample scale. The result uses the hbeta condition, the hkappa condition, the hc condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The balance equation forces the effective local sample size to grow at least at the edge-regime polynomial rate. The result uses the hn condition, the hbeta condition, the hkappa condition, the hdelta condition, the hh condition, the hbalance condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Uniform eventual expected-length upper bound for the concrete bias-aware interval, including the supremum over all laws in the admissible regime, is controlled by the frontier rate.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.HonestMixedTerm 5 declarations Disjoint-block factorization for the honest-radius mixed term
Disjoint-block factorization for the honest-radius mixed term
Local-polynomial intercept weights only depend on observations in the local-regression block. The result uses the hz condition, the hi condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Exact factorization of the atom-frequency/weight-energy mixed moment across the disjoint estimation blocks. The result uses the hJ condition, the hprob condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
At the information-balanced bandwidth, the expected square-root weight energy has the same h^beta scale as the local stochastic error. The result uses the hmodel condition, the hsampling condition, the hn condition, the hbeta condition, the hkappa condition, the hcminus condition, the hcplus condition, the hpmin condition, the hdelta condition, the hh condition, the hupper condition, the hlambda condition, the hbalance condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Integrated version of the good/bad pointwise radius decomposition. The mixed stochastic term factors exactly by sample splitting. The result uses the hJ condition, the hprob condition, the hbeta condition, the hL condition, the hh condition, the ht condition, the hb1 condition, the hlambda condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The displayed per-stratum radius is integrable under every product law. This is the bookkeeping input needed to integrate the finite sum of radii. The result uses the hprob condition, the hbeta condition, the hL condition, the hh condition, the ht condition, the hb1 condition, the hlambda condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.HonestPointwise 4 declarations Deterministic error event for the bias-aware interval
Deterministic error event for the bias-aware interval
The intermediate, realized-weight form of the Hölder bias bound. This is the form used by the honest interval, before replacing the realized l1 weight norm by its deterministic good-Gram upper bound. The result uses the hmodel condition, the hbeta condition, the hL condition, the hdelta condition, the hh condition, the hupper condition, the hlambda condition, the hgood condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Good-Gram local error decomposition retaining the empirical Hölder radius. The result uses the hmodel condition, the hbeta condition, the hL condition, the hdelta condition, the hh condition, the hupper condition, the hlambda condition, the hgood condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Retained-mean, atom-mass, and good-Gram local-regression deviations imply that the total estimator lies within the displayed honest radius. The result uses the hmodel condition, the hdelta condition, the hdelta1 condition, the hh condition, the hbeta condition, the hL condition, the htAlpha condition, the hb0 condition, the hb1 condition, the hret condition, the hatom condition, the hlocal condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The deterministic deviations used in the coverage proof put the target inside the clipped bias-aware interval. The result uses the hmodel condition, the hdelta condition, the hdelta1 condition, the hh condition, the hbeta condition, the hL condition, the htAlpha condition, the hb0 condition, the hb1 condition, the htdef condition, the hb0def condition, the hb1def condition, the hret condition, the hatom condition, the hlocal condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.LocalWindowGram 15 declarations This module identifies the fixed-stratum treatment marginal with its declared density law and transports integrals through that measure identity.
Local-window population-law bridge
This module identifies the fixed-stratum treatment marginal with its declared density law and transports integrals through that measure identity.
Unit local-window weight in a fixed stratum.
Definition (Lean source)
Monomial feature clipped outside the local window, so its global envelope is one while its weighted Gram agrees with the total local Gram.
Definition (Lean source)
the stated measurable local window weight property holds for the specified J input, the specified x input, the specified delta input, the specified h input.
Formal statement
Proof (Lean source)
the stated measurable local window feature property holds for the specified J input, the specified ell input, the specified delta input, the specified h input, the specified j input.
Formal statement
Proof (Lean source)
For a stratum, threshold, and bandwidth, the local-window weight lies between zero and one for every observation.
Formal statement
Proof (Lean source)
For a polynomial degree, threshold, bandwidth, and basis coordinate, the local-window feature has absolute value at most one for every observation.
Formal statement
Proof (Lean source)
The treatment marginal inside a fixed stratum is its stratum mass times the declared conditional treatment measure. The result uses the hmodel condition, the hkappa condition, the hcplus condition, the hpmin condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Integration form of stratumTreatmentMeasure_eq. The result uses the hmodel condition, the hkappa condition, the hcplus condition, the hpmin condition, the hf condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Integration against the declared conditional treatment measure is integration against its real density on [0,1]. The result uses the hmodel condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Positive bandwidth identifies the scaled unit window with the original treatment interval. The result uses the hh condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The population local-window mass is the stratum mass times the declared density integral over that window. The result uses the hmodel condition, the hh condition, the hwindow condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A positive interval captures a fixed positive fraction of the power mass at its upper endpoint. The result uses the hdelta condition, the hh condition, the hkappa condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The local stratum-window probability has the uniform polynomial lower bound obtained by integrating over the upper half of the window. The result uses the hmodel condition, the hkappa condition, the hcminus condition, the hcplus condition, the hpmin condition, the hdelta condition, the hh condition, the hupper condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A local-window Gram entry is the corresponding density-weighted monomial integral over the original treatment window. The result uses the hmodel condition, the hkappa condition, the hcplus condition, the hpmin condition, the hh condition, the hwindow condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The population local-window Gram dominates lambdaStar times its own local mass, using only the two-sided polynomial density envelope. The result uses the hmodel condition, the hkappa condition, the hcminus condition, the hcplus condition, the hpmin condition, the hdelta condition, the hh condition, the hupper condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.MinimaxDivergence 10 declarations Chi-squared control for the canonical minimax witnesses
Chi-squared control for the canonical minimax witnesses
The signed Bernoulli mark kernel before translating its marks to {0,1}.
Definition (Lean source)
the stated minimax mark kernel is markov property holds for the specified J input, the specified g input, the specified hgm input, the specified hg input.
Formal statement
Proof (Lean source)
Retaining the design and translating the centered mark is a measurable equivalence with the paper's observation carrier.
Definition (Lean source)
The bind construction of the witness law is precisely the attached mark kernel, transported through minimaxObsEquiv. The result uses the hJ condition, the hkappa condition, the hg condition, the hgb condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Exact one-observation chi-squared divergence for a common-design centered Bernoulli perturbation. The result uses the hJ condition, the hkappa condition, the hg condition, the hgb condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
the stated minimax data measure ac center property holds for the specified J input, the specified kappa input, the specified hJ input, the specified hkappa input, the specified g input, the specified hg input, the specified hgb input.
Formal statement
Proof (Lean source)
the stated minimax data measure sq integrable center property holds for the specified J input, the specified kappa input, the specified hJ input, the specified hkappa input, the specified g input, the specified hg input, the specified hgb input.
Formal statement
Proof (Lean source)
Exact iid tensorization of the canonical common-design experiment. The result uses the hJ condition, the hkappa condition, the hg condition, the hgb condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The squared local bump has the information-balance design integral order. The result uses the hJ condition, the hkappa condition, the hdelta condition, the hh condition, the hamp condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
the stated minimax constant product chi sq bound exp four property holds for the specified J input, the specified n input, the specified kappa input, the specified hJ input, the specified hkappa input, the specified hn input.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.MinimaxFunctional 6 declarations Clamp functional on the canonical witness family
Clamp functional on the canonical witness family
the stated minimax atom mass property holds for the specified J input, the specified kappa input, the specified delta input, the specified hkappa input, the specified hdelta input, the specified q input, the specified x input.
Formal statement
Proof (Lean source)
the stated minimax retained mean property holds for the specified J input, the specified kappa input, the specified delta input, the specified hJ input, the specified hkappa input, the specified q input, the specified hqmeas input, the specified hqbound input.
Formal statement
Proof (Lean source)
the stated minimax clamp functional property holds for the specified J input, the specified kappa input, the specified delta input, the specified hJ input, the specified hkappa input, the specified hdelta input, the specified q input, the specified hqmeas input, the specified hqbound input.
Formal statement
Proof (Lean source)
the stated minimax treatment measure real ioi property holds for the specified kappa input, the specified delta input, the specified hkappa input, the specified hdelta input.
Formal statement
Proof (Lean source)
the stated minimax global separation property holds for the specified J input, the specified kappa input, the specified delta input, the specified eps input, the specified hJ input, the specified hkappa input, the specified hdelta input, the specified heps input.
Formal statement
Proof (Lean source)
the stated minimax local separation property holds for the specified J input, the specified beta input, the specified kappa input, the specified delta input, the specified h input, the specified amplitude input, the specified hJ input, the specified hbeta input, the specified hkappa input, the specified hdelta input, the specified hh input, the specified hh1 input, the specified hamp input, the specified hamp_le input.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.MinimaxHolder 2 declarations Taylor certification for the localized minimax bump
Taylor certification for the localized minimax bump
A global smoothness and top-derivative Hölder bound imply the exact within-interval Taylor remainder convention used by HolderRegression. The result uses the hbeta condition, the hL condition, the hf condition, the htop condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Fixed amplitude and the localized smooth bump satisfy the paper's exact Taylor-remainder Hölder member uniformly over all admissible centers and bandwidths. The result uses the hbeta condition, the hL condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.MinimaxLaw 13 declarations The centered two-point law on {-1/2,1/2} is translated to a genuine Bernoulli outcome on {0,1}.
Bernoulli laws over the canonical minimax design
The centered two-point law on {-1/2,1/2} is translated to a genuine
Bernoulli outcome on {0,1}. Keeping this construction as an iterated kernel
makes the common design marginal and regression identities transparent.
The Bernoulli observation kernel with centered conditional mean g.
the stated measurable minimax outcome kernel property holds for the specified J input, the specified g input, the specified hg input.
Formal statement
Proof (Lean source)
Joint observation law induced by the canonical design and centered mean g.
Definition (Lean source)
Canonical law package associated with a centered Bernoulli regression.
Definition (Lean source)
minimax outcome kernel is a probability measure for the specified J input, the specified g input, the specified hg input, the specified p input.
Formal statement
Proof (Lean source)
minimax data measure is a probability measure for the specified J input, the specified kappa input, the specified hJ input, the specified hkappa input, the specified g input, the specified hgmeas input, the specified hg input.
Formal statement
Proof (Lean source)
the stated minimax outcome kernel map design property holds for the specified J input, the specified g input, the specified hg input, the specified p input.
Formal statement
Proof (Lean source)
the stated minimax data measure map design property holds for the specified J input, the specified kappa input, the specified g input, the specified hgmeas input, the specified hg input.
Formal statement
Proof (Lean source)
the stated minimax data measure map x property holds for the specified J input, the specified kappa input, the specified hJ input, the specified hkappa input, the specified g input, the specified hgmeas input, the specified hg input.
Formal statement
Proof (Lean source)
minimax treatment measure almost everywhere lies in the stated closed interval for the specified kappa input.
Formal statement
Proof (Lean source)
the stated minimax data measure almost everywhere treatment property holds for the specified J input, the specified kappa input, the specified g input, the specified hgmeas input, the specified hg input.
Formal statement
Proof (Lean source)
the stated minimax outcome kernel almost everywhere support property holds for the specified J input, the specified g input, the specified p input.
Formal statement
Proof (Lean source)
the stated minimax data measure almost everywhere bernoulli property holds for the specified J input, the specified kappa input, the specified g input, the specified hgmeas input.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.MinimaxMembership 3 declarations Model membership of canonical Bernoulli witnesses
Model membership of canonical Bernoulli witnesses
the stated minimax clamp model of taylor property holds for the specified J input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified hJ input, the specified hbeta input, the specified hkappa input, the specified hcminus input, the specified hcplus input, the specified hpmin input, the specified q input, the specified hqmeas input, the specified hqbound input, the specified hcont input, the specified hrange input, the specified htaylor input.
Formal statement
Proof (Lean source)
The unperturbed one-half Bernoulli regression is a member of every admissible clamp model and supplies model-class nonemptiness. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
the stated minimax constant membership model property holds for the specified J input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified deltaBar input, the specified alpha input, the specified eps input, the specified hreg input, the specified heps input.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.MinimaxRegression 1 declarations Regression identities for the canonical Bernoulli witnesses
Regression identities for the canonical Bernoulli witnesses
Integrating the outcome over a design event integrates the advertised Bernoulli mean over the common design law. The result uses the hJ condition, the hkappa condition, the hgmeas condition, the hg condition, the hT condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.MinimaxWitness 9 declarations The witness design uses uniform finite strata and the normalized polynomial density (κ + 1) a^κ on [0,1].
Canonical design for the clamp minimax witnesses
The witness design uses uniform finite strata and the normalized polynomial
density (κ + 1) a^κ on [0,1]. Outcome tilts are added in later lemmas.
Uniform probability law on the finite stratum space.
The normalized polynomial treatment law on [0,1].
the stated minimax treatment density integral property holds for the specified kappa input, the specified hkappa input.
Formal statement
Proof (Lean source)
minimax treatment measure is a probability measure for the specified kappa input, the specified hkappa input.
Formal statement
Proof (Lean source)
The common (X,A) law of every minimax witness.
Definition (Lean source)
minimax design measure is a probability measure for the specified J input, the specified kappa input, the specified hJ input, the specified hkappa input.
Formal statement
Proof (Lean source)
the stated minimax stratum measure real singleton property holds for the specified J input, the specified hJ input, the specified x input.
Formal statement
Proof (Lean source)
the stated minimax treatment measure real property holds for the specified kappa input, the specified hkappa input, the specified B input, the specified hB input, the specified hsub input.
Formal statement
Proof (Lean source)
the stated minimax design measure real rectangle property holds for the specified J input, the specified kappa input, the specified hJ input, the specified hkappa input, the specified x input, the specified B input, the specified hB input, the specified hsub input.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.PhaseRates 28 declarations The statement spells out every limiting regime and retains the almost-sure zero-threshold reduction to the ordinary bounded-mean estimator.
Four-regime threshold phase diagram
The statement spells out every limiting regime and retains the almost-sure zero-threshold reduction to the ordinary bounded-mean estimator.
Under the conditional-density model, the continuous treatment is strictly positive almost surely; the boundary singleton has no mass in any stratum. The result uses the hmodel condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
At threshold zero the observed clamp functional is the ordinary outcome mean, including the boundary point because the treatment law has no atom there. The result uses the hmodel condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
At threshold zero every empirical atom term vanishes almost surely, so the total-Gram estimator is exactly the clamped block-zero outcome mean. The result uses the hmodel condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
At the identity threshold the density-created atom vanishes, and hence the candidate frontier has exactly its root-sample-size summand. The result uses the hkappa condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The critical threshold is asymptotically separated above the design-edge scale under the declared exponent restrictions. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
At the design edge, the largest boundary-band atom term is negligible relative to the root-sample-size scale. The result uses the hbeta condition, the hkappa condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
In the interior-bandwidth regime, the atom contribution has the exact power-law form used to compare thresholds with the critical scale. The result uses the hn condition, the hd condition, the hbeta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
At the critical threshold, the interior-form atom contribution is exactly the root-sample-size scale. The result uses the hn condition, the hbeta condition, the hkappa condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The interior-form atom contribution, normalized by the root-sample-size scale, is exactly a positive power of the threshold-to-critical-scale ratio. The result uses the hn condition, the hd condition, the hbeta condition, the hkappa condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
If the threshold-to-critical-scale ratio converges to a positive constant, the normalized interior atom contribution converges to the corresponding positive power of that constant. The result uses the hbeta condition, the hkappa condition, the hc0 condition, the hratio condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A positive finite limit for a ratio gives an eventual two-sided constant sandwich of its numerator by its denominator. The result uses the hc condition, the hg condition, the hfg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
In the critical regime, the exact interior-form atom term has root-sample-size order. The result uses the hbeta condition, the hkappa condition, the hc0 condition, the hratio condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
If the threshold is asymptotically far above the critical scale, the interior atom contribution dominates the root-sample-size term. The result uses the hbeta condition, the hkappa condition, the hratio condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
In the supercritical regime, the root-sample-size contribution is eventually bounded by the exact interior-form atom contribution. The result uses the hbeta condition, the hkappa condition, the hratio condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A threshold asymptotic to a positive multiple of the critical scale lies asymptotically above the design-edge scale. The result uses the hreg condition, the hc0 condition, the hratio condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A threshold asymptotically larger than the critical scale also lies asymptotically above the smaller design-edge scale. The result uses the hreg condition, the hratio condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A threshold converging to a positive fixed value is asymptotically above the vanishing critical scale. The result uses the hreg condition, the hdelta0 condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
At the identity threshold, the concrete stabilized estimator inherits the root-sample-size risk sandwich from the minimax theorem. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Adding a nonnegative reference term preserves an asymptotic comparison when the other summand already has that reference order. The result uses the hfg condition, the hg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
If a nonnegative summand is eventually no larger than a sequence already of the target order, adding it preserves that asymptotic order. The result uses the hfs condition, the hg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Raising eventually nonnegative comparable sequences to a fixed positive real power preserves their asymptotic comparison. The result uses the ha condition, the hfg condition, the hf condition, the hg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Multiplication by a common eventually nonnegative factor preserves an asymptotic comparison. The result uses the hfg condition, the hq condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Asymptotic comparison is transitive. The result uses the hfg condition, the hgs condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
In the above-edge regime, replacing the implicit information bandwidth by its interior closed form preserves the order of the atom contribution. The result uses the hreg condition, the hdelta condition, the hfar condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
At a positive finite critical ratio, the actual implicit-bandwidth atom term and the resulting frontier both have root-sample-size order. The result uses the hreg condition, the hc0 condition, the hdelta condition, the hratio condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
At a positive finite critical ratio, adding the regular root term to the interior-form atom term preserves root-sample-size order. The result uses the hbeta condition, the hkappa condition, the hc0 condition, the hratio condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
In the supercritical moving-threshold regime, the actual implicit-bandwidth frontier is comparable to the interior atom scale, since that scale dominates the root-sample-size summand. The result uses the hreg condition, the hdelta condition, the hratio condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Below the critical scale, the actual implicit-bandwidth frontier has root-sample-size order. The result uses the hreg condition, the hdelta condition, the hratio condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.Pushforward 4 declarations The conditional treatment law is represented by its density against Lebesgue measure.
Clamp pushforward and exposure support
The conditional treatment law is represented by its density against Lebesgue measure. The clamp pushforward is stated as an equality of measures, including the Dirac mass at the threshold and the two-sided atom-mass bound.
Conditional natural-treatment measure in stratum x.
Pointwise support expressed by positivity of every open neighborhood.
The threshold clamp produces the retained continuous law plus a Dirac atom, whose mass is sandwiched by the integrated polynomial envelope. The result uses the hmodel condition, the hreg condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Every clamped treatment value is almost surely a support point of the natural conditional treatment law, including the identity case at zero. The result uses the hmodel condition, the hreg condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.RegressionVersion 11 declarations A measurable global version of the clamp regression
A measurable global version of the clamp regression
clamp design is measurable for the specified J input.
Formal statement
Proof (Lean source)
clamp outcome is measurable for the specified J input.
Formal statement
Proof (Lean source)
Extend the model's regression from its declared dose interval by zero.
clamp regression extension is measurable for the specified J input, the specified P input, the specified beta input, the specified L input, the specified hholder input.
Formal statement
Proof (Lean source)
clamp regression extension satisfies the stated identity for the specified J input, the specified P input, the specified x input, the specified a input, the specified ha input.
Formal statement
Proof (Lean source)
clamp regression extension lies in the stated closed interval for the specified J input, the specified P input, the specified beta input, the specified L input, the specified hholder input, the specified d input.
Formal statement
Proof (Lean source)
clamp outcome is integrable for the specified J input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified hmodel input.
Formal statement
Proof (Lean source)
the stated clamp regression extension almost everywhere identity mu property holds for the specified J input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified hmodel input.
Formal statement
Proof (Lean source)
The conditional-expectation regression tie implies the cellwise set-integral identity used by the causal bridge. The result uses the hmodel condition, the hkappa condition, the hcplus condition, the hpmin condition, the hB condition, the hBIcc condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Any integrable conditional-regression version satisfies the same cellwise set-integral identity; this is the smoothness-free form used by the continuity-only causal bridge. The result uses the hmodel condition, the hkappa condition, the hcplus condition, the hpmin condition, the hver condition, the hB condition, the hBIcc condition, the hmuInt condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
the stated clamp regression cond exp property holds for the specified J input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified hmodel input, the specified x₀ input.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.SampleBlocks 5 declarations These build-inline bridges restrict the canonical finite product sample to an arbitrary deterministic block, reindex that block by Fin I.card, and connect the resulting coordinate sum to the range-indexed Causalean count
Finite-product transport to deterministic sample blocks
These build-inline bridges restrict the canonical finite product sample to an
arbitrary deterministic block, reindex that block by Fin I.card, and connect
the resulting coordinate sum to the range-indexed Causalean count API through
the canonical infinite-product sample. No ambient i.i.d. stream is assumed.
Membership in the observed clamp model supplies the canonical finite-product sampling certificate at every horizon. Independence and marginal laws follow from the product measure rather than from an ambient sample stream. The result uses the hP condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Continuity-only model membership supplies the same canonical finite-product sampling certificate. The result uses the hP condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
After increasing-order reindexing, the tuple retained by a deterministic block has the ordinary product law on Fin I.card. This is the stated conclusion.
Formal statement
Proof (Lean source)
The law of a statistic summed over an arbitrary deterministic block is the law of the same statistic summed over Fin I.card product coordinates. The result uses the hf condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A range-indexed count on the canonical infinite-product stream has the same law as the corresponding sum on the finite product Fin m → X. The result uses the hf condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.ShiftedPowerCoercivity 4 declarations This module isolates the reusable compactification step behind the population Gram lower bound for polynomially thinned local designs.
Uniform coercivity for shifted-power moment matrices
This module isolates the reusable compactification step behind the population Gram lower bound for polynomially thinned local designs.
Normalized monomial moment matrices weighted by (ρ + u)^κ are uniformly coercive over all nonnegative shifts ρ when κ is nonnegative. The result uses the hkappa condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The uniform population-Gram constant is positive under positive envelope constants and a nonnegative thinning exponent. The result uses the hkappa condition, the hcminus condition, the hcplus condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
lambdaStar gives the advertised coercivity for every normalized shifted power moment matrix. The result uses the hkappa condition, the hcminus condition, the hcplus condition, the hrho condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The normalized lambdaStar coercivity, transported from the unit interval to a positive local window. The result uses the hkappa condition, the hcminus condition, the hcplus condition, the hdelta condition, the hh condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.SurjectivityLift 3 declarations Quantile lifts of observed clamp laws
Quantile lifts of observed clamp laws
A measurable bounded conditional-regression version can be realized by a single independent uniform latent variable while preserving the observed law. This uses a probability law, bounded outcomes, positive stratum masses, a measurable bounded regression, the conditional-mean identity, and stratumwise continuity; such a full-data lift exists.
Formal statement
Proof (Lean source)
Fixed-Hölder observed laws have a quantile full-data lift. The result uses the hP condition, the hJ condition, the hpmin condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Continuity-only observed laws have the same quantile full-data lift. The result uses the hP condition, the hpmin condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.TotalGram 6 declarations This file isolates the note's main realized-design bottleneck.
Uniform total-Gram stabilization
This file isolates the note's main realized-design bottleneck. Constants are quantified before laws, sample sizes, thresholds, blocks, and strata.
If the reference eigenvalue is positive and the realized Gram matrix is good, the intercept weights reproduce every polynomial basis coordinate.
Formal statement
Proof (Lean source)
Summing over the canonical enumeration of a finite set agrees with summing directly over that set.
Formal statement
On a good Gram event, every active intercept weight has the inverse-count scale dictated by coercivity. The result uses the hlambda condition, the hgood condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
On a good Gram event, the exact weights reproduce every basis monomial and obey explicit count-normalized l1 and squared-l2 bounds. The result uses the hh condition, the hlambda condition, the hgood condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The population constant used by total-Gram stabilization is positive under the standing regime constraints. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Uniform positivity, singular-design tail, exact reproduction, and l1/l2 weight control follow from admissible regime constants. The constants are uniform over laws, samples, thresholds, and strata.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.UpperEmpirical 4 declarations
Expected absolute error of a bounded empirical average over an arbitrary nonempty deterministic block of a finite product sample. The result uses the hI condition, the hf condition, the hf0 condition, the hf1 condition, the hm condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
retained estimate absolute-error satisfies the stated upper bound for the specified J input, the specified n input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified delta input, the specified hmodel input, the specified B input, the specified hcard input.
Formal statement
Proof (Lean source)
atom event integral satisfies the stated identity for the specified J input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified delta input, the specified hmodel input, the specified x input, the specified hdelta1 input.
Formal statement
Proof (Lean source)
atom estimate absolute-error satisfies the stated upper bound for the specified J input, the specified n input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified delta input, the specified hmodel input, the specified B input, the specified hcard input, the specified x input, the specified hdelta input, the specified hdelta1 input.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.UpperNoise 27 declarations Design-measurable weights for the local-regression noise term
Design-measurable weights for the local-regression noise term
clamp unit is measurable.
Formal statement
Proof (Lean source)
clamp unit lies in the stated closed interval for the specified t input.
Proof (Lean source)
abs clamp unit sub satisfies the stated upper bound for the specified t input, the specified q input, the specified hq input.
Proof (Lean source)
clamp outcome almost everywhere satisfies the stated identity for the specified J input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified hmodel input.
Formal statement
Proof (Lean source)
the stated i.i.d. product outcome support property holds for the specified J input, the specified n input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified hmodel input.
Formal statement
Proof (Lean source)
the stated clamp outcome cond exp property holds for the specified J input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified hmodel input, the specified x₀ input.
Formal statement
Proof (Lean source)
A canonical observation with the specified design and dummy outcome.
clamp design lift is measurable for the specified J input.
Formal statement
Proof (Lean source)
The realized local-polynomial weight regarded as a function only of the full design vector.
Definition (Lean source)
local regression design weight is measurable for the specified J input, the specified n input, the specified ell input, the specified B input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input.
Formal statement
Proof (Lean source)
the stated local regression design weight apply property holds for the specified J input, the specified n input, the specified ell input, the specified B input, the specified z input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input, the specified i input.
Formal statement
Proof (Lean source)
the stated weighted centered sum local regression property holds for the specified J input, the specified n input, the specified ell input, the specified B input, the specified P input, the specified z input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input.
Formal statement
Proof (Lean source)
the stated weighted centered sum local regression clamp property holds for the specified J input, the specified n input, the specified ell input, the specified B input, the specified P input, the specified z input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input.
Formal statement
Proof (Lean source)
local regression weight energy satisfies the stated upper bound for the specified J input, the specified n input, the specified ell input, the specified B input, the specified z input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input, the specified hh input, the specified hlambda input.
Formal statement
Proof (Lean source)
local regression weight energy is integrable for the specified J input, the specified n input, the specified ell input, the specified B input, the specified P input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input, the specified hh input, the specified hlambda input.
Formal statement
Proof (Lean source)
the stated finite product bernoulli count lower tail property holds for the specified N input, the specified X input, the specified P input, the specified q input, the specified hqmeas input, the specified hq01 input, the specified hN input, the specified p input, the specified hp input, the specified hmean input.
Formal statement
Proof (Lean source)
the stated i.i.d. block product law property holds for the specified J input, the specified n input, the specified P input, the specified hsampling input, the specified I input.
Formal statement
Proof (Lean source)
the stated local count lower tail property holds for the specified J input, the specified n input, the specified P input, the specified hsampling input, the specified B input, the specified x input, the specified delta input, the specified h input, the specified p input, the specified hh input, the specified hp input, the specified hmean input, the specified hcard input.
Formal statement
Proof (Lean source)
local regression weight energy integral satisfies the stated upper bound for the specified J input, the specified n input, the specified ell input, the specified P input, the specified hsampling input, the specified B input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input, the specified p input, the specified hh input, the specified hlambda input, the specified hp input, the specified hcard input, the specified hmean input.
Formal statement
Proof (Lean source)
local regression centered absolute-error satisfies the stated upper bound for the specified J input, the specified n input, the specified ell input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified hmodel input, the specified hsampling input, the specified B input, the specified x input, the specified delta input, the specified h input, the specified p input, the specified hh input, the specified hlambda input, the specified hkappa input, the specified hcplus input, the specified hpmin input, the specified hp input, the specified hcard input, the specified hmean input.
Formal statement
Proof (Lean source)
The information-balance identity expressed as the reciprocal effective sample size used by the local-regression variance bound. The result uses the hh condition, the hb condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
the stated exp neg scaled bound inv property holds for the specified t input, the specified ht input.
Formal statement
Proof (Lean source)
A deterministic conversion of the count-weighted noise expression to the balanced bandwidth rate. The constants include the split-block factor eight and the elementary exponential bound exp (-t/20) ≤ 20/t. The result uses the hn condition, the hh condition, the hD condition, the hK condition, the hm condition, the hp condition, the hb condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
On a good realized Gram event, the conditional mean part of the local polynomial estimator has the stated Hölder bias. The result uses the hmodel condition, the hbeta condition, the hL condition, the hdelta condition, the hh condition, the hupper condition, the hlambda condition, the hgood condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Pointwise good-event decomposition of local-regression error into its centered stochastic sum and deterministic Hölder bias. The result uses the hmodel condition, the hbeta condition, the hL condition, the hdelta condition, the hh condition, the hupper condition, the hlambda condition, the hgood condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The centered local-regression noise at the information-balanced bandwidth is uniformly of order h^beta. The result uses the hmodel condition, the hsampling condition, the hn condition, the hbeta condition, the hkappa condition, the hcminus condition, the hcplus condition, the hpmin condition, the hdelta condition, the hh condition, the hupper condition, the hlambda condition, the hbalance condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Integrated Good/bad decomposition for one stratum's stabilized local regression. The only exceptional contribution is the real probability of a bad Gram event. The result uses the hmodel condition, the hbeta condition, the hL condition, the hdelta condition, the hh condition, the hupper condition, the hlambda condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.UpperTotal 12 declarations
clamp functional integral satisfies the stated identity for the specified J input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified delta input, the specified hmodel input, the specified hdelta input, the specified hdelta1 input.
Formal statement
Proof (Lean source)
clamp functional lies in the stated closed interval for the specified J input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified delta input, the specified hmodel input, the specified hdelta input, the specified hdelta1 input.
Formal statement
Proof (Lean source)
local regression estimate lies in the stated closed interval for the specified J input, the specified n input, the specified ell input, the specified B input, the specified z input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input.
Formal statement
Proof (Lean source)
block average lies in the stated closed interval for the specified X input, the specified n input, the specified I input, the specified z input, the specified f input, the specified hf input.
Formal statement
Proof (Lean source)
atom estimate lies in the stated closed interval for the specified J input, the specified n input, the specified B input, the specified z input, the specified x input, the specified delta input.
Formal statement
Proof (Lean source)
the stated split block inv sqrt bound root property holds for the specified n input, the specified m input, the specified hn input, the specified hm input.
Formal statement
Proof (Lean source)
balanced gram tail satisfies the stated upper bound for the specified n input, the specified beta input, the specified kappa input, the specified delta input, the specified h input, the specified C input, the specified c input, the specified hn input, the specified hbeta input, the specified hh input, the specified hh1 input, the specified hC input, the specified hc input, the specified hbalance input.
Formal statement
Proof (Lean source)
atom coefficient lies in the stated closed interval for the specified J input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified delta input, the specified hmodel input, the specified x input, the specified hdelta1 input.
Formal statement
Proof (Lean source)
the stated abs atom coefficient bound envelope property holds for the specified J input, the specified P input, the specified beta input, the specified kappa input, the specified L input, the specified cminus input, the specified cplus input, the specified pmin input, the specified deltaBar input, the specified alpha input, the specified delta input, the specified hmodel input, the specified hreg input, the specified x input, the specified hdelta input.
Formal statement
Proof (Lean source)
Deterministic decomposition of the total estimator into the retained-block error, the atom-mass empirical errors, and the local-regression errors. The result uses the hmodel condition, the hdelta condition, the hdelta1 condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Integrated form of totalGramEstimator_error_le, with every finite-sample term exposed for the concentration and empirical-process bounds. The result uses the hmodel condition, the hdelta condition, the hdelta1 condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Explicit finite-sample risk bound at an information-balanced bandwidth, before the elementary eventual-rate simplifications. The result uses the hmodel condition, the hreg condition, the hsampling condition, the hn condition, the hdelta condition, the hh condition, the hupper condition, the hbalance condition, the hlambda condition, the htail condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.Helpers.WeightedConcentration 7 declarations This module instantiates Causalean's finite-product conditional Hoeffding theorem.
Random-design weighted concentration on the good-Gram event
This module instantiates Causalean's finite-product conditional Hoeffding theorem. The local-polynomial weights are stabilized off the good-Gram event so their realized energy is everywhere positive; the resulting tail is then restricted back to the good event used by the atom-fallback interval.
On the good-Gram event the exact equivalent-kernel weights have strictly positive realized squared energy. The result uses the hlambda condition, the hgood condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Complete-design-measurable local-polynomial weights, replaced off the good-Gram event by one fixed unit coordinate.
Definition (Lean source)
stabilized weight is measurable for the specified J input, the specified n input, the specified ell input, the specified B input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input, the specified i₀ input.
Formal statement
Proof (Lean source)
the stated stabilized weight identity on good property holds for the specified J input, the specified n input, the specified ell input, the specified B input, the specified z input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input, the specified i₀ input, the specified hgood input.
Formal statement
Proof (Lean source)
the stated stabilized weight positive energy property holds for the specified J input, the specified n input, the specified ell input, the specified B input, the specified z input, the specified x input, the specified kappa input, the specified cminus input, the specified cplus input, the specified delta input, the specified h input, the specified i₀ input, the specified hlambda input.
Formal statement
Proof (Lean source)
The finite-product random-design Hoeffding tail for the stabilized weights. This is the direct Causalean theorem at the paper's observed-sample abstraction. The result uses the hmodel condition, the hlambda condition, the ht condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Restricting the stabilized tail back to the good-Gram event recovers the paper's exact local-polynomial weighted residual sum. The result uses the hmodel condition, the hlambda condition, the ht condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.OpenQuestions 6 declarations The declaration is a never-proved proposition, not a theorem.
Open question: sharp confidence-length constant
The declaration is a never-proved proposition, not a theorem. It asks for one sharp constant over every threshold regime and attainment by intervals whose radius is built from the realized-design exact-modulus handle.
Worst-case integrated exact-modulus radius over the model and strata.
Definition (Lean source)
Worst conditional exact modulus on the realized design.
Definition (Lean source)
Conditional-modulus interval centered at the realized total-Gram estimate.
Definition (Lean source)
The threshold sequence approaches one of the finite or infinite phase regimes; oscillating sequences with no ratio limit are intentionally excluded.
The conditional modulus interval matches both the integrated realized modulus and the minimax length of the least-favorable mixed regular-plus-local experiment.
Definition (Lean source)
Does a realized-design exact-modulus interval attain one sharp asymptotic constant for L_n^star / r_n across regular, critical, atom-dominated, and fixed-threshold limits while retaining the stated model class?
Definition (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.TCausalBridge 2 declarations The theorem includes the stratumwise product identity, pointwise identification, support, simultaneous pathwise clamp decomposition, and target equality.
Full-data to observed-data clamp bridge
The theorem includes the stratumwise product identity, pointwise identification, support, simultaneous pathwise clamp decomposition, and target equality.
Latent randomization and structural-mean continuity identify the observed continuous regression on the declared threshold range and hence identify the clamp mean. Joint measurability of the potential-outcome process is part of FullDataLaw, and all remaining causal conditions are supplied by the bundled full-data model membership. The result uses the hPF condition, the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The same latent-response argument identifies the qualitative continuous regression version and the continuity-only clamp functional, without imposing a fixed-Hölder observed model or a shared latent carrier. The result uses the hPF condition, the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.TCausalFrontierLift 18 declarations All procedures remain functions only of the observed sample.
Lift of the observed frontier to the full-data causal class
All procedures remain functions only of the observed sample. The quantified
class is the full-data class, and the criteria are the two components of
causalFrontierCriteria.
Mathlib's standard-Borel disintegration kernel discharges the paper's regular-conditional-law gate. This is the stated conclusion.
Formal statement
Proof (Lean source)
Conditional on the disclosed regular-conditional-law gate, every observed model law admits a structural full-data lift and the observed and causal finite-sample criteria agree. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Conditional on the same disclosed gate, the observed-margin map is onto for the continuity-only class and its observed and causal criteria agree. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Worst-case causal risk of the same observed-sample total-Gram estimator.
Definition (Lean source)
Worst-case full-data coverage of the same observed-sample interval.
Definition (Lean source)
Worst-case full-data expected length of that interval, as an extended expectation so a non-integrable length contributes ∞.
Definition (Lean source)
The convex-hull length of a closed real interval is its nonnegative endpoint difference, including the empty-interval case. This is the stated conclusion.
Formal statement
Proof (Lean source)
The sample-dependent per-stratum radius is measurable. This is the stated conclusion.
Formal statement
Proof (Lean source)
Once all three blocks are nonempty, the total displayed confidence radius is nonnegative under the declared parameter restrictions. The result uses the hreg condition, the hn condition, the hh condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Length of the displayed bias-aware interval is measurable as a function of the observed sample. This is the stated conclusion.
Formal statement
Proof (Lean source)
For sufficiently large samples the displayed endpoints are ordered and measurable, hence the bias-aware construction is an admissible observed confidence procedure. The result uses the hreg condition, the hn condition, the hh condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Intersecting the bias-aware interval with the outcome range bounds its convex-hull length by one on every sample. This is the stated conclusion.
Formal statement
Proof (Lean source)
A real expected-length bound for the concrete interval upgrades to the extended expected-length convention used by the minimax criteria. The result uses the hupper condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Any uniformly honest concrete interval upper-bounds the observed minimax expected length by its own worst-case length. The result uses the hC condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Surjectivity and identification transport the concrete estimator's worst-case risk from the observed class to the full-data class. The result uses the hreg condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Surjectivity and identification transport coverage of the concrete bias-aware interval. The result uses the hreg condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Expected interval length depends only on the observed margin, so surjectivity transports its worst case without any target calculation. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Identification transports both observed brackets to the full-data class; the same observed estimator and interval attain both causal frontiers. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.THonestLength 24 declarations The statement gives finite-sample eventual uniform coverage, expected-length control for the concrete atom-fallback interval, and a converse for every uniformly honest confidence procedure.
Uniformly honest confidence length frontier
The statement gives finite-sample eventual uniform coverage, expected-length control for the concrete atom-fallback interval, and a converse for every uniformly honest confidence procedure.
The paper's confidence procedure at a fixed sample size.
Definition (Lean source)
Worst-case coverage of the concrete interval over i.i.d. model laws.
Definition (Lean source)
Worst-case expected length of the concrete interval.
Definition (Lean source)
Worst-case expected length of any given confidence procedure.
Definition (Lean source)
The modelwise finite-sample coverage inequality passes through the worst-model infimum defining the paper's concrete coverage criterion. The result uses the hreg condition, the hn condition, the hdelta condition, the hh condition, the hupper condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The concrete stabilized interval is an admissible uniformly covering procedure at every sample size where the bandwidth lies inside the design support. The result uses the hreg condition, the hn condition, the hdelta condition, the hh condition, the hupper condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The bias-aware interval is uniformly honest and rate-optimal in worst-case expected length, including singular-Gram samples via its atom fallback. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Worst-case continuity-only risk of the fixed one-half fallback estimator.
Definition (Lean source)
Worst-case coverage of the continuity-only Hoeffding interval.
Definition (Lean source)
Worst-case extended expected length of the continuity-only interval.
Definition (Lean source)
Worst-case causal risk of the same continuity-only observed-sample fallback estimator, over law-specific latent carriers.
Definition (Lean source)
Worst-case causal coverage of the same continuity-only interval, over law-specific latent carriers.
Definition (Lean source)
Worst-case causal expected length of the same continuity-only interval, over law-specific latent carriers.
Definition (Lean source)
The fixed-fallback estimator is measurable and remains in the outcome range. This is the stated conclusion.
Formal statement
Proof (Lean source)
Surjectivity and identification equate the concrete observed and causal worst-case risks. The result uses the hreg condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Surjectivity and identification equate the concrete observed and causal worst-case coverages. The result uses the hreg condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Surjectivity equates the concrete observed and causal worst-case expected lengths. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The fixed fallback is an admissible competitor for the observed minimax risk criterion. The result uses the hreg condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The concrete continuity interval has uniform finite-sample coverage once both deterministic blocks are nonempty. The result uses the HoeffdingBoundedAverage_of_gate condition, the hreg condition, the hdelta condition, the hcard0 condition, the hcard1 condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The concrete fixed-fallback worst-case risk attains the continuity rate. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The extended expected length of the concrete interval attains the same continuity frontier. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
At a threshold converging to a positive interior point, neither the observed nor causal continuity-only minimax risk can converge to zero. The result uses the hreg condition, the hdelta condition, the hdelta0 condition, the htend condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A threshold converging to a positive interior point also prevents the observed minimax honest length from converging to zero. The result uses the hreg condition, the hdelta condition, the hdelta0 condition, the htend condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Conditional on the disclosed Hoeffding gate, the fixed-fallback estimator and interval attain the continuity-only frontier, with identical observed and causal decision criteria. The result uses the HoeffdingBoundedAverage_of_gate condition, the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.TMinimaxRisk 18 declarations The upper bound is attached to the concrete total-Gram estimator.
Matched minimax absolute-risk frontier
The upper bound is attached to the concrete total-Gram estimator. The lower bound contains both same-class experiments and their product-divergence bounds.
Risk of the paper's concrete stabilized estimator.
Definition (Lean source)
Worst-case risk of the concrete estimator over i.i.d. laws in the model.
Definition (Lean source)
Product chi-squared divergence used by the same-class witnesses.
Definition (Lean source)
The product law from P is absolutely continuous with respect to the product law from Q, and its squared Radon--Nikodym deviation is integrable for the sample size n; together these conditions define well-posed real product chi-squared divergence.
Definition (Lean source)
The outcome in a lower-bound experiment is genuinely Bernoulli.
Definition (Lean source)
Uniform eventual upper bound for the concrete stabilized estimator, including the supremum over all model laws. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A global Bernoulli regression mean shift of the advertised size.
Definition (Lean source)
the stated minimax constant global shift property holds for the specified J input, the specified kappa input, the specified eps input, the specified heps input.
Formal statement
Proof (Lean source)
The canonical constant Bernoulli shift supplies the global root-sample witness, uniformly over every admissible threshold sequence. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A common-design Bernoulli perturbation localized to a width-h window at the threshold, with fixed small amplitude times h^beta and a continuous bump supported on [-1,1].
Definition (Lean source)
the stated minimax bump localized perturbation property holds for the specified J input, the specified beta input, the specified kappa input, the specified delta input, the specified h input, the specified amplitude input, the specified hbeta input, the specified hh input, the specified hh1 input, the specified hamp input, the specified hamp_le input.
Formal statement
Proof (Lean source)
The fixed smooth bump supplies the localized information-bandwidth witness with a product chi-squared bound uniform in the threshold sequence and sample size. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A close pair with a chi-squared budget below four gives an absolute-risk lower bound for the observed minimax problem. The result uses the hP0 condition, the hP1 condition, the hdelta0 condition, the hdelta1 condition, the hgap0 condition, the hsep condition, the hac condition, the hint condition, the hchi0 condition, the hchi4 condition, the hchi condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A quarter-strength constant Bernoulli shift gives the parametric component of the minimax lower bound while keeping chi-squared below four. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
A fixed contraction of the information bandwidth makes the localized experiment close while preserving the local frontier order. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The concrete stabilized estimator is an admissible competitor in the observed minimax problem. The result uses the hreg condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The minimax risk and concrete estimator risk are both comparable to the regular-plus-atom frontier, with explicit global and localized witnesses. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.TOneCellCalibration 12 declarations The concrete one-stratum design has density 2a, a triangular width-h Bernoulli regression perturbation, its exact integrated KL, and target separation.
One-cell early-kill calibration
The concrete one-stratum design has density 2a, a triangular width-h
Bernoulli regression perturbation, its exact integrated KL, and target separation.
The concrete one-cell assignment density.
Definition (Lean source)
Unit triangular localization around the moving threshold.
Definition (Lean source)
Null Bernoulli regression.
Definition (Lean source)
Width-h, height-h localized Bernoulli alternative for beta one.
Definition (Lean source)
Product KL of the concrete localized Bernoulli alternatives.
Definition (Lean source)
Total clamp-target separation of the concrete one-cell pair: the retained- course integral plus the collapsed-atom contribution.
Definition (Lean source)
On an interior right-hand localization window, the one-cell target separation is the atom contribution plus the exact retained-course integral. The result uses the hdelta condition, the hh condition, the hwindow condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The squared triangular perturbation has an exact design-weighted mass on an interior localization window. The result uses the hh condition, the hleft condition, the hright condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Above the one-cell edge scale, the balance bandwidth is comparable to the interior bandwidth and its localization window is eventually interior. The result uses the hdeltaBar condition, the hdelta condition, the hfar condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
On an interior quarter-height window, the concrete product KL is trapped between fixed multiples of n * delta * h^3. The result uses the hh condition, the hleft condition, the hright condition, the hquarter condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The normalized interior one-cell atom scale is the 5/3 power of the threshold measured in critical-scale units. The result uses the hn condition, the hdelta condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
For beta=kappa=one, the bandwidth, KL, separation, and transition exponent are exactly the one-cell calibration stated in the note. The result uses the hdeltaBar condition, the hdelta condition, the hfar condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LmtpThresholdAtomFrontier_Research.TPhaseDiagram 3 declarations This module assembles the rate comparisons and the zero-threshold reduction.
Four-regime threshold phase diagram
This module assembles the rate comparisons and the zero-threshold reduction.
At the identity threshold, the stabilized interval is eventually uniformly honest over the bounded-outcome model. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
At the identity threshold, the bias-aware interval's worst-case expected length inherits the root-sample-size sandwich from the honest-length theorem. The result uses the hreg condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The critical scale is separated from the design-edge scale; below, at, and above it the frontier has the four rates stated in the paper. The result uses the hreg condition. This is the stated conclusion.