Formalization: Pointwise Causal Estimation with Weak Dose Support and Gaussian Measurement Error
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 (44d8edc) — statements may have moved since the audit.
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Basic 62 declarations Public schedule space, structural laws, model assumptions and decision problems.
Public schedule space, structural laws, model assumptions and decision problems. The model has bounded fixed-dose potential outcomes; ranks constrain only lower witnesses.
The compact public dose and rank domain.
Continuous threshold profiles with the uniform topology and its Borel sigma algebra.
The threshold-profile space is equipped with its Borel measurable structure.
Definition (Lean source)
Data carried by a public Borel schedule space.
Definition (Lean source)
Public Borel schedules with jointly measurable evaluation and measurable threshold embedding.
Definition (Lean source)
Structural coordinates (X,A,Z,schedule,Y,U).
Stratum coordinate of a structural record.
Definition (Lean source)
Latent treatment coordinate of a structural record.
Definition (Lean source)
Classical error coordinate of a structural record.
Definition (Lean source)
Whole potential-outcome schedule coordinate of a structural record.
Definition (Lean source)
Observed outcome coordinate of a structural record.
Definition (Lean source)
Auxiliary rank coordinate of a structural record.
Definition (Lean source)
The prespecified target dose is one half.
Definition (Lean source)
The noncoverage level one tenth, recorded as an example value only: no result of this development uses it, since the honest-interval and frontier results quantify over the noncoverage level α.
Definition (Lean source)
Latent dose centered at the target.
Definition (Lean source)
Observed contaminated dose, formed by adding scaled classical error to the latent treatment.
Definition (Lean source)
Observed dose centered at the target.
Definition (Lean source)
Public observed record consisting of stratum, contaminated dose and outcome.
Definition (Lean source)
The structural-to-observed record map.
Definition (Lean source)
One-record observed law obtained by pushing forward the structural law.
Definition (Lean source)
Probability mass of a public confounder stratum.
Definition (Lean source)
Evaluation of a subject’s potential-outcome schedule at a fixed dose.
Definition (Lean source)
Population potential-outcome expectation at the target dose.
Definition (Lean source)
Conditional potential mean, defined by its stratum-restricted integral divided by stratum mass.
Definition (Lean source)
Public constants of the model class: a minimum stratum mass in (0, 1/2] and lower and upper weak-design envelope constants with 0 < lower ≤ upper.
Definition (Lean source)
Both strata have mass at least the public minimum and at most one minus it, the minimum being the given number.
Definition (Lean source)
Both strata of the law have strictly positive mass.
Definition (Lean source)
The latent treatment has compact support.
Definition (Lean source)
Structural law conditioned on a finite confounder stratum, by normalized restriction.
Definition (Lean source)
In each stratum of the law, the centered latent dose has a density lying between the lower envelope constant and the upper envelope constant times the absolute centered dose raised to the design exponent, the lower constant, the upper constant and the design exponent being given.
Definition (Lean source)
Radius-one Holder increment bound on the public dose interval.
Definition (Lean source)
The conditional potential means lie in the unit interval.
Definition (Lean source)
Standard Gaussian measurement-error coordinate.
Definition (Lean source)
Classical error is independent of stratum, treatment and the whole schedule.
Uniform auxiliary rank in each stratum, used only in the lower witnesses.
Definition (Lean source)
Rank-dose conditional independence through finite-stratum factorization.
Definition (Lean source)
Common-rank threshold schedules for the lower subclass.
Definition (Lean source)
Observed outcomes are consistent with the realized latent dose.
Definition (Lean source)
Whole-schedule exchangeability through exact finite-stratum factorization.
Definition (Lean source)
Binary outcomes at every fixed dose; fixed-dose null sets may differ.
Definition (Lean source)
Bounded outcomes at every fixed dose, with exactly the fixed-dose quantifier order.
Definition (Lean source)
The bounded causal model bundles exactly its ten declared member assumptions.
Definition (Lean source)
Every member law of the model gives both strata strictly positive mass, since the public minimum stratum mass is positive.
Formal statement
Proof (Lean source)
Probability laws satisfying exactly the bounded noisy-dose causal model assumptions.
Definition (Lean source)
Independent observed records from the pushed-forward structural law.
Definition (Lean source)
The sample law is the iid observed product law.
Definition (Lean source)
The constructed observed experiment satisfies the declared iid sampling predicate. This is the stated conclusion.
Formal statement
Proof (Lean source)
An independent uniform seed on the unit interval for randomized procedures.
Definition (Lean source)
Observed iid records together with an independent uniform randomization seed.
Definition (Lean source)
All measurable estimators, including independent uniform randomization.
Definition (Lean source)
Complete-lattice minimax absolute risk, with non-integrable losses retaining infinite risk.
Definition (Lean source)
Measurable connected intervals based solely on the observed sample, with unrestricted endpoint types.
Definition (Lean source)
A connected interval procedure covers the causal target with the required probability under every member law.
Definition (Lean source)
Minimum worst-law expected length among honest connected interval procedures.
Definition (Lean source)
Effective dimension of the direct weak-design estimation problem.
Definition (Lean source)
The public logarithmic sample scale.
Direct weak-design localization scale.
Definition (Lean source)
Gaussian Fourier-inversion localization scale.
Compact-support polynomial-inversion localization scale.
The exact three-regime localization scale.
Definition (Lean source)
Absolute-risk frontier obtained by raising the localization scale to the smoothness exponent.
Definition (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.CertificateMoments 16 declarations Tonelli and the weak-design envelope supply the public second moments for both signed inverse-weight sample marks.
Tonelli and the weak-design envelope supply the public second moments for both signed inverse-weight sample marks. Product sampling then gives unbiased block averages, variance and absolute-error bounds, and independence of disjoint blocks.
A nonnegative stratum mark is its conditional integral multiplied by stratum mass. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Error independence factors the conditional inverse-weight square by Tonelli. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The upper density envelope bounds each conditional inverse-weight second moment. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The unmarked structural stratum mark has second moment at most the public envelope. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Bounded realized outcomes make the marked square no larger than the unmarked square. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A finite extended second-moment envelope gives genuine square-integrability and a real bound. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The observed denominator mark has a finite square and its public second-moment bound. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The observed outcome-marked weight has a finite square and the same public bound. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Both observed marks have variance at most the public inverse-weight moment. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Averages over disjoint deterministic blocks are independent, even for different marks. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A nonempty deterministic average of square-integrable iid marks is unbiased, and its variance is the single-mark variance divided by the block size. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Cauchy--Schwarz bounds expected absolute deviation by the square root of variance. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The denominator block is unbiased and has variance at most Vq divided by its size. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The outcome-marked block is unbiased and obeys the same variance envelope. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Absolute error of each empirical inverse moment is bounded by its public standard deviation. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Empirical stratum frequency is unbiased with the Bernoulli variance bound. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.CitedGates 13 declarations Five explicit cited logical gates, and the separate direct Gaussian regression benchmark.
Five explicit cited logical gates, and the separate direct Gaussian regression benchmark. These propositions are inputs to conditional consumers and contain no proof placeholders.
Angular distance on the symmetric unit interval.
Endpoint-regularized Jacobi weight at the public spectral degree.
Definition (Lean source)
A smooth cutoff on the nonnegative half-line, supported between one half and two.
Definition (Lean source)
Petrushev and Xu (2005), Theorem 2.4, equation (2.14), arXiv:math/0508581. The smooth-filter specialization permits every positive decay exponent.
Definition (Lean source)
Kyriazis, Petrushev and Xu (2008), Theorem 2.2, equation (2.4), https://people.math.sc.edu/pencho/Publications/kpx-06-28-06-web.pdf. The constant depends on the fixed local angular radius and decay exponent.
Definition (Lean source)
NIST Digital Library of Mathematical Functions, Table 18.3.1, Jacobi row and caption, https://dlmf.nist.gov/18.3 (accessed 2026). Orthogonality and the positive squared norm.
Definition (Lean source)
NIST DLMF (accessed 2026), equation 5.11.12, https://dlmf.nist.gov/5.11.E12. Positive real-axis specialization; the shifted arguments are eventually positive.
Fixed power-law design in the separate direct Gaussian-response experiment.
Definition (Lean source)
Exact balance bandwidth of the separate power-law Gaussian-response regression benchmark.
Definition (Lean source)
Definition 2's local polynomial approximation class, retaining linear polynomials at s=1.
Definition (Lean source)
Direct regression record formed from an independent design draw and Gaussian response noise.
All-estimator pointwise absolute minimax risk in the separate direct regression experiment with the local polynomial approximation class.
Definition (Lean source)
Gaiffas (2005), Definition 2 and Theorem 1, equations (2.1), (2.4), (2.5), PDF pages 3–4, https://arxiv.org/pdf/math/0410354v3. Exact power-law specialization with absolute loss, in a separate direct regression experiment. No causal-class inclusion or honest-length assertion is carried by this gate.
Definition (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.ConditionalMean 17 declarations Product integration of schedule evaluations and bounded regression tests.
Product integration of schedule evaluations and bounded regression tests.
Normalized stratum integrals equal the corresponding indicator integrals divided by mass. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The stratum coordinate is constant under its normalized stratum law. This is the stated conclusion.
Formal statement
Proof (Lean source)
Integrable population expectations split into the two normalized stratum expectations. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The projected potential mean is a globally measurable extension of its Holder version.
Definition (Lean source)
Holder regularity makes the projected mean Borel in dose and stratum. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Projection preserves the public mean bound at every real input dose. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Integrating a fixed schedule evaluation under its stratum marginal gives the potential mean. This is the stated conclusion.
Formal statement
Proof (Lean source)
Clipped joint evaluation is bounded everywhere and agrees with the schedule almost surely.
Definition (Lean source)
The clipped schedule evaluation is jointly Borel. This is the stated conclusion.
Formal statement
Proof (Lean source)
Clipped schedule evaluations take values in the unit interval. This is the stated conclusion.
Formal statement
Proof (Lean source)
Fixed-dose boundedness justifies replacing schedule evaluation by its clipped version. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Consistency and integrated fixed-dose bounds identify the clipped random evaluation with Y. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equation (3) follows by integrating the schedule coordinate in the conditional product law. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The projected random-dose mean is measurable under the population law. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The globally projected mean is integrable by the public range bound. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Summing equation (3) over the two strata gives the bounded-test characterization. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Bounded Borel tests characterize the conditional mean on a generated sigma algebra. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DictionaryScore 11 declarations Helpers — DictionaryScore
Helpers — DictionaryScore
Each restricted stratum law is dominated by its normalized conditional law. This is the stated conclusion.
Formal statement
Proof (Lean source)
The design envelope controls nonnegative latent-dose integrals in each stratum. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Summing the two strata gives a finite-envelope bound for the marginal latent dose. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Finite public second moments imply law-level inverse integrability over the causal model. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The constant dictionary element is the degree-one polynomial inverse pair. This is the stated conclusion.
Formal statement
Proof (Lean source)
Every dictionary member satisfies its family's admissibility domain. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The factor by which the public certificate can exceed the unit-constant reference certificate: the largest of one, the upper envelope over sixty-four times the lower envelope, and the square root of the upper envelope over sixteen divided by sixteen times the minimum stratum mass times the lower envelope, for the public class constants.
Definition (Lean source)
The score scale of any public class constants is positive.
Formal statement
Proof (Lean source)
For an admissible inverse pair, the public error certificate at class constants K is at most the score scale times the unit-constant reference certificate.
Formal statement
Proof (Lean source)
A dictionary tag whose unit-constant reference score is at most a multiple of a rate has public score at most the score scale times that multiple of the rate, for a design exponent between zero and two and an error scale between zero and one quarter.
Formal statement
Proof (Lean source)
Every dictionary pair is admissible, and branch-specific witnesses control the selected public score uniformly. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DictionaryScore.Fourier 26 declarations Helpers — DictionaryScore — Fourier
Helpers — DictionaryScore — Fourier
The declared continuous extension agrees with Mathlib's sinc sixth power. This is the stated conclusion.
Proof (Lean source)
Fourier latent weights are continuous at the target as well as away from it. This is the stated conclusion.
Formal statement
Proof (Lean source)
The sixth power gives a nonnegative latent weight on the entire line. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Sinc's unit bound bounds every latent Fourier weight by one. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Away from zero, the sine unit bound gives the sixth-order localization tail. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The localization weight is even about the causal target. Under the stated conditions. This is the stated conclusion.
Nonnegative design exponents give continuous weighted Fourier moments. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Each weighted latent moment is finite on the compact dose support. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The continuous weight equals one at zero and stays positive nearby. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Positive mass near the target gives a strictly positive public denominator. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The sixth-order sinc tail dominates every design moment needed in S1 by an integrable cubic tail. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The unscaled Fourier kernel has finite whole-line moments for all exponents used in S1. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Scaling a Fourier weight scales its weighted integrand by the bandwidth power. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The exact whole-line change of variables gives the upper moment's bandwidth exponent in S1. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The weighted Fourier kernel is integrable on the entire line at every positive bandwidth. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Restricting a nonnegative whole-line moment gives the S1 upper bound with a fixed constant. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Changing variables on the latent dose interval gives the exact truncated S1 moment. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The fixed positive central moment supplies a bandwidth-independent lower constant in S1. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Both constants in the Fourier localization moment comparison are positive and independent of bandwidth. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The numerator and denominator moment comparisons assemble the S1 public bias bound. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The inverse Fourier integral is continuous in the observed dose. This is the stated conclusion.
Formal statement
Proof (Lean source)
The inverse Fourier integral has a finite uniform bound given by its multiplier norm. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A bounded observable Fourier weight is integrable under each shifted Gaussian channel. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Squaring preserves the uniform inverse-weight bound. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Compact dose support and a bounded inverse weight give finite weighted joint second moments. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The extended Fourier second moment is finite for every nonnegative design exponent. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DictionaryScore.FourierInverse 14 declarations Finite box convolutions and Gaussian inversion for the Fourier dictionary.
Finite box convolutions and Gaussian inversion for the Fourier dictionary.
The uniform frequency box whose transform is the bandwidth-scaled sinc.
The frequency box has finite absolute mass. Under the stated conditions. This is the stated conclusion. This is the stated conclusion. This is the stated conclusion. This is the stated conclusion.
Formal statement
Proof (Lean source)
Direct integration of the uniform box gives the sinc transform. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Supports of two box convolutions add their radii. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The sixth sinc power is the Fourier transform of six uniform boxes (S2--S3). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The sinc-six localization is absolutely integrable on the real line. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Fourier inversion of the finite box convolution proves compact spectral support. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The continuous transform is integrable because its spectrum is compact. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The scalar and vector Fourier conventions agree on the real line. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Compact spectral support makes the inverse Gaussian multiplier integrable. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Gaussian averaging cancels the inverse multiplier frequency by frequency. This is the stated conclusion.
Formal statement
Proof (Lean source)
Absolute Fubini gives exact cancellation of the Gaussian multiplier (S4--S5). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Exact Fourier inversion has positive finite weighted moments and finite Gaussian second moments. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The public Fourier second moment is an ordinary nonnegative joint integral. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DictionaryScore.FourierQuantitative 16 declarations Sinc-six profile prerequisites for the promoted weighted inverse-Gaussian bounds.
Sinc-six profile prerequisites for the promoted weighted inverse-Gaussian bounds.
Whole-line localization moments give three continuous spectral derivatives. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The spectral support radius agrees with the promoted theorem's convention. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Compact spectral support is independent of the noise scale. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The spectral height is controlled by the unscaled sinc-six mass. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The first absolute localization moment justifies differentiation under the Fourier integral. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The derivative height has order h squared with a fixed unscaled moment constant. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Fixed nonnegative constants supply precisely the profile hypotheses of the promoted bound. This is the stated conclusion.
Formal statement
Proof (Lean source)
Two continuous compactly supported frequency derivatives make the inverse absolutely integrable. This is the integrability part of S6, obtained from Mathlib's derivative identities. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The inverse and derivative inverse satisfy the promoted theorem's absolute inversion hypotheses. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Specializing the promoted frequency estimate proves the weighted physical-space bound in S6. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Finite ordinary and quadratic kernel energies imply joint design/noise integrability. A measure-preserving dose translation reduces this bookkeeping step to product integrals. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The complex sinc-six inverse has jointly integrable weighted second moments on the full dose line. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The public real inverse is the real part of the promoted complex inverse multiplier. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The public real second moment is bounded by the complex shifted-variance quantity. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The promoted specialization gives the full uniform inverse-variance envelope in S7. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
S1 and S7 assemble the observable certificate in S8, with its stochastic term kept under one square root for subsequent tuning. All constants are independent of n, h and sigma. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DictionaryScore.FourierTuning 8 declarations Uniform logarithmic tuning for the Fourier dictionary.
Uniform logarithmic tuning for the Fourier dictionary.
The logarithmic factor in S9 is uniformly bounded for effective sample size at least one. The fixed bandwidth multiplier twelve leaves three quarters of the exponential available for absorbing the logarithmic powers. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The Fourier scale is positive whenever the noise scale is positive. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The effective sample size exactly balances the power of the Fourier scale against its logarithmic denominator. This is the algebraic normalization used in S9. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
At twelve times the Fourier scale, S9 bounds the stochastic term by the bandwidth bias. The bound is uniform in every effective sample size at least one. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Dropping the nonnegative noise multipliers from S9 bounds the inverse effective bandwidth. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The Fourier scale is no larger than the positive noise scale. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The unweighted frequency error is controlled by the Fourier bias throughout intermediate tuning, using the inverse-power consequence of S9. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
S8 and S9 control the certificate at any bandwidth rounded up from twelve times the Fourier scale, provided the rounded bandwidth is in the public window. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DictionaryScore.FourierWitness 15 declarations Fourier dictionary tuning and comparison witness.
Fourier dictionary tuning and comparison witness.
The declared integer-power bandwidth is the usual decreasing dyadic sequence. This is the stated conclusion.
Formal statement
Proof (Lean source)
Rounding up to a dyadic bandwidth enlarges a positive scale by less than two. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Every dyadic bandwidth in the declared numerical window is a Fourier dictionary member. The lower bandwidth cutoff also implies the finite index cutoff. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A scale within the window can be rounded up to an available dictionary bandwidth. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Enlarging the bandwidth decreases every factor in the stochastic S8 bound. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The direct scale balances squared bias against inverse weighted sample size. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The exact S8 stochastic factor at the direct scale, before its bounded noise multiplier. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
At the direct scale the unweighted sample-frequency term is smaller than the bias. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
S8 at any rounded-up direct-regime bandwidth has the direct minimax rate. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
For large samples the direct scale fits the dyadic window, uniformly in the noise scale. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The first frontier regime has an actual Fourier dictionary witness at the stated rate. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
In the intermediate regime the effective Fourier sample size is at least one. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
S9 and the noise elbow place the tuned intermediate bandwidth in the dictionary window for all sufficiently large samples, uniformly in the noise scale. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The intermediate regime has a genuine Fourier dictionary witness at the frontier rate. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
This branch supplies a dictionary witness with score at most a fixed multiple of the frontier. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DictionaryScore.HeatAlgebra 28 declarations Finite inverse-heat algebra and its Gaussian Hermite expansion (roadmap S12).
Finite inverse-heat algebra and its Gaussian Hermite expansion (roadmap S12). All coefficient comparisons are finite; the shared Hermite substrate supplies Gaussian means.
Iterated polynomial derivative used in finite heat coefficient comparisons.
Definition (Lean source)
The inverse heat operator with an arbitrary public degree cutoff.
Definition (Lean source)
Iterated polynomial differentiation distributes over finite sums. This is the stated conclusion. This is the stated conclusion. This is the stated conclusion. This is the stated conclusion.
Formal statement
Proof (Lean source)
Scalar polynomial coefficients commute with iterated differentiation. This is the stated conclusion.
Formal statement
Proof (Lean source)
Every monomial derivative has its descending-factorial coefficient, including zero derivatives above the monomial degree. This is the stated conclusion.
Formal statement
Proof (Lean source)
Derivatives above any upper degree bound vanish. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The finite heat operator distributes over finite polynomial sums. This is the stated conclusion.
Formal statement
Proof (Lean source)
The finite heat operator commutes with scalar polynomial coefficients. This is the stated conclusion.
Formal statement
Proof (Lean source)
Enlarging a degree cutoff adds only identically zero heat terms. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Applying inverse heat coefficientwise gives the finite monomial decomposition prescribed in the covariance proof roadmap. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The even factorial splits into its even and odd double-factorial products. This is the stated conclusion.
Formal statement
Proof (Lean source)
Each nonzero Hermite coefficient equals the corresponding inverse-heat coefficient. This is the stated conclusion.
Formal statement
Proof (Lean source)
Unit-noise inverse heat maps a monomial to the corresponding Hermite polynomial. This is the stated conclusion.
Formal statement
Proof (Lean source)
Affine substitution multiplies the iterated derivative by the appropriate power of its slope. This is the stated conclusion.
Formal statement
Proof (Lean source)
The coefficients after affine substitution are the scaled finite Taylor coefficients. This is the stated conclusion.
Formal statement
Proof (Lean source)
Translation and scaling reduce inverse heat evaluation to the unit-noise operator. This is the stated conclusion.
Formal statement
Proof (Lean source)
A polynomial of bounded degree has the exact finite inverse-heat Hermite expansion. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The constant Hermite mode extracts each Gaussian mean. This is the stated conclusion.
Formal statement
Proof (Lean source)
Finite Hermite sums have Gaussian mean equal to their constant coefficient. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Finite coefficient comparison and Hermite means prove exact polynomial Gaussian inversion. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The even Chebyshev expansion has degree at most six times the original index. This is the stated conclusion.
Proof (Lean source)
The declared inverse weight evaluates the finite heat transform at its valid degree cutoff. This is the stated conclusion.
Formal statement
Proof (Lean source)
Gaussian expectation of every polynomial dictionary inverse equals its latent weight. This is the stated conclusion.
Formal statement
Proof (Lean source)
Orthogonality removes all mixed modes from a finite Hermite square. This is the stated conclusion.
Formal statement
Proof (Lean source)
The finite inverse-heat expansion has the exact derivative-square second moment. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Every polynomial dictionary inverse satisfies the exact identity in S12, at zero noise too. This is the stated conclusion.
Formal statement
Proof (Lean source)
One falling-factorial square is bounded by a binomial coefficient times a degree power. This is the stated conclusion.
Formal statement
Proof (Lean source)
Derivative bounds give the binomial second-moment envelope in roadmap S13. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DictionaryScore.InverseHeat 27 declarations Helpers — DictionaryScore — InverseHeat
Helpers — DictionaryScore — InverseHeat
The polynomial localization weight is continuous on the entire real line. This is the stated conclusion.
Formal statement
Proof (Lean source)
The sixth power defining the latent weight is nonnegative, even off the dose support. This is the stated conclusion.
Formal statement
Nonnegative design exponents give continuous, finite weighted polynomial moments. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Compact latent support makes each nonnegative-exponent polynomial moment integrable. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The continuous odd-degree weight is positive on a neighborhood of the target. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A positive neighborhood and the power design weight give a strictly positive denominator. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
All polynomial functions have finite Gaussian moments, by finite monomial expansion. This is the stated conclusion.
Formal statement
Proof (Lean source)
Affine substitution preserves polynomiality, so inverse-heat derivatives are Gaussian integrable. This is the stated conclusion.
Formal statement
Proof (Lean source)
Every affine Gaussian evaluation of the finite inverse-heat sum is integrable. This is the stated conclusion.
Formal statement
Proof (Lean source)
Compact weighted dose support and Gaussian moments integrate every affine polynomial. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The finite inverse-heat derivative sum is an ordinary polynomial on the whole line. This is the stated conclusion.
Formal statement
Proof (Lean source)
The squared inverse-heat weight has a finite weighted joint Gaussian moment. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Finite polynomial Gaussian moments discharge the extended second-moment obligation. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The public polynomial second moment is an ordinary nonnegative joint integral. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The public polynomial variance is the finite sum of weighted derivative-square moments (S12). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Uniform derivative bounds imply the public polynomial variance envelope in S13. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Monomial expansion gives the exact finite derivative evaluation used in S13. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
On the unit interval, coefficient absolute mass controls every polynomial derivative, with the descending factorial of any public degree bound. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The exact Hermite second moment has an unconditional coefficient-mass envelope. This isolates the remaining exponential coefficient estimate in S13 from all Gaussian algebra. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The declared polynomial inverse has a public variance bound computed directly from its finite monomial coefficients, with no derivative-bound premise (roadmap S13). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
With zero noise, only the zeroth derivative survives in the inverse-heat sum. This is the stated conclusion.
Proof (Lean source)
At zero noise the polynomial pair satisfies the exact inverse relation directly. This is the stated conclusion.
Formal statement
Proof (Lean source)
Every valid polynomial pair is admissible in the noiseless channel. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Degree one gives the constant polynomial weight everywhere. This is the stated conclusion.
Formal statement
The degree-one inverse-heat sum is exactly the constant inverse, for every noise scale. This is the stated conclusion.
Formal statement
The constant dictionary pair is admissible without any analytic inversion placeholder. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Exact polynomial inversion has positive finite weighted moments and finite Gaussian second moments. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DictionaryScore.PolynomialEnvelope 15 declarations Finite coefficient algebra completes roadmap S13 for the declared polynomial localization weights.
Exponential polynomial variance envelope
Finite coefficient algebra completes roadmap S13 for the declared polynomial localization weights. The second-kind Chebyshev recurrence bounds coefficient mass by an exponential; the quadratic substitution and sixth power preserve an exponential degree bound. Combining this with the exact Gaussian second-moment calculation gives a public variance envelope.
The coefficient norm may be computed over any range beyond the degree. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The coefficient norm is nonnegative. This is the stated conclusion.
Formal statement
Proof (Lean source)
Coefficientwise triangle inequalities control sums and differences. This is the stated conclusion.
Formal statement
Proof (Lean source)
Differences obey the same coefficientwise triangle inequality. This is the stated conclusion.
Formal statement
Proof (Lean source)
Constant multiplication scales coefficient mass exactly. This is the stated conclusion.
Formal statement
Proof (Lean source)
Finite sums preserve the coefficient triangle inequality. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Submultiplicativity iterates to every finite power. This is the stated conclusion.
Formal statement
Proof (Lean source)
The second-kind Chebyshev recurrence gives an exponential coefficient envelope. This is the stated conclusion.
Formal statement
Proof (Lean source)
Each coefficient is bounded by the whole coefficient mass. This is the stated conclusion.
Formal statement
Proof (Lean source)
The quadratic substitution in the declared localization weight has coefficient mass five. This is the stated conclusion.
Formal statement
Proof (Lean source)
Direct finite Chebyshev algebra bounds the declared sixth-power weight exponentially in its degree. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The declared polynomial's finite coefficient sum has the exponential degree envelope in S13. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The exact inverse-heat variance has a public exponential envelope, without a derivative premise. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The unit latent weight has weighted mass at most one for nonnegative design exponents. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
S13 holds with explicit universal coefficient base and prefactor. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DictionaryScore.PolynomialLocalization 13 declarations Roadmap S11: the odd polynomial weight is bounded by one, has a sixth-order tail, and is bounded below on an interval of radius proportional to the inverse degree.
Polynomial localization bounds
Roadmap S11: the odd polynomial weight is bounded by one, has a sixth-order tail, and is bounded below on an interval of radius proportional to the inverse degree. These estimates use the declared trigonometric representation, including its value at zero.
The addition formula bounds the sine of an integer multiple. This is the stated conclusion.
Proof (Lean source)
The normalized sine quotient never exceeds one on the latent support. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The numerator's unit bound gives sixth-order decay away from the target. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Jordan's inequality controls arcsine linearly throughout the dose support. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
On the inverse-degree central interval the weight has a fixed positive lower bound. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Dilation of a central power moment gives the precise localization exponent. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
S11's denominator lower bound follows from the fixed central plateau. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A rescaled cubic tail dominates all S11 weighted integrands uniformly in degree. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The dominating cubic envelope is integrable at every positive localization scale. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The envelope's whole-line integral scales with exactly the S11 moment exponent. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
S11's upper bound has a degree-independent constant for every required exponent. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The constants in S11 are positive and independent of the odd degree. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The moment comparison assembles the exact S11 bias rate for every valid degree. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DictionaryScore.PolynomialTuning 16 declarations Compact-support dictionary tuning: the odd dyadic degree window (S14) and quantitative control of the exponential inverse-heat variance factor (S15).
Compact-support dictionary tuning: the odd dyadic degree window (S14) and quantitative control of the exponential inverse-heat variance factor (S15).
Rounding down a target degree at least four gives an available odd degree between one quarter and the target. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The degree cutoff implies the finite polynomial index cutoff in the public dictionary. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
S14 rounding gives a dictionary element whenever the target is in the degree window. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The compact-support logarithmic denominator is at least one, uniformly in noise. Under the stated conditions. This is the stated conclusion.
Proof (Lean source)
A degree below L/(4096 B) makes the logarithm of the S13 square-root variance factor at most L/16; the constants are public and independent of noise. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Exponentiating S15 gives the squared variance multiplier bound directly. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The target degree L/(4096 B) eventually lies between four and n squared, uniformly over the full public noise range (S14). This is the stated conclusion.
Formal statement
Proof (Lean source)
S14 provides an actual odd polynomial dictionary element in the public tuning window. This is the stated conclusion.
Formal statement
Proof (Lean source)
At logarithmic sample sizes at least two, the squared S15 multiplier is at most n^(1/4). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
S13 and S15 give a finite public variance bounded by 16 n^(1/4), with no analytic premise on the chosen degree. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The tuned Gaussian standard deviation is at most 4 n^(-3/8). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Fixed logarithmic powers are eventually dominated by n^(3/8). This is the uniform stochastic-to-bias comparison in S16. This is the stated conclusion.
Proof (Lean source)
The S11 denominator lower bound controls the public ratio multiplier. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
If the logarithmic degree is legal and the uniform logarithmic power is absorbed, the stochastic rate n^(-3/8) m^(kappa+1) is at most the localization bias. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The rounded polynomial certificate has the inverse-degree bias rate (S16). This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The direct cutoff is eventually below the logarithmic cutoff, so high-noise polynomial tuning selects the third branch of the public frontier. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DictionaryScore.PolynomialWitness 1 declarations The compact-support inverse-heat dictionary witness, assembled from S11--S16.
The compact-support inverse-heat dictionary witness, assembled from S11--S16.
This branch supplies a dictionary witness with score at most a fixed multiple of the frontier. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DirectObservedContraction 7 declarations Direct-regime observed energy contraction, equations (17)--(18).
Direct-regime observed energy contraction, equations (17)--(18).
Weighted Cauchy--Schwarz follows from the nonnegative centered quadratic integral. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Multiplication by a continuous function preserves integrability of the compact design density. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
At each observed dose the squared signed convolution is controlled by its quadratic convolution. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Absolute Fubini preserves the signed integral under Gaussian smoothing. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Integrating the pointwise contraction gives the observed energy bound in equation (18). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The direct threshold pair has the actual observed one-record budget at every positive noise scale. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
With the direct bandwidth, the observed pair has a sample budget independent of noise and sample size. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.DirectPerturbation 11 declarations Direct-regime compact bump bounds for the observed lower-bound construction.
Direct-regime compact bump bounds for the observed lower-bound construction.
The direct-regime compact bump of equation (14), including its zero extension.
Definition (Lean source)
Squaring on the unit interval has Lipschitz constant two. This is the stated conclusion. Under the stated conditions. This is the stated conclusion. Under the stated conditions. This is the stated conclusion. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The clipped polynomial representation includes the zero extension at both endpoints. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The bump lies between zero and its tuning amplitude. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The compact bump vanishes off its stipulated support. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Clipping exposes continuity of the zero-extended bump without an endpoint exception. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The bump's increment is bounded by four times its amplitude times scaled distance. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The two distance regimes in (15) give the scale-free Hölder seminorm. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Small direct-regime amplitudes give the two actual continuous threshold profiles, with the paper's range and radius-one Hölder seminorm. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The amplitude at the target is exactly the direct tuning amplitude. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The direct bump times the power-law design is an integrable compact signed density. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.Estimator 62 declarations Public inverse pairs, deterministic dictionary selection and the split clipped estimator.
Public inverse pairs, deterministic dictionary selection and the split clipped estimator.
A public latent weight paired with its observable inverse.
Definition (Lean source)
Lebesgue moment of a public latent weight against an absolute power of the centered dose.
Definition (Lean source)
Reference denominator floor at the unit constants (stratum mass one quarter, lower envelope one quarter), used only to calibrate the dictionary tuning.
Definition (Lean source)
Reference localization-bias bound at the unit envelope constants, used only to calibrate the dictionary tuning.
Definition (Lean source)
Public lower bound for the unmarked weighted denominator: the minimum stratum mass times the lower envelope constant times the weighted moment.
Definition (Lean source)
Public localization-bias bound: the envelope ratio times the ratio of the higher to the base weighted moment.
Definition (Lean source)
Extended Gaussian inverse-weight second moment; infinite values are retained.
Real value of the reference second moment, used only after its finiteness is established.
Public extended second-moment bound: the reference moment rescaled from the reference upper envelope sixteen to the public upper envelope constant.
Definition (Lean source)
Real value of the public second-moment bound.
Definition (Lean source)
Public sum of localization bias, denominator-scaled second-moment error and stratum-frequency error.
Definition (Lean source)
Reference error certificate at the unit constants, used only to calibrate the dictionary tuning.
The public second-moment bound for class constants K is finite whenever the reference moment is, so it is a real number.
Formal statement
Proof (Lean source)
The real public second-moment bound for class constants K equals the upper envelope constant over sixteen times the real reference moment.
Formal statement
Exact, finite pointwise Gaussian inversion and a positive finite weighted moment.
Definition (Lean source)
Absolute integrability of the inverse weight under the structural law’s observed centered dose.
Definition (Lean source)
The sixth power of sinc, with its continuous value at zero.
Definition (Lean source)
Positive Fourier localization weight at the specified bandwidth.
Definition (Lean source)
Mathlib's Fourier convention uses exp(-2π i ξt); the multiplier uses ω=2πξ.
Definition (Lean source)
Polynomial extension of the odd-degree sinc-of-arcsine weight, through even U coefficients.
Evaluation of the polynomial extension of the positive odd-degree localization weight.
Definition (Lean source)
Finite polynomial inverse-heat sum of the even derivatives of the latent weight.
Definition (Lean source)
Reflection multiplies the nth polynomial coefficient by its parity sign. This is the stated conclusion. This is the stated conclusion. This is the stated conclusion. This is the stated conclusion.
Formal statement
Proof (Lean source)
An even-degree second-kind Chebyshev polynomial has no odd coefficients. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Splitting a finite sum into its even and odd indices. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The polynomial weight is the sixth power of the normalized Chebyshev evaluation. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Odd polynomial weights agree with their continuous trigonometric formula. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Public family and degree tags, with constant tags first, then Fourier indices, then polynomial indices.
Definition (Lean source)
Public family and degree tags, with constant tags first, then Fourier indices, then polynomial indices.
Definition (Lean source)
Dyadic localization bandwidth indexed by a nonnegative integer.
Definition (Lean source)
Finite candidate list in the fixed deterministic tie-breaking order.
Definition (Lean source)
The finite public Fourier, polynomial and constant dictionary with increasing-index tie order.
Definition (Lean source)
Latent weight and observable inverse associated with a public dictionary tag.
Expected-error certificate of the pair associated with a dictionary tag.
Definition (Lean source)
Reference certificate of a dictionary tag at the unit constants, used only to calibrate the dictionary tuning.
Minimum-score public tag, retaining the first tag in the fixed order when scores tie.
Definition (Lean source)
Deterministic modulo-three sample block.
All three deterministic split blocks contain at least one observed record.
Definition (Lean source)
Block-zero empirical frequency of a confounder stratum.
Definition (Lean source)
Block-one empirical inverse-weight denominator in a confounder stratum.
Definition (Lean source)
Block-two empirical outcome-marked inverse-weight numerator in a confounder stratum.
Definition (Lean source)
Empirical stratum ratio with the public denominator floor and projection to the unit outcome interval.
Definition (Lean source)
Stratum-frequency weighted sum of the clipped empirical stratum ratios.
Definition (Lean source)
Population stratum-restricted inverse-weight denominator.
Definition (Lean source)
Population stratum-restricted outcome-marked inverse-weight numerator.
Definition (Lean source)
Population localized marked-to-unmarked ratio.
Definition (Lean source)
Total selected estimator with the midpoint fallback for empty split blocks.
Definition (Lean source)
The confidence interval for the public class constants at smoothness exponent, design exponent, noncoverage level, sample size and error scale, computed from the observed records: the total estimate plus or minus its public error score divided by the noncoverage level, clipped to the unit interval, with the whole unit interval as the small-sample fallback.
Definition (Lean source)
The selected tag is a dictionary member with score no larger than any other member. This is the stated conclusion. This is the stated conclusion. This is the stated conclusion. This is the stated conclusion.
Formal statement
Proof (Lean source)
The totalized real Fourier integral is continuous: nonintegrable inputs give the zero function. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The real inverse Fourier weight is Borel measurable for every public scale and bandwidth. This is the stated conclusion.
Formal statement
Proof (Lean source)
The finite inverse-heat polynomial weight is Borel measurable. This is the stated conclusion.
Formal statement
Proof (Lean source)
Every public dictionary tag supplies a Borel measurable inverse weight. This is the stated conclusion.
Formal statement
Proof (Lean source)
The empirical stratum frequency is Borel measurable in the records. This is the stated conclusion.
Formal statement
Proof (Lean source)
The empirical denominator is measurable whenever the public inverse weight is measurable. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The empirical marked numerator is measurable whenever the public inverse weight is measurable. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The floored and clipped stratum ratio is a measurable function of the records. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The weighted estimator is measurable whenever its public inverse weight is measurable. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The total public selected estimator is a measurable function of the observed records. This is the stated conclusion.
Formal statement
Proof (Lean source)
The declared clipped confidence interval is connected, including its small-sample fallback. This is the stated conclusion.
Formal statement
Proof (Lean source)
Membership in the declared confidence interval is jointly measurable in observed records and candidate target. This is the stated conclusion.
Formal statement
Proof (Lean source)
The declared confidence interval packaged as a measurable connected procedure based solely on the observed records.
Definition (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.FixedNoise 4 declarations Fixed positive noise selects the compact-support branch and its iterated-logarithm order.
Fixed positive noise selects the compact-support branch and its iterated-logarithm order.
The public sample logarithm diverges. This is the stated conclusion.
Every fixed positive noise eventually exceeds both branch cutoffs. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The compact-support scale is bounded above and below by the iterated-logarithm scale. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Taking the fixed smoothness power preserves the two-sided scale comparison. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.FrontierElbows 6 declarations Quantitative comparison of the inverse scales at the second frontier elbow.
Quantitative comparison of the inverse scales at the second frontier elbow.
The public logarithmic sample size is at least one for nonzero samples. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
At the second elbow the inverse square-root power is the reciprocal square root. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The polynomial inverse scale at the second elbow is a fixed constant over log(en). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The logarithm of log(en) is negligible compared with log(en). This is the stated conclusion.
Proof (Lean source)
At the second elbow the Fourier logarithm is comparable to log(en). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Both inverse scales agree up to fixed constants at the second elbow. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.GaussianConvolution 22 declarations Compact signed moments, Gaussian kernels, and witness-density domination
Compact signed moments, Gaussian kernels, and witness-density domination
Centered Gaussian density on the real line for positive sigma.
Convolution of an integrable signed density with the centered Gaussian density.
Definition (Lean source)
Factorial tail in the observed Gaussian moment-series comparison.
Definition (Lean source)
The centered Gaussian density is strictly positive at every real argument when its scale is positive. Under the stated conditions. This is the stated conclusion. Under the stated conditions. This is the stated conclusion. Under the stated conditions. This is the stated conclusion. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The centered Gaussian density is invariant under reflection. This is the stated conclusion.
Formal statement
Proof (Lean source)
The compact power-law witness density is nonnegative for nonnegative degeneracy. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The common compact witness density is symmetric about zero. This is the stated conclusion.
Formal statement
Proof (Lean source)
On the short interval on the same side as the observed dose, the Gaussian kernel is bounded below by its centered value times exp(-1/2). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The Gaussian convolution integrand of the compact witness density is integrable. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Convolving the symmetric witness density with a centered Gaussian preserves reflection symmetry. This is the stated conclusion.
Formal statement
Proof (Lean source)
Integrating over the positive short interval gives the public Gaussian reference-density bound for nonnegative observed doses. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Positive Gaussian reference-density domination holds on the entire observed real line. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Every polynomial moment of a compactly supported integrable signed density is integrable. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The absolute signed moment is bounded by the support radius power times the absolute mass. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Each squared Gaussian moment coefficient is bounded by the corresponding factorial majorant. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The Gaussian squared-moment series converges by comparison with the exponential series. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The factorial tail is summable for every real scale and radius. This is the stated conclusion.
Formal statement
Proof (Lean source)
The unmatched squared-moment sum is bounded by absolute mass squared times the public factorial tail. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Completing the square expresses the Gaussian kernel quotient as a translated Gaussian times an exponential. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The centered density agrees with Mathlib’s Gaussian density at variance sigma squared. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The positive-scale centered Gaussian density integrates to one. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The Gaussian kernel quotient integrates to the exponential interaction kernel. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.GaussianEnergy 7 declarations Absolute Fubini and exponential-series integration for compact signed densities.
Absolute Fubini and exponential-series integration for compact signed densities.
A translated positive-scale Gaussian density is integrable. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The interaction exponential is bounded on the support square. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Absolute mass controls the compact exponential interaction. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Absolute Fubini converts the squared Gaussian convolution into exponential energy. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Compact signed moments justify termwise integration of the exponential interaction. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Vanishing low-order moments remove exactly the initial terms of the Gaussian energy series. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Absolute Fubini also supplies integrability of the Gaussian-weighted energy. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.GaussianInjective 1 declarations Helpers — GaussianInjective
Helpers — GaussianInjective
Gaussian convolution is injective on compactly supported signed measures represented by Jordan pairs. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.GaussianMomentSeries 17 declarations Helpers — GaussianMomentSeries
Helpers — GaussianMomentSeries
Uniform rank thresholding gives the two-point outcome law. This is the stated conclusion.
Formal statement
Proof (Lean source)
Integrating out the independent rank exposes the two observed Bernoulli marks. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Scaling and translating the standard normal gives the Gaussian kernel used in the observed density. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The Gaussian channel integrates any measurable nonnegative test against its translated density. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Conditioning on dose and integrating out Gaussian noise gives the two nonnegative mark kernels. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Centering the latent dose replaces the compact subtype measure by its power density on the real line. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Each marked convolution integrand is integrable, so its real and nonnegative integrals agree. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The success-mark density is the half-reference density plus the smoothed centered profile. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The failure-mark density is the half-reference density minus the same smoothed centered profile. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A nonnegative dose mark integrates to its centered Gaussian convolution density. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The two observed marks have exactly the Gaussian convolutions of their latent success and failure densities. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equation (11): the observed law has the half-reference density plus or minus the centered signed convolution. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Each observed alternative is dominated by twice the half-success reference law. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The observed threshold alternative is absolutely continuous with respect to the half-success reference. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The observed likelihood ratio has a finite squared deviation, including at zero noise. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Compact support and integrability justify the exact Gaussian moment identity and its convergent tail. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Explicit AC and square-integrability obligations discharge the general-space iid tensorization API. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.IdentificationBasics 9 declarations Observed stratum identification, continuous potential means, and target decomposition.
Observed stratum identification, continuous potential means, and target decomposition.
Joint schedule evaluation gives measurability at every public fixed dose. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Bounded fixed-dose potential outcomes are integrable without an added premise. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
With bounded potential outcomes, the potential mean at a dose in the public interval, conditional on a positive-mass stratum, lies between zero and one.
Formal statement
Proof (Lean source)
Overlap makes each finite-stratum normalization strictly positive. Under the stated condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
Partitioning the fixed-dose potential expectation into the two positive strata gives its target formula. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The observed stratum marginal has exactly the structural stratum mass. This is the stated conclusion.
Formal statement
Proof (Lean source)
Observational equivalence identifies the overlap probabilities directly from the marginal. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Positive Holder exponent supplies continuity of the potential mean, including at the endpoints. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Lebesgue almost-everywhere agreement of the two Holder versions identifies every public dose. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.InversePerturbation 11 declarations Scaled inverse-regime packet profiles and their weighted cancellations, equations (20)--(23).
Scaled inverse-regime packet profiles and their weighted cancellations, equations (20)--(23).
The packet derivative bound gives the global increment bound, including the zero extension. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The scaled packet is supported on the stipulated radius. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The scaled packet has the exact tuning amplitude at the target. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The packet supremum bound scales by the nonnegative tuning amplitude. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The two distance cases in (21) give a scale-free Hölder bound for the inverse packet. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The packet times the design density is an integrable compact signed density. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Small inverse-regime packet amplitudes give the two actual continuous threshold profiles, with the paper's range and radius-one Hölder seminorm. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
On a packet's support the public design density is its unclipped power law. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Change of variables transfers every weighted packet cancellation to the signed latent density. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The floor cancellation order only uses moments strictly below the packet's real cutoff. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The packet absolute-mass bound scales as h to the power beta plus kappa plus one, as in (23). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.LatentIdentification 17 declarations Latent measures, local mass ratios, continuous mean recovery, and unmarked deconvolution.
Latent measures, local mass ratios, continuous mean recovery, and unmarked deconvolution.
Unmarked and potential-mean-marked conditional latent measures used in identification.
Definition (Lean source)
Conditional latent dose measure marked by the conditional potential-outcome mean.
Definition (Lean source)
Shrinking-neighborhood mass ratio of the identified marked and unmarked latent measures.
Definition (Lean source)
Normalized positive strata give finite latent dose laws. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The density representation puts all latent dose mass on the compact interval. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The lower power envelope makes every target neighborhood have positive mass. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The Holder mean is measurable and integrable under its compact latent dose law. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Marked latent mass is the integral of the potential mean against unmarked mass. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A positive local-mass ratio approximates the target with the paper's Holder error. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Positive Holder exponent sends the shrinking-neighborhood ratio to the target mean. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The weak-design lower envelope makes Lebesgue measure dominated by latent dose mass, including when the density vanishes at the single target point. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equality of the marked and unmarked measures identifies their nonnegative mean densities almost everywhere under the common latent law. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Dominated Lebesgue mass and Holder continuity extend the identified latent density ratio to every dose, including the design zero and both support endpoints. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The observed conditional record law is a normalized restriction of the public law. This is the stated conclusion.
Formal statement
Proof (Lean source)
Observational equivalence identifies the stratum-conditional centered observed dose law. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The unmarked observed conditional dose measure is latent dose convolved with Gaussian noise. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Injective Gaussian convolution identifies the unmarked latent dose law from observations. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.LowerAssembly 10 declarations Target separation (16), (22) and observed-product distance assembly (49)--(51).
Target separation (16), (22) and observed-product distance assembly (49)--(51).
The independent uniform threshold rank makes the causal target exactly the profile at the public dose. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Symmetric profiles have causal-target difference twice the perturbation at zero, on the fixed public path space. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Equation (16) is the exact absolute separation of the direct threshold witnesses. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equation (22) uses the same normalized packet as the moment cancellations. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The direct frontier branch agrees exactly with the separation amplitude. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Tensorization (49), the exponential bound, and Cauchy--Schwarz (50) convert a single-record budget to product TV. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A common reference and the logarithmic budget log(1+τ²) give the paper's pairwise product-TV bound (51) at level τ. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Applied to actual observed marginals, the common-reference budget log(1+τ²) controls the declared experiment's total variation by τ at every noise scale, including zero. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Two laws absolutely continuous with respect to a common reference, with square-integrable likelihood-ratio deviations and chi-square divergences from it, times the sample size, at most log(26/25), have n-fold product laws within total variation one fifth of each other; this is the paper's pairwise bound (51), the level-one-fifth instance of the general product-TV bound.
Formal statement
Proof (Lean source)
For a design exponent between zero and two, when the observed witness marginals are absolutely continuous with respect to the reference witness marginal, with square-integrable likelihood-ratio deviations and chi-square divergences, times the sample size, at most log(26/25), the two declared observed experiments are within total variation one fifth at every noise scale, including zero; this is the level-one-fifth instance of the general observed-experiment bound.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.LowerCompactTuning 9 declarations Compact-support degree, bandwidth and cancellation estimates (38)--(45).
Compact-support degree, bandwidth and cancellation estimates (38)--(45).
The compact logarithm satisfies both deterministic comparisons in (38). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The ceiling in (37) preserves the two-sided degree estimate (40). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The rounded compact degree retains the fraction of the frontier in (47). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equation (44) follows from (38) and the explicit ratio lower bound (43). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equations (40)--(45) force the compact cancellation exponent to exceed four log-scales. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equations (43)--(45) follow uniformly from the compact degree lower bound and (41). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
In the public compact regime, (38) gives a degree scale at least twice the square root of L. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equations (39)--(42): a single lower bound on L ensures any fixed degree threshold, and the compact bandwidth is positive and below the noise scale. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The concrete compact degree and its floor cancellation order satisfy (40), (42), (45), (46), and (47), uniformly over the public compact noise range. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.LowerRegimes 13 declarations Helpers — LowerRegimes
Helpers — LowerRegimes
The same centered perturbation determines both threshold profiles. Direct tuning uses h0=n^(-1/d); inverse tuning uses the normalized packet, h=ell/m and J=floor(cPacket*m). Support and weighted cancellations are conclusions about that constructed perturbation.
Definition (Lean source)
Equations (14)--(15) provide legal direct-regime profiles with the full localization construction, including compact support and signed-density integrability. Under the stated conditions. This is the stated conclusion. Under the stated conditions. This is the stated conclusion. Under the stated conditions. This is the stated conclusion. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The direct profiles satisfy their localization construction and the Gaussian-series comparison (27) whenever the public noise is positive. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equations (13)--(16) and the positive-noise comparison (27) hold for the same direct profiles after a deterministic, noise-independent sample cutoff. The amplitude and bandwidth range conditions are derived from the public tuning. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The direct profile construction also supplies equation (18) for every positive noise, with its sample budget independent of the noise scale. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The direct branch supplies separation, localization, Gaussian-series comparison and observed product-TV control at level τ with one noise-independent cutoff. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equations (20)--(23) give legal inverse-regime profiles and the full scaled localization construction, using the same packet and cancellation order throughout. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The inverse profiles satisfy both the full localization construction and the observed comparison (27). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equations (30)--(35) assemble the rounded intermediate degree, legal radius, positive cancellation order and uniform Gaussian-series sample budget. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equations (35)--(36) hold for the actual intermediate threshold profiles, with one rounded packet degree and cancellation order for construction and observed distance. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The concrete compact tuning assembles (46)--(47) for the actual threshold profiles, with the same packet, bandwidth and cancellation order used in (27). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
All three law witnesses are the explicit product-seed threshold laws. Their profiles, localization, cancellations and observed Gaussian-series bounds share the same tuning data.
Definition (Lean source)
Regime tuning supplies legal threshold profiles with observed separation, observed product total variation at most a prescribed positive level τ, and Gaussian-series control. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.LowerTuning 26 declarations Lower-bound tuning: cancellation, bandwidth and sample budgets, compatible constants (19), (31), (41), (51), and uniform logarithmic size conditions.
Lower-bound tuning: cancellation, bandwidth and sample budgets, compatible constants (19), (31), (41), (51), and uniform logarithmic size conditions.
Above threshold (19), cancellation order is positive and at least half its unrounded value. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equation (29) factors the Gaussian prefactor into a bandwidth power and a noise ratio. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
When the bandwidth is below the noise scale, the ratio factor in (29) is at most one. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The direct scale has exactly the effective-dimensional sample power appearing in (18). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The bandwidth cutoff in (13) is chosen from the fixed effective dimension, so it is independent of the public noise scale. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Multiplying direct quadratic energy by n removes bandwidth dependence, as in (18). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Factorial-series terms above the cancellation order have ratio at most one half, as in (28). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Summing the geometric ratio estimate gives the first inequality in (28). This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The factorial estimate in (28) bounds the leading term by its Stirling-scale expression. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Both inequalities of (28) apply to the public Gaussian moment tail. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equation (34): the small radius and linear cancellation order give exponential suppression in the packet degree, uniformly at the intermediate-regime boundary. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The logarithmic degree choice in (30) absorbs the effective sample size in (35). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equations (29), (34), and (35) bound the complete intermediate-regime Gaussian-series sample factor by two, without a noise-dependent constant. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The decay exponent in (45) yields the compact-regime tail estimate used in (46). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The compact-regime exponential tail absorbs the sample size in (46). Under the stated conditions. This is the stated conclusion.
Proof (Lean source)
Equations (29), (45), and (46) give a uniform compact-regime Gaussian-series sample budget, after the degree choice has supplied the logarithmic decay. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equation (32): rounding the logarithmic degree preserves both comparison constants. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equation (33): the concrete intermediate radius is legal and its bandwidth is below noise. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The radius in (30) gives exactly the moment-tail parameter a²m. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equation (36): the rounded degree preserves a uniform fraction of the intermediate frontier. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The fixed degree threshold in (19) also supplies the intermediate multiplier in (32). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
After fixing the intermediate degree constant, all four small-radius restrictions in (31) can be met by one positive constant, independent of sample size and noise. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The large compact multiplier in (41) satisfies both the tail and sample-budget restrictions with the fixed support radius, independently of sample size and noise. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
One positive amplitude meets the direct and inverse range/smoothness requirements and the common logarithmic testing budget log(1+τ²) in (51). The multiplier is fixed before choosing the amplitude, as required by (48). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
For every admissible noise scale, the intermediate logarithm lies between one and the public sample logarithm once there are at least two observations; this is uniform in noise as used in (32)--(33). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A deterministic sample cutoff makes the compact degree size condition hold uniformly in noise, without adding it as an assumption on the model. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.LowerWitness 44 declarations Helpers — LowerWitness
Helpers — LowerWitness
Common fixed-envelope weak design, including the constant-density kappa=0 case.
Definition (Lean source)
The symmetric power integral used to normalize the common latent design. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Lebesgue measure on the compact dose subtype.
The common design integrates to one on the public dose subtype. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The compact-dose density is integrable, including the constant-power case. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Uniform Lebesgue mass on the unit dose and rank subtype is one. This is the stated conclusion.
Formal statement
Proof (Lean source)
The power-weighted compact dose law is a probability measure. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Independent stratum, latent dose, error and rank seed.
Definition (Lean source)
Structural threshold outcomes are built in the fixed public schedule space from a continuous profile.
Definition (Lean source)
The threshold construction is measurable in the independent product seeds. This is the stated conclusion.
Formal statement
Proof (Lean source)
The reference threshold profile has constant success probability one half.
Definition (Lean source)
The independent stratum, dose, Gaussian and rank seed has total mass one. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
For a path-space design, an admissible overlap parameter, and a threshold profile, the lower-witness law is a probability measure.
Formal statement
Proof (Lean source)
A threshold witness packaged as a probability law, with normalization proved locally.
Definition (Lean source)
Every threshold witness keeps its latent dose in the public compact interval. This is the stated conclusion.
Formal statement
Proof (Lean source)
Threshold embedding gives binary potential outcomes at every fixed public dose. This is the stated conclusion.
Formal statement
Proof (Lean source)
Binary threshold outcomes are bounded in the full model's outcome interval. This is the stated conclusion.
Formal statement
Proof (Lean source)
The observed outcome is the embedded schedule evaluated at the realized dose. This is the stated conclusion.
Formal statement
Proof (Lean source)
The witness factors every stratum/dose rectangle from the schedule and rank seed. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Both strata of every witness have probability one half. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
For a nonnegative design exponent, the witness's two strata each have mass one half.
Formal statement
Proof (Lean source)
For a nonnegative design exponent, the common half-mass strata satisfy the public overlap interval for any minimum stratum mass at most one half.
Formal statement
Proof (Lean source)
For a nonnegative design exponent, both witness strata have positive mass.
Formal statement
Proof (Lean source)
Whole-schedule exchangeability follows from the independent rank and dose seeds. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The auxiliary rank and latent dose factor within every public stratum. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The real-valued rank marginal is exactly uniform on the public unit interval. This is the stated conclusion.
Formal statement
Proof (Lean source)
Normalizing a half-mass stratum leaves the independent uniform rank law. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The probability of a lower-rank threshold is its level on the unit interval. This is the stated conclusion.
Formal statement
Proof (Lean source)
At each fixed dose, the witness evaluates the chosen profile against its auxiliary rank. This is the stated conclusion.
Formal statement
Proof (Lean source)
Integrating the independent uniform rank recovers exactly the prescribed conditional mean. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The measurement-error marginal is the independent standard Gaussian seed. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The Gaussian seed factors from every measurable joint stratum/dose/schedule event. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
For a nonnegative design exponent, the witness's conditional means lie in the unit interval, because they are the values of a threshold profile with values in the unit interval.
Formal statement
Proof (Lean source)
The radius-one Holder bound transfers from the profile to the actual conditional means. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The power design is a measurable density on the real centered-dose line. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The normalizing coefficient lies between one and twelve throughout the public exponent range. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The normalized power density meets the envelopes given by a lower constant at most its normalizing coefficient and an upper constant at least that coefficient on its support.
Formal statement
Proof (Lean source)
Conditioning on either stratum leaves the common weighted dose seed unchanged. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Subtracting the public center transports compact-dose volume to centered compact volume. This is the stated conclusion.
Formal statement
Proof (Lean source)
Weighting and centering the compact dose gives exactly the stipulated power density. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The conditional centered dose has the common density and satisfies the weak-design envelopes for a lower constant at most the power-density coefficient and an upper constant at least it. Under the stated conditions.
Formal statement
Proof (Lean source)
One full-measure event carries the embedded threshold identity at every public dose. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The assembled witness belongs to the model for any public class constants whose envelope constants bracket the power-density coefficient when the constructed profile has the required smoothness. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
All threshold profiles use the same stratum and latent-dose design. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.MarkedGaussianEnergy 6 declarations Finiteness and moment-tail control of the observed Gaussian weighted energy.
Finiteness and moment-tail control of the observed Gaussian weighted energy.
A measurable signed input gives a measurable Gaussian convolution. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Gaussian reference domination converts compact Gaussian energy to observed energy. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Compact signed densities have finite energy under the observed witness density. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The constructed threshold profile gives an integrable compact signed density. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The integrability conclusion in the observed marked-law identity is automatic for its constructed profile. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Weighted cancellations control observed Gaussian energy by the factorial tail, with the same tuning data. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.MarkedIdentification 11 declarations Weighted observation factorization for identification.
Weighted observation factorization for identification.
Weighting by a function of the mapped coordinate commutes with pushforward. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A bounded nonnegative mark gives its pushforward mass by an ordinary integral. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
An independent additive channel also factors after marking the latent coordinate. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Observational equivalence identifies the outcome-marked centered dose measure. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Bounded regression tests replace the realized mark by its conditional potential mean. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The centered latent dose and scaled Gaussian error have a product law in each stratum. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The bounded projected version is the same latent mark on the supported dose interval. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The observed outcome-marked conditional measure is the marked latent Gaussian convolution. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Mean-range finiteness supplies a finite marked latent measure without moment assumptions. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The marked law inherits compact support by absolute continuity with respect to latent dose. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Gaussian injectivity recovers the mean-marked latent law from observational equivalence. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.ObservedMarkedChiSquare 11 declarations The observed marked likelihood ratio and its exact chi-square energy (12).
The observed marked likelihood ratio and its exact chi-square energy (12).
The centered signed density of a threshold profile.
Definition (Lean source)
The success mark adds the centered convolution; the failure mark subtracts it.
Definition (Lean source)
The reference has equal success and failure densities. Under the stated conditions. This is the stated conclusion. Under the stated conditions. This is the stated conclusion. Under the stated conditions. This is the stated conclusion. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The two mark densities are nonnegative because they are convolutions of nonnegative latent densities. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The likelihood is a measurable real function on the entire observed space. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Multiplying the reference mark density by the likelihood recovers each alternative mark. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The observed alternative is the reference law weighted by its explicit marked likelihood. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The likelihood stays nonnegative for either choice of mark. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Radon--Nikodym uniqueness identifies the real observed likelihood with the explicit mark ratio. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Each reference mark contributes twice the signed-density energy to chi-square. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The exact observed marked-law chi-square formula and finiteness, rather than an oracle-treatment distance. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.ObservedPerturbationBounds 8 declarations Equation (27): observed chi-square control from compact signed perturbations and packet mass.
Equation (27): observed chi-square control from compact signed perturbations and packet mass.
The threshold mean formula identifies its signed density on the entire real line. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Equations (12), (24), and (26) give the observed moment-tail comparison for any constructed mean. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A bound on absolute signed mass gives the precise bandwidth power in equation (27). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Both signs share the same mass and moment control, hence the same observed comparison constant. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The packet's scaled mass and exact cancellations establish equation (27) for both inverse alternatives. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The compact direct bump has the bandwidth mass required after equation (27). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The latent quadratic energy in equation (18) has the direct-regime bandwidth power. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The direct pair also obeys equation (27), with cancellation order zero. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.Packet 16 declarations Standard Jacobi normalization, explicit smooth filtering, and the two packet constructions.
Standard Jacobi normalization, explicit smooth filtering, and the two packet constructions.
DLMF 18.5.7 normalization of the reused shifted hypergeometric polynomial.
Definition (Lean source)
Generalized real binomial coefficient defined by the falling factorial divided by the integer factorial.
Definition (Lean source)
The local falling-factorial binomial agrees with the binomial-ring coefficient. This is the stated conclusion. This is the stated conclusion. This is the stated conclusion. This is the stated conclusion.
Proof (Lean source)
Vandermonde convolution for the local generalized real binomial coefficients. This is the stated conclusion.
Formal statement
Proof (Lean source)
Choosing a second subset factors a generalized binomial coefficient. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Expanding the Bernstein basis gives a Vandermonde convolution in each coefficient. This is the stated conclusion.
Formal statement
Proof (Lean source)
Split a rising factorial at an index no larger than its order. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The normalized hypergeometric coefficient equals the corresponding binomial product. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Standard Jacobi's generalized binomial representation (NIST DLMF 18.5.8). This discharged citation is a build-inline algebraic obligation, not a gate. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Standard Jacobi weight on the unit symmetric interval.
Definition (Lean source)
Squared Lebesgue norm of the standard Jacobi polynomial under its Jacobi weight.
Definition (Lean source)
A concrete nonnegative smooth bump supported inside (1,2), positive on [5/4,7/4].
Finite spectral kernel of the standard Jacobi polynomials with a smooth cutoff and their integral norms.
Definition (Lean source)
Endpoint kernel at positive degeneracy, and the symmetric interior kernel at zero degeneracy.
Definition (Lean source)
The normalized tapered packet, zero outside its support; denominator positivity is a theorem.
Definition (Lean source)
Full packet conclusion, including positive normalization and all raw cancellations.
Definition (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.PacketDerivative 7 declarations Nearby-argument limits for the endpoint packet derivative estimate (P9).
Nearby-argument limits for the endpoint packet derivative estimate (P9).
Comparing nearby increments of two differentiable functions compares their derivatives. This is the division by the increment and passage to the limit used in (P9). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The finite Jacobi sum is symmetric in its two arguments. This is the stated conclusion.
Formal statement
Proof (Lean source)
The cited angular Lipschitz estimate bounds the ordinary derivative at each interior Jacobi coordinate. The same uniform constant works for all degrees and coordinates. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The angular derivative of the quadratic endpoint coordinate has the magnitude in (P9). The exclusion of zero is needed only for the arccos chain rule. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The nearby-argument Lipschitz estimate gives the derivative of the endpoint kernel along the quadratic dose coordinate, with the exact angular loss in (P9). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The cubed taper squared is controlled by the regularized weight after extracting its endpoint degree power. This drops the extra nonnegative decay factor in (P5). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The cubed taper cancels the square-root weight loss in the endpoint localization estimate. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.PacketDerivativeAssembly 3 declarations Taper and normalization assembly for the global packet derivative bound (P10).
Taper and normalization assembly for the global packet derivative bound (P10).
On the open support, differentiating the taper and the polynomial kernel gives both terms of the product rule in (P10). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Outside the closed support the packet is locally zero, hence its derivative vanishes. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Normalization and the cubed taper absorb both losses in the nearby-argument derivative bound. Continuity extends the bound to zero and the support endpoints, giving (P10) globally. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.PacketEndpoint 1 declarations Assembly of the endpoint packet bounds from normalization, localization and derivatives.
Assembly of the endpoint packet bounds from normalization, localization and derivatives.
The endpoint packet has all weighted localization, derivative and cancellation bounds. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.PacketEndpointFacts 22 declarations Endpoint packet regularity, normalization and moment cancellation.
Endpoint packet regularity, normalization and moment cancellation.
Zero extension provides the packet support for both constructions. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Squaring the dose coordinate makes the endpoint packet even. Under the stated conditions. This is the stated conclusion.
Proof (Lean source)
Legal division at the endpoint yields unit value at the target. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Odd weighted moments of any even packet cancel by reflection of the integration interval. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Each standard Jacobi polynomial is smooth as a finite sum of monomials. This is the stated conclusion.
Proof (Lean source)
A filtered kernel is smooth in its second coordinate since its spectral sum is finite. This is the stated conclusion.
Formal statement
Proof (Lean source)
Both choices of the packet kernel are finite polynomial sums. This is the stated conclusion.
Formal statement
Proof (Lean source)
The fourth-order positive taper equals an expression with a smooth cubed norm. This identity includes both support endpoints, where the taper vanishes. This is the stated conclusion.
Formal statement
Proof (Lean source)
The fourth-order taper has a continuously differentiable zero extension. This is the stated conclusion.
Formal statement
Proof (Lean source)
The finite polynomial kernel times the fourth-order taper is continuously differentiable on the whole line, including the two endpoints of its zero extension (P1), (P10). This is the stated conclusion.
Proof (Lean source)
Every active spectral degree strictly exceeds m and is strictly below 2m (P4). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Each filtered spectral summand annihilates every polynomial of degree at most m (P4). The inactive terms vanish, and the active terms use the cited Jacobi orthogonality leaf. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The zeroth Jacobi polynomial is the constant one. This is the stated conclusion.
Formal statement
Proof (Lean source)
Positivity of the zeroth squared norm supplies integrability of the Jacobi weight, including a negative endpoint exponent. No extra integrability premise is needed. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The spectral term times any polynomial is integrable under the Jacobi weight. Compactness bounds the continuous polynomial factor even when the weight is singular. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Finite-sum linearity assembles the spectral orthogonality into the filtered kernel's polynomial cancellation. This is the Jacobi-integral side of (P4). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Orthogonality cancels the transformed even-moment polynomial in (P4). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The quadratic substitution's Jacobian turns the endpoint Jacobi weight into its original dose power weight, with a fixed strictly positive scalar. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Substitution z = 2u² - 1 and Jacobi orthogonality cancel each unnormalized endpoint packet moment on the positive half interval (P4). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Legal normalization preserves the vanishing even moment on the positive half interval. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Reflection joins the two half intervals and proves the endpoint packet's full even weighted moment cancellation (P4), including the zeroth moment. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The squared weighted packet mass is bounded by its supremum times its absolute mass (P8). Integrability follows from the constructed packet's continuity on the compact interval. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.PacketGeometry 13 declarations Angular geometry and taper comparisons for endpoint packet localization (P5)--(P6).
Angular geometry and taper comparisons for endpoint packet localization (P5)--(P6).
The explicit filter is the standard smooth exponential glue composed with a quadratic. This is the stated conclusion.
Formal statement
Proof (Lean source)
The fixed filter is smooth to every order, including the two support endpoints. This is the stated conclusion.
Formal statement
Proof (Lean source)
Nonzero filter values lie strictly between the two spectral cutoffs. This is the stated conclusion.
Formal statement
Proof (Lean source)
The explicit filter satisfies the common hypothesis of both cited localization gates. This is the stated conclusion.
Formal statement
Proof (Lean source)
Compactness gives one strictly positive filter lower bound on the central spectral band. This is the stated conclusion.
Formal statement
Proof (Lean source)
The quadratic endpoint coordinate stays in the Jacobi interval. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The endpoint angular distance is exactly twice the arcsine of the dose magnitude. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The angular distance dominates the dose magnitude, so angular decay implies dose decay. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Regularization keeps the Jacobi weight strictly positive at every legal coordinate. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
At the endpoint the regularized weight dominates the normalization power. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The fourth-order taper squared is controlled by the regularized weight after extracting its endpoint degree power. This drops the extra nonnegative decay factor in (P5). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The taper cancels the square-root weight loss in the endpoint localization estimate. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The cited localization estimate and positive normalization give arbitrary uniform polynomial decay of the endpoint packet, after its fourth-order taper (P5)--(P6). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.PacketInterior 8 declarations Helpers — PacketInterior
Helpers — PacketInterior
Reflection of the binomial sum gives parity of the symmetric Jacobi system (P12). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Odd symmetric Jacobi polynomials vanish at the interior center (P12). Under the stated conditions. This is the stated conclusion.
Proof (Lean source)
Centering the symmetric filtered kernel kills the odd degrees, leaving an even kernel. This is the stated conclusion.
Formal statement
Proof (Lean source)
The taper preserves the symmetric interior kernel's evenness (P11). This is the stated conclusion.
Proof (Lean source)
On its support the fourth-order taper is exactly the symmetric Jacobi weight. This is the stated conclusion.
Formal statement
Proof (Lean source)
Interior raw moments cancel by the same finite-sum orthogonality as the endpoint system (P14). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Interior analytic bounds: the P12 center formula, elementary integral comparison, and norm/Gamma leaves give P13; P15 follows from the proved estimate chain. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The symmetric interior packet has all weighted localization, derivative and cancellation bounds. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.PacketInteriorEstimates 8 declarations Interior angular geometry and taper estimates for the P15 localization step.
Interior angular geometry and taper estimates for the P15 localization step.
The cosine Lipschitz bound turns interior angular decay into dose decay (P15). This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The symmetric regularized weight dominates the sixth power of the taper (P15). This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
At the interior center the regularized weight is at least one (P15). This is the stated conclusion.
Formal statement
Proof (Lean source)
The cubed taper absorbs the square-root weight loss of the interior kernel (P15). This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Localization and the fourth-order taper give arbitrary dose decay before normalization. The remaining P13 task is to divide this estimate by a denominator of order m. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The interior first derivative follows from the cited nearby-argument estimate (P15). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The product rule for the interior packet on its open support (P15). This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
P15 assembled after the P13 normalization estimate. The normalization premise is an intermediate proof obligation, not a new assumption of the paper theorem. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.PacketInteriorNormalization 13 declarations Interior Jacobi center evaluations (P12), active even-degree counts, and normalization assembly (P13).
Interior Jacobi center evaluations (P12), active even-degree counts, and normalization assembly (P13).
Generalized binomial coefficients at natural arguments are ordinary binomial coefficients. This is the stated conclusion.
Formal statement
Proof (Lean source)
Coefficients of the negative binomial polynomial carry the expected alternating sign. This is the stated conclusion.
Formal statement
Proof (Lean source)
The coefficient of degree twice s in the product (1+X)^n (1-X)^n is the coefficient of degree s in (1-X)^n. This is the stated conclusion.
Formal statement
Proof (Lean source)
The even symmetric Jacobi center evaluation in P12 follows by coefficient extraction. This is the stated conclusion.
Formal statement
Proof (Lean source)
Every even-degree symmetric Jacobi polynomial is nonzero at its center. This is the stated conclusion.
Formal statement
Proof (Lean source)
The norm and Gamma leaves bound the symmetric squared norm by a constant divided by degree (P13). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Wallis' elementary integral comparison bounds the squared normalized central binomial coefficient below (P12--P13). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Increasing the binomial top index transfers the central-binomial lower bound to the even Jacobi center value (P12). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The P12 center lower bound divided by the norm/Gamma upper bound gives uniform positive even spectral coefficients (P13). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
An explicit injective sequence of even degrees lies in the positive filter counting interval for every legal packet degree. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The explicit even-degree sequence contains at least a fixed positive multiple of the packet degree. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The interior normalization denominator is positive, using an active even spectral degree and the P12 center evaluation. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Counting active even degrees assembles the P13 normalization lower bound from a uniform positive lower bound on even spectral coefficients. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.PacketKernelNormalization 8 declarations Quantitative endpoint normalization by counting active filtered spectral terms (P3).
Quantitative endpoint normalization by counting active filtered spectral terms (P3).
The fixed exponential filter is nonnegative everywhere. This is the stated conclusion.
Formal statement
Proof (Lean source)
The fixed filter is strictly positive in its active interval. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Every legal packet degree has a spectral index strictly inside the filter support. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The diagonal filtered kernel is strictly positive because one active spectral term is positive. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Positivity of the endpoint packet's normalizing denominator, without an asymptotic gate. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The explicit filter is bounded by one everywhere. This is the stated conclusion.
Formal statement
Proof (Lean source)
On the fixed counting interval the explicit filter has a degree-independent positive lower bound. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Endpoint normalization has the full two-sided degree order claimed in (P3). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.PacketMass 3 declarations Weighted absolute mass from a localized packet envelope (P6--P7).
Weighted absolute mass from a localized packet envelope (P6--P7). The decay exponent kappa + 2 leaves an integrable quadratic envelope after absorbing the power-law weight.
Absorbing the weight into the decay envelope gives the bandwidth power. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The quadratic envelope on the positive half interval has mass at most 1/t. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
P7: a continuous even packet with decay exponent kappa + 2 has weighted absolute mass at most 2 C times the bandwidth power. No improper integral is needed: the residual quadratic envelope has an explicit antiderivative. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.PacketNormalization 8 declarations Endpoint Gamma identities and uniform spectral power comparisons for (P2)--(P3).
Endpoint Gamma identities and uniform spectral power comparisons for (P2)--(P3).
Standard Jacobi endpoint evaluation inherited from the shifted Vandermonde identity. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A Jacobi endpoint value is nonzero for the positive rising-factorial parameters. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The Gamma recurrence represents every positive-start rising factorial, including the negative Jacobi shape parameters permitted in the endpoint construction. Under the stated conditions. This is the stated conclusion.
Proof (Lean source)
The endpoint evaluation in (P2), with all Gamma denominators positive. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Positive finite initial terms can be absorbed into uniform power-comparison constants. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The cited Gamma asymptotic gives two-sided power bounds at every positive integer, with the finite initial segment included rather than discarded. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Dividing the squared endpoint value by its norm cancels two Gamma factors. This is the spectral coefficient used in the normalization sum (P3). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Each endpoint spectral coefficient has the exact power-law order needed in (P3), uniformly over all positive degrees, including the finite initial segment. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.PositiveRatio 16 declarations Positive inverse-weight population ratios.
Positive inverse-weight population ratios. Integrable signed weights pass through the realized conditional mean and exact Gaussian inverse; latent density envelopes then give the public positive denominator and Holder localization bias bounds.
Integrable signed dose-stratum-error weights can multiply the realized outcome. The domination is by the original weight, using the derived outcome range. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The conditional-mean bridge extends to every integrable signed test weight. The pull-out theorem includes the dominated truncation argument needed for unbounded weights. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The unmarked stratum inverse weight is integrable by restriction of the admissible weight. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The signed inverse-weight numerator is integrable because the realized outcome is bounded. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The population marked weight equals its conditional-mean weighted counterpart, including signed unbounded inverse weights. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Conditioning on a public stratum preserves independence of the centered dose and error. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
An integrable population weight remains integrable under every positive-mass stratum. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Exact Gaussian inversion turns an integrable signed observed weight into a latent weight, with any measurable multiplier for which the product is integrable. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Integrating against the centered conditional density gives the ordinary latent integral. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The unmarked population inverse moment is the positive latent weighted integral. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The marked population moment is the latent mean-weighted integral from equation (1). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The weak-design upper envelope makes every nonnegative admissible latent weight integrable. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The lower weak-design envelope supplies the sharper latent denominator lower bound. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Compact support controls the higher localization moment by the admissible base moment. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Holder continuity and the upper design envelope control the centered latent numerator. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Every admissible positive inverse pair has a positive public denominator and the stated bias bound. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.PublicCertificate 15 declarations Helpers — PublicCertificate
Helpers — PublicCertificate
Flooring at half the public lower bound cannot increase denominator error. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Clipping to the public mean range contracts distance to any mean in that range. This is the stated conclusion. Under the stated conditions.
Proof (Lean source)
The public floor and mean-range projection give the deterministic ratio stability bound. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The actual stratum estimator obeys the deterministic public ratio error bound. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Each modulo-three block contains at least the quotient of the sample size by three. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
For at least three records every split block has at least one fifth of the records. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The declared estimator's three blocks are all nonempty for sample size at least three. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Each empirical stratum frequency is nonnegative. This is the stated conclusion.
Proof (Lean source)
Frequencies in the first nonempty block sum to one over the two strata. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The estimator error splits into a convexly weighted mean error and the stratum-frequency error. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The positive latent weighted mean remains in the public outcome interval. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Distinct modulo-three blocks are disjoint. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The first-block frequency factors from the absolute error of any other block average. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The balanced split converts each moment standard deviation to the public sample-size scale. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The split, floor-clipped and projected ratio has the public finite-sample absolute-risk certificate. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.RealizedDoseMean 3 declarations Helpers — RealizedDoseMean
Helpers — RealizedDoseMean
The sigma algebra generated by dose, stratum and error.
Definition (Lean source)
The sigma algebra generated by dose and stratum.
Definition (Lean source)
Schedule exchangeability derives both realized-dose conditional means and the observed outcome bound. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.ScheduleFactorization 11 declarations Finite-stratum normalization and the schedule/dose product law used in the realized-dose argument.
Finite-stratum normalization and the schedule/dose product law used in the realized-dose argument. These results use whole-schedule exchangeability.
Each positive stratum carries a normalized probability law. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Stratum restriction divides real event masses by the positive stratum mass. This is the stated conclusion.
Formal statement
Proof (Lean source)
Whole-schedule exchangeability becomes ordinary independence in each stratum. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The conditional joint schedule/dose law is the product of its marginals. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Error independence survives positive-stratum restriction, with its marginal unchanged. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The schedule, dose, and Gaussian error have the conditional product law in equation (1). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
An almost-everywhere assertion under the population law holds in each stratum. Under the stated condition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The two positive strata suffice to recover a population almost-everywhere assertion. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Whole-schedule exchangeability integrates fixed-dose exceptional sets at the random dose. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Consistency transfers the random-evaluation bound to the observed outcome. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The derived observed-outcome bound supplies integrability without an extra premise. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.ScheduleMeasurability 2 declarations Joint evaluation supplies a countable separating family for the public schedule space.
Joint evaluation supplies a countable separating family for the public schedule space.
A measurable product event depends on countably many measurable first-coordinate sets. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Jointly measurable, extensional evaluation supplies countable separation of schedules. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.TransitionWindows 9 declarations Scale comparisons throughout fixed-factor windows about either transition.
Scale comparisons throughout fixed-factor windows about either transition.
Multiplying a positive localization radius by at most K adds at most d log K to the logarithmic denominator. Under the stated conditions. This is the stated conclusion.
Formal statement
Throughout a factor-K window the positive logarithms differ by a bounded factor. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Square roots inherit the same (slightly enlarged) logarithmic factor. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The Fourier scale varies by a fixed multiplicative factor throughout a radius window. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The polynomial scale also varies by a fixed factor in a radius window. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
At the direct elbow, the effective noisy sample size is exactly one. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The Fourier scale at the direct elbow differs by a fixed public constant. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
A constant dominating the two fixed ratios compares both scales at the first elbow. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
One constant and sample threshold compare the two scales on both full transition windows. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.Helpers.ZeroNoiseObserved 9 declarations The zero-noise observed Bernoulli likelihood and its quadratic energy.
The zero-noise observed Bernoulli likelihood and its quadratic energy.
At zero noise the observed dose directly indexes the Bernoulli likelihood.
Definition (Lean source)
The zero-noise likelihood is measurable. This is the stated conclusion.
Formal statement
Proof (Lean source)
The zero-noise likelihood is nonnegative on the full observed space. This is the stated conclusion.
Formal statement
Proof (Lean source)
The exact zero-noise observed law is a likelihood tilt of the half-success reference. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Radon--Nikodym uniqueness identifies the zero-noise observed likelihood. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The zero-noise version of (12) is exactly the latent quadratic energy, evaluated in the observed experiment. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Equation (18) holds for the observed direct profiles uniformly down to zero noise. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The uniform direct sample budget includes the zero-noise boundary. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The direct construction gives observed product total variation at most τ, including zero noise, under the common amplitude budget log(1+τ²) (51). Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.TErrorFreeReduction 2 declarations TErrorFreeReduction
TErrorFreeReduction
At zero noise the direct branch gives the exact weak-design power law. This is the stated conclusion.
Formal statement
Proof (Lean source)
Zero measurement error gives the same-class weak-design orders for minimax risk and for honest length at a noncoverage level below one half, and the separate Gaiffas experiment has comparable minimax absolute risk. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.TFiniteHonesty 11 declarations TFiniteHonesty
TFiniteHonesty
The two stratum masses form a probability partition. This is the stated conclusion.
Formal statement
Proof (Lean source)
The causal target is the stratum-weighted potential mean, by the finite partition. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The unit mean range transfers to the causal target through its probability weights. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The pushed-forward iid experiment is a probability measure. This is the stated conclusion.
Formal statement
Proof (Lean source)
Empirical stratum frequencies form a probability partition on a nonempty frequency block. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Projection and empirical probability weights keep the total estimator in the unit outcome range. This is the stated conclusion.
Formal statement
Proof (Lean source)
Nonempty modulo-three blocks require at least three observations. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Every admissible pair has a strictly positive finite-sample public score. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The interval contains any unit-range target within the declared public radius. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Clipping cannot increase the length beyond twice the public radius, the score divided by the noncoverage level. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
For any public class constants, smoothness exponent positive and at most one, design exponent between zero and two and any noncoverage level strictly between zero and one, the clipped interval covers the causal target with probability at least one minus the noncoverage level at every sample size, and its expected length is at most a constant (depending on the noncoverage level) times the frontier rate, uniformly for large samples.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.TIdentification 1 declarations Identification of latent measures, continuous potential means, and the causal target.
Identification of latent measures, continuous potential means, and the causal target.
Observational equivalence identifies both latent measures, every continuous mean value, and the causal target via local-mass limits. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.TObservableUpper 2 declarations TObservableUpper
TObservableUpper
At least three observations make each modulo-three split block nonempty. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The observable estimator and branch-specific dictionary witnesses attain the risk frontier with one noise-uniform threshold. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.TObservedLower 1 declarations TObservedLower
TObservedLower
Assuming the four cited Jacobi-packet facts, for any public class constants whose lower and upper envelope constants bracket the power-density coefficient (κ+1)2^κ, so that the class is nonempty, smoothness exponent positive and at most one, design exponent between zero and two and any prescribed positive total-variation level τ, explicit Bernoulli threshold witnesses in the model have a common design, legal ranks, target separation of the order of the frontier rate, and observed-product total variation at most τ; the separation constant depends on τ.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.TUniformFrontier 10 declarations Uniform matched risk and honest-length frontier, full transition windows, and fixed-noise order.
Uniform matched risk and honest-length frontier, full transition windows, and fixed-noise order.
Appending the same independent probability seed cannot increase total variation. This is the stated conclusion.
Proof (Lean source)
A nonnegative loss dominates its threshold times the probability of exceeding it. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The two-point testing bound implies an extended absolute-risk floor without integrability. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Connected intervals covering each of two separated laws with probability at least one minus α, whose laws are within total variation τ, have expected length at least the separation times 1 − 2α − τ. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Ignoring the independent uniform seed preserves the observable estimator's absolute risk. This is the stated conclusion.
Formal statement
Proof (Lean source)
The observable estimator is admissible for randomized minimax risk and attains its upper frontier. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
The finite-honesty interval is admissible for the infimum defining honest expected length at noncoverage level α. This is the stated conclusion. Under the stated conditions.
Formal statement
Proof (Lean source)
Every branch of the frontier is nonnegative on the public noise domain for nonzero samples. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
The observed separated witnesses imply both uniform minimax and honest-length floors at any noncoverage level below one half. Under the stated conditions. This is the stated conclusion.
Formal statement
Proof (Lean source)
Assuming the four cited Jacobi-packet facts, for any public class constants whose envelope constants bracket the power-density coefficient (κ+1)2^κ, smoothness exponent positive and at most one, design exponent between zero and two and noncoverage level strictly between zero and one half, minimax absolute risk and honest expected connected length at that level share the full uniform three-regime frontier, its elbows, and the fixed-positive-noise order; the constants depend on the noncoverage level and on the class constants.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_NoisydoseWeakdesignTransition_Research.TWeightedPacketConstruction 1 declarations TWeightedPacketConstruction
TWeightedPacketConstruction
Conditional on the four disclosed classical gates, the explicit normalized packet has every stated weighted bound and cancellation. Under the stated conditions. This is the stated conclusion.