Formalization: Uniform Expected Risk for Distance-Based Boundary Regression Designs
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs.
Basic 30 declarations This module formalizes the random-design regression laws, distance-compressed decision classes, completed and outer risks, and the logarithmic frontier rate.
Bounded uniform logarithmic penalty: common definitions
This module formalizes the random-design regression laws, distance-compressed
decision classes, completed and outer risks, and the logarithmic frontier rate.
The bivariate covariate is represented by EuclideanSpace ℝ (Fin 2), so every
metric and Hölder condition below uses the paper's Euclidean geometry.
Bivariate random-design covariates with their Euclidean ℓ2 metric.
Definition (Lean source)
One observed outcome-covariate pair.
Definition (Lean source)
An ordered i.i.d. sample of size n.
Definition (Lean source)
The unsigned-distance compressed sample at one query point.
Definition (Lean source)
A CTY random-design regression law. Its density and conditional-moment fields are pinned to the joint law, rather than supplied as free auxiliaries.
Definition (Lean source)
The product law of n independent observations from P.
Rectifiability of the support boundary, expressed by a Lipschitz parameterization of the boundary by the unit interval.
Definition (Lean source)
The coordinate cube [-r,r]², regarded as a subset of Euclidean space.
The standard Hölder ball formed using the Euclidean norm on the bivariate score carrier.
Definition (Lean source)
The CTY nonparametric law class: i.i.d. probability sampling, a compact rectifiable score support with a continuous density bounded between L⁻¹ and L, a q-Hölder regression, and a continuous conditional variance with the same envelope. The fidelity fields of CtyLaw identify all three functions with functionals of the joint law.
Definition (Lean source)
The named class as a set of law objects.
Definition (Lean source)
The labelled support is the topological support of the covariate marginal.
Formal statement
Proof (Lean source)
Every relatively open neighborhood of a support point has positive covariate-marginal mass.
Formal statement
Proof (Lean source)
Two continuous versions that agree almost everywhere under an admissible covariate marginal agree at every point of the support, including its boundary.
Formal statement
Proof (Lean source)
The unsigned-distance sample seen at query point x.
Definition (Lean source)
For each fixed point, unsigned-distance compression is measurable in the sample.
Formal statement
Proof (Lean source)
Ambient type of boundary-indexed regression rules.
Generator for a CTY rule: one common measurable map at every point.
Definition (Lean source)
Generator for a point-indexed rule. Only fixed-point sections are required to be measurable; no joint regularity in the query point is imposed.
Definition (Lean source)
Rules generated, uniformly over admissible laws, by one law-independent measurable map of the unsigned-distance data.
Definition (Lean source)
Rules generated by a law-independent point-indexed family with measurable fixed-point sections and no joint measurability or continuity in the point.
Definition (Lean source)
The extended nonnegative uniform boundary loss of a rule under a law.
The common-map minimax risk, using the ordinary nonnegative expectation on the completed sample space.
Definition (Lean source)
The point-indexed minimax risk, using outer expectation because only the fixed-point rule sections are assumed measurable.
Definition (Lean source)
The first-order distance rate a_n = (log n / n)^(1/4).
Definition (Lean source)
The frontier rate is positive once n ≥ 2.
Formal statement
Proof (Lean source)
The logarithmic distance frontier rate tends to zero.
Formal statement
Proof (Lean source)
A risk normalized by the distance frontier rate.
Definition (Lean source)
The multiplier form appearing on the left side of the paper's displayed normalization.
Definition (Lean source)
The multiplier and quotient normalizations agree once the sample size is at least two.
Formal statement
Proof (Lean source)
Causal.Basic 19 declarations This module introduces the selected-conditional-kernel causal law used by the second half of the paper, together with its known assignment geometry and the signed-distance observation.
CTY Assumptions 1--2: causal world and known geometry
This module introduces the selected-conditional-kernel causal law used by the second half of the paper, together with its known assignment geometry and the signed-distance observation.
A potential-outcome observation (Y(0), Y(1), X).
Definition (Lean source)
An ordered sample of potential-outcome observations.
Definition (Lean source)
Arm t of a potential-outcome observation.
Definition (Lean source)
The score coordinate.
Definition (Lean source)
A decorated causal law carrying one selected arm-indexed regular conditional-kernel witness. Forgetting the decoration recovers the bare data-generating law. Membership in the law class below constrains the carried selected representative pointwise.
Definition (Lean source)
The n-fold i.i.d. law of potential-outcome observations.
Definition (Lean source)
Treatment is the indicator of the known arm-one region.
Definition (Lean source)
The observed outcome obeying consistency.
Definition (Lean source)
The boundary treatment-effect curve.
The selected conditional absolute moment at exponent 2 + ν.
The fixed uniform smoothing kernel 1{|u| ≤ 1}.
Definition (Lean source)
The tuple of geometry known to every causal decision rule.
The support, assignment regions, interface, Euclidean metric, and fixed uniform kernel supplied to the estimator.
Definition (Lean source)
Signed Euclidean distance computed from a known geometry.
Definition (Lean source)
The observed signed-distance sample.
Definition (Lean source)
Observed-outcome and signed-distance pairs for an admissible causal law. The first coordinate is the law-indexed observed outcome, so consistency and the assignment partition cannot be bypassed by supplying arbitrary geometry.
Definition (Lean source)
Geometry-only implementation used by a law-independent rule. Its input type carries the Borel-partition and common-interior-frontier invariants.
Definition (Lean source)
The degree-p monomial basis (1,u,…,u^p).
Causal.CitedInterfaces 21 declarations These three named propositions record external source statements.
Cited CTY interfaces
These three named propositions record external source statements. They are never proved here; every consumer takes an explicit inhabitant.
A metric on the score space which is uniformly equivalent to Euclidean distance on the score support, exactly as in CTY Assumption 2(ii).
Definition (Lean source)
Signed distance for the general metric admitted by the cited identification theorem.
Definition (Lean source)
The Hausdorff slice denominator in CTY Assumption 2(v).
Exactly CTY Assumptions 1(i)--(iii) and 2(i), (ii), and (v), with i.i.d. sampling supplied by causalSampleLaw. Armwise potential-outcome integrability records the genuine scope in which the conditional means in Assumption 1(iii) exist. No variance envelope, higher-moment envelope, kernel, Gram, VC, local-mass, or quantitative derivative-envelope clause is imposed.
Definition (Lean source)
One source-coherent selected pair of armwise signed-distance conditional-mean versions. The disintegration identity pins both one-sided functions to one selected conditional law, avoiding arbitrary pointwise choices of condDistrib.
Definition (Lean source)
Cattaneo, Titiunik, and Yu (2026), Theorem 1, printed p. 4, DOI 10.1016/j.jeconom.2026.106266: under the displayed Assumptions 1(i)--(iii) and 2(i),(ii),(v), there is a selected source-coherent signed-distance conditional-mean version whose one-sided limits identify the boundary effect. The statement does not range over every arbitrary disintegration or version.
Definition (Lean source)
A finite set is shattered by the distance balls generated by d, with centres restricted to the score support as in CTY Assumption 2(iii).
The distance-ball family in CTY's uniform-kernel alternative has finite VC index. No Euclidean specialization or fixed numerical index is imposed.
Definition (Lean source)
The two kernel alternatives in CTY Assumption 2(iii): a nonnegative, compactly supported Lipschitz kernel, or the uniform kernel together with a finite-VC distance-ball family.
Definition (Lean source)
The population Gram matrix for the general metric/kernel regime of CTY Theorem 2.
Definition (Lean source)
The population score in the general metric/kernel normal equations.
Definition (Lean source)
The original, unwinsorized population coefficient in CTY's full metric/kernel regime.
Definition (Lean source)
The smallest Rayleigh quotient of the population Gram matrix, represented in ℝ≥0∞ so the infimum is total.
Definition (Lean source)
Lebesgue mass of a general metric/kernel arm neighborhood.
The source-sized class in CTY Theorem 2. It retains Assumptions 1(i)--(iii), all of Assumption 2, the displayed uniform density and derivative envelopes, and the two genuine liminf small-bandwidth restrictions. It is not the Euclidean/uniform-kernel P₁₂ specialization.
Definition (Lean source)
Uniform absolute population-contrast bias normalized by bandwidth over the exact Euclidean/uniform-kernel P₁₂(p,ν,L) specialization used by the upper theorem.
Definition (Lean source)
Cattaneo, Titiunik, and Yu (2026), Theorem 2, printed pp. 5--6, DOI 10.1016/j.jeconom.2026.106266: the upper-only corollary used here on the exact P₁₂(p,ν,L) specialization. A constant depending only on p and L controls the finite limsup uniformly in ν, along every positive antitone deterministic bandwidth sequence with h_n → 0 and n h_n² → ∞.
Definition (Lean source)
The unwinsorized empirical score vector.
Definition (Lean source)
Uniform empirical Gram deviation for one sample.
Definition (Lean source)
Uniform centered raw-score deviation for one sample.
Definition (Lean source)
Cattaneo, Titiunik, and Yu (2026), Supplemental Appendix SA-8.3--8.4, printed pp. 32--35, DOI 10.1016/j.jeconom.2026.106266: the expected outer Gram and centered-score suprema satisfy the two displayed maximal bounds in the small-bandwidth regime.
Definition (Lean source)
Causal.DecisionClass 6 declarations Only fixed (geometry, point) sections are measurable.
Known-geometry point-indexed causal decision class and outer risk
Only fixed (geometry, point) sections are measurable. No joint regularity in
the interface point is imposed, so the risk uses outer expectation.
Ambient causal rules take the sample, the known geometry, and a query point.
Definition (Lean source)
A law-independent family of Borel fixed sections.
Definition (Lean source)
Known-geometry point-indexed rules with Borel fixed sections and no joint regularity in the interface index.
Definition (Lean source)
Extended nonnegative interface-supremum loss.
Definition (Lean source)
The known-geometry point-indexed minimax risk under outer expectation.
Definition (Lean source)
The local and upstream outer-integral spellings agree definitionally.
Formal statement
Proof (Lean source)
Causal.EmpiricalProcess.EntropyChaining 3 declarations The hypotheses below expose exactly the envelope, variance, and polynomial covering information used by the variance-adaptive maximal inequality.
VC entropy and chaining for the bounded score class
The hypotheses below expose exactly the envelope, variance, and polynomial covering information used by the variance-adaptive maximal inequality.
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
The same entropy certificate with all witnesses chosen uniformly before the moment exponent. The L² proof's displayed constant does not depend on that exponent.
Formal statement
Proof (Lean source)
A positive coefficient clipping radius can be chosen together with the uniform entropy witnesses.
Formal statement
Proof (Lean source)
Causal.EmpiricalProcess.PopulationCoefficient 5 declarations This module bounds the original population score and then uses the class's quadratic-form Gram floor to put every population coefficient in one fixed ball.
Uniform population-coefficient radius
This module bounds the original population score and then uses the class's quadratic-form Gram floor to put every population coefficient in one fixed ball. This is the adapter needed to embed the actual score process into the bounded-coefficient entropy class.
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
The stated bandwidth is strictly positive at every sample size.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
The explicit population-coefficient radius in existential form.
Formal statement
Proof (Lean source)
Causal.EmpiricalProcess.RadialCover 2 declarations This module specializes the neutral moving-center Euclidean radial-polynomial certificate to the paper's signed-distance, uniform-kernel score.
Radial covering adapter for the winsorized score
This module specializes the neutral moving-center Euclidean radial-polynomial certificate to the paper's signed-distance, uniform-kernel score. The proof keeps the strict and non-strict signed arms separate, including the radius-zero trace, so it remains uniform for empirical laws with atoms on moving boundaries.
At every positive coefficient clipping radius there are polynomial covering constants depending only on the degree such that all laws, bandwidths, and positive winsorization levels share both an arbitrary-law L²(Q) certificate and the same empirical covering constants, with envelope B + (p+1)R.
Formal statement
Proof (Lean source)
For a positive bandwidth, winsorization level, and coefficient clipping radius, the entire finite-arm, finite-coordinate winsorized score class has a uniform polynomial L²(Q) cover over every probability measure Q, with envelope B + (p+1)R.
Formal statement
Proof (Lean source)
Causal.EmpiricalProcess.ScoreL2 10 declarations This module isolates the analytic localization estimate used by the variance-adaptive entropy theorem.
Population L² radius of the winsorized score
This module isolates the analytic localization estimate used by the
variance-adaptive entropy theorem. The Euclidean density bound controls the
probability of a bandwidth ball, while the selected conditional moment bound
controls the winsorized response without introducing the winsorization level
into the population L² radius.
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
The squared separable winsorized score is bounded pointwise by a localized sum of the two arm squares and the clipped polynomial-envelope square.
Formal statement
Proof (Lean source)
The absolute separable winsorized score is uniformly bounded by the winsorization level plus the clipped polynomial envelope.
Formal statement
Proof (Lean source)
The one-sided bandwidth enlargement has population L² radius O(h). The proof uses the defining bound q < 2h to localize every nonzero score in the radius-2h Euclidean ball.
Formal statement
Proof (Lean source)
The explicit separable score radius packaged in the existential form used by the entropy layer.
Formal statement
Proof (Lean source)
The unit-radius specialization of the separable population L² bound.
Formal statement
Proof (Lean source)
At every positive coefficient clipping radius, admissible winsorized scores have population L² norm at most C h, uniformly over centers, arms, coordinates, and winsorization levels B > h with B ≥ 1.
Formal statement
Proof (Lean source)
For every fixed polynomial degree and law-class envelope there are a positive coefficient clipping radius and a positive constant such that every admissible winsorized score has population L² norm at most C h, uniformly over centers, arms, coordinates, and all winsorization levels B > h with B ≥ 1.
Formal statement
Proof (Lean source)
Causal.EmpiricalProcess.Separability 14 declarations This is the bounded residual identified in round 13.
Countable reduction for the winsorized score class
This is the bounded residual identified in round 13. The property below says that a continuum-indexed empirical-process supremum has a fixed countable pointwise-dense subfamily. It is the bridge from outer expectation to the countable-index concentration API.
Index (arm, center, coefficient vector, coordinate) for the enlarged winsorized score class.
Definition (Lean source)
Index for the separable one-sided bandwidth enlargement. Centers are restricted to the treatment boundary and the support bandwidth approaches the target bandwidth h from the half-open interval [h,2h).
One scalar coordinate of the enlarged bounded-coefficient winsorized score class. Coefficients are clipped componentwise at the supplied radius, so this is a genuine constant-envelope class.
Definition (Lean source)
The one-sided support-bandwidth enlargement of the fixed-bandwidth score. The polynomial arguments remain normalized by h; only the closed kernel support uses q. Thus the fixed class embeds at q=h, while rational bandwidths decreasing to h resolve sample points on moving ball boundaries.
Definition (Lean source)
The centered empirical average of a real-valued function.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The two stated constructions agree under the theorem's assumptions.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The stated finite approximation exists with the asserted properties.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
The rational-center/rational-bandwidth enlargement of the bounded winsorized signed-distance score class has an almost-sure countable supremum reduction. A single conull set excludes observations whose score lies on the treatment boundary; closed kernel endpoints are approached from bandwidths in [h,2h).
Formal statement
Proof (Lean source)
The countable reduction at the canonical unit coefficient radius.
Formal statement
Proof (Lean source)
Causal.EmpiricalProcess.SeparableCover 1 declarations This file inserts the independently parameterized closed-ball support into the fixed-normalization radial-polynomial cover.
Polynomial covering for the one-sided bandwidth enlargement
This file inserts the independently parameterized closed-ball support into the fixed-normalization radial-polynomial cover. The diagonal pullback then ties the ball center to the polynomial center. The degree-zero term off the known assignment support is kept separate because signed distance is identically zero there.
The separable score class, whose kernel bandwidth ranges over [h,2h), has polynomial covering witnesses uniform in the law, bandwidth, and winsorization level.
Formal statement
Proof (Lean source)
Causal.EmpiricalProcess.VCExpectedMaximal 4 declarations This is an in-run lemma assembled from the proved Causalean symmetrization, Dudley/VC entropy, and localized critical-radius layers.
Variance-adaptive expected maximal inequality
This is an in-run lemma assembled from the proved Causalean symmetrization, Dudley/VC entropy, and localized critical-radius layers. It replaces the retired external assumption: consumers call this theorem and carry no additional empirical-process binder.
An a.e. equality with a measurable representative bounds the pointwise-majorant outer integral by the representative's lower integral.
Formal statement
Proof (Lean source)
Pointwise supremum of the centered empirical process.
Definition (Lean source)
The continuum outer integral obeys the explicit variance-adaptive VC rate before the logarithm is normalized to a problem-specific ratio.
Formal statement
Proof (Lean source)
A countably reducible VC-type class obeys the variance-adaptive two-term expected maximal inequality.
Formal statement
Proof (Lean source)
Causal.Estimator 26 declarations This module defines the empirical Gram and score, the guarded inverse, the clipped contrast, the population coefficient used by the cited bias theorem, and the pointwise selected-kernel winsorization bias lemma.
Winsorized stabilized signed-distance local polynomial estimator
This module defines the empirical Gram and score, the guarded inverse, the clipped contrast, the population coefficient used by the cited bias theorem, and the pointwise selected-kernel winsorization bias lemma.
Equip estimator matrices with the product measurable structure.
Definition (Lean source)
The estimator-matrix measurable structure is its Borel structure.
Formal statement
Proof (Lean source)
Arm membership for a signed distance.
Empirical local-polynomial Gram matrix from compressed observations.
Definition (Lean source)
Winsorized empirical local-polynomial score.
Definition (Lean source)
Quadratic-form empirical Gram guard at (2L)⁻¹.
Definition (Lean source)
The guarded coefficient: inverse score on the stable branch and zero otherwise.
Definition (Lean source)
Projection onto [-C,C].
The theorem's winsorization level B_n = a_n^(-1/3).
Definition (Lean source)
Population score in the original, unwinsorized normal equations.
Definition (Lean source)
The original population local-polynomial coefficient.
Definition (Lean source)
The winsorized, clipped, Gram-stabilized signed-distance local-polynomial rule at bandwidth h, using B(h)=h^(-1/3).
Definition (Lean source)
The fixed uniform kernel is Borel measurable.
Formal statement
Proof (Lean source)
Each coordinate of the finite monomial basis is Borel measurable.
Formal statement
Proof (Lean source)
Winsorization at a fixed level is Borel measurable.
Formal statement
Proof (Lean source)
A finite real matrix-valued map is measurable exactly when all of its entries are measurable.
Formal statement
Proof (Lean source)
Mathlib's total inverse on finite real matrices is Borel measurable.
Formal statement
Proof (Lean source)
Every coordinate of an inverse-matrix--vector product is measurable when the matrix and vector inputs are measurable.
Formal statement
Proof (Lean source)
The empirical local-polynomial Gram matrix is measurable in the compressed sample.
Formal statement
Proof (Lean source)
The winsorized empirical score is measurable in the compressed sample.
Formal statement
Proof (Lean source)
The quadratic-form Gram guard is a Borel set of finite matrices.
Formal statement
Proof (Lean source)
The guarded inverse coefficient vector is measurable in the compressed sample.
Formal statement
Proof (Lean source)
The explicit estimator is a member of the sectionwise-Borel decision class at every positive bandwidth.
Formal statement
Proof (Lean source)
Winsorization cannot remove more than the magnitude of its input.
Formal statement
Proof (Lean source)
Above a threshold at least one, the winsorization remainder is dominated by the (2+ν) moment times B⁻³ whenever ν ≥ 2.
Formal statement
Proof (Lean source)
A pointwise selected-kernel (2+ν) moment envelope gives the deterministic B⁻³ winsorization bias bound.
Formal statement
Proof (Lean source)
Causal.EuclideanBallsVC 3 declarations The statement is phrased directly as non-shattering of finite point sets of cardinality at least four, which is the paper's “VC index at most four”.
VC index of planar Euclidean balls
The statement is phrased directly as non-shattering of finite point sets of cardinality at least four, which is the paper's “VC index at most four”.
A finite planar set is shattered by closed Euclidean balls.
Closed planar Euclidean balls have VC index at most four.
Definition (Lean source)
The collection of all closed Euclidean balls in ℝ² has VC index at most four. Consequently the fixed Euclidean metric and uniform kernel meet CTY's actual VC alternative.
Formal statement
Proof (Lean source)
Causal.FiniteMaxAssembly 19 declarations This module builds the finite measurable partition used to split the causal hard-family marked-Poisson experiment into its local cells and common complement.
Causal finite-maximum assembly
This module builds the finite measurable partition used to split the causal hard-family marked-Poisson experiment into its local cells and common complement.
Equip the causal packing index set with the discrete measurable structure.
Definition (Lean source)
The disjoint hard cells and their common complement as a classifier.
Definition (Lean source)
Every causal packing cell, including the complement, is measurable.
Formal statement
Proof (Lean source)
Distinct indices select disjoint causal partition cells.
Formal statement
Proof (Lean source)
The causal packing partition covers the observation space.
Formal statement
Proof (Lean source)
The finite measurable partition formed by the causal hard cells.
Definition (Lean source)
The abstract partition has the intended causal hard cells.
Formal statement
Proof (Lean source)
A local partition-cell mass is exactly the score-cell probability.
Formal statement
Proof (Lean source)
Equal positive cell mass and raw restriction locality identify the normalized observation laws in a causal packing cell.
Formal statement
Proof (Lean source)
A canonical vertex carrying the selected causal cell bit.
Definition (Lean source)
The canonical marked-Poisson law in causal coordinate j.
Definition (Lean source)
The stated experiment law has total mass one and therefore defines a probability distribution.
Definition (Lean source)
The causal complement experiment, represented at the all-false vertex.
Definition (Lean source)
The stated experiment law has total mass one and therefore defines a probability distribution.
Definition (Lean source)
A canonical causal cell experiment depends only on its own Boolean bit.
Formal statement
Proof (Lean source)
The canonical complement experiment is common to every causal vertex.
Formal statement
Proof (Lean source)
Put the causal complement and cell blocks back into one marked sample.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
Partition splitting identifies the independent causal blocks with the canonical marked-Poisson law at the selected vertex.
Formal statement
Proof (Lean source)
Causal.FiniteMaxDecision 19 declarations This module reconstructs each fixed-geometry signed-distance section from the local compressed Poisson block and the remaining raw partition blocks.
Causal finite-maximum decoders
This module reconstructs each fixed-geometry signed-distance section from the local compressed Poisson block and the remaining raw partition blocks.
Equip the causal decision index set with the discrete measurable structure.
Definition (Lean source)
Every singleton causal decision index is measurable.
Formal statement
Proof (Lean source)
Equal assignment geometry makes the observed signed statistic identical.
Formal statement
Proof (Lean source)
The two stated constructions agree under the theorem's assumptions.
Formal statement
Proof (Lean source)
The fixed-law signed-distance sample map is measurable.
Formal statement
Proof (Lean source)
Mark a causal observation after replacing it by its observed outcome and signed distance at one fixed-geometry center.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
Compress one raw causal partition block to its signed observation.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
Reassemble the signed marked sample for decoder j.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The point estimate reconstructed from the independent causal blocks.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The midpoint decoder attached to the fixed measurable section.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
The measurable finite maximum at the selected causal packing centers.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
Compressing a canonical causal cell block gives the marked-Poisson experiment generated by the normalized signed-observation cell law.
Formal statement
Proof (Lean source)
Causal.FiniteMaxLowerBound 16 declarations This module converts the causal hard-family cell experiment into a coordinatewise testing problem and transfers its loss back to a fixed-size sample.
Causal finite-packing lower bound
This module converts the causal hard-family cell experiment into a coordinatewise testing problem and transfers its loss back to a fixed-size sample.
Equip the causal risk index set with the discrete measurable structure.
Definition (Lean source)
Every singleton causal risk index is measurable.
Formal statement
Proof (Lean source)
A polynomial-size packing eventually has enough logarithmic cardinality to absorb a sufficiently small fourth-power frontier budget.
Formal statement
Proof (Lean source)
Value of a causal rule on the retained prefix of a global marked sample.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
Maximum target error on a global causal marked configuration.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The blockwise loss used by the direct-product experiment.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
Reassembling the local signed block and the other raw blocks equals mapping the synthesized global configuration.
Formal statement
Proof (Lean source)
The two stated constructions agree under the theorem's assumptions.
Formal statement
Proof (Lean source)
The causal cell experiment inherits the finite direct-product testing lower bound from its compressed one-cell KL budgets.
Formal statement
Proof (Lean source)
Averaging the direct-product error selects a causal vertex whose global Poissonized maximum loss is large.
Formal statement
Proof (Lean source)
On the successful count event the causal global Poisson loss is the finite packing loss of the retained sample.
Formal statement
Proof (Lean source)
Failed-count zero defaults are bounded by the target envelope.
Formal statement
Proof (Lean source)
De-Poissonization for the causal finite packing maximum.
Formal statement
Proof (Lean source)
Causal.Hypercube.BernoulliKernel 5 declarations This module supplies the bounded selected conditional kernels used by the potential-outcome angular construction.
Pointwise Bernoulli kernels for the causal hard family
This module supplies the bounded selected conditional kernels used by the potential-outcome angular construction. Unlike the Gaussian-noise kernels in the support-boundary family, these kernels obey every finite conditional moment envelope uniformly in the exponent.
The real-valued Bernoulli kernel with measurable success-probability profile p.
Definition (Lean source)
A unit-range success-probability profile makes the selected Bernoulli kernel Markov.
Formal statement
Proof (Lean source)
The selected Bernoulli kernel has pointwise mean equal to its supplied success-probability profile.
Formal statement
Proof (Lean source)
The selected Bernoulli kernel has pointwise variance p(x)(1-p(x)).
Formal statement
Proof (Lean source)
Every pointwise absolute moment of order at least four equals the success probability and is therefore at most one.
Formal statement
Proof (Lean source)
Causal.Hypercube.Density 1 declarations Density and angular cancellation certificates for the hard family
Density and angular cancellation certificates for the hard family
The hypercube certificate includes uniform density and cell-mass control for every vertex.
Formal statement
Proof (Lean source)
Causal.Hypercube.Design 8 declarations The predicate in this file records the whole certified least-favourable family: common geometry, class membership, disjoint local cells, locality, target separation, radial agreement, and the two directed KL bounds.
Fixed-geometry angular hypercube
The predicate in this file records the whole certified least-favourable family: common geometry, class membership, disjoint local cells, locality, target separation, radial agreement, and the two directed KL bounds.
All quantitative certificates supplied by the rectangle-angular hypercube at separation Δ.
Definition (Lean source)
A single order-dependent bandwidth constant dominates every normalized bump derivative needed through order p + 1 and is strictly larger than the twice-cutoff threshold used in the order-zero construction.
Formal statement
Proof (Lean source)
For a fixed positive bandwidth constant, the power-law bandwidth is at most 1/24 throughout a sufficiently small positive separation interval.
Formal statement
Proof (Lean source)
The order-dependent constant and a small-separation interval jointly provide the scaled grid and the treatment-profile smooth-extension certificate. These are the geometric and smoothness leaves of the final hypercube constructor.
Formal statement
Proof (Lean source)
The geometric/smooth package supplies constructor-ready positive packing and cutoff constants. In particular, the cutoff is strictly below half the bandwidth constant, as required in the order-zero branch.
Formal statement
Proof (Lean source)
The constructor prefix with the quantitative small-separation facts kept explicit. These bounds are the common input to the Bernoulli variance, complete-cell, and localized signed-radius certificates in the final hypercube assembly.
Formal statement
Proof (Lean source)
The constructor data, analytic certificates, and normalized signed-cell comparison assemble into the complete hypercube predicate.
Formal statement
Proof (Lean source)
For every local-polynomial order, all sufficiently small separations allow the fixed-square, fixed-assignment rectangle-angular hypercube.
Formal statement
Proof (Lean source)
Causal.Hypercube.Divergence 1 declarations Adjacent signed-radius locality and divergence certificates
Adjacent signed-radius locality and divergence certificates
The hard-family predicate exposes a two-sided adjacent KL certificate at the Δ⁴/w² scale, together with common signed-radius marginals.
Formal statement
Proof (Lean source)
Causal.Hypercube.Family 17 declarations This module packages the normalized angular score measure and the two Bernoulli profiles into the selected-kernel potential-outcome law used at each hypercube vertex.
Decorated laws in the causal hard family
This module packages the normalized angular score measure and the two Bernoulli profiles into the selected-kernel potential-outcome law used at each hypercube vertex.
The causal hard law at one Boolean vertex. Its score marginal is the angular design on the fixed square and its selected arm kernels are exactly the Bernoulli kernels used to construct the joint potential-outcome law.
Definition (Lean source)
Every vertex law has the prescribed common support and assignment geometry.
Formal statement
Proof (Lean source)
At every score, the hard law's selected conditional means are the two profiles supplied to its Bernoulli kernels.
Formal statement
Proof (Lean source)
Every indexed coordinate partial of the constant control profile is 1/2 at order zero and vanishes at positive order.
Formal statement
Proof (Lean source)
The common control profile has the paper's Euclidean smooth-extension envelope for every bound at least 1/2.
Formal statement
Proof (Lean source)
Every hard-family vertex satisfies the smooth-extension clause for its control-arm regression.
Formal statement
Proof (Lean source)
Every complete hard cell has the advertised bit-independent probability under the full potential-outcome law.
Formal statement
Proof (Lean source)
The full potential-outcome law restricted to one hard cell depends on a vertex only through the bit indexing that cell.
Formal statement
Proof (Lean source)
Away from every hard cell, the full potential-outcome law is independent of the Boolean vertex.
Formal statement
Proof (Lean source)
Flipping one vertex bit changes the treatment effect at the corresponding cell center by exactly the bump amplitude.
Formal statement
Proof (Lean source)
Flipping one vertex bit changes the treatment effect at the corresponding cell center by exactly the bump amplitude.
Formal statement
Proof (Lean source)
The already-constructed hard law simultaneously supplies the common geometry, exact cell masses, bit locality, off-cell agreement, and target separation needed by the final hypercube assembly.
Formal statement
Proof (Lean source)
Every selected conditional outcome kernel in the hard family obeys the all-orders moment envelope, uniformly over scores and vertices.
Formal statement
Proof (Lean source)
The hard law's density is continuous on its support and obeys every class envelope L ≥ 48.
Formal statement
Proof (Lean source)
On the hard square, the selected Bernoulli kernels have exactly the decorated pointwise means and variances, and their variances obey every class envelope L ≥ 48.
Formal statement
Proof (Lean source)
Every hard-family vertex has the complete fixed-rectangle geometry block required by A1A2Class, including rectifiability and Hausdorff bounds.
Formal statement
Proof (Lean source)
Once the four genuinely analytic hard-square leaves are available, all remaining clauses of A1A2Class follow from the explicit score law, Bernoulli kernels, profiles, and fixed rectangle geometry.
Formal statement
Proof (Lean source)
Causal.Hypercube.HardSquareAnalytic 16 declarations This module starts the remaining local-mass, slice, and Gram block by reducing the uniform kernel to its closed-ball support.
Analytic reductions for the fixed hard square
This module starts the remaining local-mass, slice, and Gram block by reducing the uniform kernel to its closed-ball support.
The quadratic form of a scaled rank-one matrix is the scaled square of the corresponding dot product. This is the algebraic step that rewrites the population Gram form as an integral of a squared local polynomial.
Formal statement
Proof (Lean source)
Specializing the rank-one identity to the local-polynomial basis gives the squared polynomial integrand appearing in the population Gram floor.
Formal statement
Proof (Lean source)
A nonnegative local weight makes every rank-one polynomial Gram contribution positive semidefinite.
Formal statement
Proof (Lean source)
A closed axis-aligned box in the two-dimensional score space.
Definition (Lean source)
The volume of a nonempty score box is the product of its side lengths.
Formal statement
Proof (Lean source)
Coordinatewise displacement by at most half the radius stays inside the Euclidean closed ball in dimension two.
Formal statement
Proof (Lean source)
Coordinate characterization of the fixed assignment rectangle's frontier.
Formal statement
Proof (Lean source)
Every positive radius at most one cuts at least a quarter-box from the fixed treatment rectangle at each frontier point.
Formal statement
Proof (Lean source)
Every positive radius at most one cuts a fixed positive-area box from the support-side complement of the treatment rectangle.
Formal statement
Proof (Lean source)
The two fixed assignment arms have a common quadratic intersection-area lower bound at every interface point.
Formal statement
Proof (Lean source)
The uniform kernel is one exactly on its defining unit interval.
Formal statement
Proof (Lean source)
At positive bandwidth, either signed radial argument has uniform-kernel weight one exactly on the closed metric ball of that bandwidth.
Formal statement
Proof (Lean source)
The nonnegative integrand defining arm local mass is the constant h⁻² on the arm's closed bandwidth ball and zero elsewhere.
Formal statement
Proof (Lean source)
Arm local mass is the normalized Lebesgue area of the intersection of the chosen assignment arm with the closed bandwidth ball.
Formal statement
Proof (Lean source)
The fixed hard-square arms have normalized uniform-kernel local mass at least 1/8 at every interface point and every bandwidth at most one.
Formal statement
Proof (Lean source)
Every explicit angular hard law satisfies the class's uniform local-mass clause once the envelope is at least 48.
Formal statement
Proof (Lean source)
Causal.Hypercube.HardSquareClassGeometry 7 declarations This module transports the existing explicit square-frontier traversal to the fixed arm-one rectangle.
Class-level geometry of the fixed assignment rectangle
This module transports the existing explicit square-frontier traversal to the fixed arm-one rectangle. It supplies the rectifiability leaf needed by the hard-square class certificate.
Scale the unit square by two and translate it upward by one.
Definition (Lean source)
The affine image of the centered unit square is the fixed arm-one rectangle.
Formal statement
Proof (Lean source)
The square traversal transported to the fixed assignment rectangle.
Definition (Lean source)
The fixed assignment frontier is a rectifiable curve.
Formal statement
Proof (Lean source)
The hard square has the class's rectangular-support form for every envelope at least three.
Formal statement
Proof (Lean source)
The fixed rectangle frontier has one-dimensional Hausdorff mass between 1/48 and 48, the uniform bounds needed by every admissible hard law.
Formal statement
Proof (Lean source)
The fixed frontier Hausdorff bounds remain valid for every class envelope L ≥ 48.
Formal statement
Proof (Lean source)
Causal.Hypercube.HardSquareGeometry 28 declarations This file records the elementary square, rectangle, and disk facts used by the causal angular hypercube construction.
Geometry of the fixed causal hard square
This file records the elementary square, rectangle, and disk facts used by the causal angular hypercube construction.
The common square support [-3,3]².
The common arm-one rectangle [-1,1] × [0,2].
The middle of the bottom edge on which the packing points lie.
The equispaced hard-family centers on the middle of the assignment rectangle's bottom edge.
Definition (Lean source)
Every hard-family grid center lies on the prescribed middle bottom edge.
Formal statement
Proof (Lean source)
The translated hard-family grid has the same exact spacing as the lower-edge grid used by the support-boundary construction.
Formal statement
Proof (Lean source)
Distinct translated grid centers are separated by at least one grid spacing.
Formal statement
Proof (Lean source)
The local disk associated with a packing point.
Definition (Lean source)
The coordinate description of the hard square agrees with the standard score-cube representation used by the angular helpers.
Formal statement
Proof (Lean source)
The fixed hard square is Borel measurable.
Formal statement
Proof (Lean source)
The fixed hard square is compact.
Formal statement
Proof (Lean source)
The closure of the interior of the fixed hard square is the square itself.
Formal statement
Proof (Lean source)
Restricting planar Lebesgue measure to the fixed hard square has exactly that square as its topological support.
Formal statement
Proof (Lean source)
The fixed hard square has planar Lebesgue mass 36.
Formal statement
Proof (Lean source)
The arm-one rectangle is a Borel subset of the hard square.
Formal statement
Proof (Lean source)
The fixed arm-one rectangle is closed.
Formal statement
Proof (Lean source)
The fixed arm-one rectangle is compact.
Formal statement
Proof (Lean source)
The assignment rectangle, including its frontier, lies strictly inside the common score support.
Formal statement
Proof (Lean source)
The common assignment frontier is compact and lies in the interior of the fixed hard square.
Formal statement
Proof (Lean source)
The frontier shared by the two assignment arms is exactly the frontier of the arm-one rectangle.
Formal statement
Proof (Lean source)
The fixed arm-zero region is Borel measurable.
Formal statement
Proof (Lean source)
Every point of the fixed assignment rectangle lies in the support square.
Formal statement
Proof (Lean source)
The square complement of arm one and arm one form the required disjoint partition of the fixed support.
Formal statement
Proof (Lean source)
A radius-at-most-one disk centered on the selected middle bottom edge is strictly contained in the hard support square.
Formal statement
Proof (Lean source)
A planar hard cell has the usual disk area.
Formal statement
Proof (Lean source)
For every sufficiently small positive radius, the translated explicit grid supplies the cardinality, containment, three-radius separation, and full-disc disjointness required by the causal hard family.
Formal statement
Proof (Lean source)
At the paper bandwidth w = A Δ^(1/(p+1)), the explicit grid realizes the exact inverse-bandwidth cardinality rate and every geometric cell clause of A1A2HypercubeAt.
Formal statement
Proof (Lean source)
The scaled grid certificates in the constructor-ready form used by the hard-law family, retaining the stronger three-radius separation proved by the underlying explicit grid.
Formal statement
Proof (Lean source)
Causal.Hypercube.HardSquareGram 3 declarations This module isolates the finite-dimensional compactness argument behind the population-Gram floor.
Polynomial coercivity for the hard-square Gram certificate
This module isolates the finite-dimensional compactness argument behind the
population-Gram floor. Its radial energy is the polar-coordinate integral
of the squared degree-p local polynomial on a fixed nondegenerate interval.
A radial integrand over the open first-quadrant sector of a disk has the expected polar-coordinate representation. The omitted coordinate axes are Lebesgue-null, so this is the fixed π / 2 sector used at rectangle corners.
Formal statement
Proof (Lean source)
After bandwidth rescaling, the normalized squared-polynomial integral over the first-quadrant sector is exactly π / 2 times its radial energy.
Formal statement
Proof (Lean source)
The population Gram quadratic form is the integral of the squared local polynomial against the nonnegative arm and kernel weight.
Formal statement
Proof (Lean source)
Causal.Hypercube.HardSquareGramCertificate 27 declarations This module transports the hard law to its score density, restricts the Gram quadratic form to a fixed radial sector in either assignment arm, and combines the resulting polar integral with finite-dimensional polynomial
Population-Gram certificate for the hard square
This module transports the hard law to its score density, restricts the Gram quadratic form to a fixed radial sector in either assignment arm, and combines the resulting polar integral with finite-dimensional polynomial coercivity.
A component of the fixed hard-square population-Gram certificate.
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Definition (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Definition (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Definition (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Definition (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
A component of the fixed hard-square population-Gram certificate.
Formal statement
Proof (Lean source)
Causal.Hypercube.HardSquareSignedCancellation 8 declarations This module transports the quantitative polar cancellation estimate to an arbitrary score-space center.
Half-disc cancellation for signed hard-square observations
This module transports the quantitative polar cancellation estimate to an arbitrary score-space center. In particular it applies without another change of coordinates to the translated centers on the bottom edge of the hard assignment rectangle.
Reflecting horizontally through the cell center preserves every measurable signed-radius slice and reverses the angular density correction. Consequently the correction has zero integral on each such slice.
Formal statement
Proof (Lean source)
On a sufficiently small cell centered on the middle bottom edge, the hard-family signed statistic is the Euclidean radius with the sign of the vertical displacement.
Formal statement
Proof (Lean source)
The angular correction has zero integral on every measurable slice of the actual signed-distance statistic used by the hard family.
Formal statement
Proof (Lean source)
On every measurable radial slice of a translated complete disk, the angular density correction has zero mass. Point reflection through the center preserves the slice and negates the direction cosine.
Formal statement
Proof (Lean source)
On every measurable radial slice of a translated closed upper half-disc, the angular density correction has zero mass. Unlike the older grid-specific version, this statement applies directly to the hard-square centers.
Formal statement
Proof (Lean source)
The matching cancellation holds on every translated closed lower half-disc radial slice. Reflection through the center carries the upper slice to the lower slice and reverses the angular correction.
Formal statement
Proof (Lean source)
The quantitative upper-half-disc cancellation estimate is invariant under translation to an arbitrary score-space center.
Formal statement
Proof (Lean source)
The quantitative cancellation estimate at a hard-square packing center.
Formal statement
Proof (Lean source)
Causal.Hypercube.HardSquareSignedCertificate 3 declarations This file specializes the common-statistic Bernoulli comparison to the normalized hard-cell laws.
Quantitative signed-observation certificate for the hard square
This file specializes the common-statistic Bernoulli comparison to the normalized hard-cell laws. The first step identifies the signed-radius marginal by angular cancellation on every measurable fibre.
Every measurable signed-radius slice of a complete hard cell has its uniform-background mass, independently of the active bit.
Formal statement
Proof (Lean source)
The signed-radius marginal of the restricted score law is independent of the hard-cell bit.
Formal statement
Proof (Lean source)
The positive short signed-radius interval in a complete hard cell has at most its uniform-background disk mass.
Formal statement
Proof (Lean source)
Causal.Hypercube.HardSquareSignedKL 9 declarations This module identifies the observed outcome after signed-distance compression with an explicit Bernoulli mixture over the score law.
Signed-observation KL certificate for the hard square
This module identifies the observed outcome after signed-distance compression with an explicit Bernoulli mixture over the score law. It then combines the half-disc cancellation estimate with the common-statistic Bernoulli KL bound.
Inside an arbitrary separated packing cell, switching its active bit from false to true changes the regression-density product by the radial bump plus the angular cross term. Unlike the older lower-support-edge identity, this version applies to the interior hard-square cells.
Formal statement
Proof (Lean source)
The arbitrary-cell enable identity in the radial and direction-cosine coordinates used by the signed half-disc cancellation estimate.
Formal statement
Proof (Lean source)
The success profile obtained by selecting the treatment profile on a measurable arm and the control profile off that arm.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The potential outcome selected by membership of the score in an arm.
Definition (Lean source)
Restricting an explicit two-Bernoulli potential-outcome law to a score set and selecting the outcome according to a measurable arm gives the corresponding piecewise Bernoulli composition product.
Formal statement
Proof (Lean source)
On a hard cell, the raw signed observation measure is the explicit piecewise-Bernoulli composition product over the restricted score design.
Formal statement
Proof (Lean source)
The normalized signed-observation law on a hard cell depends on a vertex only through that cell's bit.
Formal statement
Proof (Lean source)
The hard family admits a bit-indexed choice of normalized cell laws, and every vertex's raw signed-observation measure is its common cell mass times the law selected by the corresponding bit.
Formal statement
Proof (Lean source)
Causal.Hypercube.HardSquareSignedNormalized 8 declarations This module chooses canonical bit representatives and transfers the raw signed-observation localization results to normalized conditional cell laws.
Normalized signed hard-cell certificate
This module chooses canonical bit representatives and transfers the raw signed-observation localization results to normalized conditional cell laws.
The canonical hypercube vertex representing one cell bit.
Definition (Lean source)
The canonical normalized signed-observation law for a cell bit.
Definition (Lean source)
The stated experiment law has total mass one and therefore defines a probability distribution.
Definition (Lean source)
Every raw cell observation measure is the common cell mass times the canonical normalized law selected by that vertex's cell bit.
Formal statement
Proof (Lean source)
The second marginal of a raw signed observation is its restricted signed-statistic marginal.
Formal statement
Proof (Lean source)
The canonical normalized bit laws have a common signed-radius marginal.
Formal statement
Proof (Lean source)
The canonical normalized bit laws agree away from the positive short-radius window.
Formal statement
Proof (Lean source)
Both KL orientations between the canonical normalized bit laws have the paper's fourth-order localized bound.
Formal statement
Proof (Lean source)
Causal.Hypercube.HardSquareSignedObservation 19 declarations This module isolates the measure normalization used by the hard-square hypercube.
Normalized signed-observation laws on hard cells
This module isolates the measure normalization used by the hard-square hypercube. The quantitative KL comparison can therefore work directly with probability laws, while the final constructor recovers the original restricted law by multiplying by the exact cell mass.
The one-observation pair (Y,D^{±}) at a fixed interface point.
Definition (Lean source)
On the treated arm, the observed coordinate of a signed observation is the treated potential outcome.
Formal statement
Proof (Lean source)
Off the treated arm, the observed coordinate of a signed observation is the control potential outcome.
Formal statement
Proof (Lean source)
On the arm-one part of a partition, signed distance is positive Euclidean distance.
Formal statement
Proof (Lean source)
On the arm-zero part of a partition, signed distance is negative Euclidean distance.
Formal statement
Proof (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The sign-dependent Bernoulli success profile of the observed outcome in the explicit hard family. The upper arm uses the perturbed treatment profile, while the lower arm uses the common control profile.
Definition (Lean source)
The observed hard-family Bernoulli parameter is Borel measurable.
Formal statement
Proof (Lean source)
Throughout the hard square, the observed-outcome success probability is uniformly bounded in the middle half of the Bernoulli parameter interval.
Formal statement
Proof (Lean source)
Signed Euclidean distance for the fixed hard-square assignment geometry, written directly as a score statistic.
Definition (Lean source)
The fixed-geometry signed-distance statistic is Borel measurable.
Formal statement
Proof (Lean source)
The signed distance carried by every explicit hard-family law is the fixed score statistic above; in particular it is independent of the vertex.
Formal statement
Proof (Lean source)
The finite signed-observation measure obtained by restricting a hard law to one packing cell and then applying the signed-distance compression.
Definition (Lean source)
The stated signed-observation measure has finite total mass.
Definition (Lean source)
The normalized probability law of a signed observation conditional on the observation lying in the selected hard cell.
Definition (Lean source)
The stated experiment law has total mass one and therefore defines a probability distribution.
Definition (Lean source)
A positive exact cell mass lets normalization be undone without a zero-measure fallback branch.
Formal statement
Proof (Lean source)
Equality after multiplication by a strictly positive finite cell mass can be cancelled. This is the normalization bridge used when a geometric calculation first identifies the signed-radius marginals of the restricted hard-cell measures.
Formal statement
Proof (Lean source)
On a fixed hard cell, equality of the underlying restricted laws implies equality of the normalized signed-observation laws. This is the locality bridge that makes the final conditional law depend only on the cell bit.
Formal statement
Proof (Lean source)
Causal.Hypercube.HardSquareSignedOutside 1 declarations This module complements the signed hard-cell KL estimate with exact equality of the two raw observation measures away from the positive short-radius window.
Exact localization for signed hard-cell observations
This module complements the signed hard-cell KL estimate with exact equality of the two raw observation measures away from the positive short-radius window.
Enabling one hard-cell bit changes its raw signed-observation measure only inside the positive short-radius window.
Formal statement
Proof (Lean source)
Causal.Hypercube.HardSquareSignedSuccess 5 declarations This module converts the half-disc angular cancellation into the setwise success-mass estimate needed by the common-statistic Bernoulli KL argument.
Signed hard-cell success-mass localization
This module converts the half-disc angular cancellation into the setwise success-mass estimate needed by the common-statistic Bernoulli KL argument.
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Causal.Hypercube.HardSquareSlice 13 declarations This module proves finiteness by parametrizing the ambient radius circle and strict positivity by exhibiting short armwise arcs with nontrivial coordinate projections.
Arm-slice certificates for the fixed hard square
This module proves finiteness by parametrizing the ambient radius circle and strict positivity by exhibiting short armwise arcs with nontrivial coordinate projections.
The two-dimensional score space is isometric to the complex plane.
Definition (Lean source)
Every radius circle in the score plane has finite one-dimensional Hausdorff measure.
Proof (Lean source)
A score coordinate is one-Lipschitz.
Formal statement
Proof (Lean source)
A score set whose coordinate projection contains a nondegenerate interval has positive one-dimensional Hausdorff measure.
Formal statement
Proof (Lean source)
A radius-circle arc written as a graph over the second coordinate.
Definition (Lean source)
A radius-circle arc written as a graph over the first coordinate.
Definition (Lean source)
Every admissible graph-over-second-coordinate arc point lies on its prescribed radius circle.
Formal statement
Proof (Lean source)
Every admissible graph-over-first-coordinate arc point lies on its prescribed radius circle.
Formal statement
Proof (Lean source)
The normal displacement of a short quarter arc is positive and at most the radius.
Formal statement
Proof (Lean source)
Every positive radius at most one cuts a positive-length arc from the fixed treatment rectangle at every frontier point.
Formal statement
Proof (Lean source)
Every positive radius at most one cuts a positive-length arc from the support-side complement of the treatment rectangle.
Formal statement
Proof (Lean source)
A uniformly positive and bounded density gives finite positive mass to each positive-length arm slice.
Formal statement
Proof (Lean source)
Every explicit angular hard law satisfies the class's finite-positive arm-slice condition once the envelope is at least 48.
Formal statement
Proof (Lean source)
Causal.Hypercube.PotentialOutcomeLaw 6 declarations This module assembles two pointwise Bernoulli selected kernels over a common score design into the (Y(0),Y(1),X) law carried by A1A2Law.
Explicit potential-outcome laws for the causal angular family
This module assembles two pointwise Bernoulli selected kernels over a common
score design into the (Y(0),Y(1),X) law carried by A1A2Law. In particular,
the selected kernels in the resulting decorated law are the same kernels used
to build its joint measure, so the disintegration field is exact.
The joint potential-outcome measure obtained by drawing the score and then two conditionally independent Bernoulli potential outcomes.
Definition (Lean source)
The score marginal of the explicit potential-outcome measure is its input design measure.
Formal statement
Proof (Lean source)
The explicit potential-outcome measure is a probability law.
Formal statement
Proof (Lean source)
Restricting two explicit potential-outcome laws to a measurable score cell gives the same measure when their restricted score designs agree and both Bernoulli profiles agree throughout that cell.
Formal statement
Proof (Lean source)
Mapping the explicit law to (X,Y(t)) recovers composition with the selected arm-t Bernoulli kernel.
Formal statement
Proof (Lean source)
Package the explicit two-kernel construction as a decorated A1A2Law. All pointwise conditional fields are definitionally tied to the same selected Bernoulli kernels used to assemble the joint potential-outcome measure.
Definition (Lean source)
Causal.Hypercube.Profiles 9 declarations This file specializes the existing smooth packing regression to the wider fixed square.
Bounded potential-outcome profiles for the causal hard square
This file specializes the existing smooth packing regression to the wider fixed square. The smaller affine slope leaves room for one positive local bump while keeping every Bernoulli parameter in the middle half.
The common control-arm Bernoulli success profile.
Definition (Lean source)
The treatment-arm profile with one smooth local bump per active bit.
Definition (Lean source)
Both hard-family potential-outcome profiles are Borel measurable.
Formal statement
Proof (Lean source)
The globally clipped profiles take values in the unit interval.
Formal statement
Proof (Lean source)
On the fixed square, the underlying smooth packing regression remains in the middle half of the unit interval.
Formal statement
Proof (Lean source)
On the fixed square, a bump of amplitude at most 1/16 keeps the treatment profile in [1/4,3/4], so global clipping is silent there.
Formal statement
Proof (Lean source)
On the hard square the global clip is inactive, so the treatment profile agrees with the underlying smooth affine-plus-bump regression.
Formal statement
Proof (Lean source)
The treatment profile on the hard square is the restriction of a globally smooth affine-plus-bump function.
Formal statement
Proof (Lean source)
Flipping one bit changes the treatment regression at its center by exactly the bump amplitude.
Formal statement
Proof (Lean source)
Causal.Hypercube.Regression 1 declarations Regression, selected-kernel moment, and Gram certificates
Regression, selected-kernel moment, and Gram certificates
Every hard-family member satisfies the Euclidean extension, conditional moment, variance, local-mass, and Gram-floor clauses through the single class certificate bundled in A1A2HypercubeAt.
Formal statement
Proof (Lean source)
Causal.Hypercube.ScoreLaw 11 declarations This module puts the existing smooth angular tilt over the fixed square [-3,3]² with baseline density 1/36.
Angular score law on the causal hard square
This module puts the existing smooth angular tilt over the fixed square
[-3,3]² with baseline density 1/36. Complete-disk cancellation gives
normalization and exact bit-independent cell mass.
The causal hard-family score density: uniform background 1/36 plus the disjoint smooth angular tilts.
Definition (Lean source)
The causal score measure supported on the fixed hard square.
Definition (Lean source)
The causal hard score density is continuous on the whole score plane.
Formal statement
Proof (Lean source)
Under three-bandwidth separation the causal density lies in the exact paper envelope [1/48,5/144].
Formal statement
Proof (Lean source)
Every admissible causal hard score law has the whole hard square as its exact topological support.
Formal statement
Proof (Lean source)
Restricting the causal score design to one packing cell erases every bit except the bit indexing that cell.
Formal statement
Proof (Lean source)
Away from all packing cells, every causal hard score law has the same restriction.
Formal statement
Proof (Lean source)
Restricting to the complement of all hard cells is bit-independent. This version includes the zero-mass region outside the hard square and therefore matches the full-law hypercube locality clause directly.
Formal statement
Proof (Lean source)
The unscaled angular density integrates to the hard square's area.
Formal statement
Proof (Lean source)
The angular score measure is normalized to total mass one.
Formal statement
Proof (Lean source)
Every complete packing cell has the exact bit-independent probability pi * w² / 36.
Formal statement
Proof (Lean source)
Causal.Hypercube.SmoothEnvelope 3 declarations This module converts the normalized bump derivative bounds into the exact coordinate-partial extension envelope required by A1A2Class.
Smooth extension leaf for the hard-square treatment profile
This module converts the normalized bump derivative bounds into the exact
coordinate-partial extension envelope required by A1A2Class.
If the finitely many normalized bump derivatives through order p + 1 obey their paper-scale bounds, the hard treatment profile has the required Euclidean smooth extension for every envelope at least 48.
Formal statement
Proof (Lean source)
At a power-law bandwidth, a bound on each normalized bump derivative by the bandwidth constant reduces the positive-order scaling inequalities to the elementary comparison delta * u⁻ʲ ≤ 1, where u^q = delta.
Formal statement
Proof (Lean source)
The paper-scale power bandwidth supplies the treatment-profile smooth extension once its zeroth derivative is controlled and the bandwidth constant dominates all normalized derivatives through order p + 1.
Formal statement
Proof (Lean source)
Causal.LawClass 23 declarations The ten conjuncts below retain the Euclidean carrier, selected conditional kernel, open-neighborhood smooth extension, uniform-kernel VC condition, Gram floor, local mass, and Hausdorff slice requirements of the paper.
The exact uniformized CTY Assumptions 1--2 class
The ten conjuncts below retain the Euclidean carrier, selected conditional kernel, open-neighborhood smooth extension, uniform-kernel VC condition, Gram floor, local mass, and Hausdorff slice requirements of the paper.
A compact axis-aligned square contained in [-L,L]².
Definition (Lean source)
Rectifiability of a specified curve, rather than of a support frontier.
Absolute coordinate partials of total order at most p on S.
Definition (Lean source)
Coordinate-partial Lipschitz quotients of total order at most p.
Definition (Lean source)
The paper's Euclidean C^{p+1}-extension envelope, using exactly the displayed maxima of scalar coordinate multi-index partial derivatives and their Lipschitz quotients. The two bounded-above guards make the real suprema faithful to those finite displayed maxima.
Definition (Lean source)
The degree-p population Gram matrix from the signed-distance design.
Definition (Lean source)
Quadratic form of a real square matrix.
Definition (Lean source)
The quantitative minimum-eigenvalue condition, expressed without a spectral API.
Definition (Lean source)
Lebesgue mass of the arm-t uniform-kernel neighborhood.
Definition (Lean source)
Hausdorff integral of the score density over an armwise distance slice.
One admissible selected disintegration kernel for a bare causal law. The pointwise clauses are properties of this witness, not of the arbitrary kernel decoration stored in A1A2Law.
Definition (Lean source)
The kernel selected from an existential class-membership certificate.
Definition (Lean source)
Conditional absolute moment computed from the selected class witness.
Definition (Lean source)
The stated conditional distribution is a Markov kernel: it is a probability law at each input and varies measurably with that input.
Formal statement
Proof (Lean source)
The selected conditional kernel disintegrates the causal law as stated.
Formal statement
Proof (Lean source)
The two stated constructions agree under the theorem's assumptions.
Formal statement
Proof (Lean source)
The two stated constructions agree under the theorem's assumptions.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Pointwise conditions on one admissible selected-kernel representative. In particular, the selected kernel's mean and variance are pinned pointwise on the support, rather than merely by the a.e. fields of A1A2Law.
Definition (Lean source)
The exact displayed L-uniformized Euclidean-distance, uniform-kernel CTY Assumptions 1--2 plus Theorem-2-envelope class. Membership existentially selects one admissible disintegration kernel and constrains that same witness pointwise; it does not constrain the arbitrary kernel decoration of P.
Definition (Lean source)
A pointwise-admissible decorated law belongs to the class.
Formal statement
Proof (Lean source)
The class as a set of causal laws.
Definition (Lean source)
The pointwise selected-kernel moment envelope implies the global armwise L^(2+ν) scope required by conditional-mean and conditional-variance APIs.
Formal statement
Proof (Lean source)
Causal.T3_A1A2PointIndexedConverse 9 declarations The proof uses the fixed-geometry hypercube, binomial good-count conditioning, the decentralized direct-product certificate, and outer-integral packaging.
Point-indexed converse on the causal A1/A2 class
The proof uses the fixed-geometry hypercube, binomial good-count conditioning, the decentralized direct-product certificate, and outer-integral packaging.
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Membership in the single fixed support, assignment rectangle, and interior boundary used by the causal hard subclass.
Definition (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
The causal outer risk after restricting the law supremum to the fixed hard geometry.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
For every polynomial order and moment exponent, the causal point-indexed outer-expectation minimax risk has a positive normalized liminf once the uniform envelope exceeds a threshold depending only on p.
Formal statement
Proof (Lean source)
Causal.T4_WinsorizedUpper 41 declarations The result is conditional on exactly three cited CTY interfaces: identification, sequential first-order bias, and the supplement's expected Gram/raw-score bounds.
Outer-expected upper bound for the explicit winsorized estimator
The result is conditional on exactly three cited CTY interfaces: identification, sequential first-order bias, and the supplement's expected Gram/raw-score bounds. The bounded winsorized-score maximal inequality is proved in run and introduces no fourth hypothesis.
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
The stated rate schedule is nonincreasing as sample size increases.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
As sample size grows, the stated sequence converges to zero.
Formal statement
Proof (Lean source)
As sample size grows, the stated effective sample-size sequence diverges to infinity.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
The observed outcome is integrable under the stated causal law.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Definition (Lean source)
The two stated constructions agree under the theorem's assumptions.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Definition (Lean source)
From a sufficiently large sample size onward, the two stated bandwidth schedules coincide.
Formal statement
Proof (Lean source)
The T4 bandwidth is strictly positive at every sample size.
Formal statement
Proof (Lean source)
The T4 bandwidth is nonincreasing as sample size increases.
Formal statement
Proof (Lean source)
As sample size grows, the T4 bandwidth converges to zero.
Formal statement
Proof (Lean source)
As sample size grows, the stated effective sample-size sequence diverges to infinity.
Formal statement
Proof (Lean source)
As sample size grows, the stated effective sample-size sequence diverges to infinity.
Formal statement
Proof (Lean source)
As sample size grows, the stated effective sample-size sequence diverges to infinity.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Uniform outer risk of the explicit estimator at the frontier bandwidth.
Definition (Lean source)
At h_n=a_n and B_n=a_n⁻¹ᐟ³, the explicit clipped and Gram-stabilized rule has uniform outer risk at most a constant multiple of a_n.
Formal statement
Proof (Lean source)
Causal.T5_MatchedFrontier 3 declarations This theorem combines the point-indexed converse with the explicit estimator.
Matched causal frontier
This theorem combines the point-indexed converse with the explicit estimator.
It is about the exact P₁₂(p,ν,L) class, not the distinct full
P_NP(L,q) support-boundary problem.
The minimax outer risk is bounded by the outer risk of the explicit stabilized local-polynomial rule once its frontier bandwidth is positive.
Formal statement
Proof (Lean source)
An eventual constant-times-frontier-rate bound for the explicit rule gives the corresponding normalized limsup bound.
Formal statement
Proof (Lean source)
The outer-expected minimax rate on the exact Euclidean/uniform-kernel causal class is a_n, for every L ≥ L₀(p). The three cited CTY interfaces remain explicit antecedents. The conclusion contains exactly the lower and upper frontier for a1a2OuterRisk and the explicit stabilized-estimator upper bound.
Formal statement
Proof (Lean source)
Causal.WinsorizedScoreMaximal 8 declarations The score-specific VC closure, envelope, and variance calculation are local.
Expected maximal bound for the bounded winsorized score
The score-specific VC closure, envelope, and variance calculation are local.
The final step calls the in-run vcExpectedMaximalInequality; there is no
external empirical-process assumption.
Winsorized empirical residual score evaluated at the original population coefficient.
Definition (Lean source)
Interface supremum of the centered winsorized score process.
Definition (Lean source)
The two stated constructions agree under the theorem's assumptions.
Formal statement
Proof (Lean source)
The two stated constructions agree under the theorem's assumptions.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
Under the stated assumptions, the theorem gives the displayed quantitative upper or lower bound.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
The bounded-envelope adaptation of the CTY expected maximal argument. The continuum-index empirical-process engine is proved in this repository by vcExpectedMaximalInequality; the constant is uniform in the moment offset and depends only on p and L.
Formal statement
Proof (Lean source)
Helpers.AnalyticMeasurability 5 declarations The common-map loss is jointly Borel, so its boundary-superlevel projections are analytic.
Analytic-set interface for completed boundary risks
The common-map loss is jointly Borel, so its boundary-superlevel projections are analytic. Causalean's universal-measurability substrate turns those analytic projections into completion-measurable sets and identifies completed integration with outer integration.
The loss generated by one common measurable map is jointly Borel on the compact boundary and the sample space.
Formal statement
Proof (Lean source)
The common-map boundary loss is upper-semi-analytic: each strict superlevel set is an analytic projection of a Borel set.
Formal statement
Proof (Lean source)
The boundary supremum of a common-map rule is measurable on the completed sample space.
Formal statement
Proof (Lean source)
The completed expectation of a common-map boundary loss equals its outer expectation.
Formal statement
Proof (Lean source)
The completed common-map risk dominates the outer point-indexed risk.
Formal statement
Proof (Lean source)
Helpers.AngularCellMass 2 declarations This module proves that angular tilting does not change the mass of any grid-centered half-disc.
Common cell masses for the angular packing
This module proves that angular tilting does not change the mass of any grid-centered half-disc. It isolates the cell-mass part of the finite hard family certificate from the later joint-law and KL arguments.
The angular density integrates over a grid cell to the cell's Lebesgue volume, independently of the packing vertex.
Formal statement
Proof (Lean source)
Every angular design assigns a grid cell exactly its Lebesgue volume; in particular, its mass is independent of the Boolean packing vertex.
Formal statement
Proof (Lean source)
Helpers.AngularCoordinates 7 declarations This file relates the Euclidean-space representation of CTY scores to the ordinary product plane used by Mathlib's polar-coordinate integration lemmas.
Coordinate bridge for the angular packing
This file relates the Euclidean-space representation of CTY scores to the ordinary product plane used by Mathlib's polar-coordinate integration lemmas.
The two ordinary real coordinates of a Euclidean CTY score.
Definition (Lean source)
Coordinate extraction preserves planar Lebesgue measure.
Formal statement
Proof (Lean source)
Coordinate extraction is a measurable embedding as well as measure-preserving.
Formal statement
Proof (Lean source)
Coordinate extraction commutes with subtraction.
Formal statement
Proof (Lean source)
The explicit planar radius of the coordinate difference is exactly the Euclidean distance between the corresponding CTY scores.
Formal statement
Proof (Lean source)
Relative to a lower-edge grid center, membership in its Euclidean closed ball is the same as the corresponding planar-radius inequality.
Formal statement
Proof (Lean source)
A sufficiently small ball around a lower-edge grid center is cut by the packing square exactly along the horizontal diameter: in centered planar coordinates, its packing cell is the closed upper half-disc.
Formal statement
Proof (Lean source)
Helpers.AngularDesign 28 declarations This file packages the paper's angular density as a Lebesgue density supported on the fixed square.
Angular packing design measure
This file packages the paper's angular density as a Lebesgue density supported
on the fixed square. It records the measurable-density, continuity, envelope,
positivity, and absolute-continuity facts needed by the eventual CtyLaw
constructor.
Coordinate cubes are Borel measurable.
Formal statement
Proof (Lean source)
The fixed square supporting the angular packing has unit Lebesgue mass.
Proof (Lean source)
The square supporting the angular construction is convex.
Proof (Lean source)
The square supporting the angular packing is compact.
Proof (Lean source)
The origin is an interior point of the square supporting the angular construction.
Proof (Lean source)
The closure of the interior of the supporting square is the whole square.
Proof (Lean source)
Restricting planar Lebesgue measure to the closed supporting square has exactly that square as its topological support.
Formal statement
Proof (Lean source)
The real-valued angular design density, extended by zero away from the fixed square.
Definition (Lean source)
On the square, the extended design density is the angular density.
Formal statement
Proof (Lean source)
Away from the square, the extended design density vanishes.
Formal statement
Proof (Lean source)
Within one square-truncated packing cell, the extended design density depends on a vertex only through that cell's Boolean coordinate.
Formal statement
Proof (Lean source)
Outside all packing cells, the extended design density is independent of the packing vertex (and equals one on the supporting square).
Formal statement
Proof (Lean source)
The square-supported angular density is Borel measurable.
Formal statement
Proof (Lean source)
Restricted to the square, the angular design density is continuous.
Formal statement
Proof (Lean source)
The extended density inherits the paper's uniform envelope on its square support.
Formal statement
Proof (Lean source)
In particular, the angular design density is strictly positive at every point of the square.
Formal statement
Proof (Lean source)
The covariate design measure associated with an angular packing vertex.
Definition (Lean source)
Restricting the score design to one packing cell erases every Boolean coordinate except the coordinate indexing that cell.
Formal statement
Proof (Lean source)
Outside the union of the square-truncated packing cells, every angular design restricts to the same unit-density square measure.
Formal statement
Proof (Lean source)
An angular design is the restriction of Lebesgue measure to the square, tilted there by the untruncated angular density.
Formal statement
Proof (Lean source)
Every admissibly separated angular design has the fixed square as its exact topological support.
Formal statement
Proof (Lean source)
The all-false angular design is exactly Lebesgue measure restricted to the supporting square.
Formal statement
Proof (Lean source)
The all-false angular design has the supporting square as its exact topological support.
Formal statement
Proof (Lean source)
Every angular design measure is absolutely continuous with respect to Lebesgue measure.
Formal statement
Proof (Lean source)
A grid-centered angular correction has zero integral over the whole supporting square, because it vanishes away from its own half-disc cell.
Formal statement
Proof (Lean source)
Every separated angular grid density integrates to one over the square.
Formal statement
Proof (Lean source)
Every admissibly separated angular design on the explicit grid is a probability measure.
Formal statement
Proof (Lean source)
With every angular bit off, the square-supported design is a probability measure. Later normalization reduces the general vertex to this baseline by showing that each active cosine tilt has zero integral.
Formal statement
Proof (Lean source)
Helpers.AngularFullDisc 2 declarations The causal hard-square construction places its angular cells on an interior assignment boundary.
Full-disc angular cancellation
The causal hard-square construction places its angular cells on an interior assignment boundary. Its score cells are therefore complete disks rather than the support-boundary half-disks used by the original angular packing. This module supplies the corresponding zero-mass cancellation.
A radial angular correction integrates to zero on every complete disk. Point reflection through the disk center preserves Lebesgue measure and the disk while negating the direction cosine.
Formal statement
Proof (Lean source)
A separated angular density integrates over each complete packing disk to the disk's ordinary Lebesgue area, independently of every Boolean bit.
Formal statement
Proof (Lean source)
Helpers.AngularGrid 32 declarations This file constructs an explicit equispaced family of centers on the middle half of the lower edge of the unit square.
Lower-edge angular packing grid
This file constructs an explicit equispaced family of centers on the middle half of the lower edge of the unit square. It proves boundary membership, exact pairwise distances, quantitative separation, and disjointness of the associated closed half-disc cells.
A point of the Euclidean score plane specified by its two coordinates.
Definition (Lean source)
The first coordinate of an explicitly specified score point.
Formal statement
Proof (Lean source)
The second coordinate of an explicitly specified score point.
Formal statement
Proof (Lean source)
Euclidean distance between two points on a horizontal line is their one-dimensional horizontal distance.
Formal statement
Proof (Lean source)
Euclidean distance between two points on a vertical line is their one-dimensional vertical distance.
Formal statement
Proof (Lean source)
Every non-corner point on the lower edge belongs to the frontier of the unit square.
Formal statement
Proof (Lean source)
The explicit equispaced Fin M grid on the middle half of the square's lower edge.
Definition (Lean source)
Formula for the horizontal coordinate of a grid center.
Formal statement
Proof (Lean source)
Every grid center lies on the lower edge.
Formal statement
Proof (Lean source)
Grid centers remain strictly inside the middle horizontal span, hence avoid both lower corners.
Formal statement
Proof (Lean source)
Grid centers lie strictly in the middle half of the lower edge, so in particular none of them is a corner of the square.
Formal statement
Proof (Lean source)
Every grid center lies on the frontier of the unit square.
Formal statement
Proof (Lean source)
Exact pairwise distance formula for the equispaced lower-edge grid.
Formal statement
Proof (Lean source)
Distinct grid centers are separated by at least one grid spacing.
Formal statement
Proof (Lean source)
If twice the radius is smaller than one grid spacing, the square-truncated closed balls around distinct centers are disjoint.
Formal statement
Proof (Lean source)
A radius at most one third of the grid spacing gives the paper's 3w center separation.
Formal statement
Proof (Lean source)
Positive cells whose radius is at most one third of the grid spacing are pairwise disjoint after truncation to the square.
Formal statement
Proof (Lean source)
Number of lower-edge grid points used at cell radius w. The factor 12 leaves enough slack for the paper's 3w separation.
Definition (Lean source)
The paper-scale radius: the qth power scale of the frontier rate.
Definition (Lean source)
At every positive smoothness order, the paper-scale radius is eventually positive and small enough for the explicit grid geometry.
Formal statement
Proof (Lean source)
For small positive radii, the explicit grid has at least a constant multiple of w⁻¹ points.
Formal statement
Proof (Lean source)
At the frontier-rate radius, the explicit grid meets the theorem's a_n⁻¹ᐟᵠ cardinality lower bound with constant 1/24.
Formal statement
Proof (Lean source)
The spacing of the grid selected by angularGridSize is at least three times its cell radius.
Formal statement
Proof (Lean source)
The radius-dependent explicit grid simultaneously has the required cardinality, frontier membership, corner avoidance, 3w separation, and pairwise-disjoint square-truncated cells.
Formal statement
Proof (Lean source)
Eventually, the frontier-rate grid simultaneously realizes every geometric part of the angular packing: the sharp radius scale, inverse-radius cardinality, non-corner frontier centers, three-radius separation, and pairwise-disjoint square-truncated cells.
Formal statement
Proof (Lean source)
Once the frontier rate is at most one, it is no larger than its qth-root bandwidth for every positive integer smoothness order.
Formal statement
Proof (Lean source)
The frontier rate is eventually at most one.
Formal statement
Proof (Lean source)
The deliberately small regression-bump amplitude used by the angular construction. The factor 1024 leaves room for the clipped angular tilt.
Definition (Lean source)
Eventually the packing amplitude is positive, lies below the regression envelope, and its full angular-cutoff radius fits inside the packing bandwidth.
Formal statement
Proof (Lean source)
Eventually the explicit grid geometry and all elementary amplitude/cutoff side conditions needed by the angular hard family hold at the same sample size. This is the common threshold consumed by the family constructor.
Formal statement
Proof (Lean source)
The fourth power of the frontier rate exactly cancels the sample size, leaving the logarithmic budget used in the adjacent KL calculation.
Formal statement
Proof (Lean source)
The selected packing amplitude spends exactly a 1024⁻⁴ fraction of the logarithmic KL budget before construction-specific constants.
Formal statement
Proof (Lean source)
Helpers.AngularHolder 17 declarations This module records the support fact that turns the pointwise derivative scaling estimates into bounds independent of the number of packing cells.
Hölder assembly for separated packing bumps
This module records the support fact that turns the pointwise derivative scaling estimates into bounds independent of the number of packing cells. It is the first step in the Hölder-ball certificate for the angular family.
At a positive integer smoothness order, the standard Euclidean Hölder ball is exactly a bounded-derivative ball whose top required derivative is Lipschitz. This removes the ceiling and real-power bookkeeping from the angular packing's eventual Hölder certificate.
Formal statement
Proof (Lean source)
The first Fréchet derivative of the affine baseline has operator norm at most the absolute slope.
Formal statement
Proof (Lean source)
Every derivative of the affine baseline of order at least two vanishes.
Formal statement
Proof (Lean source)
Every positive-order derivative of the affine baseline is independent of the evaluation point.
Formal statement
Proof (Lean source)
A finite sum of selected localized packing bumps is smooth to every finite order. This is the smoothness half of the eventual Hölder-ball certificate; separation is only needed for its uniform derivative bounds.
Formal statement
Proof (Lean source)
Every iterated derivative of a positive-bandwidth localized bump is supported in the corresponding closed ball.
Formal statement
Proof (Lean source)
At a point, derivatives of two distinct separated packing bumps cannot both be nonzero.
Formal statement
Proof (Lean source)
A separated family of localized bumps has at most one nonzero iterated derivative at each point.
Formal statement
Proof (Lean source)
An explicit normalized-bump derivative bound transfers to a separated bump sum without acquiring a factor depending on the grid size.
Formal statement
Proof (Lean source)
The norm of any derivative of a separated bump sum is bounded by the single-bump scaling bound, with no factor depending on the grid size.
Formal statement
Proof (Lean source)
The top derivative of a separated bump sum is globally Lipschitz, with the one-bump scaling constant and no dependence on the number of cells.
Formal statement
Proof (Lean source)
A supplied normalized-bump derivative bound gives the corresponding Lipschitz estimate for a separated bump sum. This explicit-constant variant lets the final Hölder assembly use one finite family of constants.
Formal statement
Proof (Lean source)
At every point of the supporting square, clipping is inactive throughout a neighborhood. This is stronger than pointwise equality on the square and therefore transfers ambient Fréchet derivatives at boundary points.
Formal statement
Proof (Lean source)
On the supporting square, the clipped packing regression is smooth to every finite order. This packages the neighborhood-level inactivity of the clip into the first conjunct of the eventual Hölder-ball certificate.
Formal statement
Proof (Lean source)
On the supporting square, every ambient iterated derivative of the clipped kernel regression equals that of the smooth packing regression.
Formal statement
Proof (Lean source)
Unit derivative and top-derivative Lipschitz bounds for the separated bump sum assemble with the small affine baseline to put the clipped regression in every envelope-L integer Hölder ball with L ≥ 4. The two bump bounds are exactly the conclusions supplied by the scaling lemmas above once their paper-scale scalar factors have been bounded.
Formal statement
Proof (Lean source)
Uniform normalized-bump derivative constants whose paper-scale factors are at most one imply the complete clipped-regression Hölder certificate.
Formal statement
Proof (Lean source)
Helpers.AngularLaw 11 declarations This file packages the measure-theoretic assembly common to every vertex of the angular hard family.
Faithful Bernoulli--Gaussian regression laws
This file packages the measure-theoretic assembly common to every vertex of
the angular hard family. Given a normalized score design with its exact
support and a bounded measurable regression, it constructs a CtyLaw whose
declared density, regression, and conditional variance are the corresponding
functionals of the joint Bernoulli-plus-Gaussian law.
The faithful CTY law obtained from a score design and a measurable Bernoulli regression by adding independent standard Gaussian noise.
Definition (Lean source)
The packaged Bernoulli--Gaussian law belongs to the CTY class once the geometric, density, Holder, and variance certificates for its supplied profiles have been established.
Formal statement
Proof (Lean source)
The score marginal of the packaged CTY law is the input design measure.
Formal statement
Proof (Lean source)
The packaged CTY law exposes the supplied regression pointwise, including at boundary points where the conditional-mean identity itself is only a.e.
Formal statement
Proof (Lean source)
The packaged CTY law exposes the Bernoulli-plus-Gaussian conditional variance pointwise.
Formal statement
Proof (Lean source)
The faithful law at one vertex of the angular packing family. Its score design is the angularly tilted square density and its Bernoulli regression is the globally clipped packing regression, which agrees with the smooth paper regression throughout the square.
Definition (Lean source)
Every angular packing law has the fixed square as its declared support.
Formal statement
Proof (Lean source)
The score marginal of an angular packing law is exactly its explicitly constructed angular design measure.
Formal statement
Proof (Lean source)
On the square, the angular packing law's regression is exactly the smooth packing regression used in the paper construction.
Formal statement
Proof (Lean source)
At every grid center, the faithful law's regression equals the Boolean center value used by the finite packing certificate.
Formal statement
Proof (Lean source)
All non-Hölder obligations for membership of an angular packing vertex in the CTY class follow from the explicit square design and Bernoulli--Gaussian construction. The remaining hypothesis is precisely the scaled-bump Hölder estimate.
Formal statement
Proof (Lean source)
Helpers.AngularLocality 3 declarations This module lifts locality of the score design and regression kernel to locality of the faithful joint Bernoulli--Gaussian law.
Cellwise locality of the angular hard family
This module lifts locality of the score design and regression kernel to locality of the faithful joint Bernoulli--Gaussian law. It then applies that bridge to one square-truncated packing cell.
Two Bernoulli--Gaussian joint laws have identical restrictions over a measurable score cell when their restricted score designs agree and their Bernoulli parameters agree throughout that cell.
Formal statement
Proof (Lean source)
The joint law restricted to a packing cell depends on the Boolean vertex only through the bit indexing that cell.
Formal statement
Proof (Lean source)
The joint law outside all square-truncated packing cells is independent of the Boolean packing vertex.
Formal statement
Proof (Lean source)
Helpers.AngularMeasure 38 declarations This file defines the smooth radial cutoff and cosine tilt used to perturb the design density inside a packing cell.
Angular density profile for the square packing
This file defines the smooth radial cutoff and cosine tilt used to perturb the
design density inside a packing cell. It proves the cutoff identities, the
uniform tilt envelope, and the zero-mass polar cancellation. The denominator
is clipped below by the cutoff scale; on the region where the cutoff is one it
is exactly the paper's b r denominator.
Smooth cutoff which is zero when b r ≤ cA δ and one when 2 cA δ ≤ b r.
Definition (Lean source)
The angular cutoff always takes values in the unit interval.
Formal statement
Proof (Lean source)
The angular cutoff vanishes below its inner radial threshold.
Formal statement
Proof (Lean source)
The angular cutoff equals one beyond twice its inner radial threshold.
Formal statement
Proof (Lean source)
The cutoff is a continuous function of the radius.
Formal statement
Proof (Lean source)
The radial bump profile appearing in the angular density correction.
Definition (Lean source)
The radial profile takes values in the unit interval.
Formal statement
Proof (Lean source)
A positive-bandwidth radial profile vanishes at every radius outside its bandwidth.
Formal statement
Proof (Lean source)
The radial profile is continuous.
Formal statement
Proof (Lean source)
The scaled Euclidean bump used in the regression is exactly the radial profile used in the angular cancellation formula.
Formal statement
Proof (Lean source)
The clipped angular tilt. Clipping only regularizes the denominator in the transition region; once the cutoff is one this is exactly -2 δ φ(r/w) / (b r).
Definition (Lean source)
The angular tilt is continuous in the radius at every positive cutoff scale.
Formal statement
Proof (Lean source)
At envelope parameter cA, the angular tilt has absolute value at most 2/cA.
Formal statement
Proof (Lean source)
With the paper's choice cA ≥ 8, the density tilt is bounded by one quarter.
Formal statement
Proof (Lean source)
The multiplicative density factor in polar coordinates.
Definition (Lean source)
The paper's choice cA ≥ 8 keeps the angular density factor in [3/4, 5/4], uniformly over radius and angle.
Formal statement
Proof (Lean source)
In particular, every angular density factor is strictly positive.
Formal statement
Proof (Lean source)
The cosine of the polar direction around a packing center, with the value at the center fixed to zero. This coordinate formula avoids choosing a global angle on the score plane.
Definition (Lean source)
The coordinate direction cosine has absolute value at most one.
Formal statement
Proof (Lean source)
One center's signed angular correction to the design density.
Definition (Lean source)
The cutoff removes the apparent directional singularity at the center, so each angular correction is continuous on the whole score plane.
Formal statement
Proof (Lean source)
Each active angular correction is uniformly bounded by one quarter.
Formal statement
Proof (Lean source)
A center contributes no angular density correction outside its packing bandwidth.
Formal statement
Proof (Lean source)
The design density obtained by summing the active disjoint angular corrections over the packing grid.
Definition (Lean source)
The finite angularly tilted design density is continuous.
Formal statement
Proof (Lean source)
The finite angularly tilted design density is Borel measurable.
Formal statement
Proof (Lean source)
Three-bandwidth separation ensures that at most one angular correction is nonzero at any score point, so summing the family does not enlarge its pointwise envelope.
Formal statement
Proof (Lean source)
The angularly tilted design density remains in the paper's uniform density envelope.
Formal statement
Proof (Lean source)
Inside one closed packing ball, the angular density depends on the bit vector only through that ball's coordinate.
Formal statement
Proof (Lean source)
Away from every closed packing ball, all angular corrections vanish and the design density is the common unit baseline.
Formal statement
Proof (Lean source)
Below the inner cutoff radius the angular tilt vanishes identically.
Formal statement
Proof (Lean source)
Beyond twice the cutoff radius the clipped tilt agrees with the paper's unclipped cancellation formula.
Formal statement
Proof (Lean source)
Outside the bump bandwidth the angular density perturbation vanishes.
Formal statement
Proof (Lean source)
Outside the bump bandwidth the perturbed polar density factor is exactly the common baseline density.
Formal statement
Proof (Lean source)
Once the cutoff is fully active, the radial bump contribution and the affine-times-angular contribution cancel after integrating over the half-circle.
Formal statement
Proof (Lean source)
The cosine angular density correction has zero total mass on every upper half-disc.
Formal statement
Proof (Lean source)
The direction cosine used by the angular density is the Cartesian first coordinate divided by Euclidean radius after passing to centered planar coordinates.
Formal statement
Proof (Lean source)
Each angular correction integrates to zero on its square-truncated grid cell. This is the normalization bridge for every tilted design vertex.
Formal statement
Proof (Lean source)
Helpers.AngularPacking 37 declarations This file provides the low-level probability and geometry primitives for the square-support hypercube construction.
Angular hard-family packing
This file provides the low-level probability and geometry primitives for the
square-support hypercube construction. The complete certificate is stated
downstream in AngularPackingTheorem, after the faithful law constructor is
available without an import cycle.
The fixed unit square supporting every law in the hard family.
The square used by the hard family is compact.
Formal statement
Proof (Lean source)
Any envelope at least one half contains the packing square in its ambient coordinate cube.
Formal statement
Proof (Lean source)
The half-disc cell cut out by the square at a boundary packing point.
Definition (Lean source)
The explicit lower-edge grid centers lie on the frontier of the packing square.
Formal statement
Proof (Lean source)
The explicit grid yields pairwise disjoint packing cells whenever twice the cell radius is smaller than one grid spacing.
Formal statement
Proof (Lean source)
Whenever the frontier-rate radius is small, the explicit grid supplies the entire geometric prefix of AngularPackingAt, with constants c₀ = 1/24 and both radius-comparison constants equal to one.
Formal statement
Proof (Lean source)
The one-observation unsigned radial-outcome law at a query point.
Definition (Lean source)
The one-observation radial-outcome law is a probability measure.
Formal statement
Proof (Lean source)
The n-observation distance-compressed law at a query point.
Definition (Lean source)
The distance-compressed i.i.d. sample law is a probability measure.
Formal statement
Proof (Lean source)
The compressed i.i.d. sample law is exactly the finite product of the one-observation radial-outcome law. This is the bridge that permits KL tensorization directly after distance compression.
Formal statement
Proof (Lean source)
A finite one-observation radial KL bound tensorizes to the compressed sample law. Absolute continuity and log-likelihood integrability are the standard finite-KL guards required by product tensorization.
Formal statement
Proof (Lean source)
Unsigned-distance compression of an i.i.d. sample cannot increase its Kullback--Leibler divergence.
Formal statement
Proof (Lean source)
The common additive standard-Gaussian channel used to turn Bernoulli outcomes into the smooth conditional outcome laws of the packing.
Definition (Lean source)
The stated conditional distribution is a Markov kernel: it is a probability law at each input and varies measurably with that input.
Definition (Lean source)
At input b, the additive standard-Gaussian channel has law N(b,1).
Formal statement
Proof (Lean source)
Convolution with the common additive Gaussian noise in the packing cannot increase the Bernoulli-stage Kullback--Leibler divergence.
Formal statement
Proof (Lean source)
The conditional outcome law obtained by adding independent standard Gaussian noise to a real-valued Bernoulli draw.
Definition (Lean source)
The Bernoulli-plus-Gaussian outcome law is the explicit mixture of the unit-variance Gaussians centered at one and zero.
Formal statement
Proof (Lean source)
Adding the common Gaussian noise preserves the quadratic KL bound for Bernoulli parameters in the middle half of the unit interval.
Formal statement
Proof (Lean source)
For a success probability in the unit interval, the Bernoulli-plus-Gaussian outcome law is a probability measure.
Formal statement
Proof (Lean source)
The identity is integrable under every Bernoulli-plus-Gaussian outcome law, including parameter values outside the unit interval.
Formal statement
Proof (Lean source)
The identity is square-integrable under every Bernoulli-plus-Gaussian outcome law. This supplies the CtyLaw.sq_integrable field of the eventual hard-family construction.
Formal statement
Proof (Lean source)
The conditional mean of a Bernoulli draw plus centered Gaussian noise is its Bernoulli success probability.
Formal statement
Proof (Lean source)
The second moment about an arbitrary center under N(m,1) equals one plus the squared displacement from the Gaussian mean.
Formal statement
Proof (Lean source)
The conditional variance of a Bernoulli draw plus independent standard Gaussian noise is 1 + p(1-p).
Formal statement
Proof (Lean source)
The measurable Bernoulli-plus-Gaussian kernel of a regression function.
Definition (Lean source)
A unit-range regression function makes the outcome kernel Markov.
Formal statement
Proof (Lean source)
The joint (Y,X) law from a design and the explicit outcome kernel.
Definition (Lean source)
A probability design and unit-range regression give a probability law.
Formal statement
Proof (Lean source)
The score marginal is exactly the supplied design law.
Formal statement
Proof (Lean source)
Disintegration recovers the supplied outcome kernel almost everywhere.
Formal statement
Proof (Lean source)
The second moment of a Bernoulli draw plus standard Gaussian noise is 1+p.
Formal statement
Proof (Lean source)
The outcome coordinate of the explicit joint law is square-integrable.
Formal statement
Proof (Lean source)
The conditional mean is the regression used in the construction.
Formal statement
Proof (Lean source)
The conditional variance is 1+p(1-p).
Formal statement
Proof (Lean source)
Helpers.AngularPackingOnePointKL 6 declarations This module connects the common-radius KL interface to the angular packing, including its middle-half parameter clipping and short-radius mass bound.
Construction-specific one-point KL bound
This module connects the common-radius KL interface to the angular packing, including its middle-half parameter clipping and short-radius mass bound.
Pointwise clipping to the middle half of the Bernoulli parameter range.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The clipped success parameter lies in the displayed closed interval.
Formal statement
Proof (Lean source)
On an admissible angular design, middle-half clipping is silent almost everywhere because the design is supported on the packing square.
Formal statement
Proof (Lean source)
The radius marginal of an admissible angular design assigns at most the density envelope times the enclosing planar disk area to a short interval.
Formal statement
Proof (Lean source)
For the fixed angular constants, one changed bit has one-observation radius--outcome KL at most the declared fourth-order envelope.
Formal statement
Proof (Lean source)
Helpers.AngularPackingTheorem 18 declarations This downstream module states the complete finite packing certificate and its eventual fixed-constant construction.
Angular hard-family certificate
This downstream module states the complete finite packing certificate and its
eventual fixed-constant construction. Keeping it downstream of AngularLaw
lets the assembly use the faithful CTY-law constructor without an import cycle.
The full finite hard-family certificate at sample size n, with constants fixed outside n.
Definition (Lean source)
The score marginal of a faithful angular packing law assigns each grid cell exactly its Lebesgue volume, independently of the Boolean vertex.
Formal statement
Proof (Lean source)
All lower-edge grid cells have the same Lebesgue volume. Translation along the lower edge carries one closed half-disc exactly onto any other and preserves planar Lebesgue measure.
Formal statement
Proof (Lean source)
At the selected amplitude, the faithful angular laws take their declared Boolean values at every grid center, and the two values have the exact fixed frontier-rate separation.
Formal statement
Proof (Lean source)
The faithful angular laws satisfy both exact locality clauses appearing in AngularPackingAt: a cell sees only its own bit, while the law off the union of cells is independent of the entire Boolean vertex.
Formal statement
Proof (Lean source)
Adjacent faithful angular laws have the same complete unsigned-radius law at the grid center whose bit is changed.
Formal statement
Proof (Lean source)
Flipping one packing bit preserves the full unsigned-radius law at the corresponding grid center.
Formal statement
Proof (Lean source)
The derivative-scaling leaves for the normalized bump assemble into the complete CTY-class certificate for every vertex of the angular family. This is the Hölder part of the final packing construction; none of its bounds depend on the number of cells or on the Boolean vertex.
Formal statement
Proof (Lean source)
The radial-cancellation and disintegration leaves jointly give the common radius marginal and explicit radial fibre representations for both endpoints of every adjacent edge of the Boolean hypercube.
Formal statement
Proof (Lean source)
The two Boolean regression values at a packing center have exactly the smoothness-normalized frontier-rate separation.
Formal statement
Proof (Lean source)
For an admissible sample size, the normalized amplitude and frontier-rate bandwidth satisfy every derivative scaling inequality through order q.
Formal statement
Proof (Lean source)
The smoothness-normalized amplitude turns the derivative/scaling leaves into the complete Hölder-class certificate for an angular packing vertex.
Formal statement
Proof (Lean source)
Eventually the smoothness-normalized amplitude is positive, stays inside the regression envelope, and its complete angular-cancellation radius lies inside the frontier-rate cell bandwidth.
Formal statement
Proof (Lean source)
Every radius beyond one eighth of the frontier rate lies in the region where the angular cutoff is fully active for the smoothness-normalized amplitude. This is the numerical bridge used by radial outcome cancellation.
Formal statement
Proof (Lean source)
On every measurable tail beginning at one eighth of the frontier rate, the scaled angular cutoff is fully active. This is the exact quantified form needed by the radial-slice cancellation argument.
Formal statement
Proof (Lean source)
Assembly interface for the final angular certificate. It isolates the three genuinely radial obligations (common cell mass, equality off the active radius, and compressed KL) from the already-closed geometry, class, locality, and center-value parts of the construction.
Formal statement
Proof (Lean source)
At the smoothness-normalized amplitude, the already-proved geometric, Hölder, locality, support, center-value, and radial-marginal leaves reduce the full angular packing certificate to its three remaining radial estimates.
Formal statement
Proof (Lean source)
For every admissible smoothness order and envelope, fixed positive constants and a fixed α < 1/8 yield the CTY square-support angular hard family for all sufficiently large sample sizes.
Formal statement
Proof (Lean source)
Helpers.AngularRadial 12 declarations This module strengthens the polar cancellation identities to measurable radial subsets and transports them to the square-truncated cells used by the angular packing.
Radial cancellation for angular packing cells
This module strengthens the polar cancellation identities to measurable radial subsets and transports them to the square-truncated cells used by the angular packing. These setwise identities are the leaf input for equality of adjacent radius pushforwards.
Cartesian direction-cosine cancellation continues to hold after restricting an open upper half-disc to any measurable set of radii.
Formal statement
Proof (Lean source)
Closing the diameter of the half-disc does not alter setwise radial Cartesian direction-cosine cancellation.
Formal statement
Proof (Lean source)
Translation preserves closed-half-disc cancellation on every measurable radial subset.
Formal statement
Proof (Lean source)
At a lower-edge angular grid center, every radial weight times the horizontal direction cosine integrates to zero on each measurable radial slice of the square-truncated cell.
Formal statement
Proof (Lean source)
An angular correction integrates to zero on every measurable radial slice of its square-truncated packing cell.
Formal statement
Proof (Lean source)
Every measurable radial slice of a grid cell has its unperturbed Lebesgue mass under the angular density, independently of the active bit.
Formal statement
Proof (Lean source)
The score design assigns every measurable radial slice of a grid cell exactly its Lebesgue volume, uniformly over packing vertices.
Formal statement
Proof (Lean source)
Outside one grid cell, two angular design densities agree whenever all Boolean coordinates other than that cell's coordinate agree.
Formal statement
Proof (Lean source)
The restrictions of two adjacent angular score designs to the complement of the changed grid cell are identical.
Formal statement
Proof (Lean source)
The radius pushforwards of two angular score designs agree whenever the vertices differ, if at all, only at the queried grid cell.
Formal statement
Proof (Lean source)
On every measurable set of radii where the angular cutoff is fully active, the radial bump contribution is exactly cancelled by the affine-times-angular contribution after integration over the upper half-disc.
Formal statement
Proof (Lean source)
Translation of the fully-active radial outcome cancellation to a packing center. This is the form used when the lower-edge half-disc is written in the ambient score coordinates.
Formal statement
Proof (Lean source)
Helpers.AngularRadialAlgebra 4 declarations This module isolates the pointwise product identity behind the radial-outcome cancellation.
Pointwise algebra for angular radial fibres
This module isolates the pointwise product identity behind the radial-outcome cancellation. It evaluates the regression and design density in the changed cell before the later integral argument discards the purely angular terms.
Before the cutoff is fully active, the uncancelled radial success-mass increment is exactly the bump amplitude times the complementary cutoff.
Formal statement
Proof (Lean source)
The uncancelled radial success-mass increment has absolute value at most the bump amplitude. This is the pointwise input to the exceptional-radius Bernoulli KL estimate.
Formal statement
Proof (Lean source)
Inside the changed cell, a true packing bit contributes exactly its radial bump, while its flipped false bit contributes only the affine baseline.
Formal statement
Proof (Lean source)
The cell product identity in the radial-profile and direction-cosine coordinates consumed by the polar cancellation lemmas.
Formal statement
Proof (Lean source)
Helpers.AngularRadialAssembly 2 declarations This module turns the polar cancellation identity for the changed half-disc into equality of the complete radius--outcome laws beyond an active cutoff.
Assembly of angular radial-fibre cancellation
This module turns the polar cancellation identity for the changed half-disc into equality of the complete radius--outcome laws beyond an active cutoff.
For a true changed bit, the conditional-mean mass of every fully active radial slice is unchanged by flipping that bit.
Formal statement
Proof (Lean source)
If the angular cutoff is fully active beyond R, flipping a bit leaves the complete radius--outcome law unchanged on that tail.
Formal statement
Proof (Lean source)
Helpers.AngularRadialFibre 3 declarations This module assembles the pointwise product identity and polar cancellation leaves needed by the eventual equality of radial outcome fibres.
Radial fibre cancellation for adjacent angular packing laws
This module assembles the pointwise product identity and polar cancellation leaves needed by the eventual equality of radial outcome fibres.
Integrating the clipped regression under an angular design is exactly Lebesgue integration of the untruncated regression times its design density on the part of the set lying in the packing square. This is the bookkeeping bridge between the faithful score law and the polar cancellation identities.
Formal statement
Proof (Lean source)
At a lower-edge grid center, a radial weight times the horizontal direction cosine integrates to zero on every open-half-disc radial slice.
Formal statement
Proof (Lean source)
For a true bit, the outcome-weighted design-density difference integrates to zero on every fully active radial slice of its cell.
Formal statement
Proof (Lean source)
Helpers.AngularRadialKL 1 declarations This module packages the finite-KL bookkeeping needed to tensorize a one-observation radial-outcome estimate.
KL assembly for angular radial laws
This module packages the finite-KL bookkeeping needed to tensorize a one-observation radial-outcome estimate. In particular, absolute continuity and log-likelihood integrability are consequences of a finite real KL bound; they need not be proved separately by the angular construction.
A finite real bound on one-observation radial KL supplies the absolute continuity and log-likelihood integrability guards required by product tensorization.
Formal statement
Proof (Lean source)
Helpers.AngularRadialOnePointKL 15 declarations This module supplies the paper-local common-radius kernel representation and the quantitative exceptional-radius estimate used by the angular packing.
One-point KL bound for the angular radial construction
This module supplies the paper-local common-radius kernel representation and the quantitative exceptional-radius estimate used by the angular packing.
The success-weighted radius measure associated with a score law and a Bernoulli regression.
Definition (Lean source)
The measurable radial Bernoulli parameter obtained as the density of the success-weighted radius measure with respect to the radius marginal.
Definition (Lean source)
The success-weighted radius measure is absolutely continuous with respect to the radius marginal whenever the regression is at most one.
Formal statement
Proof (Lean source)
Integrating the radial success parameter over a measurable radial set recovers the success-weighted score integral on its preimage.
Formal statement
Proof (Lean source)
A scorewise middle-half bound passes to the Radon--Nikodym radial success parameter.
Formal statement
Proof (Lean source)
A globally clipped version of the radial success parameter. Clipping is silent almost everywhere under the radius marginal but makes the associated Bernoulli--Gaussian kernel a Markov kernel without exceptional values.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The clipped success parameter lies in the displayed closed interval.
Formal statement
Proof (Lean source)
The two stated constructions agree under the theorem's assumptions.
Formal statement
Proof (Lean source)
The Bernoulli--Gaussian kernel over an arbitrary measurable base type.
Definition (Lean source)
The stated conditional distribution is a Markov kernel: it is a probability law at each input and varies measurably with that input.
Formal statement
Proof (Lean source)
Two Bernoulli--Gaussian mixtures over possibly different base spaces have the same outcome mass when the base masses and integrated success parameters agree.
Formal statement
Proof (Lean source)
After forgetting score direction, a Bernoulli--Gaussian score mixture is a composition product over the radius marginal with the clipped radial success parameter, followed by swapping radius and outcome coordinates.
Formal statement
Proof (Lean source)
A setwise bound on success-weighted radial masses gives the corresponding almost-everywhere bound on the two radial Bernoulli parameters.
Formal statement
Proof (Lean source)
The common-radius disintegration and a localized radial-parameter bound give a one-observation KL estimate proportional to the exceptional radial mass.
Formal statement
Proof (Lean source)
Helpers.AngularRadialOutcome 8 declarations This module rewrites the one-observation distance-compressed law of an angular packing vertex directly as the pushforward of its score-first disintegration.
Radial outcome representation for the angular packing
This module rewrites the one-observation distance-compressed law of an angular packing vertex directly as the pushforward of its score-first disintegration. The representation is the bridge from radial cancellation to the exceptional- radius equality and one-point KL estimates used by the final certificate.
Equality of radius pushforwards gives equality of the base mass on every measurable radial slice. This is the mass half of the Bernoulli--Gaussian radial-fibre comparison.
Formal statement
Proof (Lean source)
A rectangle under a radius--outcome pushforward of a composition product is the fibre probability integrated over the corresponding radial slice of the base measure. This is the rectangle-level disintegration identity used to turn the setwise polar cancellation lemmas into equality of radial-outcome measures.
Formal statement
Proof (Lean source)
Equality of all outcome probabilities on all radial slices beyond R assembles into equality of the two restricted radius--outcome laws. The hypothesis is deliberately rectangle-level, matching the output of the polar integral calculations.
Formal statement
Proof (Lean source)
The one-point radial-outcome law of an angular packing vertex is the pushforward of the explicit score design and Bernoulli--Gaussian fibre kernel. This keeps the score first until the final map, exposing the radial fibres used by the cancellation argument.
Formal statement
Proof (Lean source)
Rectangle probabilities of the angular radial-outcome law are obtained by integrating its explicit Bernoulli--Gaussian fibre over a radial slice of the angular score design.
Formal statement
Proof (Lean source)
The fully-active angular outcome cancellation, transported from planar coordinates to the Euclidean score space at a lower-edge grid center. This is the score-space form consumed by the radial fibre-law comparison.
Formal statement
Proof (Lean source)
On a fixed score slice, a Bernoulli--Gaussian mixture is determined by the slice mass and the slice integral of its Bernoulli parameter. This is the measure-theoretic bridge from the two polar cancellation identities to equality of radial outcome fibres.
Formal statement
Proof (Lean source)
Rectangle-level radial fibre identities for two angular vertices imply equality of their complete radius--outcome laws beyond the stated cutoff. This packages the explicit score-first disintegrations with the product-set extension argument, so the packing theorem only has to supply the polar slice calculation.
Formal statement
Proof (Lean source)
Helpers.AngularRadialQuantitative 6 declarations This module strengthens the exact active-tail cancellation with the localized absolute bound needed for the one-point KL estimate.
Quantitative angular radial cancellation
This module strengthens the exact active-tail cancellation with the localized absolute bound needed for the one-point KL estimate.
The one-dimensional polar success increment is bounded by the bump amplitude after multiplication by the nonnegative half-circle Jacobian.
Formal statement
Proof (Lean source)
On any measurable radial slice of an upper half-disc, the combined bump and cosine-squared success-mass increment is bounded by the bump amplitude times the slice area.
Formal statement
Proof (Lean source)
Translation of the quantitative half-disc bound to a lower-edge angular grid center in score coordinates.
Formal statement
Proof (Lean source)
For a true changed bit, the success-weighted mass difference on any radial slice is bounded by the amplitude times the area of that slice inside the changed half-disc.
Formal statement
Proof (Lean source)
The cell-area bound is dominated by the common radius marginal on the same measurable radial set.
Formal statement
Proof (Lean source)
The localized success-mass estimate holds in either orientation of the changed packing bit.
Formal statement
Proof (Lean source)
Helpers.AngularScaledDelta 11 declarations This module fixes the derivative scale used by the angular hard family and records both its exact fourth-power budget and the eventual comparison with the logarithm of the boundary-grid size.
Smoothness-normalized angular amplitude
This module fixes the derivative scale used by the angular hard family and records both its exact fourth-power budget and the eventual comparison with the logarithm of the boundary-grid size.
A fixed choice of a uniform bound for the jth derivative of the normalized packing bump.
Definition (Lean source)
The chosen normalized-bump derivative bound is nonnegative.
Formal statement
Proof (Lean source)
The chosen constant bounds the corresponding normalized-bump derivative at every score.
Formal statement
Proof (Lean source)
A fixed numerical envelope for the construction-specific one-observation radial KL estimate.
Definition (Lean source)
A positive, smoothness-dependent scale dominating all derivative bounds needed through order q, while explicitly absorbing the smoothness order and the construction-specific one-observation KL envelope.
Definition (Lean source)
The derivative scale is positive.
Formal statement
Proof (Lean source)
Every derivative bound through order q is dominated by the common smoothness-dependent scale.
Formal statement
Proof (Lean source)
The bump amplitude with its smoothness-dependent derivative normalization. It remains a fixed positive multiple of the paper's frontier rate.
Definition (Lean source)
The smoothness-normalized amplitude is an exact fixed positive multiple of the frontier rate.
Formal statement
Proof (Lean source)
The smoothness-normalized amplitude has the exact fourth-power budget needed by the one-point radial KL estimate.
Formal statement
Proof (Lean source)
Any construction-specific one-point KL constant small enough for the fixed derivative normalization eventually fits under one sixteenth of the logarithmic grid budget.
Formal statement
Proof (Lean source)
Helpers.BumpHolder 43 declarations This file isolates the compactly supported Euclidean bump used in the packing regressions.
Smooth radial bumps for the angular packing
This file isolates the compactly supported Euclidean bump used in the packing regressions. It records its range, support, smoothness, and the corresponding facts after translation and rescaling.
A fixed smooth Euclidean bump, equal to one on the ball of radius 1/2 and supported in the open unit ball.
Definition (Lean source)
The normalized radial bump used by the packing construction.
Definition (Lean source)
The normalized bump equals one at its center.
Formal statement
Proof (Lean source)
The normalized bump takes values in [0,1].
Formal statement
Proof (Lean source)
The normalized bump vanishes outside the open unit ball.
Formal statement
Proof (Lean source)
The normalized radial bump is smooth to every finite order.
Formal statement
Proof (Lean source)
The normalized packing bump depends only on Euclidean radius.
Formal statement
Proof (Lean source)
Every iterated Fréchet derivative of the normalized packing bump is uniformly bounded.
Formal statement
Proof (Lean source)
The last derivative required by an arbitrary positive Hölder order has a global Hölder modulus.
Formal statement
Proof (Lean source)
A translated bump of amplitude delta and bandwidth w.
Definition (Lean source)
A localized packing bump is the normalized radial profile evaluated at its distance from the center.
Formal statement
Proof (Lean source)
A localized bump takes its prescribed amplitude at its center.
Formal statement
Proof (Lean source)
A nonnegative localized bump is bounded by its amplitude.
Formal statement
Proof (Lean source)
A positive-bandwidth localized bump vanishes at distance at least w from its center.
Formal statement
Proof (Lean source)
Translation and nonzero rescaling preserve smoothness of the radial bump.
Formal statement
Proof (Lean source)
The small affine baseline used in every member of the hard family.
Definition (Lean source)
A slope of absolute value at most 1/2 keeps the affine baseline in [1/4,3/4] throughout the unit square.
Formal statement
Proof (Lean source)
The affine baseline is smooth to every finite order.
Formal statement
Proof (Lean source)
The regression profile obtained by adding the active disjoint radial bumps to the common affine baseline.
Definition (Lean source)
Every finite packing regression is smooth to every finite order.
Formal statement
Proof (Lean source)
Every finite packing regression is Borel measurable.
Formal statement
Proof (Lean source)
Inside one closed packing ball, the regression depends on the bit vector only through that ball's coordinate.
Formal statement
Proof (Lean source)
Away from every closed packing ball, all radial bumps vanish and the regression equals the common affine baseline.
Formal statement
Proof (Lean source)
At a separated grid center all other radial bumps vanish, so the regression value depends only on that center's bit.
Formal statement
Proof (Lean source)
The two possible regression values at a packing center are separated by exactly the bump amplitude.
Formal statement
Proof (Lean source)
The two declared regression values at a packing center, indexed by its Boolean coordinate.
Definition (Lean source)
A separated packing regression takes exactly its declared Boolean value at every grid center.
Formal statement
Proof (Lean source)
For a nonnegative bump amplitude, the two declared center values are separated by exactly that amplitude.
Formal statement
Proof (Lean source)
At the selected packing amplitude, the two center values have the exact fixed-constant frontier-rate separation used by AngularPackingAt.
Formal statement
Proof (Lean source)
At any point, a three-bandwidth-separated family of localized bumps has total active amplitude between zero and the amplitude of one bump.
Formal statement
Proof (Lean source)
With the paper's small affine slope and bump amplitude, every packing regression stays in [1/4,3/4] on the unit square.
Formal statement
Proof (Lean source)
The globally bounded version of the packing regression used to define a Markov outcome kernel. It agrees with the paper regression everywhere on the supporting square, where the latter already lies in the middle half of the unit interval.
Definition (Lean source)
The clipped packing regression takes values in the unit interval on the whole ambient score space.
Formal statement
Proof (Lean source)
Clipping does not alter a packing regression value that is already in the unit interval.
Formal statement
Proof (Lean source)
On the supporting square, the globally clipped kernel regression agrees with the paper's smooth packing regression.
Formal statement
Proof (Lean source)
Within one square-truncated packing cell, the globally clipped regression depends on a packing vertex only through that cell's Boolean coordinate.
Formal statement
Proof (Lean source)
The globally clipped packing regression is Borel measurable.
Formal statement
Proof (Lean source)
The globally clipped packing regression is continuous.
Formal statement
Proof (Lean source)
The conditional variance profile generated by a Bernoulli regression and independent unit Gaussian noise.
Definition (Lean source)
Within a packing cell, the conditional variance depends only on the same single bit as the regression.
Formal statement
Proof (Lean source)
The conditional variance profile is continuous (indeed smooth).
Formal statement
Proof (Lean source)
Under the bump envelope hypotheses, the entire conditional variance profile lies in [1,5/4] on the packing square.
Formal statement
Proof (Lean source)
For every paper envelope L ≥ 4, the preceding variance interval is contained in [L⁻¹,L].
Formal statement
Proof (Lean source)
Helpers.BumpHolderScaling 3 declarations This module records the exact iterated-Fréchet derivative formula for the translated and rescaled bump used by the angular packing.
Derivative scaling for localized packing bumps
This module records the exact iterated-Fréchet derivative formula for the
translated and rescaled bump used by the angular packing. It is kept separate
from BumpHolder so the core bump module remains focused and short.
Every iterated derivative of a localized packing bump has the expected amplitude and inverse-bandwidth scaling.
Formal statement
Proof (Lean source)
The derivative scaling formula transfers every global normalized-bump bound to a localized bump with the exact amplitude and bandwidth factors.
Formal statement
Proof (Lean source)
The top derivative of a localized bump inherits the normalized bump's Hölder modulus after translating and rescaling both arguments.
Formal statement
Proof (Lean source)
Helpers.ClassInclusion 4 declarations The common-map class embeds in the point-indexed class by taking every section equal to the common map.
Strict inclusion of distance decision classes
The common-map class embeds in the point-indexed class by taking every section equal to the common map. Strictness is witnessed by a coordinate-valued rule on the square-support product law.
Every common-map rule is a point-indexed rule with constant sections.
Formal statement
Proof (Lean source)
The point-indexed witness that returns the first coordinate of the query point, independently of the data.
Definition (Lean source)
For an admissible square-support law, the coordinate witness has measurable fixed sections but cannot be represented by one common distance map.
Formal statement
Proof (Lean source)
For every positive sample size in the stated CTY regime, the inherited common-map distance class is a proper subset of the sectionwise-Borel point-indexed class.
Formal statement
Proof (Lean source)
Helpers.CoordinateEnvelope 1 declarations This file converts uniform Fréchet-derivative bounds into the scalar coordinate-partial suprema used by the paper's Euclidean extension class.
Coordinate-partial envelope assembly
This file converts uniform Fréchet-derivative bounds into the scalar coordinate-partial suprema used by the paper's Euclidean extension class.
Uniform bounds on all required Fréchet derivatives and their Lipschitz increments imply the exact scalar coordinate-partial extension envelope.
Formal statement
Proof (Lean source)
Helpers.FiniteMaxCore 32 declarations The angular packing, marked Poisson experiment, coordinatewise direct-product bound, midpoint decoding, and de-Poissonization are assembled once here for an arbitrary point-indexed rule.
Finite-packing Poisson experiment core
The angular packing, marked Poisson experiment, coordinatewise direct-product bound, midpoint decoding, and de-Poissonization are assembled once here for an arbitrary point-indexed rule.
Equip the packing index set with the discrete measurable structure.
Definition (Lean source)
The continuous uniform mark law on (0,1] used to put every finite Poisson configuration into a canonical order.
The stated experiment law has total mass one and therefore defines a probability distribution.
Definition (Lean source)
The packing-mark distribution assigns zero probability to every individual mark.
Definition (Lean source)
The packing cells together with their common complement form the finite partition used to split the marked Poisson experiment.
Definition (Lean source)
Every packing-partition cell is measurable.
Formal statement
Proof (Lean source)
Distinct packing-partition cells are disjoint.
Formal statement
Proof (Lean source)
The packing-partition cells cover the observation space.
Formal statement
Proof (Lean source)
The classifier partition associated with the packing cells.
Definition (Lean source)
The abstract classifier has exactly the intended packing cells.
Formal statement
Proof (Lean source)
The mass of a packing cell can be read from the score marginal.
Formal statement
Proof (Lean source)
Equal positive packing-cell mass and the angular locality certificate identify the normalized within-cell observation laws.
Formal statement
Proof (Lean source)
The complete canonical marked-Poisson experiment in a packing cell is a function only of that cell's Boolean coordinate.
Formal statement
Proof (Lean source)
On laws supported by the common packing square, the abstract complement cell restriction is exactly the construction's common off-cell restriction.
Formal statement
Proof (Lean source)
A zero-intensity canonical marked-Poisson law is independent of its observation law.
Formal statement
Proof (Lean source)
The canonical marked-Poisson complement experiment is common to all vertices, including when the common complement has zero mass.
Formal statement
Proof (Lean source)
Replace the score of a marked observation by its distance from one packing center, retaining the outcome and the ordering mark.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The distance-compressed marked configuration in one packing cell.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
Reassemble, for decoder j, the marked distance configuration from its compressed own cell, the raw off-cell blocks, and the common complement.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The Poissonized point estimate computed from the compressed own cell and raw off-cell blocks, with zero fallback when fewer than n atoms arrive.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The midpoint decoder induced by a point-indexed Borel section, with zero output on the failed Poisson-count event.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
The measurable maximum of the losses at finitely many packing points.
A point-indexed rule has a measurable finite packing loss whenever its fixed sections are represented by the measurable maps in its certificate.
Formal statement
Proof (Lean source)
If the midpoint decoder for two separated values chooses the wrong bit, the corresponding estimation error is at least half their separation.
Formal statement
Proof (Lean source)
The nearest-midpoint decoder can be wrong only when the estimate is at least half the endpoint separation away from the true endpoint.
Formal statement
Proof (Lean source)
A wrong midpoint decision at one packing center forces the finite maximum loss to exceed half the certified center-value separation.
Formal statement
Proof (Lean source)
Helpers.FiniteMaxDepoisson 4 declarations This file transfers the canonical marked-Poisson maximum loss to the retained fixed-size sample and controls the failed-count event.
Retention and de-Poissonization for the finite packing maximum
This file transfers the canonical marked-Poisson maximum loss to the retained fixed-size sample and controls the failed-count event.
Mapping a canonical marked configuration to distances before taking its successful prefix is the same as taking the observation prefix first.
Formal statement
Proof (Lean source)
On the successful count event, the global Poisson loss is exactly the finite packing loss of the retained fixed-size sample.
Formal statement
Proof (Lean source)
The count of a canonical marked-Poisson configuration is Poisson.
Formal statement
Proof (Lean source)
The Poissonized risk is at most the retained fixed-size risk plus the failed-count probability times a uniform zero-default bound.
Formal statement
Proof (Lean source)
Helpers.FiniteMaxExperiment 21 declarations This file identifies the hard-family marked Poisson law with the common complement block and independent coordinate-cell blocks used by the coordinatewise direct-product theorem.
The finite angular marked-Poisson experiment
This file identifies the hard-family marked Poisson law with the common complement block and independent coordinate-cell blocks used by the coordinatewise direct-product theorem.
Equip the packing-experiment index set with the discrete measurable structure.
Definition (Lean source)
Every singleton packing-experiment index is measurable.
Formal statement
Proof (Lean source)
A canonical vertex whose only potentially nonzero coordinate is j.
Definition (Lean source)
Activating the selected packing coordinate sets that coordinate to its prescribed bit.
Formal statement
Proof (Lean source)
The canonical marked-Poisson experiment for coordinate j and bit b.
Definition (Lean source)
The stated experiment law has total mass one and therefore defines a probability distribution.
Definition (Lean source)
The common complement block, represented at the all-false vertex.
Definition (Lean source)
The stated experiment law has total mass one and therefore defines a probability distribution.
Definition (Lean source)
Put the common block and coordinate blocks back into the sum-indexed family and superpose them in increasing mark order.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
Pointwise measurable mapping commutes with a finite Poisson sample law.
Formal statement
Proof (Lean source)
Mapping only the observation coordinate commutes with a finite marked Poisson sample law.
Formal statement
Proof (Lean source)
The two-cell partition of outcome-distance space into radii at most w and radii larger than w.
Definition (Lean source)
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Formal statement
Proof (Lean source)
The canonically ordered short-radius block is a measurable image of the full raw marked-Poisson outcome-distance experiment.
Formal statement
Proof (Lean source)
For a law supported by the packing square, mapping its restriction to a packing cell into outcome-distance coordinates gives the corresponding short-radius restriction of the one-point distance law.
Formal statement
Proof (Lean source)
Mapping a marked configuration pointwise without changing its marks commutes definitionally with canonical mark ordering.
Formal statement
Proof (Lean source)
Normalising a positive packing-cell restriction and then mapping to outcome-distance coordinates gives the normalised short-radius law.
Formal statement
Proof (Lean source)
A compressed canonical cell experiment is the canonical short-radius block of the full one-point outcome-distance marked-Poisson experiment.
Formal statement
Proof (Lean source)
The compressed cell KL budget is at most twice the fixed-size packing budget, exactly the factor introduced by mean-2n Poissonization.
Formal statement
Proof (Lean source)
Splitting the hard-family Poisson law gives the direct-product experiment with one common complement coordinate and one bit-dependent law per cell.
Formal statement
Proof (Lean source)
Helpers.FiniteMaxLowerBound 1 declarations This module assembles the angular packing, marked Poisson direct-product experiment, midpoint loss conversion, and de-Poissonization.
Shared finite-packing maximum lower bound
This module assembles the angular packing, marked Poisson direct-product experiment, midpoint loss conversion, and de-Poissonization.
Uniformly over point-indexed rules and all sufficiently large n, one law from the angular hard family makes the measurable finite packing maximum at least a positive constant times the frontier rate.
Formal statement
Proof (Lean source)
Helpers.FiniteMaxRisk 12 declarations This file converts the coordinatewise direct-product testing error into a finite-coordinate Poissonized loss and then back into the retained fixed-size sample loss.
Direct-product error and finite packing risk
This file converts the coordinatewise direct-product testing error into a finite-coordinate Poissonized loss and then back into the retained fixed-size sample loss.
The Poissonized value at one center as a function of the synthesized canonical global marked configuration.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The average probability that at least one coordinate decoder is wrong.
Definition (Lean source)
For measurable decoders, average simultaneous error is exactly one minus average simultaneous success.
Formal statement
Proof (Lean source)
The angular cell experiment inherits the finite direct-product lower bound after midpoint decoding.
Formal statement
Proof (Lean source)
Reassembling the distance-compressed own cell with the other raw cells is the same as mapping the synthesized global configuration.
Formal statement
Proof (Lean source)
Maximum Poissonized center loss on a global marked configuration.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The corresponding loss on the independent common/cell blocks.
Definition (Lean source)
The stated statistic is a measurable function of the observed data, so it is a valid random quantity.
Formal statement
Proof (Lean source)
The two stated constructions agree under the theorem's assumptions.
Formal statement
Proof (Lean source)
Averaging the direct-product decoder error selects one Boolean vertex whose canonical marked-Poisson maximum loss is at least separation/2 times the average error probability.
Formal statement
Proof (Lean source)
Helpers.Poissonization 10 declarations This file specializes the shared finite-sample and de-Poissonization substrate to the accepted run’s observation law and frontier rate.
Run-specific Poissonization specializations
This file specializes the shared finite-sample and de-Poissonization substrate to the accepted run’s observation law and frontier rate.
This declaration establishes the displayed property of the stated causal construction under its listed assumptions.
Definition (Lean source)
The infinite i.i.d. observation stream is a probability law.
Definition (Lean source)
Every finite prefix of the infinite i.i.d. stream has the original product sample law.
Formal statement
Proof (Lean source)
A mean-2n count paired with an independent infinite i.i.d. observation stream. The first n stream coordinates implement the retained sample on the successful-count event.
Definition (Lean source)
The independent Poisson-count and i.i.d.-stream pairing is a probability law.
Definition (Lean source)
The count coordinate of the stream construction is Poisson with mean 2n.
Formal statement
Proof (Lean source)
Taking the first n observations from the stream construction gives exactly the original i.i.d. sample law.
Formal statement
Proof (Lean source)
A coupling of a mean-2n Poisson count with an exactly i.i.d. retained sample of size n.
Definition (Lean source)
The marked mean-2n experiment can retain the n smallest marks and hence couple back to an exact P^n sample.
Formal statement
Proof (Lean source)
Read the first n observations from a configuration that is already in canonical mark order, forgetting the marks.
Formal statement
Proof (Lean source)
Helpers.SquareBoundary 12 declarations This file gives an explicit piecewise-linear traversal of the boundary of the unit square and proves the Lipschitz and image properties needed by the CTY law class.
Rectifiable boundary of the packing square
This file gives an explicit piecewise-linear traversal of the boundary of the unit square and proves the Lipschitz and image properties needed by the CTY law class.
The horizontal coordinate of the counterclockwise square-boundary path.
Definition (Lean source)
The vertical coordinate of the counterclockwise square-boundary path.
Definition (Lean source)
An explicit traversal of the four edges of the unit square.
Definition (Lean source)
Both scalar coordinates of the square-boundary path are globally 4-Lipschitz.
Formal statement
Proof (Lean source)
The explicit square-boundary traversal is globally Lipschitz.
Formal statement
Proof (Lean source)
A point is on the frontier of the unit square exactly when both coordinates are bounded by 1/2 and at least one coordinate is extremal.
Formal statement
Proof (Lean source)
The second quarter of the path parametrizes the right edge.
Formal statement
Proof (Lean source)
The fourth quarter of the path parametrizes the left edge.
Formal statement
Proof (Lean source)
The third quarter of the path parametrizes the top edge.
Formal statement
Proof (Lean source)
The first quarter of the path parametrizes the bottom edge.
Formal statement
Proof (Lean source)
The explicit path has exactly the frontier of the unit square as its image on the unit interval.
Formal statement
Proof (Lean source)
The boundary of the packing square is rectifiable, witnessed by the explicit eight-Lipschitz traversal above.
Formal statement
Proof (Lean source)
T1_SameClassLogConverse 1 declarations The inherited common-map result uses the same finite-packing maximum as the point-indexed theorem.
CTY common-map same-class logarithmic converse
The inherited common-map result uses the same finite-packing maximum as the point-indexed theorem. Its identification of completed expectation with outer expectation uses Causalean's universal measurability of analytic sets.
The inherited CTY common-map minimax risk has a positive normalized liminf at the logarithmic distance rate on the same nonparametric law class.
Formal statement
Proof (Lean source)
T2_PointIndexedLogConverse 2 declarations The headline theorem lower-bounds outer-expectation risk over the exact CTY law class while permitting arbitrary law-independent point-indexed families whose fixed-point sections are Borel measurable.
Point-indexed logarithmic converse
The headline theorem lower-bounds outer-expectation risk over the exact CTY law class while permitting arbitrary law-independent point-indexed families whose fixed-point sections are Borel measurable. No joint regularity in the point is assumed.
The finite angular packing gives an eventual positive multiple of the frontier rate uniformly over all point-indexed rules.
Formal statement
Proof (Lean source)
For every q ≥ 1 and L ≥ 4, the point-indexed outer-expectation minimax risk has a positive normalized liminf at the logarithmic distance rate.