Formalization: Estimating Optimal Treatment Value with Many Covariate Cells and Shrinking Overlap
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs. Note: this index was generated at a different commit than the paper's audited pin (15d86b3) — statements may have moved since the audit.
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Basic 37 declarations The finite PMF abstraction retains arbitrary and null covariate cells.
Vanishing-overlap optimal value: finite observed and causal models
The finite PMF abstraction retains arbitrary and null covariate cells. The measure-theoretic PO and MinimaxATE systems use a different model, so only their generic minimax risk primitives are imported.
For the displayed parameters, Obs is the object specified by this definition.
For the displayed parameters, DiscreteLaw is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, jointMass is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, cellIdx is the object specified by this definition.
For the displayed parameters, cellVector is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, cellMass is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, armMass is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, propensity is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, outcomeMean is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, productLaw is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, FullObs is the object specified by this definition.
For the displayed parameters, PotentialLaw is the object specified by this definition.
For the displayed parameters, fullMass is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, observedMarginal is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, poCellMass is the object specified by this definition.
For the displayed parameters, poAtom is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, poArmAtom is the object specified by this definition.
For the displayed parameters, poTreatMass is the object specified by this definition.
For the displayed parameters, poPotentialMass is the object specified by this definition.
For the displayed parameters, poRegression is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, oracleValue is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, IidSampling is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, Overlap is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, Consistency is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, ConditionalExchangeability is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, ObservedClass is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, CausalClass is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, observedValue is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, Estimator is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, ModelLaw is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, CausalModelLaw is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, observedRisk is the object specified by this definition.
For the displayed parameters, minimaxRisk is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, causalRisk is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, causalMinimaxRisk is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, logAlphabet is the object specified by this definition.
For the displayed parameters, rateScale is the object specified by this definition.
Definition (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.ArmwiseExtension 20 declarations Armwise anchored four-cell extension
Armwise anchored four-cell extension
For the displayed parameters, armMassVecFormula is the object specified by this definition. For the displayed parameters, armMassVecFormula is the defined object.
For the displayed parameters, totalMassVecFormula is the object specified by this definition. For the displayed parameters, totalMassVecFormula is the defined object.
Definition (Lean source)
For the displayed parameters, anchoredDenomFormula is the object specified by this definition. For the displayed parameters, anchoredDenomFormula is the defined object.
Definition (Lean source)
For the displayed parameters, armDelta is the object specified by this definition. For the displayed parameters, armDelta is the defined object.
Ambient formula used by the analytic API; its paper domain is pinned below.
Definition (Lean source)
The coordinatewise nonnegative four-vector domain of the armwise construction.
Definition (Lean source)
Arm mass on the nonnegative four-vector domain.
Definition (Lean source)
Total mass on the nonnegative four-vector domain.
Definition (Lean source)
Anchored denominator on the nonnegative four-vector domain.
Definition (Lean source)
For the displayed parameters, armwiseExtension is the object specified by this definition. For the displayed parameters, armwiseExtension is the defined object.
Definition (Lean source)
Observed atom masses supply the construction's domain without an extra assumption. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Analytic extension of the modulus; the paper realization below restricts its domain. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.ConsistencyFrontier 6 declarations The final paragraph of the weighted-separation roadmap reduces uniform consistency to convergence of the uncapped rate.
Uniform consistency from the risk frontier
The final paragraph of the weighted-separation roadmap reduces uniform consistency to convergence of the uncapped rate. These helpers prove that reduction from two-sided risk bounds; they do not assert the still-open bounds themselves.
Capping a nonnegative sequence at one preserves convergence to zero. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The rate is nonnegative, including the zero-sample convention for division. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The capped paper rate vanishes exactly when its uncapped ratio vanishes. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Worst-case squared observed risk is nonnegative without a boundedness assumption. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Every admissible estimator has worst-case risk at least the minimax value. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Once the uniform lower bound and the explicit estimator's upper bound are proved, their risk sandwich gives the roadmap's exact triangular consistency criterion. The bounds are inputs to this assembly lemma, not new model assumptions. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.Estimator 42 declarations The final estimator is a finite sum over counts and marks.
Observable capped-Poisson Jackson factorial estimator
The final estimator is a finite sum over counts and marks. The Jackson polynomial is selected from the canonical tensor convolution representation.
For the displayed parameters, sampleCellCount is the object specified by this definition.
For the displayed parameters, sampleArmCount is the object specified by this definition.
For the displayed parameters, sampleSuccessCount is the object specified by this definition.
For the displayed parameters, projectUnit is the object specified by this definition.
For the displayed parameters, empiricalValue is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, jacksonDegree is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, poissonIntensityFormula is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, markedCount is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, pilotCenterFormula is the object specified by this definition.
For the displayed parameters, pilotHalfWidthFormula is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, pilotLower is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, pilotUpperFormula is the object specified by this definition.
Definition (Lean source)
Pilot empirical mass on the paper's positive intensity domain. For the displayed parameters, pilotCenter is the object specified by this definition.
Pilot half-width with all positive calibration inputs explicit. For the displayed parameters, pilotHalfWidth is the object specified by this definition.
Definition (Lean source)
Pilot upper endpoint on the positive width and intensity domain. For the displayed parameters, pilotUpper is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, pilotMidpoint is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, pilotRadiusFormula is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, pilotRectangle is the object specified by this definition.
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the displayed parameters, jacksonPolynomialPair is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, jacksonCoeff is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, factorialCellValue is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, armRadiusFormula is the object specified by this definition.
For the displayed parameters, armWeightFormula is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, clippingScaleFormula is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, clippedCellValueFormula is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, cappedStatisticFormula is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, poissonWeight is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, armwiseEstimatorFormula is the object specified by this definition.
Definition (Lean source)
The Poisson comparison intensity for a positive sample size. For the displayed parameters, poissonIntensity is the object specified by this definition.
Definition (Lean source)
The pilot radius on the positive width, intensity, and logarithm domain. For the displayed parameters, pilotRadius is the object specified by this definition.
Definition (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
An arm radius is the sum of two strictly positive coordinate radii.
Definition (Lean source)
Sensitivity on nonnegative pilot centers and the public positive overlap domain.
Definition (Lean source)
The paper's strictly positive clipping scale; the unrestricted analytic extension is clippingScaleFormula.
For the displayed parameters, clippedCellValue is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, cappedStatistic is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, armwiseEstimator is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, armwiseEstimatorWitness is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, armwiseWorstRisk is the object specified by this definition.
Definition (Lean source)
Worst-case causal squared risk of the same observed-sample armwise estimator.
Definition (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.FixedSampleFactorial 7 declarations Deterministic sample split and multinomial factorial statistic
Deterministic sample split and multinomial factorial statistic
For the displayed parameters, pilotSize is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, evalSize is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, pilotIndices is the object specified by this definition.
For the displayed parameters, evalIndices is the object specified by this definition.
For the displayed parameters, pilotCount is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, evalCount is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, multinomialFactorialLift is the object specified by this definition.
Definition (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.JacksonPacket 9 declarations Localized high-frequency Jackson packet
Localized high-frequency Jackson packet
For the displayed parameters, packetKernel is the object specified by this definition.
For the displayed parameters, kernelCoeff is the object specified by this definition.
For the displayed parameters, packetCoeffPlus is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, packetCoeffMinus is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, packetOscillation is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, packetAntideriv is the object specified by this definition.
For the displayed parameters, torusDistance is the object specified by this definition.
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerDense 15 declarations The absolute-value Fejér certificate supplies symmetric, supported, moment-matched priors with an inverse-degree gap, as required by (43)--(44).
Dense boundary-propensity lower experiment
The absolute-value Fejér certificate supplies symmetric, supported, moment-matched priors with an inverse-degree gap, as required by (43)--(44). The two treated Poisson coordinates have the exact Gram identity (47); the untreated coordinates are common to both hypotheses and contribute one.
The Fejér inverse approximation bound and the symmetric dual-prior construction give the inverse-degree absolute-value gap in (44). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Symmetry cancels the signed first moment, so only the absolute-value moment contributes to the centers of the target in (46). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the displayed parameters, denseTreatedMean is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, denseTreatedLaw is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, denseTreatedLikelihood is the object specified by this definition.
Definition (Lean source)
Legal amplitudes and supported prior parameters yield legal Poisson means. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (47): both treated outcomes contribute, giving exactly 4 r a². The calculation is valid at support endpoints, including zero alternative means. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The dense likelihood is jointly measurable in parameter and counts. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
A supported parameter yields a nonnegative genuine likelihood. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The two-coordinate likelihood recovers the actual Poisson law, even when a supported endpoint makes one alternative intensity zero. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The dense treated counts form a measurable probability experiment. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
For the displayed parameters, denseTreatedKernel is the object specified by this definition.
Definition (Lean source)
The symmetric priors are concentrated on the radius-one support used in the exponential-Gram mixture theorem. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Moment annihilation through K removes all lower terms in (47). The product-mixture testing distance is at most d times the square root of the remaining exponential tail, exactly as in the dense splice. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Universal choices of the amplitude coefficient and logarithmic degree make the dense product mixture TV at most 1/8. The calibration condition r a² ≤ η K is provided by the amplitude choice (45). In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerDenseFullCounts 15 declarations The untreated counts have a common law.
Dense lower bounds with all observed Poisson counts
The untreated counts have a common law. Mixing the full experiment factors this law out of each predictive mixture, so the treated-count TV bound and the target concentration prove the same lower bound for full-count estimators.
The two untreated outcomes in every cell are independent Poisson counts with the common intensity q = B n (1 - ε)/(2 d).
Full counts, arranged as treated counts followed by untreated counts.
Definition (Lean source)
The full-count fibre is the product of the treated experiment and its parameter-independent untreated law. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The full count experiment has probability fibres. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The untreated law factors out of the prior-predictive mixture. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Adding all untreated counts cannot increase the predictive TV bound. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Reorder all four observed counts into treated and untreated blocks, with outcome false at index zero and outcome true at index one.
Definition (Lean source)
The full dense kernel is exactly the independent Poisson counts of the legal observed law, after a reversible reordering of all four coordinates. No coordinate of the observed experiment is discarded. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The dense fuzzy-testing step (48): concentration and likelihood TV are both derived; the alphabet condition makes target deviations negligible. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The Fejér symmetric priors attain the dense risk order a²/K². The separation is proved by the approximation certificate, never assumed. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Above a universal alphabet cutoff the logarithmic dense experiment has risk at least a universal multiple of a²/K_d², with concentration derived. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Return the full Poisson experiment to the usual observed histogram alphabet, using the inverse of the count reordering.
Definition (Lean source)
On the prior support the full histogram kernel is precisely the independent four-cell observed Poisson experiment. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reordering all observed counts preserves the squared Bayes risk exactly. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The dense lower bound holds for arbitrary estimators using every observed histogram count, with the legal observed value as its target. The priors, gap, concentration and full-likelihood TV bound are proved. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerDenseObserved 16 declarations Construct the boundary-propensity law in (45) and identify its target with (46), the target used by the proved dense concentration and testing bounds.
Legal observed laws for the dense lower experiment
Construct the boundary-propensity law in (45) and identify its target with (46), the target used by the proved dense concentration and testing bounds.
Four observed atom masses for uniform cells, boundary propensity ε, untreated mean one half and treated mean one half plus a θ.
Definition (Lean source)
Legal amplitudes make every observed atom nonnegative. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The four atom masses sum to one over the uniform finite alphabet. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The dense construction is an actual probability law, including the endpoint amplitudes where a Bernoulli atom can vanish.
Definition (Lean source)
The probability-law construction preserves the specified real masses. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Uniform cells, boundary propensity and the two specified outcome means hold exactly; thus the dense construction belongs to the observed class. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The legal dense observed target is precisely the target already used in the dense Bayes-risk bound, rather than an auxiliary surrogate. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the full observed Poisson experiment the treated intensities are exactly those in the proved dense likelihood calculation (47), and the untreated intensities are common to every parameter vector. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full dense Poisson experiment has total mean Bn, with no random normalizer penalty, as required in the transfer following (49). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Clip only outside the supported dense prior interval.
Every extended parameter gives a legal Bernoulli mean. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Clipping leaves all prior-supported parameters unchanged. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Clipping the negative tail does not change the bounded positive part. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
A legal dense observed law for every parameter vector; on the prior support this is exactly (45).
Definition (Lean source)
The all-parameter legal model has exactly the measurable target used in the testing theorem. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The dense testing bound applies to the actual legal observed value. The Fejér priors and their separation, target concentration, and Poisson mixture TV bound are all supplied by the proved dense lower theorem. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerDenseRisk 14 declarations The target in (46) is the average positive part of the symmetric prior parameters.
Dense target concentration and fuzzy testing
The target in (46) is the average positive part of the symmetric prior parameters. Its variance is at most a²/d, giving the dense testing step (48). The extension below clips only outside the legal prior support.
For the displayed parameters, densePositivePart is the object specified by this definition.
For the displayed parameters, densePriorTarget is the object specified by this definition.
Definition (Lean source)
The positive-part extension is measurable. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The extended dense target is measurable. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
On the legal support the extension gives exactly the summand in (46). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Symmetry identifies the positive-part expectation with half the absolute moment. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independent dense prior coordinates concentrate the target around its symmetric scalar center, with no assumed concentration inequality. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Chebyshev supplies the dense prior target-deviation probabilities. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the displayed parameters, denseProductPoissonKernel is the object specified by this definition.
Definition (Lean source)
The product kernel has probability fibres. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Mixing the product kernel gives the predictive law of the proved TV bound. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The dense fuzzy-testing step (48): concentration and likelihood TV are both derived; the alphabet condition makes target deviations negligible. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The Fejér symmetric priors attain the dense risk order a²/K². The separation is proved by the approximation certificate, never assumed. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Above a universal alphabet cutoff the logarithmic dense experiment has risk at least a universal multiple of a²/K_d², with concentration derived. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerFiniteAlphabet 7 declarations The last step of the lower-bound roadmap uses a common Bernoulli mean shift.
The finite-alphabet boundary-propensity lower experiment
The last step of the lower-bound roadmap uses a common Bernoulli mean shift. Uniform covariate labels carry no information about that shift, so this submodel has the same information as the single occupied cell experiment.
The constant dense parameter has exactly the scalar shifted target. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The central law has positive mass at every atom, so every shifted law is absolutely continuous with respect to it. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Real singleton masses agree with the observed atom coordinates. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The exact one-observation information is four times the overlap floor and the squared mean shift, independently of the covariate alphabet. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Tensorization and a small information budget give a fixed-sample squared-risk testing floor for the legal constant boundary submodel. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The boundary-propensity two-point experiment yields the parametric fallback uniformly over every finite alphabet, with no alphabet cutoff. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The parametric fallback covers the finite exceptional set below the large-alphabet cutoff. Together the two experiments give the paper rate for every legal sample size, alphabet and overlap floor. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerHistogramTransfer 9 declarations The ordered-prefix law pays only the short-count probability.
Fixed-sample estimators in the lower Poisson count experiment
The ordered-prefix law pays only the short-count probability. Uniform histogram reconstruction and kernel averaging then give a deterministic, parameter-free count estimator with the same risk bound, including parameter-dependent rates.
Read a fixed prefix and project the fixed-sample estimator to the unit interval. For the displayed parameters, lowerPrefixEstimator is the object specified by this definition.
Definition (Lean source)
The exact prefix pushforward bounds its risk by fixed risk plus shortage. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Average the reconstructed prefix over all orderings of a histogram. This estimator depends on the fixed estimator and fallback only.
Definition (Lean source)
The deterministic count estimator is measurable on the observed histogram space. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Reconstruction followed by Jensen transfers the risk to all observed counts. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A mean at least Bn/2 gives the uniform shortage penalty from roadmap (49). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independent count rates agree with the four observed atom masses. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The same parameter-free count estimator transfers every dense fibre. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The transfer also allows the sparse total rate to depend on its normalizer. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerPriorTransfer 8 declarations Integrate the parameter-free histogram comparison over the legal packet and Fejér priors.
Integrating the fixed-sample lower comparison
Integrate the parameter-free histogram comparison over the legal packet and Fejér priors. Both full-count Bayes bounds give fixed-sample minimax lower bounds, with only the explicit Poisson shortage penalty from roadmap (49).
Finite sample estimators have uniformly bounded observed risk, because the sample alphabet is finite and the observed value lies in the unit interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging a projected prefix leaves the histogram statistic bounded by one. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
A bounded histogram estimator's nonnegative integral loss agrees exactly with the ENNReal squared risk used by fuzzy testing. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
On legal sparse vectors, integrating the fibre transfer costs at most the fixed estimator's worst-case risk plus the uniform shortage penalty. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The packet lower experiment yields a fixed-sample sparse minimax bound. Both prior risks are bounded by the same fixed estimator's worst-case risk; thus only the uniform Poisson shortage term is lost in the comparison. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Supported scalar dense priors put every product coordinate in the legal parameter interval, so clipping has no effect on the comparison experiment. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The dense full-count prior comparison integrates to the same fixed-sample worst risk and shortage penalty as the sparse comparison. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The Fejér dense lower experiment transfers to fixed-sample minimax risk, retaining its a²/K² order and subtracting only the explicit shortage penalty. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerRateCalibration 2 declarations Roadmap (33), (40), and (45)--(48) optimize the supported sparse endpoint and the legal dense amplitude.
Choosing the lower-experiment endpoint and amplitude
Roadmap (33), (40), and (45)--(48) optimize the supported sparse endpoint and the legal dense amplitude. These bounds retain the explicit fixed-sample shortage penalty; no testing or approximation conclusion is assumed.
Choosing the endpoint in (33) gives the capped sparse rate in (40), whenever the intensity-dependent endpoint is at least two. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Taking the square root of the largest legal dense squared amplitude optimizes (48), including the amplitude cap needed for Bernoulli legality. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerRateSplice 4 declarations The complementary endpoint ranges in roadmap (40) and (48) give one large-alphabet lower bound.
Splicing the sparse and dense lower experiments
The complementary endpoint ranges in roadmap (40) and (48) give one large-alphabet lower bound. Different universal logarithmic degrees in the two experiments are compared explicitly. The Poisson shortage penalty is absorbed by a universal inflation, yielding the exact paper rate.
The sparse packet experiment and the dense boundary experiment together cover every intensity, with a single positive lower constant and alphabet cutoff. This is the range splice in (40)--(48), before absorbing (49). In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Comparing the rounded degree with the paper logarithm converts the spliced bound to the exact capped rate, uniformly in the inflation B. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Squaring the inverse-inflation exponential bound makes the shortage penalty negligible compared with the lower constant's 1/B scaling. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
One universal inflation absorbs the Poisson shortage penalty, completing the large-alphabet fixed-sample lower bound in the exact paper rate. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerSparse 9 declarations Pointwise envelope and normalization bounds used in equations (37)--(39) of the weighted-separation proof roadmap.
Sparse target normalization
Pointwise envelope and normalization bounds used in equations (37)--(39) of the weighted-separation proof roadmap.
The positive-part functional is nonnegative and bounded by its cell normalizer. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A bounded nonnegative intensity has second moment scale at most M times its mean. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The scalar envelope gives the second-moment scale in roadmap equation (37). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The sparse denominator stays above one half throughout the closed overlap range. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The empirical average of the scalar functional is between zero and S_d. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Normalization perturbs H_d by at most the denominator error, as in equation (38). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The normalized target is close to a deterministic prior center by two errors. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Applying the exact sparse likelihood identity gives the target-center estimate for the actual observed law, including arbitrary boundary intensities. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating the pointwise estimate reduces target concentration to the two second moments appearing in roadmap equations (37)--(39). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerSparseCalibration 5 declarations The even logarithmic degree from (32) makes the target concentration condition (39) hold above a universal alphabet cutoff.
Universal sparse alphabet calibration
The even logarithmic degree from (32) makes the target concentration condition (39) hold above a universal alphabet cutoff. This removes the numerical concentration premise from the explicit packet Bayes lower bound.
For the displayed parameters, lowerLogDegree is the object specified by this definition.
Definition (Lean source)
Rounding the degree preserves its logarithmic lower bound and costs at most two logarithmic units, uniformly for every legal alphabet. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Logarithmic degree squared is negligible relative to alphabet size. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Proof (Lean source)
A single alphabet cutoff enforces the target-deviation bound (39) for all endpoints and overlap floors in the theorem's range. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Above a universal alphabet cutoff the explicit packet yields the sparse Bayes lower order without any assumed concentration or testing bound. All numerical side conditions are derived from the logarithmic degree. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerSparseFullCounts 10 declarations Reorder the four counts in each cell without losing any observations.
Sparse lower bounds for the full observed histogram
Reorder the four counts in each cell without losing any observations. Identify this experiment with the inflated Poisson counts of the normalized sparse law, and transport the packet Bayes lower bound to arbitrary histogram estimators.
All observed histogram counts, reversibly arranged into four-count cells.
Definition (Lean source)
The observed histogram version of the full sparse four-count experiment.
Definition (Lean source)
The full observed experiment has probability fibres. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Normalization of the observed law cancels the total-mean inflation, yielding exactly the four unnormalized Poisson intensities in (34). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reordering the independent observed counts gives precisely the full sparse product experiment. The Poisson total mean is B n S, as in (49). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Undoing the count reordering recovers the exact independent Poisson histogram law of the legal sparse observed model on the prior support. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every histogram estimator has exactly the same Bayes risk after the reversible arrangement into cells; none of the four counts is discarded. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Clip only outside the prior support to obtain a legal normalized sparse observed model at every centered parameter vector. For the displayed parameters, sparseObservedModel is the object specified by this definition.
Definition (Lean source)
The legal observed model has exactly the normalized target used in sparse concentration and fuzzy testing. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The explicit packet sparse lower order holds for every estimator using all observed histogram counts and the actual legal observed value as target, with concentration and likelihood closeness derived from the packet construction and the logarithmic alphabet cutoff. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerSparseMoments 7 declarations Roadmap equation (37) follows from bounded intensities with common first moment one and independence across cells.
Sparse prior concentration
Roadmap equation (37) follows from bounded intensities with common first moment one and independence across cells. Square integrability is derived from the support envelope, rather than imposed as an extra premise.
A supported intensity of mean one has variance at most its support endpoint. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The functional envelope yields the scalar variance bound in (37), uniformly including zero overlap and the upper boundary of the intensity support. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independent cell variances give the inverse-alphabet concentration factor for their average; the cells need not have identical distributions. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The empirical average of the positive-part functional has the H_d variance bound of (37), derived from the intensity support and first moments. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The sparse denominator has expectation one, so its squared error about one is its variance. This proves the S_d assertion of roadmap (37). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The H_d variance estimate is also its integrated squared deviation from its prior mean, the second assertion of (37) in precisely its roadmap form. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equations (37)--(39) control the normalized sparse target around its nonrandom prior center. This retains both denominator and numerator errors. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerSparseRisk 17 declarations The supported, mean-one product priors concentrate the normalized target around their scalar functional centers.
Sparse prior testing risk
The supported, mean-one product priors concentrate the normalized target around their scalar functional centers. Chebyshev and the full sparse product-mixture TV bound then give the auxiliary squared-risk lower bound in roadmap (40), before the fixed-sample transfer.
Extend a centered sparse intensity to the legal support by clipping. On either supported centered prior this equals the original intensity. For the displayed parameters, sparseClippedIntensity is the object specified by this definition.
Definition (Lean source)
The normalized sparse value, extended measurably to all centered vectors. The extension agrees with the actual sparse observed value on legal vectors. For the displayed parameters, sparsePriorTarget is the object specified by this definition.
Definition (Lean source)
Clipping puts every extended intensity in the legal interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the supported prior, translation followed by clipping is the identity. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full independent sparse Poisson experiment as a parameter kernel. For the displayed parameters, sparseProductPoissonKernel is the object specified by this definition.
Definition (Lean source)
Clipping is measurable, including the endpoints of the intensity support. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The extended target is a measurable function of the centered vector. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Translation and clipping preserve every measurable prior integral on the support. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The extended sparse target stays in the unit interval at every vector. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Product copies of a supported mean-one prior satisfy the normalized target second-moment estimate (39), with the center expressed as a scalar prior integral. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Chebyshev converts the derived sparse target second moment into the prior-tail bound used by fuzzy testing; no target concentration is assumed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The product sparse experiment has probability fibres at every centered vector. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Mixing the full sparse product kernel against the centered product prior is exactly the product predictive law bounded in (36). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equations (36)--(40), before fixed-sample transfer: the exact supported priors and their derived concentration give an estimator-wise Bayes-risk lower bound. The numerical alphabet condition is (39); the likelihood closeness is proved by the sparse full-likelihood theorem, not assumed. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The explicit Jackson-packet witness attains the auxiliary sparse testing lower order M/K². Both its expectation gap and its mixture TV bound are proved, and (39) is exposed as a numerical alphabet condition to be calibrated in the final sparse/dense assembly. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The centered product priors put all their mass on legal sparse vectors. Thus the extensions used in testing do not introduce illegal prior parameters. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On every legal vector the testing target is exactly the value of the normalized sparse observed law in the paper, by the full likelihood identity. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerSparseTV 5 declarations The four-coordinate Poisson laws form a measurable probability kernel.
Total variation for the sparse product-Poisson mixtures
The four-coordinate Poisson laws form a measurable probability kernel. The supported moment-matching API converts their exact Gram formula into the product total-variation estimate in roadmap equation (36).
The sparse Poisson experiment is measurable as a function of intensity. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The centered sparse experiment, with probability fibres at every real parameter. For the displayed parameters, sparseCenteredPoissonKernel is the object specified by this definition.
Definition (Lean source)
Moment-matched packet priors have product-mixture TV bounded by the alphabet size times the square root of the tail from equation (34). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A geometric one-cell error becomes at most 1/8 after tensorization when the degree exceeds a universal multiple of log(ed). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (34)--(36): one universal small support scale and one universal logarithmic degree scale make the full sparse product experiments indistinguishable. The support constraint is precisely the second branch of (33). In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerSparseTesting 8 declarations Centering the explicit constrained priors preserves their matched moments and places their support in the radius-M/2 interval.
Sparse moment-matched likelihood separation
Centering the explicit constrained priors preserves their matched moments and places their support in the radius-M/2 interval. The full four-coordinate Poisson Gram identity then gives the unmatched exponential-series bound (34).
Translating a supported prior by its reference midpoint gives support radius M/2. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every centered moment through K agrees for the completed packet priors. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full sparse likelihood is jointly measurable in its intensity and counts. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Legal sparse intensities give nonnegative likelihoods on every count vector. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The scalar Poisson likelihood recovers each atom, including zero intensity. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full four-coordinate sparse likelihood is the actual Poisson density, so the Gram calculation applies to probability experiments rather than merely formal functions of the counts. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (34): moment matching removes every low-degree term in the full four-coordinate Poisson mixture, with the exact midpoint radius. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact full-likelihood series argument obeys the scalar upper bound in (34), including the two untreated-outcome coordinates. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.LowerTransfer 18 declarations Identification and causal completion preserve the attained risks, their worst-case supremum, and the all-estimator minimax value.
Lower Transfer scaffold
Identification and causal completion preserve the attained risks, their worst-case supremum, and the all-estimator minimax value. The remaining Poisson shortage estimate in roadmap (49) is proved uniformly over the sparse normalizer. Projection and the first-label risk transfer below implement the loss comparison after (49); constructing the label map from the count experiment remains open.
Identification makes the causal risk equal the risk at the observed margin. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every risk attained in either model class is attained in the other: observed margins give one inclusion and causal completion gives the reverse. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each estimator has the same worst-case risk for the observed and causal targets. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Identification and completion preserve the armwise estimator's worst-case risk. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Taking the infimum over the shared estimator class preserves the exact risk equality. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A two-sided observed minimax bound transfers unchanged to the causal target. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Squared observed risk is nonnegative for every estimator and observed law. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The admissible deterministic armwise estimator upper-bounds the minimax infimum. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The lower Gaussian Poisson tail gives the exact shortage exponent before uniformizing over the normalizer in roadmap (49). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The shortage exponent increases above n. Evaluating it at Bn/2 gives exactly the exponent in roadmap (49). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Any Poisson experiment with total mean at least Bn/2 satisfies the uniform shortage probability in roadmap (49). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The sparse normalizer is at least one half, so the conditional total count of every legal sparse experiment obeys the same shortage bound. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The uniform shortage estimate applies to a count on any probability space once its conditional Poisson law has been established. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Exponential shortage can be made an arbitrarily small inverse-sample penalty by increasing its positive exponent coefficient. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A single universal inflation B makes the shortage penalty smaller than any specified positive multiple of 1/n, uniformly over all sample sizes. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every finite observed estimator can be projected without increasing its risk. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Use the first n labels on a sufficiently large count and zero on shortage. If the label block has the fixed-sample law, projection and an indicator bound transfer its risk with at most the shortage probability as an additive penalty. The label block may include unobserved continuation labels on shortage; the transferred statistic uses none of them there. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Combining the first-label transfer with (49) gives the uniform Poisson penalty used in both the sparse and dense lower experiments. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.PacketCompletion 4 declarations Moment annihilation and weighted normalization give the exact identity t + u = 1/2.
Common-atom completion of the explicit Jackson packet
Moment annihilation and weighted normalization give the exact identity
t + u = 1/2. Consequently the packet parts admit the common-atom
completion from roadmap (6)--(7), with no loss in their kink response.
Strict positivity of the weight is proved for the paper's range, so the
explicit prior witness has no normalization premise. The uniform kink-response
bound remains open.
Degree-zero annihilation equates the actual masses of the two packet parts. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equal degree-zero and degree-one moments split the combined weighted normalization equally between the two Jordan parts, as in roadmap (6). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Positive weight makes the concrete packet admissible for the common-atom map: its positive mass is at most one half, hence strictly less than one. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The explicit packet completes to probability priors supported on [0,M], with mean one and matching moments through K. The common atom lies in [1/2,2], and the objective gap is exactly the normalized circle response. This assembles the construction portion of roadmap (30), using proved positivity of the normalization weight. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.PacketIntegrationByParts 8 declarations The two integrations retain the endpoint slopes on each smooth arc.
Integration by parts for the localized packet
The two integrations retain the endpoint slopes on each smooth arc. These boundary terms supply the kink atoms in roadmap (25).
Finite Fourier construction supplies all differentiability needed for integration by parts, without extra packet regularity hypotheses. The stated conclusion holds.
Formal statement
Proof (Lean source)
Twice integration by parts on one smooth arc, with the actual translated Jackson packet. The endpoint slopes are retained rather than discarded. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact intensity and speed at the two kinks. The speed determines the atomic mass, uniformly in the overlap parameter. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the central arc the intensity is strictly above one; on the outer arcs it is strictly below one. Endpoints are excluded to retain kink atoms. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Differentiating the periodic Fourier series retains the circle period, so the outer boundary terms cancel in integration by parts. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Proof (Lean source)
Twice integration by parts on the three smooth arcs, with both derivative jumps retained. This is roadmap (25), for any translated packet center. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Evenness of the finite cosine antiderivative identifies the opposite kink in the exact response formula. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The uniform lower response of one localized packet, roadmap (28). The universal scale suppresses both the opposite kink and the smooth term; no response bound or integration identity is assumed. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.PacketKinkSeparation 5 declarations Roadmap (26)--(27): the circular distance between the kinks stays at least four times the inverse square root of M.
Separation of the two packet kinks
Roadmap (26)--(27): the circular distance between the kinks stays at least four times the inverse square root of M. Jackson antiderivative localization therefore suppresses the opposite atomic contribution even when M = K².
The shortest arc between the two kinks passes through the endpoint π. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The opposite kink remains at circular distance at least 4/√M, including at the dense endpoint. This is the lower bound in roadmap (26). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Localization and kink separation give the opposite-center response bound C M/N³. This is the antiderivative estimate used in roadmap (27). In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The opposite atomic contribution has order M^(3/2)/N³, uniformly in M. Its coefficient is the actual derivative jump √(M-1)/2 of roadmap (24). In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
A universal packet scale prevents the opposite kink from canceling even half of the center response, uniformly over the full range M ≤ K². In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.PacketLowerOrder 29 declarations The positive and negative packet parts are finite measures supported on [0,M], with every polynomial moment integrable.
Concrete Jackson packet measures
The positive and negative packet parts are finite measures supported on [0,M],
with every polynomial moment integrable. These construction properties implement
roadmap (30). Exact pushforward, signed-pairing, and absolute-density formulas
recover the circle packet and its weighted normalization when the weight is
positive. The Fourier support argument proves matching of every moment through
degree K. Strict positivity and the kink-response lower bound remain open.
The cosine coordinate in the Jackson-packet lower construction.
Definition (Lean source)
The two translated, high-frequency Jackson waves centered at the kink.
Definition (Lean source)
The exact weighted variation used to normalize the signed packet.
Definition (Lean source)
Positive Jordan part of the normalized Jackson packet, pushed to [0,M].
Definition (Lean source)
Negative Jordan part of the same signed packet, pushed to [0,M].
Definition (Lean source)
The cosine coordinate is continuous on the entire circle parameter line. The stated conclusion holds.
Formal statement
Proof (Lean source)
Nonnegative endpoints put every cosine intensity in the desired support. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Pushing any measure through the cosine coordinate concentrates it on [0,M]; in particular no Jordan-part mass escapes the paper's interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The concrete positive packet is supported on the constrained-prior interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The concrete negative packet has the same constrained-prior support. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The translated packet wave is continuous, including zero degree. The stated conclusion holds.
Formal statement
Proof (Lean source)
Either Jordan density is integrable on the compact circle interval, even before positivity of the normalization weight is proved. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The compactly supported positive density defines a finite measure. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The compactly supported negative density also defines a finite measure. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Compact support makes every polynomial moment of both concrete packet parts integrable; no moment regularity premise is necessary. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The only remaining common-atom domain obligation for these concrete packet parts is the positive part's strict mass bound. Finiteness and first-moment integrability follow from the construction. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Change of variables and the real density formula recover either packet part exactly, without a positivity assumption on the normalization weight. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The signed difference of the pushed-forward packet parts is exactly the normalized circle pairing, as used in roadmap (30). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The sum of the two packet-part integrals is the absolute-density pairing; there is no loss of variation in the explicit positive/negative construction. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The circle normalization weight is nonnegative for the paper's support range. Its strict positivity is a separate Fourier/kink-response obligation. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
With positive normalization weight, the two explicit packet parts have combined weighted mass exactly one, the normalization in roadmap (30). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The normalization can be read directly as the sum of the two masses and first moments, ready for the degree-zero/one annihilation identities. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual kink objective has the exact signed-packet response, despite its irrelevant singular encoding outside the nonnegative supporting interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integer cosine modes are unchanged after a full circle turn. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Proof (Lean source)
Fourier reconstruction makes the packet periodic before translation. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Proof (Lean source)
Translation preserves the integral of a periodic function over one turn. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A translated high-frequency packet annihilates every low-frequency real trigonometric polynomial. This is the Fourier-support argument in (16). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every degree-at-most-K polynomial in the intensity has zero circle pairing with the explicit two-center packet, exactly as in roadmap (16). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual pushed-forward positive and negative packets match every moment through degree K; no positivity or moment-matching premise is assumed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.PacketPositivity 5 declarations Nonnegative Fourier coefficients, including a strictly positive coefficient at frequency one, make the Jackson kernel strictly maximal at its center.
Strict positivity of the explicit packet normalization
Nonnegative Fourier coefficients, including a strictly positive coefficient at frequency one, make the Jackson kernel strictly maximal at its center. The other translated wave therefore cannot cancel the centered wave at the kink. Continuity then gives strictly positive weighted variation.
Every normalized Jackson coefficient is nonnegative. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
At order at least two, the frequency-one coefficient is strictly positive. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A cosine strictly below one forces a strict drop from the kernel's center. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
At the kink, the centered wave dominates the other translated wave. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The explicit packet weight is positive throughout the paper's support range. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.PacketResponseLower 8 declarations Evenness adds the two localized responses in roadmap (29).
Separation attained by the completed Jackson packet
Evenness adds the two localized responses in roadmap (29). Fourier annihilation removes the affine term, and normalization followed by common-atom completion gives the explicit lower-prior witness in (30).
The modulated Jackson kernel is even, so reflection preserves its response. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The two kink centers give exactly equal responses, by reflection on the circle. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The whole packet pairs with the nonlinear remainder as twice one response. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Fourier annihilation removes the affine part of phi, retaining the exact sum of the two nonlinear kink responses in roadmap (29). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full unnormalized packet has a uniform response of order sqrt(M)/K, including zero overlap and the endpoint M = K². In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Normalization costs at most the universal weighted-variation bound 36. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The explicit common-atom completion attains the uniform weighted lower separation, with support, mean one, and all K moments supplied by the constructed constrained-prior pair, as required by roadmap (30). In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The attained packet gap forces the claimed order of the weighted best approximation error: every admissible polynomial has the same moment pairing, so the proved residual envelope bounds the gap before taking the infimum. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.PacketSmoothRemainder 17 declarations Roadmap (22) and (25): the absolutely continuous curvature of the scalar kink composition is uniformly bounded by a constant times M.
Smooth remainder in the packet response
Roadmap (22) and (25): the absolutely continuous curvature of the scalar kink composition is uniformly bounded by a constant times M. Its pairing with the localized twice antiderivative is therefore of order M/N².
The nonlinear remainder after subtracting the affine term in roadmap (10). For the displayed parameters, packetRemainder is the object specified by this definition.
The curvature on the upper smooth arc, by the chain rule. For the displayed parameters, packetUpperCurvature is the object specified by this definition.
Definition (Lean source)
The density of the smooth second derivative; values at the two kinks are set to zero, since the derivative jumps are handled separately as atoms. For the displayed parameters, packetSmoothCurvature is the object specified by this definition.
Definition (Lean source)
The affine term and the nonlinear remainder recover the original functional. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The cosine coordinate has the derivative used in roadmap (11). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The squared coordinate speed is z(M-z), keeping the curvature bound linear in M rather than quadratic. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The upper smooth branch has the rational slope stated in roadmap (22). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Differentiating the upper slope gives the actual chain-rule curvature. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On either open smooth arc the curvature density is exactly the ordinary second derivative of the nonlinear remainder composed with z(t). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The smooth upper-arc curvature is bounded by 5M, uniformly in ε. The speed identity is essential here: estimating the sine factor alone would give the wrong power of M. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Both smooth arcs obey the same linear-in-M bound from roadmap (22). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (22), stated directly for the original composed remainder on each smooth arc. No regularity or curvature hypothesis is assumed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite Fourier antiderivative is continuous. The stated conclusion holds.
Formal statement
Proof (Lean source)
Every integer Fourier frequency of the antiderivative has period 2π. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Proof (Lean source)
The smooth curvature density is measurable, despite the two jumps. The stated conclusion holds.
Formal statement
Proof (Lean source)
The smooth density is integrable on the circle, without additional regularity premises. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Circle translation preserves the Jackson L¹ bound, so the smooth term in roadmap (25) has absolute value at most CM/N² for every center. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.PacketWeightBound 5 declarations Roadmap (18)--(19): translating the two positive kernel envelopes together cancels their sine terms.
Uniform weighted variation of the Jackson packet
Roadmap (18)--(19): translating the two positive kernel envelopes together cancels their sine terms. The second Jackson moment then bounds the weight uniformly, including the endpoint M = K².
Fourier reconstruction gives the kernel period needed for circle translation. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The sum of the translated weights has no sine term; both centers are at z = 1. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Positive kernel envelopes dominate the absolute modulated packet pointwise. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A translated weighted kernel integral can be moved back to its center. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The normalizing weighted variation is universally bounded throughout the paper's full range. This is roadmap (19), with the explicit constant 36. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.SparseFamily 15 declarations Normalized sparse family and its full four-coordinate Poisson likelihood
Normalized sparse family and its full four-coordinate Poisson likelihood
For the displayed parameters, sparseNormalizerFormula is the object specified by this definition.
Normalizing mass on the public positive-overlap domain. For the displayed parameters, sparseNormalizer is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, sparseUnnormalizedMass is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, sparseMass is the object specified by this definition.
Definition (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the displayed parameters, sparseLaw is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, sparseReference is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, poissonCellMean is the object specified by this definition.
For the displayed parameters, poissonCellLaw is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, oneCellLikelihood is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, sparseGramCoefficient is the object specified by this definition.
Definition (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperAggregation 4 declarations Roadmap equations (30) and (32) aggregate cellwise pilot second moments and square-root approximation biases.
Finite-sum bounds for upper-risk aggregation
Roadmap equations (30) and (32) aggregate cellwise pilot second moments and square-root approximation biases. These lemmas retain null cells and use only the probability-mass normalization and the active-branch rate bound.
Equation (30): probability masses control the squared sum of their square roots. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The square-root part of the bias in (32) has squared size at most R. The positive scale is m ε L in the active branch. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (32) with an explicit universal constant on the active branch R ≤ 8. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (30): summing a cellwise radius-second-moment estimate uses only total mass one. Here v is the second moment already established by the pilot calculation (19). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperArmMean 13 declarations Roadmap equation (5) combines the centered selected-arm variance with the empty-arm contribution.
Bernoulli arm-mean second moments
Roadmap equation (5) combines the centered selected-arm variance with the empty-arm contribution. The finite observed law allows boundary means and null cells throughout the residual calculation.
Multiplying the totalized arm mean by its arm mass recovers the success mass, including a null arm. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Integrals restricted to one observed arm reduce to its two outcome atoms. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The binary outcome residual is centered on every arm, including null arms. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The binary residual second moment is at most one quarter of the arm mass. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The sum of squares of selected-arm averaging coefficients is the totalized inverse count. This is the finite-design variance factor in equation (5). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The selected design-weighted residual is the centered empirical numerator scaled by its arm count; at an empty arm it is zero. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional Bernoulli centering removes cross-coordinate terms even though the averaging denominator depends on the entire observed design. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Separating the empty arm from the centered numerator gives the exact pointwise variance-plus-empty-arm decomposition. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (5) for an actual observed arm. The inverse occupied-count term and the empty-arm term are bounded separately using equation (4). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Occupied-cell propensity overlap gives the same lower mass bound in each arm. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Multiplying equation (5) by cell mass removes the unknown cell mass from its bound. Null cells vanish before any division. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (6): the squared mass-weighted maximum arm error is at most 3d/((n+1)ε), using the two Bernoulli arm-mean bounds. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The projected empirical-ratio estimator has the parametric upper bound needed on the bounded-alphabet branch; both terms in equation (6) are derived under the actual iid law. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperBadPilotAggregation 6 declarations The exponential estimates in (22) absorb the clipping inflation and yield an alphabet-decaying cell loss.
Aggregating actual bad-pilot losses
The exponential estimates in (22) absorb the clipping inflation and yield an alphabet-decaying cell loss. Summing these actual losses on the active branch gives the variance-scale rate in (31), including null cells.
An exponential tail at the logarithmic alphabet scale absorbs any smaller prescribed polynomial inflation and decay. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The precise squared clipping inflation in (22) is absorbed by the exponential bad-pilot tail, retaining the paper's d⁻⁴ factor. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual bad-pilot cell loss has the d⁻⁴ bound in (22), without an occupied-cell premise: null cells are localized almost surely. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the active branch, d times the summed actual bad-pilot squared loss is at most a universal multiple of d/(m ε L). This controls both its variance contribution and the Cauchy–Schwarz bound for its total bias. No cross-cell or evaluation-count independence is required. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual absolute bad-pilot error retains the d⁻² decay in (22), including null cells and arbitrary evaluation counts. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The total actual bad-pilot absolute bias, squared after summing cells, is controlled on the active branch. No cross-cell independence is needed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperBadPilotCenter 7 declarations The fourth marginal score moment and the rectangle failure probability give an exponentially small second moment for each coordinate on any pilot failure.
Coordinate moments on failed pilot rectangles
The fourth marginal score moment and the rectangle failure probability give an exponentially small second moment for each coordinate on any pilot failure. Unlike an aggregate mass bound, this retains each coordinate's true mass for the armwise inverse-propensity weighting in roadmap (22b). The actual pilot-center functional inherits these moments through the armwise modulus; summing outcome masses retains one inverse-overlap power in its mass term.
Every coordinate score moment through degree four has its own true-mass scale, obtained from the marginal Poisson law and the raw-score comparison. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Even when a different coordinate fails localization, a coordinate's second score moment is exponentially small with its own mass scale. Hölder uses the marginal fourth moment and the full rectangle failure probability; no coordinate independence is needed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A weighted coordinate score retains each weight next to its own true-mass scale on rectangle failure. This is the finite Cauchy–Schwarz assembly needed before substituting inverse arm propensities in roadmap (22b). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual pilot-center functional has an exponentially small second moment on rectangle failure. Each inverse propensity remains attached to its own coordinate mass, before any overlap-floor simplification. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing the two outcome masses before applying overlap preserves one inverse-overlap power in the mass term of the bad-pilot second moment. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The center-value component of roadmap (22) has the required normalized mass and overlap scales on failed rectangles, without coordinate independence. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The center-error first moment on failed rectangles follows from its normalized second moment and the exponentially small failure probability. This completes the center component of roadmap (22), retaining the square root of one inverse-overlap power in the mass term. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperBadPilotClipped 3 declarations The width and center estimates in roadmap (22) control the actual cell statistic on bad pilots, as required after (28).
Actual clipped-cell moments on failed pilot rectangles
The width and center estimates in roadmap (22) control the actual cell statistic on bad pilots, as required after (28). Evaluation counts may be arbitrary: clipping supplies the pathwise bound without evaluation moments.
The pilot center functional is square-integrable by domination by total midpoint mass. This regularity holds on failed rectangles as well. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On failed pilot rectangles, the actual clipped occupied-cell absolute error is exponentially small on the normalized mass and overlap scales of (22). No law or moment assumption on evaluation counts is needed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On failed pilot rectangles, the actual clipped occupied-cell loss is exponentially small on the normalized mass and overlap scales of (22). No law or moment assumption on evaluation counts is needed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperBadPilotScale 4 declarations The clipping-scale component of roadmap (22) follows from its affine square envelope and the joint first score moment on rectangle failure.
Clipping-scale moments on failed pilot rectangles
The clipping-scale component of roadmap (22) follows from its affine square envelope and the joint first score moment on rectangle failure. The midpoint and failure event remain coupled throughout the argument.
The total midpoint mass is at most the true mass plus the aggregate deviation-and-width score, including failed pilots. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The bad-pilot second moment of the clipping scale has an exponential factor multiplying only mass-normalized deviations. The probability term and joint score term are both derived from the independent Poisson laws. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The clipping-scale component of (22) has the same mass and overlap scales as (19), with an exponentially small multiplier. In particular the mass term has only one inverse-overlap power even on failed pilot rectangles. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cauchy–Schwarz couples the failed-rectangle probability to its clipping-scale second moment, giving the first-moment component of roadmap (22). The mass term retains a square root of one inverse-overlap power. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperBias 9 declarations On the localization event, the empirical half width is controlled by the true coordinate's square-root scale.
Localized pilot geometry for Jackson bias
On the localization event, the empirical half width is controlled by the true coordinate's square-root scale. The boundary-distance factor loses its additive level term, including at zero coordinates. These are the deterministic pilot inputs to roadmap equations (11) and (20).
Solving the localization inequality replaces the empirical square-root scale by the true coordinate scale plus a level-sized remainder. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The localized half width has a true-mass envelope with a constant depending only on the universal pilot multiplier. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
For a localized nonnegative interval, its boundary-distance product is controlled by true mass times level, with no level-squared remainder. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the actual pilot interval, the coordinate half width obeys the true-mass envelope used before equation (20). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual pilot face-distance factor retains the true coordinate's square-root scale, and vanishes at a zero coordinate. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The coordinate radius is bounded by the same true-mass scale as its half width whenever the true coordinate lies above the pilot lower endpoint. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On a localized rectangle, summing the coordinate radius bounds gives the true arm-mass scale used in equation (20). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The arm's two boundary-distance factors have no additive level remainder, including arms with zero true mass. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The localized boundary factors keep the inverse arm masses attached to their coordinates. Applying the observed armwise square-root bound (21) produces one square-root inverse-overlap factor, as needed for (20). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperBinomialCounts 12 declarations Roadmap equation (4) controls the inverse occupied-arm count and the empty-arm probability.
Binomial count bounds for the empirical-ratio branch
Roadmap equation (4) controls the inverse occupied-arm count and the empty-arm probability. These bounds retain the extra trial in the denominator and allow success probability one.
A function of the success count in iid Boolean trials has the binomial expectation. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (4)'s reciprocal bound for iid Boolean success counts. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Empty iid Boolean counts have the exact binomial zero probability. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The probability of no binomial successes is bounded by the reciprocal expected count with one extra trial, as in equation (4). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The empty-count expectation obeys the second inequality in equation (4). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A measurable event indicator pushes its probability law to the Boolean Bernoulli law. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Under iid sampling, any function of an event count has the binomial expectation. This transports equation (4) from Boolean trials to actual observed-category counts. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The event selecting one covariate cell and treatment arm has mass equal to its atom sum. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The observed arm count has the binomial expectation formula under the actual iid law. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (4)'s occupied-count reciprocal bound for an observed cell and arm. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Empty observed arms have the exact binomial zero probability, including null arms. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (4)'s empty-arm probability bound holds for every occupied observed arm. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperBoundedAlphabet 2 declarations The empirical-ratio risk bound from roadmap equations (4)–(6), together with unit-range loss, gives the headline minimum-rate bound whenever d is below the fixed universal cutoff.
Completed bounded-alphabet upper branch
The empirical-ratio risk bound from roadmap equations (4)–(6), together with unit-range loss, gives the headline minimum-rate bound whenever d is below the fixed universal cutoff. No unknown cell mass enters the final constant.
Below a fixed alphabet cutoff, the logarithmic rate scale is uniformly bounded. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the bounded-alphabet branch the exact headline estimator satisfies the minimum-form rate, with a constant depending only on the fixed cutoff. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperCap 6 declarations Roadmap equations (35)–(36) compare coupled unit-range scalar statistics, transfer the quarter-mean Poisson tail, and absorb its penalty into the observable rate.
Restoring the Poisson cap
Roadmap equations (35)–(36) compare coupled unit-range scalar statistics, transfer the quarter-mean Poisson tail, and absorb its penalty into the observable rate. These estimates do not impose a relation between log n and d.
The alphabet logarithm is bounded by the alphabet size. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The cap's exponential penalty is at most twice the inverse sample size. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (36): the cap penalty has the unsaturated observable rate scale. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (35) in real probability for any count with the quarter-mean Poisson law. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Coupled unit-range statistics agreeing below the cap differ in risk by at most one unit of loss times the overflow probability. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Restoring the cap converts the uncapped m=n/8 risk to the fixed-n scale, with an explicit additive universal constant for overflow. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperClipping 14 declarations The clipping step in roadmap equation (28) contracts squared error around an in-interval polynomial mean.
Clipping bias and squared-error contraction
The clipping step in roadmap equation (28) contracts squared error around an in-interval polynomial mean. Its change in expectation is controlled by the second moment around the clipping center divided by the clipping width.
Translating symmetric clipping gives the interval used by the cell estimator. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Proof (Lean source)
The paper's cell clipping contracts squared error at every target in its interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A positive clipping width controls clipping displacement by a quadratic tail scale. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact cell statistic obeys the quadratic clipping-displacement bound. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating the displacement bound gives the clipping bias in equation (28). The second moment is an input to this transfer lemma, rather than an assumed risk rate. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Projection to the unit interval contracts the loss relative to the observed target. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating the pointwise contraction proves the second-moment part of (28). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
An unbiased factorial lift transfers its center second moment to clipping bias. This is the first part of (28) before substituting the factorial moment bound (27). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Zero oscillation scale makes clipping exactly equal to its center. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The clipped cell statistic stays within its chosen width of the center, regardless of the evaluation counts or pilot localization. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On bad pilots the cell error is bounded by width plus center error. This is the pathwise inequality following roadmap (28), retaining the local scales rather than substituting unit loss. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The bad-pilot squared error is controlled by twice the width square and twice the center-error square, precisely the two quantities in roadmap (22). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On any pilot event, the integrated absolute cell error is controlled by the local width and center deviation. This is the first-moment use of roadmap (22) and does not require an integrability premise on the cell statistic. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating over any pilot event transfers the tail width and center second moments to the actual clipped cell loss. Applying this to the bad-pilot event is the second-moment use of roadmap (22) after (28). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperDegreeCalibration 5 declarations Roadmap equation (27) chooses a universal small degree coefficient so the linear and quadratic exponential growth in (26) costs only d^(1/16).
Universal Jackson degree calibration
Roadmap equation (27) chooses a universal small degree coefficient so the linear and quadratic exponential growth in (26) costs only d^(1/16). The additive degree floor contributes a universal multiplicative constant.
The degree floor costs at most two in addition to the tuned logarithmic degree. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The degree floor and minimum degree two retain at least half the tuned logarithmic degree, uniformly without a large-alphabet cutoff. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
A logarithmic degree bound controls the quadratic exponent without a log n term. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
One universal positive tuning coefficient suffices for any fixed nonnegative linear and quadratic moment-growth constants. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The tuned Jackson degree has at most d^(1/16) exponential moment inflation, with a universal prefactor, as in roadmap (27). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperEmpiricalRatio 20 declarations The observed value lies in the unit interval, and the constant branch has risk at most one quarter in the saturated regime.
Nonpolynomial upper-bound branches
The observed value lies in the unit interval, and the constant branch has risk
at most one quarter in the saturated regime. Empirical arm means stay in the
unit interval even for empty arms. The pathwise empirical-ratio error splits
into mass error and mass-weighted arm error, giving the two squared-loss terms
in roadmap equation (6) after projection. Weighted Cauchy–Schwarz reduces arm
error to individual second moments without excluding null cells. The iid
cell-indicator mean-square bound proves the mass term is at most d / n.
The covariate cell masses of a finite observed probability law sum to one. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The oracle observed value is between zero and one for every finite observed law. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The constant one-half estimator has squared risk at most one quarter. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The logarithmic alphabet scale is positive for a nonempty alphabet. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the constant branch the minimum-form rate scale is exactly one. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The large-alphabet constant branch is measurable and has risk at most one quarter. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The saturated branch satisfies the desired minimum-form risk bound with constant one quarter. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Successes form a subset of the observations in each treatment arm. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The empirical arm mean lies in the unit interval, including empty arms. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The two empirical arm means have a maximum in the unit interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The cell error splits into empirical mass error and mass-weighted arm error. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Summing the cell bounds gives the pathwise decomposition preceding equation (6). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Projection and the pathwise decomposition reduce squared loss to the two terms in (6). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Cauchy–Schwarz bounds the squared total mass error by the sum of cellwise errors. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Probability-weighted Cauchy–Schwarz controls the arm error without dividing by cell masses. In particular, null cells contribute zero. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The projected empirical statistic is controlled by individual mass and arm squared errors, as required for the expectation bounds in equation (6). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating the cellwise inequality reduces empirical-ratio risk to marginal second moments. All integrability conditions are automatic on the finite observed sample space. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The one-observation indicator of a covariate cell has mean equal to its cell mass. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Under iid sampling, each empirical cell mass has mean squared error at most its mass over n. The bound also holds for null cells, without a positivity assumption on their mass. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (6)'s mass-error term is bounded by d/n under the actual iid observed law. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperFactorial 15 declarations Roadmap equations (23)–(26) connect independent Poisson factorial moments to actual pilot rectangles and the centered Jackson factorial statistic.
Localized factorial moments
Roadmap equations (23)–(26) connect independent Poisson factorial moments to actual pilot rectangles and the centered Jackson factorial statistic.
Positive pilot level gives strictly positive coordinate radii, even at zero counts. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Membership in the pilot interval is precisely the centering condition for the normalized factorial envelope, including a lower endpoint truncated at zero. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (23) specializes the exact mixed factorial identity to intensity m q. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equations (24)–(25) give the four-coordinate exponential envelope on the actual pilot rectangle. The factor eight comes from the pilot variance bound. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every scalar factorial lift has an integrable square under a Poisson law. This regularity is derived from raw factorial moments, rather than assumed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Independent Poisson coordinates make every normalized factorial monomial L². No integrability premise is needed for the subsequent polynomial assembly. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual Jackson factorial statistic is square-integrable under the independent Poisson experiment. This derives all regularity needed for clipping. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Centering the factorial cell statistic at any fixed value preserves L², so its second moments exist without extra integrability assumptions. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual factorial cell statistic is unbiased for evaluation of its centered Jackson monomial expansion at the Poisson mean (roadmap equation (23)). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Clipping around a fixed center contracts squared error at the unclipped mean when that mean lies in the clipping interval. Its risk is bounded by the original second moment around the fixed center, as in roadmap equation (28). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
At intensities m times q, the factorial statistic has exactly the centered Jackson polynomial as its expectation, with the intensity normalization canceled. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing normalized monomials costs the square of the coefficient ℓ¹ norm, rather than an extra alphabet factor. This is the finite polynomial step of (26). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the localized pilot rectangle, equation (26) holds for the estimator's actual centered factorial cell statistic, with its explicit coefficient norm. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Combining the exact Poisson mean, derived L² regularity, the localized factorial envelope, and clipping displacement proves the bias transfer in (28) for the actual statistic. The coefficient norm remains explicit for (14). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On a localized pilot rectangle, clipping the actual Poisson factorial statistic preserves the second-moment envelope around its exact polynomial mean provided that mean lies in the clipping interval. The coefficient norm remains explicit; this is the contraction step of the second assertion of equation (28). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperGoodBadAssembly 7 declarations Roadmap (29) splits each actual cell error into its disjoint good- and bad-pilot parts.
Good- and bad-pilot risk assembly
Roadmap (29) splits each actual cell error into its disjoint good- and bad-pilot parts. Independent cell variances add; the good bias is summed before squaring, and the bad bias is controlled by its second moments.
Pairwise independence suffices for (29): only distinct-cell covariances enter the variance of the sum. This matches the implemented marked experiment. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Disjoint good and bad errors yield the independent-cell risk estimate in (29). Only the full cell statistics need be independent. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Measurable pilot events provide the disjoint error split automatically. Both pieces inherit L² regularity from the cell statistic, so this step introduces no extra moment assumption on the localized pieces. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The good-pilot estimates (19), (20), (28) and the bad-pilot squared cell estimate (22) imply the full independent-cell rate (34). The bad error retains its actual second moment; no unit-loss replacement is used. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The squared cellwise Jackson approximation envelopes sum to at most 18 times the active rate, including null cells. This retains the approximation term in (28) when passing from polynomial loss to loss around the cell target. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The good-pilot target loss includes both the factorial fluctuation and the squared Jackson approximation error. Summing that extra error with (32) preserves (34); the bad-pilot contribution is still its actual second moment. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Measurable good-pilot events turn the target-loss estimates of (20), (22), and (28) into the independent-cell rate. The Jackson squared error is retained, and the localized L² properties follow from the full cell statistics. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperIndependentAggregation 7 declarations Roadmap equations (29)–(34) add the independent cell variances and square the sum of their biases.
Independent-cell risk assembly
Roadmap equations (29)–(34) add the independent cell variances and square the sum of their biases. The rate assembly below consumes cellwise estimates; it does not assume the risk bound for the estimator.
Squared loss decomposes into variance and squared bias for an L² statistic. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independent cell variances add, while their biases add before squaring, as required in the passage to equation (29). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cellwise variance envelopes and absolute bias envelopes give a sum-risk bound. The squared bias is kept intact, avoiding a spurious factor of the alphabet size. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equations (32)–(33) absorb the entire summed bias, including the clipping displacement. The only random-scale input is the cellwise pilot moment estimate (19). In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Equations (29)–(34): independent cell statistics obey the active-branch rate once their integrated variance and bias estimates and the pilot second moments have been proved. The constant is uniform in the alphabet and the intensity. These are intermediate cell estimates, not a premise asserting estimator risk. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Projection to the unit interval is continuous, including at both endpoints. The stated conclusion holds.
Formal statement
Proof (Lean source)
The final projection in equation (34) preserves any risk bound assembled for the unprojected sum. Its squared-loss integrability follows from the original L² statistic and pointwise contraction, so no extra regularity premise is needed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperJacksonCoefficients 10 declarations The centered Jackson polynomial's cube oscillation yields the explicit Chebyshev coefficient envelope (14).
Jackson coefficient and localized second-moment bounds
The centered Jackson polynomial's cube oscillation yields the explicit Chebyshev coefficient envelope (14). Combining it with the localized Poisson factorial bound proves (26) and the clipping second-moment bound (28), with no assumed coefficient envelope.
A four-variable polynomial bounded on the cube has the sharp tensor Chebyshev coefficient envelope. Specializing the library's path result to a constant path gives a scalar bound with no variation term. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (14) for the exact normalized polynomial chosen by the estimator. The coefficient norm is derived from (12), polynomial degree control, and Chebyshev extraction, including the centering constant. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The coefficient envelope applies to every actual pilot rectangle, without localization of the true parameter or extra count regularity assumptions. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Squaring the explicit coefficient factor costs only an exponential linear in the Jackson order. The coarse numerical constant is universal and is sufficient for the logarithmic degree calibration in (27). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equations (14) and (25) give the full coefficient-times-factorial envelope in (26), with fixed universal linear and quadratic growth constants. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual localized factorial statistic satisfies equation (26) with its random armwise scale and universal exponential growth constants. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The clipping contraction in (28) has the same derived exponential scale as (26). Localization supplies mean containment through the Jackson construction. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Positive radii and nonnegative centers make the clipping scale strictly positive. Each anchored arm weight is at least one. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The first assertion of (28) follows from the factorial mean identity, clipping displacement, and the derived coefficient envelope. The scale positivity needed for division is provided by the pilot construction. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A universal logarithmic degree tuning absorbs the derived coefficient and factorial inflation into the d^(1/16) scale in (27), for every pilot rectangle. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperJacksonOscillation 10 declarations The estimator's chosen polynomial inherits the tensor convolution oscillation bound (12).
Jackson mean containment in the clipping interval
The estimator's chosen polynomial inherits the tensor convolution oscillation bound (12). Polynomial uniqueness on the cube recovers its coordinate degrees, so the finite coefficient expression used by the factorial mean represents that same convolution, rather than an unrelated approximation polynomial.
Nonnegative centers and radii give a nonnegative armwise clipping scale. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The armwise modulus bounds every point in a nonnegative rectangle by its center oscillation scale, retaining the arm weights and radii together. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual pair selected in the estimator represents the canonical tensor convolution whenever its construction conditions hold. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Polynomial uniqueness on the cube recovers the normalized representative's coordinate degree bound even though the affine existence interface exposes only the physical representative's degrees. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite centered coefficient sum used in the Poisson mean is exactly the normalized Jackson polynomial evaluation, without a truncation remainder. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A normalized positive Jackson kernel preserves a uniform oscillation bound around any fixed center. Continuity supplies the integral's regularity. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (12) holds for the exact finite coefficient expression appearing as the Poisson factorial mean. The oscillation scale is derived from the modulus and the positive normalized kernel rather than assumed as a containment premise. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The pilot's centered rectangle is nonnegative by the truncated lower endpoint, with no extra regularity or positivity premise on the counts. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the actual pilot rectangle, the exact factorial mean belongs to the clipping interval for every positive alphabet size, including null cells. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Localization alone suffices for the clipping second-moment transfer in (28): the mean containment and nonnegative width are supplied by the Jackson construction. The coefficient norm remains explicit for the later bound (14). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperLocalizedBias 6 declarations The true-mass radius and boundary estimates are combined with occupied-cell overlap.
Inverse-arm weighted localized bias envelope
The true-mass radius and boundary estimates are combined with occupied-cell overlap. This reduces the right side of roadmap (11) to the square-root and linear scales preceding degree calibration in (20), without detaching an inverse arm mass from its radius.
An occupied cell's inverse arm fraction lies between one and the inverse public overlap floor. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Weighting the localized radii by their own inverse arm fractions retains one square-root inverse-overlap factor and one linear inverse-overlap factor. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The entire occupied-cell envelope in (11), including its unweighted term, reduces to the localized scales needed in (20). This is a deterministic bound on the approximation envelope; it does not assume a polynomial error bound. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A degree at least a positive multiple of the log scale converts the boundary and radius terms into the normalized bias scales in (20). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The pre-calibration square-root scale is the log scale times the normalized scale; the identity also covers null cell masses. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
For occupied cells, the actual pilot envelope has the two bias scales in roadmap (20) once the degree is logarithmic. This bounds the envelope itself and leaves the tensor Jackson approximation step explicit upstream. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperLocalizedClipping 4 declarations One universal degree tuning yields both assertions of roadmap (28).
Calibrated localized clipping
One universal degree tuning yields both assertions of roadmap (28). Combining its mean displacement with the occupied-cell Jackson bias (20) controls the actual clipped statistic around the cell target.
The same universal degree choice controls clipping bias and second moment. The Poisson laws provide the factorial mean and integrability; localization provides containment. No coefficient or moment bound is assumed. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Combining (20) and both parts of (28) controls the actual clipped occupied-cell mean and loss around the statistical target. The polynomial approximation error is retained explicitly in the squared-loss bound. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
A zero-count pilot always contains the null atom, including at its lower boundary. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The null-cell instance of (20) and (28) controls the clipped statistic's mean and second moment around the zero target, without inverse arm masses. The degree tuning is the same universal tuning used for occupied cells. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperLogAbsorption 7 declarations The polynomial decay in roadmap equations (31) and (33) absorbs both the second and fourth powers of the logarithmic alphabet scale.
Absorbing the logarithmic factors in upper-risk aggregation
The polynomial decay in roadmap equations (31) and (33) absorbs both the second and fourth powers of the logarithmic alphabet scale. These estimates are uniform over all nonempty alphabets, without imposing a relation to n.
Any positive polynomial decay absorbs a fixed positive integer power of L_d. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The two logarithmic ratios in (31) and (33) have one universal envelope for each fixed positive decay exponent. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the active branch, the summed pilot second-moment scale is controlled by the logarithmic envelope that appears in (31) and (33). Here a = m ε. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (33)'s Cauchy–Schwarz step for the integrated random clipping scales. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equations (31) and (33): the pilot moment sum, multiplied by any fixed sublinear alphabet power, is at most a universal constant times R = d/(m ε L). The premise is the cellwise pilot estimate (19), rather than a risk bound. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (33), including its final absorption into R, for actual integrated clipping scales. The second-moment premise is exactly the pilot estimate (19). In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (31) with the variance inflation d^(1/16) used by the factorial lift. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperMarkedAssembly 5 declarations Roadmap (29)–(34) is assembled for the actual marked-count construction.
Good-pilot inputs for the implemented marked statistic
Roadmap (29)–(34) is assembled for the actual marked-count construction. Count laws, pairwise cell independence, L² regularity, pilot-scale moments, and bad-pilot losses are discharged. Only the two integrated good-pilot content estimates remain as explicit inputs, retaining Jackson squared error.
The true cell vector belongs to the rectangle constructed from the actual pilot-marked observations.
Definition (Lean source)
Localization of the implemented pilot is a measurable event. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Actual pilot counts within a cell are independent Poisson coordinates. This discharges the independence input in the bad-pilot estimate (22). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The implemented bad-pilot cell loss satisfies (22), including null cells. No distributional or moment inputs remain for the caller. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the implemented statistic, only the good-pilot first and second moment content estimates remain in (29)–(34). The Jackson approximation term is retained; bad-pilot loss, independence, and regularity are derived. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperMarkedConditioning 8 declarations The actual pilot and evaluation vectors are independent.
Averaging fixed-pilot bounds in the implemented experiment
The actual pilot and evaluation vectors are independent. Their joint law and Fubini decomposition justify freezing the pilot in roadmap (26)–(28), then averaging the resulting cell loss bounds.
The four actual counts of a cell with a specified pilot/evaluation mark. For the displayed parameters, markedPoissonCellCounts is the object specified by this definition.
Definition (Lean source)
Either actual count vector is measurable. The stated conclusion holds.
Formal statement
Proof (Lean source)
The pilot and evaluation vectors of the same cell depend on disjoint marked atoms, so freezing the entire pilot preserves the evaluation law. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The law of either actual cell vector is the same fourfold Poisson product. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The joint law needed to average the fixed-pilot clipping bounds is a product, with no conditional-law assumption left to discharge. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating any integrable function of the actual two count vectors is exactly averaging its fixed-pilot evaluation integral against the pilot law. This applies to the good-pilot first and squared losses in (28). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A nonnegative fixed-pilot loss bound averages to the corresponding bound for the actual marked experiment. Integrability of the pilot envelope is transported by its proved count law. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A fixed-pilot absolute bias bound averages to the corresponding bound for the actual marked experiment. Integrability of the pilot envelope is transported by its proved count law. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperMarkedCounts 13 declarations The histogram law realizes roadmap equations (7)–(8) for the counts used by markedPoissonStatistic.
Actual marked Poisson counts and cell regularity
The histogram law realizes roadmap equations (7)–(8) for the counts used by
markedPoissonStatistic. Marginal laws then discharge the unconditional
square-integrability required by the variance assembly in equation (29).
All observation–mark singleton counts in the uncapped finite sample. For the displayed parameters, markedPoissonHistogram is the object specified by this definition.
Definition (Lean source)
The complete histogram is measurable on each fixed-count fibre. The stated conclusion holds.
Formal statement
Proof (Lean source)
The actual marked histogram has the product law of independent singleton Poisson counts, including zero-mass symbols. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
A coordinate of the marked histogram is exactly the implementation's pilot or evaluation count, with the same four-coordinate encoding. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Either mark gives the intended intensity n/8 times the observed atom mass. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
All pilot and evaluation atom counts are mutually independent under the actual uncapped experiment, as in roadmap (8). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
One implemented clipped contribution before the final unit projection. For the displayed parameters, markedPoissonCellValue is the object specified by this definition.
Definition (Lean source)
Each actual marked count is measurable, including on unbounded count fibres. The stated conclusion holds.
Formal statement
Proof (Lean source)
Marginal Poisson laws supply unconditional L² regularity for every actual clipped cell, without assuming any moment bound for its factorial polynomial. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The sum whose projection defines the actual marked statistic is L². In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Distinct cells use disjoint sets of observation–mark atom counts. Their actual clipped contributions are consequently independent, including bad pilots. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (29) holds for the actual unprojected marked statistic: distinct cell variances add, and the total bias is squared only after summation. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The unit projection in the implemented uncapped statistic preserves the variance-plus-squared-bias upper bound for its actual cell sum. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperMarkedGoodSquare 4 declarations Fixed-pilot Jackson approximation and clipping bounds are averaged using the actual independent marked vectors.
Integrated good-pilot moments and active risk
Fixed-pilot Jackson approximation and clipping bounds are averaged using the actual independent marked vectors. This proves the occupied-cell first- and first- and second-moment inputss of roadmap (29), retaining the squared approximation term rather than absorbing it into factorial variance.
One universal degree tuning proves the integrated good-pilot occupied cell bias and squared loss for the implemented statistic. All count laws, independence, localization and integrability inputs are discharged. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
One universal degree tuning proves the integrated good-pilot occupied cell loss for the implemented statistic. All count laws, independence, localization and integrability inputs are discharged. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The actual pilot clipping scale is nonnegative at every finite sample. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equations (19), (20), (22), and (28) yield the active-branch risk for the implemented uncapped statistic. Both good-pilot content inputs are proved here, including null cells, with the same universal degree tuning. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperMarkedMoments 5 declarations The actual marked counts discharge the pilot moment input in roadmap (19) and its mass-normalized sum in (30).
Implemented marked-pilot moments
The actual marked counts discharge the pilot moment input in roadmap (19) and its mass-normalized sum in (30). These are unconditional bounds, including null cells and bad pilots.
The clipping scale computed from the actual pilot-marked counts. For the displayed parameters, markedPoissonClippingScale is the object specified by this definition.
Definition (Lean source)
The actual pilot scale is L² even on failed localization events. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (19) holds for the implemented counts, with no assumed count law or pilot regularity left for a caller to discharge. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (30) for the actual pilot: the mass term sums to one, including zero-mass cells, so the envelope contains no extra factor d on that term. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equations (29)–(34) for the implemented statistic. Only the still-to-be-proved cellwise variance and bias content estimates remain as inputs: count laws, independence, square-integrability, and pilot moments are discharged here. The constant is uniform in n, d, the overlap floor, and the observed law. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperNullCell 6 declarations The null-cell case following roadmap equation (11) uses the quadratic cosine displacement at the lower corner and the kernel's second moment.
Null-cell Jackson bias
The null-cell case following roadmap equation (11) uses the quadratic cosine displacement at the lower corner and the kernel's second moment. No inverse arm mass is introduced. The bound applies to the exact factorial mean.
At a zero lower corner, each displaced coordinate has a quadratic envelope. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The Jackson convolution at a zero lower corner is controlled solely by the second kernel moment, including when the target functional has a tie. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact coefficient expression used by the factorial mean has the null-cell second-order bias bound; polynomial uniqueness and convolution evaluation link the bound to the estimator's chosen polynomial. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Zero pilot counts put the midpoint exactly one radius above the origin. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual zero-count pilot's factorial mean obeys the null-cell bias bound preceding equation (20), with no division by any cell or arm mass. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Logarithmic degree calibration gives the null-cell instance of (20). The sole inverse-overlap term is the linear normalized scale. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperNullMarked 4 declarations At a null cell both count vectors vanish almost surely.
Null-cell loss without factorial inflation
At a null cell both count vectors vanish almost surely. The factorial lift then equals its Jackson mean, which is inside the clipping interval. Thus only the null-corner approximation error remains in roadmap (20)/(28).
At a null cell clipping has no displacement or stochastic inflation: the random-pilot loss is bounded by the null-corner Jackson error alone. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Evaluation coordinates of one implemented marked cell are independent; this specializes the independent marked histogram to the false mark. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The actual null-cell statistic satisfies the normalized approximation bound almost surely for every positive degree coefficient. All count-law and independence inputs are supplied by the implemented marked experiment. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Both good-pilot content estimates for an implemented null cell hold without a scale-moment or factorial-inflation term. Only the squared Jackson approximation scale remains in the second moment. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperNullPilot 6 declarations The null-cell argument after roadmap (11) applies to the actual random pilot: zero cell mass forces all four Poisson counts to vanish almost surely.
Random pilots at null cells
The null-cell argument after roadmap (11) applies to the actual random pilot: zero cell mass forces all four Poisson counts to vanish almost surely. This transfers the calibrated zero-pilot bounds (20)/(28) to the random-pilot statistic, without conditioning on a positive-probability pilot event.
Zero cell mass forces every observed atom in that cell to have zero mass. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The marginal Poisson laws alone force the entire null-cell count vector to vanish almost surely; independence is unnecessary for this conclusion. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A null cell is localized almost surely on the actual random pilot rectangle, including its lower boundary, as required in the paragraph after (11). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
With both pilot and evaluation Poisson counts at a null cell, the actual clipped cell statistic is almost surely a deterministic constant. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Null cells contribute no variance to the independent-cell assembly (29). Their approximation bias need not vanish and is still controlled by (20). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The same universal degree tuning as (28) bounds the actual random-pilot null-cell mean and second moment. The marginal count laws derive the zero pilot, rather than imposing it as an extra localization assumption. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperOccupiedCell 4 declarations A reference-point modulus is integrated against the positive tensor kernel.
Occupied-cell Jackson bias
A reference-point modulus is integrated against the positive tensor kernel. The weights remain attached to the true arm masses, as in roadmap (11), and the localized pilot envelope then yields (20).
Only a modulus anchored at the evaluation point is needed for the boundary Jackson estimate; no uniform Lipschitz bound over pairs of points is imposed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The estimator's finite coefficient mean inherits the boundary estimate from a physical-coordinate modulus at its true reference vector. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating the armwise modulus at an occupied cell proves equation (11) for the exact coefficient expression, including boundary means and ties. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the actual localized pilot rectangle, logarithmic degree calibration proves the occupied-cell bias bound (20) for the factorial mean itself. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperPilot 19 declarations The pilot radius controls the normalized Poisson variance on every localized rectangle.
Pilot radius variance control
The pilot radius controls the normalized Poisson variance on every localized rectangle. Midpoint-based radius bounds prove roadmap (17); keeping each anchored denominator with its radius proves (18) and the deterministic clipping-scale envelope (22a). The pilot midpoint deviations and the observed-cell modulus prove (22b), retaining each inverse arm mass with its own outcome-coordinate deviations.
Truncating the lower endpoint at zero moves the midpoint above the pilot count center. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The midpoint coordinates are nonnegative for positive exposure and level. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The radius never exceeds the original half width, including intervals truncated at zero. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The coordinate radius is bounded by the square-root scale at the rectangle midpoint (17). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing the two coordinate radii yields the armwise square-root scale in (17). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The anchored denominator gives the arm square-root term a single inverse-overlap scale (18). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Weighting an arm radius by the anchored denominator preserves its square-root scale (18). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual pilot arm radius and random anchored weight satisfy equation (18) jointly. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each unweighted pilot arm radius is also bounded by the total-mass overlap scale. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full clipping scale has the deterministic total-mass envelope (22a), without separating random arm denominators from their radii. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The localized coordinate variance is controlled by the logarithmic pilot level, including coordinates whose pilot interval meets zero (roadmap equation (24)). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Truncating a nonnegative pilot center at zero moves its midpoint by at most its half width, including intervals that meet the boundary. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each midpoint error is bounded by the pilot-count error plus the random half width; no localization event is needed in equation (22b). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing within an arm before weighting preserves the outcome-coordinate shell bound used in equation (22b). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On an occupied observed cell, overlap makes the anchored denominator exactly the observed arm mass, as required in roadmap equations (1) and (22b). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The cell-value perturbation keeps the inverse observed arm mass attached to its armwise deviations. The constant four absorbs the unweighted modulus term. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (22b) for the actual pilot: every arm's inverse propensity remains paired with the sum of that arm's count deviations and half widths. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The clipping definition bounds cell error by its width plus the center's error, even when the true cell lies outside the pilot rectangle. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual clipped cell statistic obeys the bad-pilot deterministic envelope preceding (29), with the center term reduced to the coordinate shells in (22b). The nonnegative width follows from the construction, not an extra premise. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperPilotMoments 7 declarations Roadmap equation (19) follows from the deterministic anchored-radius bound, a linear envelope for the pilot midpoint, and the marginal Poisson means.
Pilot clipping-scale second moments
Roadmap equation (19) follows from the deterministic anchored-radius bound, a linear envelope for the pilot midpoint, and the marginal Poisson means. The elementary square-root envelope avoids needing joint independence for this step.
A pilot midpoint is controlled by a linear count envelope, including at zero. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The four-coordinate mass is the sum of the four outcome atoms. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The total pilot midpoint mass has a linear envelope with four width terms. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Squaring the anchored-radius envelope keeps only one inverse-overlap power in the term proportional to the random total midpoint mass. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A normalized marginal Poisson pilot count is integrable and has mean q. Both properties are transported from the first raw factorial moment. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (19) for the actual pilot clipping scale. Only marginal Poisson laws are needed; null cells and arbitrarily small positive overlap are included. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed-cell form of (19), with exactly the paper's mass and overlap scales. Positivity is not required of the cell mass, so null cells are retained. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperPilotRegularity 4 declarations The variance assembly in roadmap (29) requires square-integrable cell statistics before splitting good and bad pilots.
Unconditional pilot and clipped-cell regularity
The variance assembly in roadmap (29) requires square-integrable cell statistics before splitting good and bad pilots. Marginal Poisson score moments supply this regularity, even off the localization event. Clipping removes any need for unconditional moments of the pilot-selected factorial polynomial or independence between pilot and evaluation counts here.
The aggregate pilot deviation-and-width score is square-integrable under its marginal Poisson laws, without a joint independence assumption. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Total midpoint mass is square-integrable on the entire pilot space. The deterministic displacement bound dominates it by the true mass plus the aggregate score, so bad pilots are included. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The random clipping scale has an integrable square on good and bad pilots. Its anchored-radius square envelope is affine in the integrable midpoint mass. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual clipped cell statistic is square-integrable for any measurable evaluation counts. Its random center and width dominate it pathwise, and both have already derived pilot moments; no evaluation moment gate is needed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperPilotTail 11 declarations Roadmap (15)--(16): the actual truncated pilot interval fails only on the empirical-radius bad event.
Pilot localization and bad-coordinate moments
Roadmap (15)--(16): the actual truncated pilot interval fails only on the empirical-radius bad event. Marginal Poisson concentration bounds its probability and its second and fourth deviation-plus-width moments. A union bound controls failure of the four-coordinate rectangle, including null atoms.
The paper's pilot width is exactly the library's empirical Poisson radius. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
For a nonnegative true atom, truncation at zero does not change the criterion for failure of its pilot interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every power through four of a coordinate's deviation-plus-width score is integrable under its Poisson law. This derives the regularity needed for (16). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (16), for moment orders two and four, on the actual coordinate failure event. The larger library bad event also controls the width score; no tail or integrability premise is added. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The marginal moment estimate (16) transports to the actual random pilot counts by their Poisson laws. Independence is unnecessary for this step. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full four-coordinate localization rectangle fails with probability at most eight times the exponential scalar tail (15). Only marginal laws are used, so no joint independence or positive cell mass is assumed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Failure of the actual pilot rectangle is contained in the empirical-radius bad union used by the independent-product moment theorem. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
All four-coordinate score powers needed for the bad-pilot comparison are integrable, derived from the marginal Poisson laws rather than assumed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (16) jointly controls every coordinate's score on failure of any coordinate. This retains the cross-coordinate terms needed in (22), which a sum of the scalar bad moments alone does not control. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The total pilot midpoint displacement is bounded by the joint score, including pilots whose intervals fail to contain the true vector. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Joint bad-pilot moments also control movement of the actual midpoint. This supplies the unweighted center-displacement component of (22b) without separating the random midpoint from the rectangle-failure event. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperPoissonization 15 declarations Roadmap equations (7)–(8) use iid observation–fair-mark pairs, stopped at an independent Poisson count.
Marked Poissonization of the observable estimator
Roadmap equations (7)–(8) use iid observation–fair-mark pairs, stopped at an independent Poisson count. The statistic below is the uncapped version of the actual capped statistic, with intensity fixed by the original sample size. Its fixed-count fibres and prefix identities connect that experiment to the finite Rao–Blackwell sum in equation (37).
Fair Boolean marks form a probability law.
Definition (Lean source)
The uncapped statistic uses all pairs in a finite marked sample, while retaining the intensity and degree chosen from the original sample size.
Definition (Lean source)
The marked statistic has unit range even when its count exceeds the sample cap. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reading the statistic is measurable on the countable finite-sample space. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Boundedness supplies squared-loss integrability without an added regularity premise. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Below the cap, the uncapped marked statistic equals the implemented capped statistic on the first k observations and their marks. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Fair Boolean marks have constant singleton mass, including the empty array. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating independent fair marks is exactly the finite average used by the observable estimator. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Iid observation–mark pairs integrate as a finite fair-mark average of iid observation expectations. This identifies the auxiliary averaging law exactly. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Taking the first k fair marks from n fair marks preserves their product law. This removes unused marks from each count fibre. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite fair-mark average of a prefix statistic is independent of how many unused fair marks are appended. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
On a count fibre that fits the sample, the marked Poisson squared-loss integral is its Poisson mass times the exact fair-mark average of capped risk. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The count-capped part of the Poisson risk is the weighted auxiliary risk appearing in the finite Rao–Blackwell inequality, with no unused marks. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The missing mass in the finite count average is the quarter-mean Poisson overflow probability, so equation (35) applies to the implemented weights. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (37) and restoration of the cap for the actual implemented estimator. Its fixed-sample risk is bounded by the uncapped marked Poisson risk plus the exponential cap penalty; no auxiliary risk bound is assumed. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperRaoBlackwell 12 declarations The fair-mark average and the capped Poisson weights implement the auxiliary expectation in roadmap equation (37).
Finite Rao–Blackwell risk transfer
The fair-mark average and the capped Poisson weights implement the auxiliary expectation in roadmap equation (37). The omitted Poisson tail is an atom at zero, so its squared loss must be included when applying Jensen.
The projection used in every capped statistic has range in the unit interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
Every auxiliary capped statistic has range in the unit interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Poisson weights are nonnegative, including at zero intensity. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full Poisson weight series has total mass one. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Truncating Poisson weights at the sample cap produces a subprobability. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Fair marks on k observations have total weight one. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Proof (Lean source)
Squared loss decreases under a finite subprobability average when its missing mass is assigned the statistic zero. This explicitly retains the loss on the cap tail. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging over the fair marks contracts squared loss pathwise. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the active branch the deterministic estimator contracts the auxiliary squared loss, including the zero statistic when the Poisson count exceeds the cap. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite Rao–Blackwell estimator stays in the unit interval in every branch. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The estimator's unit-range loss provides the uniform bounded-risk part of the minimum-form bound, independently of the unknown cell masses and propensities. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equation (37) for the actual finite estimator: its observed risk is at most the Poisson-weighted, fair-mark auxiliary risk plus the cap-tail loss at zero. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.UpperRiskAssembly 3 declarations Equations (34)–(37) transfer an uncapped marked-experiment estimate to the actual observed estimator and combine all three branches.
Observable upper-risk assembly
Equations (34)–(37) transfer an uncapped marked-experiment estimate to the actual observed estimator and combine all three branches. The remaining input is explicitly the uncapped experiment estimate; no headline theorem is asserted here without that analytic input.
On the active branch, cap restoration and finite Rao–Blackwellization convert the uncapped intensity-scale estimate into the observed minimum rate. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A uniform uncapped marked-experiment bound on active parameters suffices for the actual estimator on every branch; the cutoff enters only through a bounded logarithm in the empirical branch. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Taking the supremum over all legal observed laws preserves the assembled three-branch rate. Measurability follows from the finite observed sample alphabet, so the remaining input is only the marked-experiment content bound. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.WeightedApproximation 8 declarations Weighted scalar approximation and constrained moment priors
Weighted scalar approximation and constrained moment priors
For the displayed parameters, phiEpsFormula is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, phiEps is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, weightedApproxError is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, ConstrainedPriorPair is the object specified by this definition.
For the displayed parameters, CommonAtomDomain is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, commonAtomCompletion is the object specified by this definition.
For the displayed parameters, constrainedPriorSeparationFormula is the object specified by this definition.
Definition (Lean source)
For the displayed parameters, constrainedPriorSeparation is the object specified by this definition.
Definition (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.WeightedBestApproximation 3 declarations The reverse comparison in roadmap (3)--(8) starts with a best weighted approximant.
Attainment of the weighted polynomial approximation error
The reverse comparison in roadmap (3)--(8) starts with a best weighted approximant. Multiplication by the continuous reciprocal weight embeds the degree-bounded polynomial space in the continuous functions on the compact interval. Its finite dimension gives a compact minimizing ball, hence an actual minimizer rather than an assumed dual certificate.
The weighted infimum is attained by a polynomial of the prescribed degree. This is the minimizer used to construct the active residual set in roadmap (3). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A continuous perturbation with the residual's strict sign at every active extremum decreases its norm. This is the compact active-set perturbation argument in roadmap (3), allowing the weighted direction q/(1+z). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A best weighted residual has K+2 alternating active points. A missing alternation would give a sign polynomial whose weighted perturbation strictly improves the attained minimum, contradicting optimality as in roadmap (3). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.WeightedDualCompletion 2 declarations The finite dual's positive and negative atomic parts have equal mass and first moment.
Common-atom completion of the optimal finite weighted dual
The finite dual's positive and negative atomic parts have equal mass and first moment. Their weighted normalization gives t+u=1/2. Completing them by the same atom preserves the exact optimal gap, proving E ≤ Delta.
A finite weighted-normalized annihilator completes to a feasible pair, preserving the exact functional pairing. This implements roadmap (6)--(7) for the optimal witness as well as for any finite annihilator. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Completing the optimal finite dual yields a mean-one probability-prior pair whose absolute gap is exactly E, proving the reverse comparison (8). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.WeightedDuality 13 declarations Roadmap equation (2): moment matching and the mean-one normalization bound the constrained prior separation by four times the best weighted error.
Weighted dual comparison and common-atom normalization
Roadmap equation (2): moment matching and the mean-one normalization bound the constrained prior separation by four times the best weighted error. Equations (6)--(7): adding the same atom to the two Jordan parts produces probability priors of mean one without changing their moment or functional differences. The weighted dual witness for the reverse comparison remains to be built.
Weighted normalization places the common atom between one half and two. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
A continuous function on the supporting interval is integrable; no extra moment-integrability assumption is needed for the compactly supported witness. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Filling the missing mass by a Dirac atom yields a probability measure. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Adding the common atom preserves support when its location is in the interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
The integral under a completed measure is the old integral plus the atom's contribution. This applies to moments and to the weighted objective. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Two supported Jordan parts of a weighted-normalized moment annihilator complete to feasible priors, with the exact common-atom construction (6)--(7). All moment integrability follows from compact support. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The identical added atom cancels from every integrable functional gap. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Compact support makes the weighted objective integrable, so the common-atom completion preserves its gap without any additional regularity hypothesis. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Matching monomial moments matches every polynomial of the permitted degree. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Compactness bounds each polynomial's weighted residual, and its supremum controls the residual pointwise on the supporting interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Mean-one probability priors integrate the residual envelope to twice its weighted error; moment matching therefore bounds their gap by four times it (roadmap equation (2), before taking the infimum). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The identical Dirac priors at one make the feasible set nonempty. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Taking the polynomial infimum and the feasible-prior supremum proves the upper half of the weighted dual comparison (roadmap equations (2) and (8)). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.WeightedFiniteDual 1 declarations Alternating active residuals give finite Lagrange weights annihilating every polynomial through degree K.
An optimal finite weighted moment annihilator
Alternating active residuals give finite Lagrange weights annihilating every polynomial through degree K. Normalizing their weighted variation produces the exact optimal dual gap from roadmap (4)--(5).
There is a finite weighted-normalized moment annihilator attaining the weighted approximation error exactly, rather than only its order lower bound. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.WeightedUpperOrder 3 declarations The angular regularity of the nonlinear remainder and the promoted Jackson first-moment estimate give the universal sqrt(M)/K upper order in roadmap (14).
Weighted upper approximation by Jackson smoothing
The angular regularity of the nonlinear remainder and the promoted Jackson first-moment estimate give the universal sqrt(M)/K upper order in roadmap (14).
An even periodic continuous function has an even Jackson-smoothed trigonometric approximant, with error controlled by its angular Lipschitz constant. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Jackson smoothing of the bounded nonlinear remainder, followed by the inverse cosine-coordinate affine substitution, gives an admissible degree-K polynomial with uniform error of order sqrt(M)/K (roadmap (14)). In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The explicit Jackson approximant bounds the weighted polynomial infimum with a universal constant, uniformly on the closed overlap interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.Helpers.WeightedUpperRegularity 4 declarations The remainder in roadmap (10) is uniformly Lipschitz in the square-root intensity coordinate.
Angular regularity for weighted Jackson approximation
The remainder in roadmap (10) is uniformly Lipschitz in the square-root intensity coordinate. The half-angle identity then gives the sqrt(M) angular Lipschitz bound needed for the weighted upper approximation (14).
Clipping the lower quadratic branch confines its slope to [-2,0]. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The clipped rational upper branch has slope bounded by two in the square-root intensity coordinate, including intervals crossing the kink. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The nonlinear remainder has a universal Lipschitz constant in sqrt(z), uniform over the entire closed overlap interval. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
The half-angle coordinate gives the uniform angular regularity asserted before roadmap (14), without differentiability at either kink. In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.OpenQuestions 4 declarations Open leading-constant question
Open leading-constant question
For the displayed parameters, AdmissiblePath is the object specified by this definition.
Definition (Lean source)
For no explicit parameters, DistinctPathLimitsQuestion is the object specified by this definition.
Definition (Lean source)
For no explicit parameters, SharpPathConstantQuestion is the object specified by this definition.
Definition (Lean source)
For no explicit parameters, PathLimitQuestion is the object specified by this definition.
Definition (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.TAllEstimatorLower 1 declarations All-estimator lower risk
All-estimator lower risk
A universal positive constant times the vanishing-overlap rate is a lower bound for the minimax squared error at every sample size, alphabet size, and admissible overlap level.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.TConsistencyThreshold 4 declarations Uniform consistency threshold and fixed-parameter reductions
Uniform consistency threshold and fixed-parameter reductions
For the displayed parameters, UniformlyConsistent is the object specified by this definition.
Definition (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Uniform consistency holds exactly when the alphabet-to-effective-sample-size ratio tends to zero; moreover, for a fixed alphabet the minimax risk is comparable to one capped by the inverse effective sample size, and for fixed overlap it is comparable to one capped by the alphabet-to-sample-size log ratio.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.TIdentification 25 declarations Identification and completion of finite observed laws
Identification and completion of finite observed laws
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the displayed parameters, completionBernoulliMass is the object specified by this definition. For the displayed parameters, completionBernoulliMass is the defined object.
Definition (Lean source)
For the displayed parameters, completionFullMass is the object specified by this definition. For the displayed parameters, completionFullMass is the defined object.
Definition (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
For the displayed parameters, bernoulliCompletion is the object specified by this definition. For the displayed parameters, bernoulliCompletion is the defined object.
Definition (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
In the econometric construction, the displayed inputs and assumptions imply the stated mathematical conclusion. Under the stated hypotheses, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every admissible observed law has a compatible potential-outcome completion, the oracle value of every admissible causal law equals the value identified from its observed marginal, and each covariate cell's armwise extension equals its mass times the larger conditional outcome mean.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.TMatchedFrontier 1 declarations Matched observed and causal frontiers
Matched observed and causal frontiers
Universal constants sandwich both the observed and causal minimax risks at the vanishing-overlap rate, while the explicit armwise estimator lies between the observed minimax risk and the same upper rate and its causal risk lies between the causal minimax risk and that upper rate.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.TObservableUpper 1 declarations Uniform observable upper risk
Uniform observable upper risk
There are universal positive tuning constants and a measurable armwise estimator whose worst-case squared error over every admissible observed model is bounded above by a universal constant times the vanishing-overlap rate.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_OptvalueVanishingoverlapRate_Research.TWeightedSeparationAndFrontier 2 declarations Weighted moment-prior separation and the minimax frontier
Weighted moment-prior separation and the minimax frontier
The full weighted approximation comparison and its explicit completed Jackson-packet witness, with a common universal lower constant. The optimal finite dual proves E ≤ Delta; the packet proves the lower order and supplies the required supported, mean-one, moment-matched witness. In the econometric construction, no additional assumptions imply the stated mathematical conclusion. The stated conclusion holds.
Formal statement
Proof (Lean source)
The weighted approximation error, constrained-prior separation, and an explicit completed packet pair all have the square-root mass scale; universal constants then match the observed and causal minimax risks to the vanishing-overlap rate, and an estimator sequence is uniformly consistent exactly when the alphabet-to-effective-sample-size ratio tends to zero.