Formalization: Outcome-free Records and the Minimax Precision of Conditional Treatment Effect Estimation
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs. Note: this index was generated at a different commit than the paper's audited pin (44d8edc) — statements may have moved since the audit.
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Basic 60 declarations Two-channel point-CATE annotation frontier: Basic constructions and obligations.
Basic
Two-channel point-CATE annotation frontier: Basic constructions and obligations.
Euclidean covariates, with coordinatewise cube support. Given the specified input d, cov is the corresponding construction.
Definition (Lean source)
Closed design cube. Given the specified input d, cube is the corresponding construction.
Definition (Lean source)
Given the specified input d, x0 is the corresponding construction.
Definition (Lean source)
Given the specified input d, uniform law is the corresponding construction.
Definition (Lean source)
Given the specified input d, full record is the corresponding construction.
Given the specified input a, bit is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input w, observed is the corresponding construction.
Definition (Lean source)
Given the specified input p, bern is the corresponding construction.
Given the specified input p, the specified input hp, the measurable bern conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input p, the specified input hp, bern kernel is the corresponding construction.
Definition (Lean source)
A probability law with raw measurable conditional versions. Class membership below quantifies over admissible replacements with the same underlying measure.
Definition (Lean source)
Given the specified input d, the specified input P, obs law is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input P, xa law is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input P, the specified input x, raw contrast is the corresponding construction.
Definition (Lean source)
The public parameter domain: the covariate dimension d is at least one, the propensity smoothness alpha and the control-mean smoothness beta lie in (0, 1], the effect smoothness gamma lies in [1, 3], the Hölder radius L exceeds one half, and the overlap level eps lies strictly between 0 and one half. All constants in the results may depend on these parameters.
Definition (Lean source)
multi order is the corresponding construction.
Definition (Lean source)
Given the specified input k, coordinate directions is the corresponding construction.
Given the specified input f, the specified input x, coordinate partial is the corresponding construction.
Definition (Lean source)
Exact coordinate-partial Hölder norm, infinite when the required continuous derivatives do not exist. Given the specified input f, the specified input s, holder norm is the corresponding construction.
Definition (Lean source)
Given the specified input f, the specified input s, the specified input L, the specified input hL, the holder norm le iff conclusion holds.
Formal statement
Proof (Lean source)
The cube has a nonempty open interior, so within-cube derivatives are unique. Given the specified input d, the unique diff on cube conclusion holds.
Formal statement
Proof (Lean source)
Coordinate partials of smooth functions add on the closed cube. Given the specified input f, the specified input g, the specified input N, the specified input hf, the specified input hg, the multi-index, its order bound, the specified input x, the specified input hx, the coordinate partial add conclusion holds.
Formal statement
Proof (Lean source)
The exact extended Hölder norm obeys the triangle inequality. Given the specified input f, the specified input g, the specified input s, the holder norm add le conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input P, uniform design is the corresponding construction.
Definition (Lean source)
Given the specified input P, conditional exchangeability is the corresponding construction.
Definition (Lean source)
The overlap condition at level eps: the overlap level eps is positive and, on the design cube, the law P has a propensity between eps and 1 − eps.
Definition (Lean source)
Under overlap at the overlap level eps, the propensity of the law P is a probability on the design cube.
Formal statement
Proof (Lean source)
Witness-level propensity smoothness, applied by PrimitiveClass to its admissible W. Given the specified input alpha, the specified input L, the specified input W, propensity holder is the corresponding construction.
Definition (Lean source)
Witness-level control-mean smoothness, applied by PrimitiveClass to its admissible W. Given the specified input beta, the specified input L, the specified input W, control holder is the corresponding construction.
Definition (Lean source)
Witness-level effect smoothness. After W is selected, rawContrast W agrees with the canonical tau on the cube. Given the specified input gamma, the specified input L, the specified input W, effect holder is the corresponding construction.
Definition (Lean source)
The control-arm mean range condition: on the design cube, the admissible version W has a control mean that is a probability, between 0 and 1.
Definition (Lean source)
The treated-arm mean range condition: on the design cube, the admissible version W has a treated mean that is a probability, between 0 and 1.
Definition (Lean source)
Membership is existential over conditional-margin witnesses of the underlying law. The carrier's raw versions do not enter this predicate.
Definition (Lean source)
Designated admissible versions are selected from membership, never from the raw carrier. Given the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, canonical law is the corresponding construction.
Definition (Lean source)
Given the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the canonical law spec conclusion holds.
Formal statement
Proof (Lean source)
For a law P in the model class, the overlap level eps is positive.
Formal statement
Proof (Lean source)
For a law P in the model class, the overlap level eps is at most one half, since the propensity at the cube centre lies between eps and 1 − eps.
Formal statement
Proof (Lean source)
The supplied propensity and arm means are admissible conditional-margin witnesses. Given the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, designated propensity is the corresponding construction.
Definition (Lean source)
Given the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, designated control is the corresponding construction.
Definition (Lean source)
Given the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, designated treated is the corresponding construction.
Definition (Lean source)
Canonical continuous contrast on the cube, obtained from admissible witnesses. Given the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input x, tau is the corresponding construction.
Definition (Lean source)
The closed cube has dense interior, including in dimension zero. Given the specified input d, the cube subset closure interior conclusion holds.
Proof (Lean source)
Uniform-design almost-everywhere equality determines continuous versions on the cube. Given the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input hfg, the uniform law continuous versions conclusion holds.
Formal statement
Proof (Lean source)
Finite Hölder norm supplies continuity on the entire closed cube. Given the specified input f, the specified input s, the specified input L, the specified input h, the holder norm continuous on conclusion holds.
Formal statement
Proof (Lean source)
Clamp a raw version only outside its probability range. Given the specified input p, version clip is the corresponding construction.
Given the specified input p, the version clip mem conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input p, the specified input hp, the version clip eq conclusion holds.
Formal statement
Proof (Lean source)
the measurable version clip conclusion holds.
Formal statement
Proof (Lean source)
Clipped Bernoulli kernels are Markov kernels even when raw versions are unbounded. Given the specified input f, the specified input hf, the bern kernel version clip markov conclusion holds.
Formal statement
Proof (Lean source)
A probability marginal rules out the zero fallback in composition-product. Given the specified input P, the specified input j, the specified input hj, the specified input f, the specified input hf, the specified input hm, the bern kernel sfinite of margin conclusion holds.
Formal statement
Proof (Lean source)
Conditional Bernoulli margins identify admissible continuous probability versions. Given the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input hfcont, the specified input hgcont, the specified input hfprob, the specified input hgprob, the specified input hm, the bern margin versions unique conclusion holds.
Formal statement
Proof (Lean source)
Full support of the uniform design and continuity make admissible versions unique on the closed cube, including its boundary. Given the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input Q, the specified input hP, the specified input hQ, the specified input hlaw, the admissible versions unique conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, big delta is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input gamma, s crit is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, q star is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input gamma, the specified input n, oracle rate is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input n, the specified input m, upper rate is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input n, the specified input m, sharp rate is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input n, the specified input m, the sharp rate eq upper rate conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input zeta, annotation region is the corresponding construction.
Definition (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Estimator 23 declarations Two-channel point-CATE annotation frontier: Estimator constructions and obligations.
Estimator
Two-channel point-CATE annotation frontier: Estimator constructions and obligations.
Given the specified input D, treatment records is the corresponding construction.
Given the specified input n, outcome count is the corresponding construction.
Definition (Lean source)
Given the specified input n, the specified input m, treatment count is the corresponding construction.
Definition (Lean source)
Given the specified input n, the specified input m, role split is the corresponding construction.
Given the specified input D, the specified input h, the specified input J, the specified input x, eta hat is the corresponding construction.
Given the specified input D, the specified input h, the specified input J, the specified input u, r hat is the corresponding construction.
Definition (Lean source)
Given the specified input D, the specified input h, the specified input J, the specified input u, the specified input v, q raw is the corresponding construction.
Definition (Lean source)
Given the specified input D, the specified input h, the specified input J, q hat is the corresponding construction.
Given the specified input D, the specified input h, the specified input J, rect moments is the corresponding construction.
Given the specified input P, the specified input n, the specified input m, the specified input h, the specified input J, q pop is the corresponding construction.
Definition (Lean source)
Given the specified input P, the specified input n, the specified input m, the specified input h, the specified input J, the specified input u, r bar is the corresponding construction.
Definition (Lean source)
Given the specified input D, the specified input h, the specified input J, the specified input u, the r hat rectangular conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input Q, lambda min is the corresponding construction.
Clipping to the effect range: a real number x is truncated to the interval from −1 to 1, the range of a difference of two probabilities.
The Gram guard level for the overlap level eps: half of eps·(1 − eps), the smallest value of e·(1 − e) when the propensity e lies between eps and 1 − eps.
Definition (Lean source)
For an overlap level eps that is positive and below one, the Gram guard level is positive.
Formal statement
Proof (Lean source)
Under the public parameter domain, the Gram guard level is positive for the overlap level eps.
Formal statement
Proof (Lean source)
Given the overlap level eps, the specified input h, the specified input J, the specified input D, t hat is the corresponding construction: the clipped local-polynomial estimate when the smallest Rayleigh quotient of the empirical Gram matrix is at least the Gram guard level of eps, and zero otherwise.
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input n, the specified input m, h star is the corresponding construction.
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input n, the specified input m, j star is the corresponding construction.
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input n, the specified input m, the specified input D, the overlap level eps, t up is the corresponding construction.
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input n, the specified input m, the specified input w, the overlap level eps, sharp decision is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input n, the specified input m, the overlap level eps, frontier handle is the corresponding construction.
Definition (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Experiment 10 declarations Two-channel point-CATE annotation frontier: Experiment constructions and obligations.
Experiment
Two-channel point-CATE annotation frontier: Experiment constructions and obligations.
Given the specified input d, the specified input n, the specified input m, dataset is the corresponding construction.
Given the specified input d, the specified input n, the specified input m, sample is the corresponding construction.
Definition (Lean source)
Given the specified input P, the specified input n, the specified input m, experiment is the corresponding construction.
Given the specified input d, the specified input n, the specified input m, decision is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input n, the specified input m, oracle decision is the corresponding construction.
Definition (Lean source)
Given the specified input P, the specified input n, the specified input m, sample law is the corresponding construction.
Definition (Lean source)
Given the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input T, the specified input P, the specified input hP, risk is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input n, the specified input m, the specified input T, the specified input P, class risk is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input n, the specified input m, minimax risk is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input n, the specified input m, oracle risk is the corresponding construction.
Definition (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.AnnotationImprovement 5 declarations The supervised-normalized frontier is a maximum of a vanishing oracle power and a negative power of the total-to-labeled count ratio.
Strict annotation improvement
The supervised-normalized frontier is a maximum of a vanishing oracle power and a negative power of the total-to-labeled count ratio.
A negative power of an eventually positive sequence vanishes exactly when it diverges. Given the specified input f, the specified input a, the specified input ha, the specified input hf, the annotation negative power zero iff conclusion holds.
Formal statement
Proof (Lean source)
In the rough regime the normalized frontier is exactly the two powers in the roadmap. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input hs, the specified input n, the specified input m, the specified input hn, the annotation supervised ratio formula conclusion holds.
Formal statement
Proof (Lean source)
The oracle-to-supervised decay exponent is positive precisely in the rough regime. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input hs, the annotation improvement exponent pos conclusion holds.
Formal statement
Proof (Lean source)
The total-to-labeled ratio diverges exactly when the auxiliary-to-labeled ratio does. Given the specified input mseq, the annotation total ratio at top iff conclusion holds.
Formal statement
Proof (Lean source)
Strict numerical improvement requires rough smoothness and a divergent auxiliary ratio. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input mseq, the annotation rate improvement iff conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.AnnotationLiminf 3 declarations The exact annotation threshold converts eventual oracle-order attainment into an eventual positive lower bound on the normalized total sample count.
Oracle attainment and positive liminf
The exact annotation threshold converts eventual oracle-order attainment into an eventual positive lower bound on the normalized total sample count.
A positive extended-real liminf is equivalent to an eventual positive real lower bound. Given the specified input f, the of real liminf pos iff conclusion holds.
Formal statement
Proof (Lean source)
The annotation region is exactly a lower threshold on the normalized total count. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input n, the specified input m, the specified input hn, the specified input zeta, the specified input hz, the annotation region count iff conclusion holds.
Formal statement
Proof (Lean source)
Some finite oracle tolerance is equivalent to a positive normalized-count liminf. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input mseq, the annotation region liminf iff conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.CitedGates 3 declarations Two-channel point-CATE annotation frontier: Helpers/CitedGates constructions and obligations.
Helpers/CitedGates
Two-channel point-CATE annotation frontier: Helpers/CitedGates constructions and obligations.
Kennedy, Balakrishnan, Robins and Wasserman (2024), Section 3, Lemma 1, absolute-loss specialization; citation handle cite:kennedybalakrishnanrobinswasserman2024-lemma1. Source: https://arxiv.org/html/2203.00837v4#Thmlemma1. This follows from the sharp absolute fuzzy-testing bound, applied to the two kernel ranges inside the ambient model. the published fuzzy testing conclusion holds.
Formal statement
Proof (Lean source)
The numerical rate and smoothness split displayed in the published point-CATE benchmark. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input n, kbrw benchmark rate is the corresponding construction.
Definition (Lean source)
Kennedy, Balakrishnan, Robins and Wasserman (2024), Section 3, Theorem 1: only the numerical exponents and smoothness cutoff at nuisance-average smoothness. Citation handle cite:kennedybalakrishnanrobinswasserman2024-theorem1; source https://arxiv.org/html/2203.00837v4#Thmtheorem1. This disclosed logical input asserts no source-model risk guarantee or minimax transfer. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, published cate benchmark is the corresponding construction.
Definition (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.Hellinger 16 declarations Two-channel point-CATE annotation frontier: Helpers/Hellinger constructions and obligations.
Helpers/Hellinger
Two-channel point-CATE annotation frontier: Helpers/Hellinger constructions and obligations.
Given the specified input B, the specified input C, hellinger sq is the corresponding construction.
Definition (Lean source)
A common s-finite reference kernel with jointly measurable conditional densities. Given the specified input Z, the specified input B, the specified input C, has conditional densities is the corresponding construction.
Square-root differences are homogeneous of degree one in their densities. Given the specified input a, the specified input b, the specified input c, the specified input ha, the specified input hb, the specified input hc, the sqrt difference square mul conclusion holds.
Formal statement
Proof (Lean source)
The sum-of-laws definition agrees with any finite dominating reference measure. Given the specified input B, the specified input C, the specified input hB, the specified input hC, the hellinger sq eq density conclusion holds.
Formal statement
Proof (Lean source)
Products of integrable nonnegative densities represent products of their laws. Given the specified input E, the specified input B, the specified input f, the specified input hf, the specified input hf0, the specified input hB, the pi real density conclusion holds.
Formal statement
Proof (Lean source)
A finite absolutely continuous law has its real Radon--Nikodym density. Given the specified input B, the specified input hB, the real rn deriv density conclusion holds.
Formal statement
Proof (Lean source)
Explicit densities can be used in the sum-of-laws Hellinger definition. Given the specified input B, the specified input C, the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input hf0, the specified input hg0, the specified input hB, the specified input hC, the hellinger sq real density conclusion holds.
Formal statement
Proof (Lean source)
Affinity of two normalized nonnegative densities lies in the unit interval. Given the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input hf0, the specified input hg0, the specified input hf1, the specified input hg1, the density affinity mem unit conclusion holds.
Formal statement
Proof (Lean source)
Squared Hellinger distance subadditivity for finite products of probability laws. Given the specified input E, the specified input B, the specified input C, the hellinger sq pi le sum conclusion holds.
Formal statement
Proof (Lean source)
Normalizing two measurable densities against their sum gives a bounded density. Given the specified input a, the specified input b, the density ratio le one conclusion holds.
Formal statement
Proof (Lean source)
A law's density against the sum of two laws is the normalized original density. Given the specified input B, the specified input C, the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input hB, the specified input hC, the with density density ratio conclusion holds.
Formal statement
Proof (Lean source)
Measurable densities bounded by one have integrable squared square-root differences. Given the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input hf0, the specified input hg0, the specified input hf1, the specified input hg1, the integrable sqrt difference bounded conclusion holds.
Formal statement
Proof (Lean source)
Joint laws with a common marginal have the average conditional squared Hellinger distance. Given the specified input Z, the specified input B, the specified input C, the specified input hBC, the hellinger sq comp prod common conclusion holds.
Formal statement
Proof (Lean source)
Appending a common finite measure multiplies squared Hellinger distance by its mass. Given the specified input Z, the specified input B, the specified input C, the specified input G, the hellinger sq prod common conclusion holds.
Formal statement
Proof (Lean source)
A common independent probability factor preserves squared Hellinger distance. Given the specified input Z, the specified input B, the specified input C, the specified input G, the hellinger sq prod probability conclusion holds.
Formal statement
Proof (Lean source)
the hellinger block calculus conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.HolderAlgebra 4 declarations Algebraic bounds for the exact coordinate Hölder norm used by the marked priors.
Algebraic bounds for the exact coordinate Hölder norm used by the marked priors.
Scalar multiplication commutes with each continuous coordinate partial on the cube. Given the specified input f, the specified input a, the specified input N, the specified input hf, the multi-index, its order bound, the specified input x, the specified input hx, the coordinate partial const mul conclusion holds.
Formal statement
Proof (Lean source)
A finite Hölder bound scales by the absolute value of a scalar. Given the specified input f, the specified input s, the specified input A, the specified input a, the specified input hA, the specified input hf, the holder norm const mul bound conclusion holds.
Formal statement
Proof (Lean source)
Constant functions have Hölder norm at most their absolute value, at every order. Given the specified input c, the specified input s, the holder norm const bound conclusion holds.
Formal statement
Proof (Lean source)
Adding two finite Hölder bounds adds their radii. Given the specified input f, the specified input g, the specified input s, the specified input A, the specified input B, the specified input hA, the specified input hB, the specified input hf, the specified input hg, the holder norm add bound conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.IndependentExchangeability 2 declarations Conditional exchangeability for the explicit independent Bernoulli extension.
Conditional exchangeability for the explicit independent Bernoulli extension.
For Borel success-probability functions p and q, the two potential-outcome Bernoulli kernels are Borel jointly.
Formal statement
Proof (Lean source)
The independent construction satisfies conditional exchangeability with its explicit product kernel for the two potential outcomes. Given the specified input d, the specified input e, the specified input p, the specified input q, the specified input he, the specified input hp, the specified input hq, the independent primitive exchangeability conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.LocalPolynomial 1 declarations Two-channel point-CATE annotation frontier: Helpers/LocalPolynomial constructions and obligations.
Helpers/LocalPolynomial
Two-channel point-CATE annotation frontier: Helpers/LocalPolynomial constructions and obligations.
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the local polynomial projection facts conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.LocalPolynomial.Basis 10 declarations Two-channel point-CATE annotation frontier: Helpers/LocalPolynomial/Basis constructions and obligations.
Helpers/LocalPolynomial/Basis
Two-channel point-CATE annotation frontier: Helpers/LocalPolynomial/Basis constructions and obligations.
Each of the three prescribed Legendre formulas is uniformly bounded on the reference interval. Given the specified input k, the specified input u, the specified input hu, the legendre abs le four conclusion holds.
Formal statement
Proof (Lean source)
Scaling an admissible coarse window preserves the reference-interval bound. Given the specified input d, the specified input h, the specified input hh, the specified input x, the specified input hx, the specified input u, the coarse basis abs bound conclusion holds.
Formal statement
Proof (Lean source)
The finite coarse vector has a bound depending only on the public dimension. Given the specified input d, the specified input h, the specified input hh, the specified input x, the specified input hx, the coarse basis vector bound conclusion holds.
Formal statement
Proof (Lean source)
Expanding a finite orthonormal kernel gives its rank as the squared product-space norm. Given the specified input b, the specified input hb, the specified input ho, the finite orthonormal kernel square conclusion holds.
Formal statement
Proof (Lean source)
The prescribed fine kernel has squared integral equal to its finite rank. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the fine kernel square integral conclusion holds.
Formal statement
Proof (Lean source)
The assigned half-open cells are disjoint, including their last closed face. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input x, the specified input z, the specified input w, the specified input hz, the specified input hw, the cell index unique conclusion holds.
Formal statement
Proof (Lean source)
Fine coordinates lie in the same reference interval after centering in their cell. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input x, the specified input u, the fine basis abs bound conclusion holds.
Formal statement
Proof (Lean source)
Orthonormality of the cell's constant entry normalizes the absolute basis integral. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input u, the fine basis abs integral bound conclusion holds.
Formal statement
Proof (Lean source)
Only one cell contributes to a kernel row; its normalization cancels the grid scale. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input x, the fine kernel abs row bound conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the kernel basis bounds conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.LocalPolynomial.CellPolynomial 5 declarations Affine changes of the degree-two Legendre basis preserve total degree.
# Polynomial copies on fine cells Affine changes of the degree-two Legendre basis preserve total degree. Thus cellwise scalar multiples of coarse polynomials belong to the fine space.
Triangular coefficients for a one-dimensional affine Legendre change. Given the specified input k, the specified input j, the specified input a, the specified input b, legendre affine coeff is the corresponding construction.
Definition (Lean source)
An affine substitution in a Legendre entry uses only lower degrees. Given the specified input k, the specified input hk, the specified input a, the specified input b, the specified input t, the legendre affine expansion conclusion holds.
Formal statement
Proof (Lean source)
The change-of-basis matrix is triangular. Given the specified input k, the specified input j, the specified input hk, the specified input hj, the specified input a, the specified input b, the legendre affine coeff above conclusion holds.
Formal statement
Proof (Lean source)
The tensor expansion keeps only multiindices of total degree at most two. Given the specified input d, the specified input u, the specified input a, the specified input b, the specified input t, the legendre tensor affine expansion conclusion holds.
Formal statement
Proof (Lean source)
A separate scalar on each cell times a coarse entry is a fine-basis expansion. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input u, the specified input c, the cellwise coarse expansion conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.LocalPolynomial.Residual 1 declarations Two-channel point-CATE annotation frontier: Helpers/LocalPolynomial/Residual constructions and obligations.
Helpers/LocalPolynomial/Residual
Two-channel point-CATE annotation frontier: Helpers/LocalPolynomial/Residual constructions and obligations.
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the residual projection bounds conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.LocalPolynomial.ResidualControl 9 declarations Cell coverage, cell geometry, and the orthogonal best-approximation inequality used for the control-regression residual in the local polynomial roadmap.
# Cellwise control-regression approximation Cell coverage, cell geometry, and the orthogonal best-approximation inequality used for the control-regression residual in the local polynomial roadmap.
The prescribed face assignments cover every point of the localization box. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input x, the specified input hx, the localization cell cover conclusion holds.
Formal statement
Proof (Lean source)
Points in the same cell are separated by at most its side times √d. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input z, the specified input x, the specified input y, the specified input hx, the specified input hy, the cell distance bound conclusion holds.
Formal statement
Proof (Lean source)
Subtracting any fine-basis expansion leaves the same orthogonal residual. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input f, the specified input hf, the specified input v, the projection best approximation conclusion holds.
Formal statement
Proof (Lean source)
Coarse constant orthonormality normalizes the localization measure. Given the specified input d, the specified input h, the specified input hh, the specified input hh', the localization probability conclusion holds.
Formal statement
Proof (Lean source)
Every cell centre belongs to its assigned cell. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input z, the cell center mem conclusion holds.
Formal statement
Proof (Lean source)
A bounded measurable Hölder function is approximated by cellwise constants with the precise fine-scale exponent in the paper's roadmap. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input f, the specified input hf, the specified input B, the specified input K, the specified input s, the specified input hK, the specified input hs, the specified input hB, the specified input hmod, the holder control projection residual conclusion holds.
Formal statement
Proof (Lean source)
For a primitive law P in the model class at overlap level eps, the designated control regression is globally Borel.
Formal statement
Proof (Lean source)
At exponents at most one, the frozen Hölder norm gives the function's modulus. Given the specified input d, the specified input f, the specified input s, the specified input L, the specified input hs, the specified input hs', the specified input hL, the specified input hf, the specified input x, the specified input y, the specified input hx, the specified input hy, the holder norm low order modulus conclusion holds.
Formal statement
Proof (Lean source)
The control-regression half of the residual estimates is fully derived from class membership and the prescribed cellwise constant construction. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the control projection bounds conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.LocalPolynomial.ResidualPropensity 2 declarations The cell-center propensity approximant retains the entire coarse polynomial.
# Propensity times coarse-polynomial residual The cell-center propensity approximant retains the entire coarse polynomial. Hölder continuity and orthogonal best approximation give the fine-scale bound for every coarse basis entry.
Multiplication by a coarse entry preserves the cell-center approximation rate. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input f, the specified input hf, the specified input B, the specified input K, the specified input s, the specified input hK, the specified input hs, the specified input hB, the specified input hmod, the specified input u, the holder propensity projection residual conclusion holds.
Formal statement
Proof (Lean source)
Class membership supplies the propensity residual bound uniformly in the coarse entry. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the propensity projection bounds conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.LocalPolynomial.Taylor 11 declarations Two-channel point-CATE annotation frontier: Helpers/LocalPolynomial/Taylor constructions and obligations.
Helpers/LocalPolynomial/Taylor
Two-channel point-CATE annotation frontier: Helpers/LocalPolynomial/Taylor constructions and obligations.
The zero multi-index evaluates the zeroth within-cube derivative. Given the specified input d, the specified input f, the specified input x, the coordinate partial zero index conclusion holds.
Formal statement
Proof (Lean source)
The centre belongs to the design cube in every dimension. Given the specified input d, the x0 mem cube conclusion holds.
Formal statement
Proof (Lean source)
The canonical contrast agrees with its admissible raw version on the cube. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input x, the specified input hx, the tau eq canonical contrast conclusion holds.
Formal statement
Proof (Lean source)
A first-order Hölder norm bounds the contrast's Lipschitz modulus on the cube. Given the specified input d, the specified input alpha, the specified input beta, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input hL, the specified input x, the specified input y, the specified input hx, the specified input hy, the tau lipschitz gamma one conclusion holds.
Formal statement
Proof (Lean source)
A localization window has radius at most its side times the square root of dimension. Given the specified input d, the specified input h, the specified input hh, the specified input x, the specified input hx, the loc cube distance center bound conclusion holds.
Formal statement
Proof (Lean source)
The only multi-index of total order zero is the zero index. Given the specified input d, the poly idx order zero iff conclusion holds.
Formal statement
Proof (Lean source)
The degree-zero Taylor polynomial is the function's value at the centre. Given the specified input d, the specified input f, the specified input x, the taylor poly zero degree conclusion holds.
Formal statement
Proof (Lean source)
A single constant-basis coefficient represents a constant polynomial. Given the specified input d, the specified input h, the specified input c, the specified input x, the pv constant coefficient conclusion holds.
Formal statement
Proof (Lean source)
At smoothness one, the prescribed Taylor construction is the constant centre value. Given the specified input d, the specified input alpha, the specified input beta, the specified input L, the overlap level eps, the specified input hdom, the taylor coefficient bounds gamma one conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the taylor coefficient bounds conclusion holds.
Formal statement
Proof (Lean source)
Taylor approximation and center reproduction on every oracle window contained in the design cube. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the oracle taylor approximation conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.OracleMean 11 declarations Bounded inverse-propensity tests identify the conditional effect, and uniform design transports the oracle evaluation kernel to its local projection mean.
# Oracle response identification Bounded inverse-propensity tests identify the conditional effect, and uniform design transports the oracle evaluation kernel to its local projection mean.
Overlap bounds both inverse-propensity test functions on their cube support. Given the specified input d, the specified input P, the specified input he, the specified input f, the specified input B, the specified input hB, the specified input hf, the specified input hs, the overlap level eps, the oracle inverse test bound conclusion holds.
Formal statement
Proof (Lean source)
The supplied inverse-propensity response has effect mean against every bounded cube-supported Borel test, by cancellation in the two identified arm moments. Given the specified input d, the specified input P, the specified input hdesign, the specified input hex, the specified input he, the specified input hm0, the specified input hm1, the specified input f, the specified input hf, the specified input B, the specified input hB, the specified input hfB, the specified input hs, the overlap level eps, the oracle response test mean conclusion holds.
Formal statement
Proof (Lean source)
The oracle kernel's record expectation is the known-design local projection of the canonical effect, throughout the full admissible oracle bandwidth range. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh, the specified input hh', the oracle summand mean conclusion holds.
Formal statement
Proof (Lean source)
Full-window coarse orthonormality normalizes the oracle localization law. Given the specified input d, the specified input h, the specified input hh, the oracle localization probability conclusion holds.
Formal statement
Proof (Lean source)
The oracle evaluation kernel reproduces every coarse polynomial at the target. Given the specified input d, the specified input h, the specified input hh, the specified input theta, the oracle polynomial reproduction conclusion holds.
Formal statement
Proof (Lean source)
Polynomial reproduction converts a uniform approximation remainder into an oracle mean bias bound, with the explicit finite-dimensional kernel constant. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh, the specified input theta, the specified input B, the specified input hB, the specified input herr, the specified input htarget, the oracle projection bias bound conclusion holds.
Formal statement
Proof (Lean source)
Averaging all labeled oracle responses preserves their local projection mean; auxiliary records and the independent randomizer integrate out exactly. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input hn, the specified input h, the specified input hh, the specified input hh', the oracle average mean conclusion holds.
Formal statement
Proof (Lean source)
The untruncated oracle sample average inherits the polynomial approximation bias without any loss from the auxiliary channel or randomization. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input hn, the specified input h, the specified input hh, the specified input hh', the specified input theta, the specified input B, the specified input hB, the specified input herr, the specified input htarget, the oracle average bias bound conclusion holds.
Formal statement
Proof (Lean source)
Full-window Taylor reproduction bounds the bias uniformly over the primitive class. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the oracle uniform average bias conclusion holds.
Formal statement
Proof (Lean source)
At the prescribed oracle bandwidth the uniform average bias has the oracle rate. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the oracle tuned average bias conclusion holds.
Formal statement
Proof (Lean source)
The original-record experiment preserves the iid variance reduction for any labeled statistic. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input hn, the specified input F, the specified input hF, the oracle iid centered second moment conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.OracleRisk 12 declarations The labeled sample average has the variance reduction and clipping contraction needed to combine its full-window Taylor bias with its stochastic error.
# Oracle sampling and risk assembly The labeled sample average has the variance reduction and clipping contraction needed to combine its full-window Taylor bias with its stochastic error.
The untruncated localized inverse-propensity record statistic. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input z, oracle record is the corresponding construction.
Definition (Lean source)
The raw oracle average, with auxiliary records and randomization ignored. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input w, oracle average is the corresponding construction.
Definition (Lean source)
Class membership fixes the observed covariate marginal to the known design. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the oracle observed design conclusion holds.
Formal statement
Proof (Lean source)
Finite averaging preserves the bounded summands' finite moments. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh, the oracle average mem lp conclusion holds.
Formal statement
Proof (Lean source)
The iid second-moment reduction gives an explicit oracle sampling bound. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input hn, the specified input h, the specified input hh, the specified input hh', the oracle average centered square bound conclusion holds.
Formal statement
Proof (Lean source)
Cauchy--Schwarz converts the sampling second moment to absolute deviation. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input hn, the specified input h, the specified input hh, the specified input hh', the oracle average absolute deviation conclusion holds.
Formal statement
Proof (Lean source)
The target evaluation coordinates have a bound independent of bandwidth. Given the specified input d, the specified input h, the specified input hh, the oracle target energy bound conclusion holds.
Formal statement
Proof (Lean source)
Inverse effective sample size has standard deviation equal to the oracle rate. Given the specified input d, the specified input n, the specified input gamma, the specified input hn, the specified input hg, the oracle bandwidth sqrt identity conclusion holds.
Formal statement
Proof (Lean source)
The tuned oracle average has a uniform absolute sampling deviation at the oracle rate. Given the specified input d, the specified input gamma, the specified input hg, the overlap level eps, the oracle tuned absolute deviation conclusion holds.
Formal statement
Proof (Lean source)
The continuous target lies in the clipping interval by the two arm-mean range conditions. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the oracle target in clip conclusion holds.
Formal statement
Proof (Lean source)
The stipulated smoother clips exactly the raw oracle sample average. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input w, the oracle smoother eq clip average conclusion holds.
Formal statement
Proof (Lean source)
Taylor bias plus iid sampling deviation bounds the clipped oracle risk uniformly. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the oracle smoother upper rate conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.OracleSmoother 21 declarations Explicit supplied-propensity smoothing, bounded record moments, full-window Legendre geometry, and bandwidth identities for the oracle upper-risk proof.
Oracle smoother primitives
Explicit supplied-propensity smoothing, bounded record moments, full-window Legendre geometry, and bandwidth identities for the oracle upper-risk proof.
Explicit clipped known-design degree-two smoother of the inverse-propensity pseudo-outcome. Given the specified input d, the specified input gamma, the specified input n, the specified input m, the specified input w, the specified input e, oracle smoother is the corresponding construction.
Definition (Lean source)
The inverse-propensity response is a bounded signed binary outcome under overlap. Given the specified input a, the specified input y, the specified input e, the specified input he, the specified input he', the overlap level eps, the oracle binary response bound conclusion holds.
Formal statement
Proof (Lean source)
The zero extension of the supplied propensity also preserves the global response bound. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input z, the oracle designated response bound conclusion holds.
Formal statement
Proof (Lean source)
The evaluation kernel has a uniform bound on the localized cube. Given the specified input d, the specified input h, the specified input hh, the specified input x, the specified input hx, the oracle evaluation kernel bound conclusion holds.
Formal statement
Proof (Lean source)
Every localized oracle summand has finite moments, before averaging or clipping. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh, the specified input Z, the specified input hZ, the oracle summand mem lp top conclusion holds.
Formal statement
Proof (Lean source)
Oracle windows up to unit side length remain in the known-design cube. Given the specified input d, the specified input h, the specified input hh, the oracle loc cube subset cube conclusion holds.
Formal statement
Proof (Lean source)
Known-design weighted integration equals localization for the full oracle window. Given the specified input d, the specified input h, the specified input hh, the specified input hh', the specified input f, the oracle uniform localization integral conclusion holds.
Formal statement
Proof (Lean source)
Coarse Legendre orthonormality is a scaling identity for every positive window. Given the specified input d, the specified input h, the specified input hh, the specified input u, the specified input v, the oracle coarse orthonormal conclusion holds.
Formal statement
Proof (Lean source)
Full-window coarse coordinates are square integrable by their orthonormal norms. Given the specified input d, the specified input h, the specified input hh, the specified input u, the oracle coarse basis mem lp conclusion holds.
Formal statement
Proof (Lean source)
The squared oracle evaluation-kernel norm is the sum of squared target coordinates. Given the specified input d, the specified input h, the specified input hh, the oracle evaluation kernel square integral conclusion holds.
Formal statement
Proof (Lean source)
Uniform-design scaling gives the exact squared weighted-kernel energy. Given the specified input d, the specified input h, the specified input hh, the specified input hh', the oracle weighted kernel square integral conclusion holds.
Formal statement
Proof (Lean source)
Bounded pseudo-outcomes and the exact kernel energy bound the oracle record second moment. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh, the specified input hh', the specified input Z, the specified input hZ, the specified input hdesign, the oracle summand second moment bound conclusion holds.
Formal statement
Proof (Lean source)
The oracle bandwidth is positive and its whole support fits in the design cube. Given the specified input d, the specified input n, the specified input gamma, the specified input hn, the specified input hg, the oracle bandwidth bounds conclusion holds.
Formal statement
Proof (Lean source)
At the oracle bandwidth the Taylor remainder has exactly the oracle rate. Given the specified input d, the specified input n, the specified input gamma, the specified input hn, the oracle bandwidth bias identity conclusion holds.
Formal statement
Proof (Lean source)
The oracle bandwidth also balances the stochastic standard-deviation term exactly. Given the specified input d, the specified input n, the specified input gamma, the specified input hn, the specified input hg, the oracle bandwidth sampling identity conclusion holds.
Formal statement
Proof (Lean source)
Given dimension d, smoothness γ, sample sizes n and m, and a Borel supplied propensity e, the explicit oracle smoother is Borel.
Formal statement
Proof (Lean source)
For a primitive law P in the model class at overlap level eps and sample sizes n and m, the oracle smoother using its designated propensity is Borel.
Formal statement
Proof (Lean source)
Clipping bounds the smoother on every dataset, including inputs outside the model support. Given the specified input d, the specified input gamma, the specified input n, the specified input m, the specified input w, the specified input e, the oracle smoother bounded conclusion holds.
Formal statement
Proof (Lean source)
The oracle decision space requires a Borel section for every supplied function. The zero branch makes the explicit smoother a total admissible rule. Given the specified input d, the specified input gamma, the specified input n, the specified input m, oracle smoother decision is the corresponding construction.
Definition (Lean source)
The total oracle rule agrees with the stipulated smoother on every class member. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input n, the specified input m, the specified input w, the oracle smoother decision designated conclusion holds.
Formal statement
Proof (Lean source)
A uniform risk bound for the explicit smoother transfers to oracle minimax risk by using its total Borel extension as the candidate decision. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input n, the specified input m, the specified input B, the specified input hbound, the oracle risk le of oracle smoother conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.PopulationBiasGeometry 11 declarations Finite orthonormal expansions give the bilinear projection identity and the orthogonality cancellation used in the population-bias roadmap.
# Population bias projection geometry Finite orthonormal expansions give the bilinear projection identity and the orthogonality cancellation used in the population-bias roadmap. The causal response and Gram action give the exact bias identity; projection contraction and Cauchy–Schwarz give its coordinate and Euclidean bounds.
A finite orthonormal projection preserves square integrability. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input f, the specified input hf, the population projection mem lp conclusion holds.
Formal statement
Proof (Lean source)
Orthogonal projection preserves each fine-basis coefficient. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input f, the specified input hf, the specified input z, the population projection coefficient conclusion holds.
Formal statement
Proof (Lean source)
Pairing a projected function with any square-integrable function is the finite coefficient inner product. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input f, the specified input g, the specified input hf, the specified input hg, the population projection inner conclusion holds.
Formal statement
Proof (Lean source)
A control-mean residual pairs only with the residual of the propensity feature. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input f, the specified input g, the specified input hf, the specified input hg, the population residual inner identity conclusion holds.
Formal statement
Proof (Lean source)
Applying the population Gram matrix to polynomial coefficients gives the localized bilinear projection formula. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input n, the specified input m, the specified input hn, the specified input h, the specified input hh, the specified input hh', the specified input J, the specified input hJ, the specified input theta, the specified input u, the population gram action conclusion holds.
Formal statement
Proof (Lean source)
For a primitive law P in the model class at overlap level eps, the designated treated mean is Borel.
Formal statement
Proof (Lean source)
For a primitive law P in the model class at overlap level eps, the canonical treatment contrast is Borel.
Formal statement
Proof (Lean source)
Interior arm means give square-integrable designated means and contrast. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh, the specified input hh', the population causal mem lp conclusion holds.
Formal statement
Proof (Lean source)
Subtracting the population Gram action cancels the control mean except for its orthogonal projection residual. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input n, the specified input m, the specified input hn, the specified input h, the specified input hh, the specified input hh', the specified input J, the specified input hJ, the specified input theta, the specified input u, the population bias coordinate identity conclusion holds.
Formal statement
Proof (Lean source)
Projection contraction and overlap control the two Taylor-error pairings; Cauchy–Schwarz controls the product of the two nuisance residuals. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input n, the specified input m, the specified input hn, the specified input h, the specified input hh, the specified input hh', the specified input J, the specified input hJ, the specified input theta, the specified input C, the specified input hC, the specified input herr, the specified input he, the specified input hmu, the specified input u, the population bias coordinate bound conclusion holds.
Formal statement
Proof (Lean source)
Coordinatewise absolute bounds imply the Euclidean bound in fixed dimension. Given the specified input v, the specified input B, the specified input hB, the specified input hv, the population finite norm bound conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.PopulationCausalEntries 2 declarations The observed outcome moments are transported to the designated admissible versions and substituted into the population rectangular response formula.
# Localized causal response entries The observed outcome moments are transported to the designated admissible versions and substituted into the population rectangular response formula.
Localization transports both observed response moments to designated causal versions. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh, the specified input hh', the specified input f, the specified input hf, the specified input B, the specified input hB, the specified input hfB, the population localized causal moments conclusion holds.
Formal statement
Proof (Lean source)
The population response vector uses the causal response mean in its projection correction. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input n, the specified input m, the specified input hn, the specified input h, the specified input hh, the specified input hh', the specified input J, the specified input hJ, the specified input u, the population response causal entries conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.PopulationEntries 6 declarations Finite kernel expansion and independence of the two roles compute the population Gram entries directly from the original-record experiment.
Population Gram entries
Finite kernel expansion and independence of the two roles compute the population Gram entries directly from the original-record experiment.
Bounded treatment features remain integrable after averaging over the outcome role. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input f, the specified input hf, the specified input B, the specified input hfB, the population outcome role integrable conclusion holds.
Formal statement
Proof (Lean source)
Products of bounded features are integrable over the rectangular role average. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input B, the specified input C, the specified input hfB, the specified input hgC, the population rectangular role integrable conclusion holds.
Formal statement
Proof (Lean source)
Coarse products and coarse-fine products have finite bounds on the localization box. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input u, the specified input v, the specified input z, the population basis product bounds conclusion holds.
Formal statement
Proof (Lean source)
Expanding the fine kernel decomposes the raw Gram entry into finite role averages. Given the specified input d, the specified input n, the specified input m, the specified input D, the specified input h, the specified input J, the specified input u, the specified input v, the q raw finite role expansion conclusion holds.
Formal statement
Proof (Lean source)
Raw Gram entries are integrable and have the expected localized coordinate formula. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input n, the specified input m, the specified input hn, the specified input h, the specified input hh, the specified input hh', the specified input J, the specified input hJ, the specified input u, the specified input v, the population raw gram entries conclusion holds.
Formal statement
Proof (Lean source)
Symmetrization preserves the symmetric localized population Gram formula. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input n, the specified input m, the specified input hn, the specified input h, the specified input hh, the specified input hh', the specified input J, the specified input hJ, the specified input u, the specified input v, the population gram entries conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.PopulationGram 20 declarations Two-channel point-CATE annotation frontier: Helpers/PopulationGram constructions and obligations.
Helpers/PopulationGram
Two-channel point-CATE annotation frontier: Helpers/PopulationGram constructions and obligations.
The squared norm of a finite orthonormal expansion is the squared coefficient norm. Given the specified input b, the specified input hb, the specified input hortho, the specified input v, the finite orthonormal square norm conclusion holds.
Formal statement
Proof (Lean source)
Coarse orthonormality supplies square integrability of each polynomial basis entry. Given the specified input d, the specified input h, the specified input hh, the specified input hh', the specified input u, the coarse basis mem lp conclusion holds.
Formal statement
Proof (Lean source)
Polynomial coefficient vectors define square-integrable localization polynomials. Given the specified input d, the specified input h, the specified input hh, the specified input hh', the specified input v, the pv mem lp conclusion holds.
Formal statement
Coarse orthonormality identifies polynomial and coefficient squared norms. Given the specified input d, the specified input h, the specified input hh, the specified input hh', the specified input v, the pv square norm conclusion holds.
Formal statement
Proof (Lean source)
Overlap at level eps bounds the weighted squared integral below by eps·(1 − eps) times its norm. Given the specified input μ, the specified input e, the specified input f, the overlap level eps, its nonnegativity, the specified input he, the specified input hf, the specified input hoverlap, the overlap weighted square lower conclusion holds.
Formal statement
Proof (Lean source)
The overlap contribution and the projection residual give the deterministic positivity bound. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input e, the specified input f, the specified input he, the specified input hf, the specified input hef, the specified input hoverlap, the overlap level eps, the projection overlap lower conclusion holds.
Formal statement
Proof (Lean source)
Every admissible localization box lies inside the design cube. Given the specified input d, the specified input h, the specified input hh', the loc cube subset cube conclusion holds.
Formal statement
Proof (Lean source)
For a primitive law P in the model class at overlap level eps, the designated propensity is Borel on the whole covariate space.
Formal statement
Proof (Lean source)
Localization inherits the overlap interval from primitive-class membership. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh', the designated propensity overlap loc law conclusion holds.
Formal statement
Proof (Lean source)
The deterministic population expression has the claimed coefficient lower bound. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh, the specified input hh', the specified input J, the specified input v, the population expression positivity conclusion holds.
Formal statement
Proof (Lean source)
A bounded propensity preserves square integrability under localization. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh', the specified input f, the specified input hf, the designated propensity mul mem lp conclusion holds.
Formal statement
Proof (Lean source)
The first population energy is integrable because overlap bounds its multiplier. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh', the specified input f, the specified input hf, the designated propensity square integrable conclusion holds.
Formal statement
Proof (Lean source)
Pythagoras turns the population first energy minus the projected energy into an overlap energy plus the nonnegative projection residual. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh, the specified input hh', the specified input J, the specified input hJ, the specified input f, the specified input hf, the population projection energy identity conclusion holds.
Formal statement
Proof (Lean source)
A finite bilinear integral matrix acts on coefficients by integrating the product of their two finite expansions. Given the specified input a, the specified input b, the specified input hab, the specified input v, the finite bilinear integral quadratic conclusion holds.
Formal statement
Proof (Lean source)
The quadratic form of a finite coefficient Gram matrix is the sum of the squared coefficient expansions. Given the specified input c, the specified input v, the finite coefficient gram quadratic conclusion holds.
Formal statement
Proof (Lean source)
Finite kernel integration expands the projection in its orthonormal basis. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input f, the specified input hf, the specified input x, the projection finite expansion conclusion holds.
Formal statement
Proof (Lean source)
Projection energy is exactly the sum of squared orthonormal coefficients. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input f, the specified input hf, the projection square coefficients conclusion holds.
Formal statement
Proof (Lean source)
The weighted polynomial's fine coefficients are linear combinations of the weighted coarse-basis coefficients. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh, the specified input hh', the specified input J, the specified input hJ, the specified input v, the specified input z, the weighted pv projection coefficient conclusion holds.
Formal statement
Proof (Lean source)
The population coordinate formula implies the full quadratic projection identity by finite expansion, without an empirical invertibility assumption. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh, the specified input hh', the specified input J, the specified input hJ, the specified input Q, the specified input hQ, the specified input v, the population gram quadratic of entries conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input P, the specified input hP, the specified input n, the specified input m, the specified input hn, the specified input h, the specified input hh, the specified input hh', the specified input J, the specified input hJ, the specified input v, the population positivity conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.PopulationMoments 16 declarations Conditional Bernoulli integration and localization identities used to compute the population rectangular Gram matrix from the original-record experiment.
Treatment moments under the uniform design
Conditional Bernoulli integration and localization identities used to compute the population rectangular Gram matrix from the original-record experiment.
For covariate dimension d, the observation map is Borel, including its treatment-dependent outcome selection.
Formal statement
Proof (Lean source)
A primitive treatment-margin identity guarantees that its Bernoulli kernel is s-finite. Given the specified input d, the specified input P, the primitive propensity kernel sfinite conclusion holds.
Formal statement
Proof (Lean source)
The treatment-record law is a probability measure. Given the specified input d, the specified input P, the xa law probability conclusion holds.
Formal statement
Proof (Lean source)
Discarding outcomes in an observed record gives exactly the treatment-record marginal. Given the specified input d, the specified input P, the obs law map treatment conclusion holds.
Formal statement
Proof (Lean source)
The observed-record law is a probability measure. Given the specified input d, the specified input P, the obs law probability conclusion holds.
Formal statement
Proof (Lean source)
Integrating a treatment bit against its Bernoulli law returns its probability. Given the specified input p, the specified input c, the specified input hp, the bern bit integral conclusion holds.
Formal statement
Proof (Lean source)
Uniform-design integration of a bounded covariate function times treatment uses the primitive law's conditional treatment margin. Given the specified input d, the specified input P, the specified input hdesign, the specified input hoverlap, the specified input f, the specified input hf, the specified input B, the specified input hB, the overlap level eps, the xa law treatment moment conclusion holds.
Formal statement
Proof (Lean source)
Weighted integration under the uniform design is exactly localization integration. Given the specified input d, the specified input h, the specified input hh, the specified input hh', the specified input f, the uniform law localization integral conclusion holds.
Formal statement
Proof (Lean source)
A bounded function on the localization box has a globally bounded weighted extension. Given the specified input d, the specified input h, the specified input hh, the specified input f, the specified input B, the specified input hB, the specified input hf, the specified input x, the loc weight mul norm bound conclusion holds.
Formal statement
Proof (Lean source)
A localized treatment moment uses the designated admissible version, even when the raw primitive carrier stores different conditional versions. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input hh, the specified input hh', the specified input f, the specified input hf, the specified input B, the specified input hB, the specified input hfB, the designated local treatment moment conclusion holds.
Formal statement
Proof (Lean source)
The independent randomizer has unit mass. the population randomizer probability conclusion holds.
Formal statement
Proof (Lean source)
The original-record experiment is a probability measure. Given the specified input d, the specified input P, the specified input n, the specified input m, the population experiment probability conclusion holds.
Formal statement
Proof (Lean source)
Dataset-only statistics integrate out the independent public randomizer. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input F, the experiment integral dataset conclusion holds.
Formal statement
Proof (Lean source)
An outcome-discarded labeled record has the treatment-record marginal. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input f, the specified input hf, the specified input j, the experiment labeled treatment integral conclusion holds.
Formal statement
Proof (Lean source)
Different labeled records give a product of treatment-record expectations. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input i, the specified input j, the specified input hij, the experiment distinct labeled treatment integral conclusion holds.
Formal statement
Proof (Lean source)
A treatment-role record and an outcome-role record have independent expectations, including treatment records from the auxiliary block. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input i, the specified input j, the specified input hi, the specified input hj, the experiment role product integral conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.PopulationOutcomeEntries 4 declarations Finite expansion of the response correction and independence of the two roles identify the population vector using observed outcome moments.
# Population outcome entries Finite expansion of the response correction and independence of the two roles identify the population vector using observed outcome moments. The terminal response is the observed outcome, without an additional treatment mark.
Localization makes any locally bounded Borel record statistic essentially bounded. Given the specified input d, the specified input h, the specified input hh, the specified input X, the specified input hX, the specified input f, the specified input hf, the specified input B, the specified input hB, the specified input hfB, the population localized record mem lp conclusion holds.
Formal statement
Proof (Lean source)
Independent role averages of separated bounded features factor into their means. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input hn, the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input hf2, the specified input hg2, the population rectangular observed product mean conclusion holds.
Formal statement
Proof (Lean source)
The response correction is a sum of products of treatment and observed-outcome features. Given the specified input d, the specified input n, the specified input m, the specified input D, the specified input h, the specified input J, the specified input u, the r hat finite role expansion conclusion holds.
Formal statement
Proof (Lean source)
The population response vector has the finite projection-coefficient formula under the original-record experiment. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input n, the specified input m, the specified input hn, the specified input h, the specified input hh, the specified input hh', the specified input J, the specified input hJ, the specified input u, the population response observed entries conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.PopulationOutcomeMoments 7 declarations Exchangeability removes the treatment bit under bounded test functions, and conditional Bernoulli margins identify the selected potential-outcome moment.
# Causal outcome moments Exchangeability removes the treatment bit under bounded test functions, and conditional Bernoulli margins identify the selected potential-outcome moment.
A Bernoulli law with an admissible probability has unit mass. Given the specified input p, the specified input hp, the population bern probability conclusion holds.
Formal statement
Proof (Lean source)
Exchangeability factors the treatment bit from a bounded potential-outcome test. Given the specified input d, the specified input P, the specified input hdesign, the specified input hex, the specified input he, the specified input H, the specified input hH, the specified input B, the specified input hB, the specified input hbound, the specified input hsupp, the overlap level eps, the population exchangeability bit moment conclusion holds.
Formal statement
Proof (Lean source)
A conditional Bernoulli margin identifies bounded potential-outcome test moments. Given the specified input d, the specified input P, the specified input hdesign, the specified input j, the specified input hj, the specified input mu, the specified input hmu, the specified input hmu0, the specified input hmargin, the specified input f, the specified input hf, the specified input B, the specified input hB, the specified input hfB, the population arm margin moment conclusion holds.
Formal statement
Proof (Lean source)
A bounded cube-supported test remains bounded after multiplication by overlap. Given the specified input d, the specified input P, the specified input he, the specified input f, the specified input B, the specified input hB, the specified input hf, the specified input hs, the overlap level eps, the population test mul propensity bound conclusion holds.
Formal statement
Proof (Lean source)
The treated observed outcome moment is the propensity times the treated arm mean. Given the specified input d, the specified input P, the specified input hdesign, the specified input hex, the specified input he, the specified input hmu, the specified input f, the specified input hf, the specified input B, the specified input hB, the specified input hfB, the specified input hs, the overlap level eps, the population treated outcome moment conclusion holds.
Formal statement
Proof (Lean source)
The untreated observed outcome moment uses the complementary propensity. Given the specified input d, the specified input P, the specified input hdesign, the specified input hex, the specified input he, the specified input hmu, the specified input f, the specified input hf, the specified input B, the specified input hB, the specified input hfB, the specified input hs, the overlap level eps, the population control outcome moment conclusion holds.
Formal statement
Proof (Lean source)
The observed response moment combines the two identified arm moments. Given the specified input d, the specified input P, the specified input hdesign, the specified input hex, the specified input he, the specified input hm0, the specified input hm1, the specified input f, the specified input hf, the specified input B, the specified input hB, the specified input hfB, the specified input hs, the overlap level eps, the population outcome moment conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.PopulationRoles 9 declarations Finite role counts, integrability of localized treatment features, and exact expectations of the independent rectangular role products.
Population averages over the two roles
Finite role counts, integrability of localized treatment features, and exact expectations of the independent rectangular role products.
Localization weights a covariate feature and its treatment bit. Given the specified input d, the specified input h, the specified input f, the specified input z, weighted treatment feature is the corresponding construction.
Given bandwidth h and a Borel covariate feature f, the localized treatment feature is Borel.
Formal statement
Proof (Lean source)
A localized feature inherits a global bound from its bound on the localization box. Given the specified input d, the specified input h, the specified input hh, the specified input f, the specified input B, the specified input hB, the specified input hfB, the specified input z, the weighted treatment feature norm bound conclusion holds.
Formal statement
Proof (Lean source)
For record position i, evaluating the concatenated treatment record at i is Borel.
Formal statement
Proof (Lean source)
Bounded Borel statistics are integrable under a probability measure. Given the specified input f, the specified input hf, the specified input B, the specified input hB, the population integrable bounded conclusion holds.
Formal statement
Proof (Lean source)
The outcome and treatment roles have their prescribed cardinalities. Given the specified input n, the specified input m, the population role cardinalities conclusion holds.
Formal statement
Proof (Lean source)
Both role counts are strictly positive whenever there are at least two labeled records. Given the specified input n, the specified input m, the specified input hn, the population role counts pos conclusion holds.
Formal statement
Proof (Lean source)
Averaging the labeled outcome-role treatment features preserves their population mean. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input hn, the specified input f, the specified input hf, the specified input B, the specified input hfB, the population outcome role mean conclusion holds.
Formal statement
Proof (Lean source)
Independent rectangular averaging gives the product of the two marginal means. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input hn, the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input B, the specified input C, the specified input hfB, the specified input hgC, the population rectangular role mean conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.RateAlgebra 6 declarations Two-channel point-CATE annotation frontier: Helpers/RateAlgebra constructions and obligations.
Helpers/RateAlgebra
Two-channel point-CATE annotation frontier: Helpers/RateAlgebra constructions and obligations.
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the rate exponent identities conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input n, the specified input m, the specified input hn, the rate branches conclusion holds.
Formal statement
Proof (Lean source)
Below the smoothness cutoff, the total-count boundary exponent exceeds one. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input hs, the q star gt one conclusion holds.
Formal statement
Proof (Lean source)
With no auxiliary records, the pair branch is the stated supervised power. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input n, the specified input hn, the supervised rate branches conclusion holds.
Formal statement
Proof (Lean source)
Inverting a decreasing positive power gives its exact sample threshold. Given the specified input x, the specified input epsilon, the specified input D, the specified input g, the specified input hx, the specified input he, the specified input hD, the specified input hg, the decreasing power threshold conclusion holds.
Formal statement
Proof (Lean source)
The maximum of the two frontier branches gives both exact acquisition requirements. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input n, the specified input m, the specified input hn, the specified input epsilon, the specified input he, the sharp rate acquisition iff conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.RectangularBlockLaw 8 declarations An iid full-observation representation projects the auxiliary records to treatment records.
# Joint law of the original-record roles An iid full-observation representation projects the auxiliary records to treatment records. Selecting disjoint index blocks then gives exactly the independent role product law needed by the rectangular variance calculation.
Disjoint injective selections from an iid sequence have the independent block law. Given the specified input N, the specified input t, the specified input ell, the specified input i, the specified input j, the specified input hi, the specified input hj, the specified input hij, the rectangular iid block law conclusion holds.
Formal statement
Proof (Lean source)
Projecting outcome-free records from a longer iid observation sequence realizes the dataset law. Given the specified input d, the specified input n, the specified input m, the specified input P, the rectangular iid dataset law conclusion holds.
Formal statement
Proof (Lean source)
Enumerating both prescribed roles preserves their independent treatment/outcome product law. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input i, the specified input j, the specified input hi, the specified input hj, the specified input hit, the specified input hjl, the rectangular dataset block law conclusion holds.
Formal statement
Proof (Lean source)
An enumeration of the treatment role by its prescribed count. Given the specified input n, the specified input m, rectangular treatment enumeration is the corresponding construction.
Definition (Lean source)
An enumeration of the outcome role by its prescribed count. Given the specified input n, the specified input m, rectangular outcome enumeration is the corresponding construction.
Definition (Lean source)
The selected records in the two roles, including their deterministic enumeration. Given the specified input d, the specified input n, the specified input m, the specified input w, rectangular role data is the corresponding construction.
Definition (Lean source)
The original-record role vector has precisely the independent role product law. Given the specified input d, the specified input n, the specified input m, the specified input P, the rectangular role data law conclusion holds.
Formal statement
Proof (Lean source)
The rectangular role sum equals the ordinary finite sum over the enumerated role vector. Given the specified input d, the specified input n, the specified input m, the specified input w, the specified input H, the rectangular role sum enumeration conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.RectangularCoordinates 5 declarations Both types of coordinate are instances of the original-record marked moment bound.
# Coordinate bounds for the rectangular vector and raw Gram matrix Both types of coordinate are instances of the original-record marked moment bound. Their constants depend only on dimension, and hence are uniform in the law, sample counts, and localization grid.
A common finite variance constant for vector and raw-matrix coordinates. Given the specified input d, rectangular coordinate constant is the corresponding construction.
Coarse basis coordinates times a binary mark share a dimension-only local bound. Given the specified input d, the specified input h, the specified input hh, the specified input x, the specified input hx, the specified input u, the specified input a, the rectangular coarse mark bound conclusion holds.
Formal statement
Proof (Lean source)
A product of two coarse coordinates and a binary mark has the same common bound. Given the specified input d, the specified input h, the specified input hh, the specified input x, the specified input hx, the specified input u, the specified input v, the specified input a, the rectangular coarse pair mark bound conclusion holds.
Formal statement
Proof (Lean source)
The vector coordinate's centered energy has the claimed rectangular sampling order. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input hn, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input u, the rectangular r coordinate bound conclusion holds.
Formal statement
Proof (Lean source)
Every raw Gram coordinate has the same dimension-only centered-energy bound. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input hn, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input u, the specified input v, the rectangular q coordinate bound conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.RectangularKernelEnergy 20 declarations Uniform design converts the squared, doubly localized projection kernel into its rank times the inverse squared localization volume.
# Rectangular kernel second moments Uniform design converts the squared, doubly localized projection kernel into its rank times the inverse squared localization volume. Bounded record marks and coarse features preserve this order. These are the kernel-energy steps of the rectangular sampling roadmap.
The fine projection kernel is globally bounded at every fixed resolution. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input x, the specified input y, the rectangular fine kernel abs bound conclusion holds.
Formal statement
Proof (Lean source)
The localization weight is nonnegative and at most its fixed height. Given the specified input d, the specified input h, the specified input hh, the specified input x, the rectangular loc weight bounds conclusion holds.
Formal statement
Proof (Lean source)
A bounded fine kernel remains square integrable with either one or two localization weights. Given the specified input W, the specified input Z, the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input X, the specified input Y, the specified input hX, the specified input hY, the specified input a, the specified input b, the rectangular weighted kernel mem lp conclusion holds.
Formal statement
Proof (Lean source)
Product localization is obtained by applying the one-variable identity twice. Given the specified input d, the specified input h, the specified input hh, the specified input hh', the specified input F, the specified input hfull, the specified input hloc, the rectangular product localization integral conclusion holds.
Formal statement
Proof (Lean source)
Under uniform design, the squared weighted kernel has exactly rank divided by squared volume. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the rectangular uniform kernel square integral conclusion holds.
Formal statement
Proof (Lean source)
Independent uniform covariates retain the exact weighted-kernel energy under record maps. Given the specified input W, the specified input Z, the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input X, the specified input Y, the specified input hX, the specified input hY, the uniform pushforward identities, the rectangular record kernel square integral conclusion holds.
Formal statement
Proof (Lean source)
Locally bounded record features multiply kernel energy by their squared bounds. Given the specified input W, the specified input Z, the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input X, the specified input Y, the specified input hX, the specified input hY, the uniform pushforward identities, the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input A, the specified input B, the specified input hA, the specified input hB, the specified input hfA, the specified input hgB, the rectangular marked kernel energy le conclusion holds.
Formal statement
Proof (Lean source)
Primitive-class membership fixes the actual covariate marginal, regardless of raw versions. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the rectangular primitive uniform design conclusion holds.
Formal statement
Proof (Lean source)
A treatment-role record has uniform covariates. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the rectangular xa law covariates conclusion holds.
Formal statement
Proof (Lean source)
An outcome-role record has uniform covariates. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the rectangular obs law covariates conclusion holds.
Formal statement
Proof (Lean source)
Binary record marks have absolute value at most one. Given the specified input a, the rectangular bit abs le one conclusion holds.
Proof (Lean source)
The vector correction kernel has second moment at most a dimension constant times rank over squared volume. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input u, the rectangular r kernel energy conclusion holds.
Formal statement
Proof (Lean source)
The raw Gram correction kernel has the same rank-over-squared-volume order. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input u, the specified input v, the rectangular q kernel energy conclusion holds.
Formal statement
Proof (Lean source)
A locally bounded record feature has a globally bounded weighted extension. Given the specified input W, the specified input d, the specified input h, the specified input hh, the specified input X, the specified input hX, the specified input f, the specified input hf, the specified input B, the specified input hB, the specified input hfB, the rectangular localized mark mem lp top conclusion holds.
Formal statement
Proof (Lean source)
Bounded record marks and uniform design give a resolution-independent conditional kernel bound. Given the specified input Z, the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input Y, the specified input hY, its uniform pushforward identity, the specified input g, the specified input hg, the specified input B, the specified input hB, the specified input hgB, the specified input x, the rectangular kernel slice abs le conclusion holds.
Formal statement
Proof (Lean source)
The squared localization weight integrates to inverse localization volume under uniform design. Given the specified input W, the specified input d, the specified input h, the specified input hh, the specified input hh', the specified input X, the specified input hX, its uniform pushforward identity, the rectangular record loc weight square integral conclusion holds.
Formal statement
Proof (Lean source)
First conditional integration has second moment of inverse-volume order, with no rank factor. Given the specified input W, the specified input Z, the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input X, the specified input Y, the specified input hX, the specified input hY, the uniform pushforward identities, the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input A, the specified input B, the specified input hA, the specified input hB, the specified input hfA, the specified input hgB, the rectangular marked kernel row energy conclusion holds.
Formal statement
Proof (Lean source)
The finite projection kernel is symmetric in its covariate arguments. Given the specified input d, the specified input h, the specified input J, the specified input x, the specified input y, the rectangular fine kernel symmetric conclusion holds.
Formal statement
Proof (Lean source)
Reversing the independent roles gives the same inverse-volume bound for the second conditional integration. Given the specified input W, the specified input Z, the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input X, the specified input Y, the specified input hX, the specified input hY, the uniform pushforward identities, the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input A, the specified input B, the specified input hA, the specified input hB, the specified input hfA, the specified input hgB, the rectangular marked kernel column energy conclusion holds.
Formal statement
Proof (Lean source)
The roadmap's two conditional energies and kernel rank give the full variance order for each rectangular correction. Given the specified input W, the specified input Z, the specified input d, the specified input n, the specified input m, the specified input hn, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input X, the specified input Y, the specified input hX, the specified input hY, the uniform pushforward identities, the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input A, the specified input B, the specified input hA, the specified input hB, the specified input hfA, the specified input hgB, the rectangular marked kernel variance bound conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.RectangularMomentBounds 11 declarations The joint role law transfers the independent rectangular variance calculation to the actual data.
# Original-record rectangular moment bounds The joint role law transfers the independent rectangular variance calculation to the actual data. Centered first-order averages and corrections are combined by the squared-difference inequality, without an independence assertion.
A rectangular average of a record kernel on the original dataset. Given the specified input d, the specified input n, the specified input m, the specified input H, the specified input w, rectangular average is the corresponding construction.
The rectangular average is exactly its finite enumerated counterpart. Given the specified input d, the specified input n, the specified input m, the specified input H, the rectangular average enumeration conclusion holds.
Formal statement
Proof (Lean source)
A square-integrable kernel gives a square-integrable original-record rectangular average. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input H, the specified input hH, the rectangular original average mem lp conclusion holds.
Formal statement
Proof (Lean source)
The original-record rectangular average has the independent pair expectation. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input hn, the specified input H, the specified input hHm, the specified input hH, the rectangular original average mean conclusion holds.
Formal statement
Proof (Lean source)
Any independent-block centered variance bound transfers to the original rectangular average. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input H, the specified input hHm, the specified input B, the specified input hb, the rectangular original average variance le conclusion holds.
Formal statement
Proof (Lean source)
A first-order average over the labeled outcome role. Given the specified input d, the specified input n, the specified input m, the specified input f, the specified input w, rectangular outcome average is the corresponding construction.
The outcome average is the ordinary iid average of the enumerated outcome records. Given the specified input d, the specified input n, the specified input m, the specified input f, the specified input w, the rectangular outcome average enumeration conclusion holds.
Formal statement
Proof (Lean source)
The first-order outcome average is square-integrable and has the observation-law mean. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input hn, the specified input f, the specified input hfm, the specified input hf, the rectangular outcome average moments conclusion holds.
Formal statement
Proof (Lean source)
The centered difference of the two actual moments obeys the sum of their variance bounds. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input hn, the specified input f, the specified input hfm, the specified input hf, the specified input H, the specified input hHm, the specified input hH, the specified input B, the rectangular-average variance bound, the rectangular original moment variance le conclusion holds.
Formal statement
Proof (Lean source)
A bounded localized observation feature has inverse-volume second moment. Given the specified input W, the specified input d, the specified input h, the specified input hh, the specified input hh', the specified input X, the specified input hX, its uniform pushforward identity, the specified input f, the specified input hf, the specified input B, the specified input hB, the specified input hfB, the rectangular localized mark energy conclusion holds.
Formal statement
Proof (Lean source)
Localized bounded marks give the sampling envelope for an actual moment coordinate. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input hn, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input f0, the specified input f, the specified input g, the specified input hf0, the specified input hf, the specified input hg, the specified input M, the specified input hM, the specified input hf0M, the specified input hfM, the specified input hgM, the rectangular marked moment bound conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.RectangularRoleTransport 7 declarations The treatment and outcome records in a rectangular pair have the product of their respective marginal laws, including pairs using auxiliary records.
# Transport of rectangular kernels to original records The treatment and outcome records in a rectangular pair have the product of their respective marginal laws, including pairs using auxiliary records. Consequently their kernel energies are those calculated under the product law.
Distinct labeled records have their full observation product law. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input H, the specified input hH, the specified input i, the specified input j, the specified input hij, the rectangular distinct labeled pair integral conclusion holds.
Formal statement
Proof (Lean source)
Any Borel rectangular kernel has the product-law expectation on a pair of disjoint roles. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input H, the specified input hH, the specified input i, the specified input j, the specified input hi, the specified input hj, the rectangular role pair integral conclusion holds.
Formal statement
Proof (Lean source)
Squared kernel energy on an original-record pair equals its independent product-law energy. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input H, the specified input hH, the specified input i, the specified input j, the specified input hi, the specified input hj, the rectangular role pair square integral conclusion holds.
Formal statement
Proof (Lean source)
Averaging a full observation statistic over the outcome role has the usual iid variance. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input hn, the specified input f, the specified input hf, the rectangular outcome role centered energy conclusion holds.
Formal statement
Proof (Lean source)
The outcome-role first-order centered energy has labeled-sample inverse-volume order. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input hn, the specified input f, the specified input hf, the rectangular outcome role energy le conclusion holds.
Formal statement
Proof (Lean source)
The vector correction's squared kernel bound holds on every actual rectangular pair. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input u, the specified input i, the specified input j, the specified input hi, the specified input hj, the rectangular experiment r kernel energy conclusion holds.
Formal statement
Proof (Lean source)
The raw Gram correction's squared kernel bound holds on every actual rectangular pair. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input u, the specified input v, the specified input i, the specified input j, the specified input hi, the specified input hj, the rectangular experiment q kernel energy conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.RectangularSampling 1 declarations Two-channel point-CATE annotation frontier: Helpers/RectangularSampling constructions and obligations.
Helpers/RectangularSampling
Two-channel point-CATE annotation frontier: Helpers/RectangularSampling constructions and obligations.
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the rectangular sampling bound conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.RectangularUStat 12 declarations Exact second moments and the Hoeffding variance identity for two independent finite iid blocks.
Helpers/RectangularUStat
Exact second moments and the Hoeffding variance identity for two independent finite iid blocks. Slice means preserve square integrability; the centered kernel splits into orthogonal row, column, and degenerate energies.
Square-integrability on a product gives square-integrable slices almost everywhere. Given the specified input W, the specified input Z, the specified input H, the specified input hH, the rectangular mem lp slices conclusion holds.
Formal statement
Proof (Lean source)
The squared expectation is no greater than the second moment. Given the specified input W, the specified input F, the specified input hF, the rectangular sq integral le conclusion holds.
Formal statement
Proof (Lean source)
Integrating one coordinate of a square-integrable product function preserves L². Given the specified input W, the specified input Z, the specified input H, the specified input hH, the rectangular mem lp mean conclusion holds.
Formal statement
Proof (Lean source)
An iid average has second moment equal to its squared mean plus scaled variance. Given the specified input W, the specified input t, the specified input ht, the specified input F, the specified input hF, the rectangular iid second moment conclusion holds.
Formal statement
Proof (Lean source)
Averaging the first coordinate preserves square integrability on the remaining product. Given the specified input W, the specified input Z, the specified input t, the specified input H, the specified input hH, the rectangular average mem lp conclusion holds.
Formal statement
Proof (Lean source)
The second moment after averaging one coordinate follows from iid variance and Fubini. Given the specified input W, the specified input Z, the specified input t, the specified input ht, the specified input H, the specified input hH, the rectangular average square conclusion holds.
Formal statement
Proof (Lean source)
Almost every slice mean of a first-coordinate average is the corresponding original mean. Given the specified input W, the specified input Z, the specified input t, the specified input ht, the specified input H, the specified input hH, the rectangular average mean conclusion holds.
Formal statement
Proof (Lean source)
Slice integration commutes with a finite first-coordinate average. Given the specified input W, the specified input Z, the specified input t, the specified input H, the specified input hH, the rectangular average other mean conclusion holds.
Formal statement
Proof (Lean source)
Iterated iid averaging gives the exact uncentered rectangular second moment. Given the specified input W, the specified input Z, the specified input t, the specified input ell, the specified input ht, the specified input hl, the specified input H, the specified input hH, the rectangular second moment conclusion holds.
Formal statement
Proof (Lean source)
A product function has the same inner product with a first-coordinate function as its slice mean. Given the specified input W, the specified input Z, the specified input H, the specified input g, the specified input hH, the specified input hg, the rectangular mean inner conclusion holds.
Formal statement
Proof (Lean source)
The centered rectangular kernel splits into orthogonal row, column, and degenerate energies. Given the specified input W, the specified input Z, the specified input H, the specified input hH, the specified input hzero, the rectangular anova energy conclusion holds.
Formal statement
Proof (Lean source)
Two independent finite iid blocks give the rectangular Hoeffding variance identity. Given the specified input W, the specified input Z, the specified input t, the specified input ell, the specified input ht, the specified input hl, the specified input H, the specified input hH, the rectangular ustat variance conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.RectangularVarianceBounds 10 declarations The Hoeffding identity bounds a rectangular average using uncentered slice and kernel second moments.
# Rectangular variance bounds The Hoeffding identity bounds a rectangular average using uncentered slice and kernel second moments. The prescribed role counts then yield the paper's two sample-size denominators. No independence between a first-order moment and its rectangular correction is required.
Centering a square-integrable real statistic cannot increase its second moment. Given the specified input f, the specified input hf, the rectangular centered energy le conclusion holds.
Formal statement
Proof (Lean source)
The orthogonal degenerate remainder has no more energy than the original kernel. Given the specified input W, the specified input Z, the specified input H, the specified input hH, the rectangular degenerate energy le conclusion holds.
Formal statement
Proof (Lean source)
The rectangular variance is bounded by the uncentered row, column, and kernel energies. Given the specified input W, the specified input Z, the specified input t, the specified input ell, the specified input ht, the specified input hl, the specified input H, the specified input hH, the rectangular variance le slice energies conclusion holds.
Formal statement
Proof (Lean source)
The floor split reserves at least one third of the labeled records and half of all treatment records. Given the specified input n, the specified input m, the specified input hn, the rectangular role count bounds conclusion holds.
Formal statement
Proof (Lean source)
Role reciprocals have the labeled and total-record orders required by the variance bound. Given the specified input n, the specified input m, the specified input hn, the rectangular role inverse bounds conclusion holds.
Formal statement
Proof (Lean source)
Uniform slice and kernel energies give the rectangular sampling order after the floor split. Given the specified input W, the specified input Z, the specified input n, the specified input m, the specified input hn, the specified input H, the specified input hH, the specified input B, the specified input E, the specified input hB, the specified input hE, the specified input hrow, the specified input hcol, the specified input hkernel, the rectangular role variance bound conclusion holds.
Formal statement
Proof (Lean source)
A first-order moment and its rectangular correction need no independence for this energy bound. Given the specified input f, the specified input g, the specified input hf, the specified input hg, the rectangular difference energy le conclusion holds.
Formal statement
Proof (Lean source)
Symmetrization is a contraction for the squared Frobenius norm. Given the specified input B, the rectangular symmetrization energy le conclusion holds.
Formal statement
Proof (Lean source)
Symmetrization about a symmetric population matrix contracts the squared deviation. Given the specified input B, the specified input Q, the specified input hQ, the rectangular symmetrized deviation le conclusion holds.
Formal statement
Proof (Lean source)
The roadmap's kernel and conditional-mean bounds give precisely the two-term sampling envelope. Given the specified input W, the specified input Z, the specified input n, the specified input m, the specified input d, the specified input hn, the specified input h, the specified input C, the specified input k, the specified input hh, the specified input hC, the specified input hk, the specified input H, the specified input hH, the specified input hrow, the specified input hcol, the specified input hkernel, the rectangular sampling from kernel energies conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.ScaledHolder 6 declarations Global derivative bounds and a bounded/Lipschitz interpolation argument give uniform bounds in the paper's exact coordinate-partial Hölder norm.
Hölder bounds for dilated smooth compact profiles
Global derivative bounds and a bounded/Lipschitz interpolation argument give uniform bounds in the paper's exact coordinate-partial Hölder norm.
The direction list has a dimension-only bound, sufficient for multilinear estimates. Given the specified input d, the specified input k, the coordinate directions norm le conclusion holds.
Formal statement
Proof (Lean source)
A smooth compact profile has globally bounded derivatives at each fixed order. Given the specified input d, the specified input f, the specified input hf, the specified input hs, the specified input j, the compact profile derivative bound conclusion holds.
Formal statement
Proof (Lean source)
Bounded smooth derivatives interpolate to a global fractional Hölder modulus. Given the specified input d, the specified input f, the specified input hf, the specified input hs, the specified input j, the specified input a, the specified input ha, the specified input ha1, the compact profile derivative modulus conclusion holds.
Formal statement
Proof (Lean source)
Translation and dilation give the exact derivative scaling of a profile. Given the specified input d, the specified input f, the specified input hf, the specified input h, the specified input j, the specified input x, the dilated profile derivative conclusion holds.
Formal statement
Proof (Lean source)
The exact coordinate partial is controlled by the ambient derivative operator norm. Given the specified input d, the specified input f, the specified input hf, the specified input x, the specified input hx, the coordinate partial le operator conclusion holds.
Formal statement
Proof (Lean source)
Smooth compact profiles obey the exact Hölder norm bound after dilation. Given the specified input d, the specified input f, the specified input hf, the specified input hsupp, the specified input s, the specified input hs, the compact profile scaled holder conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.TuningBalance 4 declarations Algebraic bounds for the two sampling terms under the prescribed public tuning.
# Public bandwidth and grid balance Algebraic bounds for the two sampling terms under the prescribed public tuning.
A bandwidth above the sample power balances a sampling monomial against its bias. Given the specified input x, the specified input H, the specified input D, the specified input p, the specified input g, the specified input hx, the specified input hH, the specified input hD, the specified input heq, the specified input hb, the bandwidth monomial balance conclusion holds.
Formal statement
Proof (Lean source)
Rounding the grid power changes its cell side by at most a factor two. Given the specified input H, the specified input t, the specified input hH, the specified input hH1, the specified input ht, the ceil grid side bounds conclusion holds.
Formal statement
Proof (Lean source)
A factor-two cell-side bound gives the corresponding pair-sampling bound. Given the specified input x, the specified input H, the specified input delta, the specified input t, the specified input d, the specified input hx, the specified input hH, the specified input hd, the specified input hgrid, the grid pair sampling le conclusion holds.
Formal statement
Proof (Lean source)
The prescribed tuning balances approximation and both sampling channels. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the tuning balance conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.UpperAssembly 26 declarations Two-channel point-CATE annotation frontier: Helpers/UpperAssembly constructions and obligations.
Helpers/UpperAssembly
Two-channel point-CATE annotation frontier: Helpers/UpperAssembly constructions and obligations.
Population bias assembly from the causal outcome identities and projection bounds. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the population bias bound conclusion holds.
Formal statement
Proof (Lean source)
Unit quadratic forms are bounded below by the sum of absolute matrix entries. Given the specified input d, the specified input Q, the unit quadratic bdd below conclusion holds.
Formal statement
Proof (Lean source)
The Rayleigh infimum is at most every unit-vector quadratic form. Given the specified input d, the specified input Q, the specified input v, the specified input hv, the lambda min le unit quadratic conclusion holds.
Formal statement
Proof (Lean source)
the measurable bit conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the measurable treatment records conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input J, the measurable eta hat conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input J, the specified input u, the measurable r hat conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input J, the specified input u, the specified input v, the measurable q hat conclusion holds.
Formal statement
Proof (Lean source)
The guard is the intersection of closed inequalities over all unit vectors. Given the specified input d, the specified input a, the is closed lambda min ge conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input J, the overlap level eps, the measurable t hat total conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input J, the specified input hn, the specified input hh, the specified input hh', the specified input hJ, the overlap level eps, the t hat measurable conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input n, the specified input m, the specified input hn, the sharp decision measurable conclusion holds.
Formal statement
Proof (Lean source)
A positive Rayleigh infimum excludes a nonzero kernel and makes the matrix invertible. Given the specified input d, the specified input Q, the specified input hmin, the is unit of lambda min pos conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input Q, the specified input hQ, the specified input hmin, the specified input R, the specified input theta, the good branch resolvent conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input x, the specified input y, the specified input hy, the clipping contraction conclusion holds.
Formal statement
Proof (Lean source)
Localization boxes are compact, including degenerate parameter values. Given the specified input d, the specified input h, the is compact loc cube conclusion holds.
Proof (Lean source)
A measurable function supported on a localization box and dominated there by a continuous function is essentially bounded after any measurable covariate map. Given the specified input d, the specified input h, the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input hbound, the specified input hsupp, the specified input X, the specified input hX, the compact supported mem lp top conclusion holds.
Formal statement
Proof (Lean source)
Localized finite products of coarse polynomial entries are essentially bounded on any sample space. Given the specified input d, the specified input h, the specified input us, the specified input X, the specified input hX, the weighted coarse mem lp top conclusion holds.
Formal statement
Proof (Lean source)
Each cellwise basis entry is essentially bounded after a measurable covariate map. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input z, the specified input X, the specified input hX, the fine basis mem lp top comp conclusion holds.
Formal statement
Proof (Lean source)
Each empirical Gram entry is essentially bounded at every fixed admissible resolution. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input u, the specified input v, the q hat mem lp top conclusion holds.
Formal statement
Proof (Lean source)
The original-record experiment, including its independent randomizer, is a probability law. Given the specified input d, the specified input n, the specified input m, the specified input P, the experiment probability conclusion holds.
Formal statement
Proof (Lean source)
The squared Frobenius deviation of the empirical Gram matrix is integrable, as a finite sum of bounded measurable terms. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input h, the specified input J, the specified input hh, the specified input hJ, the q hat square deviation integrable conclusion holds.
Formal statement
Proof (Lean source)
A constant-polynomial coordinate supplies a unit vector for the Rayleigh infimum. Given the specified input d, the specified input Q, the unit quadratic nonempty conclusion holds.
Formal statement
Proof (Lean source)
Finite Cauchy–Schwarz bounds the squared quadratic form of a unit vector by the squared Frobenius norm. Given the specified input E, the specified input v, the specified input hv, the quadratic sq le frobenius sq conclusion holds.
Formal statement
Proof (Lean source)
Failure of the empirical Rayleigh guard forces a squared Frobenius deviation of at least the squared guard threshold. Given the specified input d, the specified input Q, the specified input B, the specified input hB, the specified input hcut, the gram cutoff sq deviation conclusion holds.
Formal statement
Proof (Lean source)
Population positivity and the rectangular second-moment bound control the probability that the empirical Gram guard fails. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the gram cutoff probability conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.UpperRiskGeometry 8 declarations Rayleigh coercivity, inverse stability, and pointwise clipped-error bounds used in the fixed-tuning risk assembly.
# Geometry of the guarded rectangular estimator Rayleigh coercivity, inverse stability, and pointwise clipped-error bounds used in the fixed-tuning risk assembly.
The unit-vector Rayleigh lower bound extends homogeneously to every vector. Given the specified input d, the specified input Q, the specified input a, the specified input ha, the specified input v, the rayleigh coercivity conclusion holds.
Formal statement
Proof (Lean source)
The guard bounds the squared Euclidean norm of the inverse image by the reciprocal squared threshold. Given the specified input d, the specified input Q, a guard threshold g, its positivity, the specified input hmin, the specified input R, the good branch inverse sq bound conclusion holds.
Formal statement
Proof (Lean source)
Finite Cauchy–Schwarz in Euclidean square-root notation. Given the specified input v, the specified input w, the finite dot abs le conclusion holds.
Formal statement
Proof (Lean source)
On the good branch the projected inverse amplifies a residual by at most the reciprocal guard threshold. Given the specified input d, the specified input Q, the specified input hQ, the specified input hmin, the specified input R, the specified input theta, the specified input r, the good branch projected error conclusion holds.
Formal statement
Proof (Lean source)
The Euclidean square-root norm satisfies the triangle inequality. Given the specified input v, the specified input w, the finite sqrt triangle conclusion holds.
Formal statement
Proof (Lean source)
The Frobenius norm bounds matrix action in the Euclidean norm. Given the specified input E, the specified input v, the finite matrix mul vec sqrt le conclusion holds.
Formal statement
Proof (Lean source)
A sample residual decomposes into vector noise, population bias, and Gram noise. Given the specified input R, the specified input Rbar, the specified input theta, the specified input Q, the specified input Qbar, the rectangular residual sqrt le conclusion holds.
Formal statement
Proof (Lean source)
The good-branch clipped error is controlled by sampling deviations and population bias. Given the specified input d, the specified input n, the specified input m, the specified input D, the specified input h, the specified input J, the specified input theta, the specified input Rbar, the specified input Qbar, the specified input y, the specified input hy, the specified input hcenter, the specified input hgood, the overlap level eps, the t hat good branch error conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.UpperRiskMoments 8 declarations Integrability and Cauchy–Schwarz bounds converting the rectangular second moments into the mean error of the guarded estimator.
# Expected rectangular sampling deviations Integrability and Cauchy–Schwarz bounds converting the rectangular second moments into the mean error of the guarded estimator.
The square root of a nonnegative integrable function is integrable on a finite measure. Given the specified input f, the specified input hf, the specified input hf0, the upper integrable sqrt conclusion holds.
Formal statement
Proof (Lean source)
Cauchy–Schwarz in expectation bounds a mean square root by the square root of its mean. Given the specified input f, the specified input hf, the specified input hf0, the upper integral sqrt le conclusion holds.
Formal statement
Proof (Lean source)
The outcome moment's squared Euclidean deviation is integrable. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input hn, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the r hat square deviation integrable conclusion holds.
Formal statement
Proof (Lean source)
A failed guard is dominated by the Frobenius deviation itself. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input P, the specified input hP, the specified input n, the specified input m, the specified input hn, the specified input h, the specified input hh, the specified input hh', the specified input J, the specified input hJ, the specified input D, the gram cutoff indicator le sqrt conclusion holds.
Formal statement
Proof (Lean source)
Fixed-tuning risk is controlled by population approximation and the square root of the rectangular variance scale. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the rectangular risk sqrt variance conclusion holds.
Formal statement
Proof (Lean source)
The squared inverse square-root rate is the reciprocal scale. Given the specified input x, the specified input hx, the upper inverse half sq conclusion holds.
Formal statement
Proof (Lean source)
Rank and cell-side bookkeeping converts rectangular variance to the stated sampling rates. Given the specified input d, the specified input n, the specified input m, the specified input J, the specified input h, the specified input hn, the specified input hh, the specified input hJ, the rectangular variance sqrt le rates conclusion holds.
Formal statement
Proof (Lean source)
The clipped rectangular estimator attains the fixed-tuning risk envelope uniformly over the primitive class. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the rectangular fixed tuning risk conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Helpers.UpperRiskPointwise 7 declarations Uniform deterministic error envelopes for the rectangular estimator, separating the two sampling deviations, the population bias, and the failed guard.
# Pointwise upper-risk assembly Uniform deterministic error envelopes for the rectangular estimator, separating the two sampling deviations, the population bias, and the failed guard.
The two arm-mean range conditions place the designated contrast in the clipping interval. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input x, the specified input hx, the tau mem clipping interval conclusion holds.
Formal statement
Proof (Lean source)
Clipping, including the zero fallback, always produces an output in the prescribed interval. Given the specified input d, the specified input n, the specified input m, the specified input D, the specified input h, the specified input J, the overlap level eps, the t hat mem clipping interval conclusion holds.
Formal statement
Proof (Lean source)
The absolute error is uniformly bounded by the diameter of the clipping interval. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input D, the specified input h, the specified input J, the t hat absolute error le conclusion holds.
Formal statement
Proof (Lean source)
The localization center is in every positive-bandwidth box. Given the specified input d, the specified input h, the specified input hh, the x0 mem loc cube conclusion holds.
Proof (Lean source)
Uniform pointwise assembly follows from the local polynomial approximation and the causal population-bias bridge. The failed-guard term is kept explicit for the probability bound. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the rectangular pointwise error bound conclusion holds.
Formal statement
Proof (Lean source)
The clipped estimator has finite absolute-loss risk on every primitive-class law. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input h, the specified input J, the specified input hMeas, the t hat risk le diameter conclusion holds.
Formal statement
Proof (Lean source)
The pointwise assembly reduces fixed-tuning risk to the two mean Euclidean deviations and the failed-guard indicator, while retaining a finite uniform cap. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the rectangular risk envelope reduction conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.ComponentHellinger 5 declarations Positive record likelihoods give the component density floor (MC23).
Component Hellinger estimate
Positive record likelihoods give the component density floor (MC23). The square-root identity converts the two-amplitude density difference into the squared Hellinger estimate (MC30–MC31).
A common positive density floor controls squared square-root differences. Given the specified input f, the specified input g, the specified input t, the specified input ht, the specified input hf, the specified input hg, the sqrt difference sq le of floor conclusion holds.
Formal statement
Proof (Lean source)
Small marked amplitudes give every record likelihood a uniform positive floor. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input sigma, the specified input ha, the specified input hb, the specified input he, the specified input hm, the specified input x, the specified input s, the specified input i, the marked record likelihood lower conclusion holds.
Formal statement
Proof (Lean source)
Averaging positive record products preserves the component density floor. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input ha, the specified input hb, the specified input he, the specified input hm, the specified input x, the specified input V, the specified input s, the marked component density lower conclusion holds.
Formal statement
Proof (Lean source)
A bounded density difference and a positive floor imply the integrated Hellinger bound. Given the specified input f, the specified input g, the specified input hf, the specified input hg, the specified input t, the specified input D, the specified input ht, the specified input hD, the specified input hfloor, the specified input hdiff, the density hellinger le of floor conclusion holds.
Formal statement
Proof (Lean source)
The component squared Hellinger estimate retains both nuisance amplitudes, uniformly in the two channel sizes and in the common probability reference. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the marked component hellinger bound conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.ComponentInformation 3 declarations Contrast deletion and cancellation of the common one-channel sign marginals retain both nuisance amplitudes in the component density difference (MC24–MC29).
Component likelihood information bound
Contrast deletion and cancellation of the common one-channel sign marginals retain both nuisance amplitudes in the component density difference (MC24–MC29).
Both sign-array marginals agree between hypotheses, for arbitrary functions of one array. Given the specified input d, the specified input h, the specified input delta, the specified input control, the specified input F, the marked channel marginal expectation conclusion holds.
Formal statement
Proof (Lean source)
Squared channel-product growth is bounded by the full-record growth factor. Given the specified input p, the component channel power bound conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the component information bound conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.ComponentNormalization 7 declarations Each record likelihood integrates to one against fair observed spins.
Normalization of conditional component densities
Each record likelihood integrates to one against fair observed spins. Independent fair spins therefore normalize every selected record product and its finite prior mixture, as required by the MC32 product-distance argument.
A labeled likelihood has total mass one under the two fair reference spins. Given the specified input d, the specified input P, the specified input x, the specified input he, the specified input hm, the label likelihood integral one conclusion holds.
Formal statement
Proof (Lean source)
An auxiliary likelihood has total mass one under a fair treatment spin. Given the specified input d, the specified input P, the specified input x, the specified input he, the auxiliary likelihood integral one conclusion holds.
Formal statement
Proof (Lean source)
A selected product of record likelihoods is normalized by independent fair spins, including when no records are selected. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input x, the specified input V, the specified input he, the specified input hm, the record likelihood product integral one conclusion holds.
Formal statement
Proof (Lean source)
Averaging normalized selected record products over a probability prior gives normalized component densities, even for the empty selected set. Given the specified input d, the specified input n, the specified input m, the specified input H, the specified input theta, the specified input x, the specified input V, the specified input hw, the specified input he, the specified input hm, the component density integral one conclusion holds.
Formal statement
Proof (Lean source)
The prescribed marked construction normalizes every component for every covariate vector; probability clipping supplies valid margins without extra premises. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input x, the specified input V, the marked component density integral one conclusion holds.
Formal statement
Proof (Lean source)
Prior averages of nonnegative record likelihoods are nonnegative densities. Given the specified input d, the specified input n, the specified input m, the specified input H, the specified input theta, the specified input hw, the specified input x, the specified input V, the specified input s, the component density nonneg conclusion holds.
Formal statement
Proof (Lean source)
Each marked component density defines a probability law on the common fair spin reference, supplying the normalization required by Hellinger subadditivity. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input x, the specified input V, the marked component density probability conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.ComponentProduct 9 declarations Finite spin coordinates may have different types in the labeled and auxiliary channels.
Hellinger assembly over independent finite coordinate blocks
Finite spin coordinates may have different types in the labeled and auxiliary channels. Regrouping their product weights proves affinity tensorization over components, the finite-product step of MC32.
Regroup a dependent finite product distribution by the owner of each coordinate. Given the specified input S, the specified input owner, the specified input w, the specified input G, the finite dependent fiber weighted sum conclusion holds.
Formal statement
Proof (Lean source)
Expectations multiply for functions of disjoint coordinate blocks, including empty blocks. Given the specified input S, the specified input owner, the specified input w, the specified input hw, the specified input F, the specified input hF, the finite dependent fiber expectation factorization conclusion holds.
Formal statement
Proof (Lean source)
A finite product reference with coordinate measures μ integrates block-dependent functions multiplicatively. Given the specified input S, the specified input owner, the specified input F, the specified input hF, the integral finite block product conclusion holds.
Formal statement
Proof (Lean source)
Affinity tensorizes across disjoint blocks of a finite product reference with coordinate measures μ. Given the specified input S, the specified input owner, the specified input f, the specified input g, the specified input hf0, the specified input hg0, the specified input hf, the specified input hg, the density affinity finite blocks conclusion holds.
Formal statement
Proof (Lean source)
Normalized component densities combine by Hellinger subadditivity on their actual shared spin space with coordinate measures μ, provided they use disjoint coordinate blocks. Given the specified input S, the specified input owner, the specified input f, the specified input g, the specified input hf0, the specified input hg0, the specified input hf1, the specified input hg1, the specified input hf, the specified input hg, the density hellinger finite blocks le sum conclusion holds.
Formal statement
Proof (Lean source)
A selected component density depends only on its selected record spins. Given the specified input d, the specified input n, the specified input m, the specified input H, the specified input theta, the specified input x, the specified input V, the specified input s, the specified input t, the specified input hl, the specified input ha, the component density spin congr conclusion holds.
Formal statement
Proof (Lean source)
The marked conditional Hellinger discrepancy is at most the sum of the component discrepancies (the tensorization part of MC32). No extra independence assumption is needed: the fair reference spins are independent by construction. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input hd, the specified input hdh, the specified input hh, the specified input x, the specified input hx, the marked conditional hellinger le component sum conclusion holds.
Formal statement
Proof (Lean source)
A component sum regrouped by size counts exactly the informative components. Given the specified input size, the specified input info, the specified input N, the specified input hsize, the specified input W, the finite size weighted count conclusion holds.
Formal statement
Proof (Lean source)
MC32 before integration over covariates: only components of size at least two containing a label contribute, and they are grouped by their exact size. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the marked conditional hellinger count bound conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.Components 27 declarations Two-channel point-CATE annotation frontier: Lower/Components constructions and obligations.
Lower/Components
Two-channel point-CATE annotation frontier: Lower/Components constructions and obligations.
Given the specified input x, the specified input xp, max dist is the corresponding construction.
Given the specified input h, the specified input delta, the specified input x, the specified input i, the specified input j, record adj is the corresponding construction.
Given the specified input x, the specified input xp, the max dist comm conclusion holds.
Proof (Lean source)
Given the specified input h, the specified input delta, the specified input x, the record adj symmetric conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input h, the specified input delta, the specified input x, the record adj irreflexive conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input h, the specified input delta, the specified input x, record graph is the corresponding construction.
Definition (Lean source)
For bandwidth h, proximity radius δ, and the covariate record x, the connected components of the record graph form a finite type.
Definition (Lean source)
Given the specified input h, the specified input delta, the specified input x, the specified input c, component vertices is the corresponding construction.
Definition (Lean source)
Given the specified input H, the specified input theta, the specified input x, the specified input V, the specified input s, component density is the corresponding construction.
Definition (Lean source)
Explicit conditional factorization over the covariate proximity graph. Given the specified input H, the specified input h, the specified input delta, the specified input n, the specified input m, conditional factorization is the corresponding construction.
Definition (Lean source)
The uninformative components have identical full conditional laws, expressed in their fair-spin densities. Given the specified input H, the specified input h, the specified input delta, the specified input n, the specified input m, uninformative components agree is the corresponding construction.
Definition (Lean source)
Telescoping a product of bounded factors controls its perturbation by the sum of the factor perturbations, including the empty product. Given the specified input V, the specified input f, the specified input g, the specified input M, the specified input hM, the specified input hf, the specified input hg, the finite product perturbation bound conclusion holds.
Formal statement
Proof (Lean source)
A product of small perturbations of one keeps the amplitude as a factor. Given the specified input V, the specified input f, the specified input M, the specified input D, the specified input hM, the specified input hf, the specified input hD, the finite product deviation bound conclusion holds.
Formal statement
Proof (Lean source)
Averaging over a finite probability prior preserves a uniform absolute bound. Given the specified input S, the specified input w, the specified input F, the specified input hw, the specified input hmass, the specified input D, the specified input hF, the finite prior absolute bound conclusion holds.
Formal statement
Proof (Lean source)
Equal one-channel marginals cancel, leaving only the product of the two centered channel factors in the difference between mixture expectations (MC27). Given the specified input S, the specified input wplus, the specified input wminus, the specified input A, the specified input B, the specified input hp, the specified input hm, the specified input hA, the specified input hB, the finite prior common marginals cancel conclusion holds.
Formal statement
Proof (Lean source)
The difference of two finite mixture expectations retains both channel amplitudes when their separate marginals agree (MC27--MC28). Given the specified input S, the specified input wplus, the specified input wminus, the specified input A, the specified input B, the specified input hwp, the specified input hwm, the specified input hp, the specified input hm, the specified input hA, the specified input hB, the specified input UA, the specified input UB, the specified input hUA, the specified input hUB, the specified input hAb, the specified input hBb, the finite prior two channel bound conclusion holds.
Formal statement
Proof (Lean source)
Two product channels with common marginal expectations retain the product of their factor amplitudes, rather than either amplitude alone. Given the specified input S, the specified input V, the specified input W, the specified input f, the specified input g, the specified input wplus, the specified input wminus, the specified input hwp, the specified input hwm, the specified input hp, the specified input hm, the specified input hA, the specified input hB, the specified input M, the specified input DA, the specified input DB, the specified input hM, the specified input hDA, the specified input hDB, the specified input hf, the specified input hg, the specified input hfd, the specified input hgd, the finite prior product channel bound conclusion holds.
Formal statement
Proof (Lean source)
Adding the two contrast-deletion errors to the centered channel bound assembles the finite-mixture information estimate of MC26--MC29. Given the specified input S, the specified input wplus, the specified input wminus, the specified input A, the specified input B, the specified input Fplus, the specified input Fminus, the specified input hwp, the specified input hwm, the specified input hp, the specified input hm, the specified input hA, the specified input hB, the specified input UA, the specified input UB, the specified input Dplus, the specified input Dminus, the specified input hUA, the specified input hUB, the specified input hAb, the specified input hBb, the specified input hdelp, the specified input hdelm, the finite prior contrast deletion bound conclusion holds.
Formal statement
Proof (Lean source)
Regrouping independent sign coordinates by their owner factors a finite weighted sum. Given the specified input S, the specified input owner, the specified input w, the specified input G, the finite fiber weighted sum conclusion holds.
Formal statement
Proof (Lean source)
Expectations of functions depending on separate coordinate blocks multiply under a normalized product prior. Given the specified input S, the specified input owner, the specified input w, the specified input hw, the specified input F, the specified input hF, the finite fiber expectation factorization conclusion holds.
Formal statement
Proof (Lean source)
A nonzero frame is supported inside the localization cube and one grid radius. Given the specified input d, the specified input h, the specified input delta, the specified input hh, the specified input z, the specified input x, the specified input hx, the frame nonzero support conclusion holds.
Formal statement
Proof (Lean source)
At a record, only the sign pairs of its nonzero frames affect the likelihood. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input x, the specified input s, the specified input i, the specified input sigma, the specified input sigma', the specified input hs, the record likelihood active signs conclusion holds.
Formal statement
Proof (Lean source)
Disjoint active frame blocks factor the conditional likelihood across graph components. Given the specified input d, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input hd, the specified input hdh, the specified input hh, the specified input n, the specified input m, the marked conditional factorization conclusion holds.
Formal statement
Proof (Lean source)
An auxiliary likelihood ignores the flipped outcome signs and hypothesis index. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input sigma, the specified input x, the specified input s, the specified input i, the specified input hi, the auxiliary record likelihood flip conclusion holds.
Formal statement
Proof (Lean source)
A component containing only auxiliary records has the same density under both sign priors. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input x, the specified input V, the specified input hV, the specified input s, the auxiliary component density equality conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the uninformative component equality conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.FrameRegularity 9 declarations Uniform low-order Hölder bounds for the signed, locally supported tensor frames.
Uniform low-order Hölder bounds for the signed, locally supported tensor frames.
The piecewise frame equals a globally smooth product of two transition factors. Given the specified input z, the specified input t, the frame1d product conclusion holds.
Formal statement
Proof (Lean source)
Translations of the fixed smooth frame share a single Lipschitz constant. the frame1d uniform lipschitz conclusion holds.
Formal statement
Proof (Lean source)
Products of unit-bounded factors have a telescoping difference bound. Given the specified input s, the specified input f, the specified input g, the specified input hf, the specified input hg, the unit product difference le conclusion holds.
Formal statement
Proof (Lean source)
The dilated macro bump has a dimension-only Lipschitz bound at scale h. Given the specified input d, the macro bump uniform lipschitz conclusion holds.
Formal statement
Proof (Lean source)
Each tensor frame has a Lipschitz bound uniform over its integer translate. Given the specified input d, the frame uniform lipschitz conclusion holds.
Formal statement
Proof (Lean source)
Bounded overlap at the two endpoints controls signed-frame differences independently of grid size. Given the specified input d, the sign field uniform lipschitz conclusion holds.
Formal statement
Proof (Lean source)
A coordinate partial of total order zero is the original function. Given the specified input d, the specified input f, the specified input hk, the specified input x, the coordinate partial order zero conclusion holds.
Formal statement
Proof (Lean source)
A bounded field with a scale-dependent Lipschitz bound has the corresponding fractional Hölder norm. Given the specified input d, the specified input f, the specified input s, the specified input delta, the specified input B, the specified input K, the specified input hs, the specified input hs1, the specified input hd, the specified input hd1, the specified input hB, the specified input hK, the specified input hb, the specified input hlip, the bounded lipschitz scaled holder conclusion holds.
Formal statement
Proof (Lean source)
Signed frames obey the prescribed exact Hölder norm uniformly in the sign array and grid size. Given the specified input d, the specified input s, the specified input hs, the specified input hs', the sign field holder conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.Frames 40 declarations Two-channel point-CATE annotation frontier: Lower/Frames constructions and obligations.
Lower/Frames
Two-channel point-CATE annotation frontier: Lower/Frames constructions and obligations.
Given the specified input theta, theta sign is the corresponding construction.
Definition (Lean source)
Given the specified input t, flat exp is the corresponding construction.
Definition (Lean source)
Given the specified input t, frame angle is the corresponding construction.
Definition (Lean source)
Given the specified input z, the specified input t, frame1d is the corresponding construction.
Definition (Lean source)
Given the specified input h, the specified input x, macro bump is the corresponding construction.
Given the specified input h, the specified input delta, grid radius is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input h, the specified input delta, frame idx is the corresponding construction.
Given the specified input h, the specified input delta, the specified input z, the specified input x, frame is the corresponding construction.
Given the specified input d, the specified input h, the specified input delta, sign array is the corresponding construction.
Given the specified input h, the specified input delta, the specified input sigma, the specified input control, the specified input x, sign field is the corresponding construction.
the measurable flat exp conclusion holds.
Formal statement
Proof (Lean source)
the measurable frame angle conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input z, the measurable frame1d conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input h, the measurable macro bump conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input h, the specified input delta, the specified input z, the measurable frame conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input h, the specified input delta, the specified input sigma, the specified input control, the measurable sign field conclusion holds.
Formal statement
Proof (Lean source)
The flat exponential is nonnegative, including on its zero branch. Given the specified input t, the flat exp nonneg conclusion holds.
Formal statement
Proof (Lean source)
The normalizing value of the macro bump is strictly positive. the flat exp one pos conclusion holds.
Formal statement
Below one, the flat exponential is bounded by its normalizing value. Given the specified input t, the specified input ht, the flat exp le one value conclusion holds.
Every normalized coordinate factor lies in the unit interval. Given the specified input t, the macro bump factor mem conclusion holds.
Proof (Lean source)
The tensor macro bump has values between zero and one in every dimension. Given the specified input h, the specified input x, the macro bump mem conclusion holds.
Formal statement
Proof (Lean source)
The macro bump is normalized to one at the interior target point. Given the specified input h, the macro bump at x0 conclusion holds.
Proof (Lean source)
A frame vanishes at and beyond the left end of its support. Given the specified input z, the specified input t, the specified input ht, the frame1d zero left conclusion holds.
Formal statement
Proof (Lean source)
A frame vanishes at and beyond the right end of its support. Given the specified input z, the specified input t, the specified input ht, the frame1d zero right conclusion holds.
Formal statement
Proof (Lean source)
On one grid interval the two adjacent frames are the cosine and sine pair. Given the specified input j, the specified input t, the specified input hl, the specified input hu, the frame1d adjacent square conclusion holds.
Formal statement
Proof (Lean source)
Only the two frames adjacent to the integer floor can contribute. Given the specified input t, the specified input z, the specified input hz, the frame1d zero of not adjacent conclusion holds.
Formal statement
Proof (Lean source)
Each one-dimensional frame is bounded in absolute value by one. Given the specified input z, the specified input t, the abs frame1d le one conclusion holds.
Formal statement
Proof (Lean source)
Tensor frames inherit the macro bump's unit bound. Given the specified input h, the specified input delta, the specified input z, the specified input x, the abs frame le one conclusion holds.
Formal statement
Proof (Lean source)
Only the two adjacent indices in each coordinate can support a tensor frame. Given the specified input h, the specified input delta, the specified input z, the specified input x, the specified input hz, the frame zero of not coordinate adjacent conclusion holds.
Formal statement
Proof (Lean source)
The signed tensor field is uniformly bounded by the number of adjacent tensor indices. Given the specified input h, the specified input delta, the specified input sigma, the specified input control, the specified input x, the abs sign field le conclusion holds.
Formal statement
Proof (Lean source)
Any finite index set containing the adjacent pair has squared-frame sum one. Given the specified input s, the specified input t, the specified input h0, the specified input h1, the frame1d square sum conclusion holds.
Formal statement
Proof (Lean source)
The finite grid contains both adjacent frames whenever the argument is in its interior. Given the specified input R, the specified input t, the specified input hl, the specified input hu, the frame1d grid square sum conclusion holds.
Formal statement
Proof (Lean source)
Outside its localization cube the macro bump is identically zero. Given the specified input h, the specified input hh, the specified input x, the specified input hx, the macro bump zero outside conclusion holds.
Formal statement
Proof (Lean source)
An index failing the geometric support filter has a zero tensor frame at a cube point. Given the specified input h, the specified input delta, the specified input x, the specified input hx, the specified input z, the specified input hz, the frame tensor zero of filter conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input h, the specified input delta, the specified input hh, the specified input hh', the specified input hd, the specified input hdh, the specified input x, the frame square partition conclusion holds.
Formal statement
Proof (Lean source)
The prescribed flat exponential is Mathlib's smooth glue function. the flat exp eq glue conclusion holds.
Formal statement
Proof (Lean source)
For bandwidth h, the fixed macro bump is globally smooth, including its support boundary.
Formal statement
Proof (Lean source)
The fixed macro bump has compact support. Given the specified input d, the macro bump compact support conclusion holds.
Formal statement
Proof (Lean source)
Dilation of the fixed centered macro profile is exactly the prescribed bump. Given the specified input h, the specified input x, the macro bump dilation conclusion holds.
Formal statement
Given the specified input d, the specified input s, the specified input hs, the specified input hs', the macro square holder conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.FuzzyBlockTesting 22 declarations Transport the cited product-experiment testing inequality to a single observation consisting of the entire original-record dataset, with its randomizer included.
Fuzzy testing on one full data block
Transport the cited product-experiment testing inequality to a single observation consisting of the entire original-record dataset, with its randomizer included. The finite-prior identities preserve the marked information bound under this randomization and express the two mixtures using a common product prior.
Squared Hellinger distance is invariant under a measurable embedding. Given the specified input B, the specified input C, the specified input f, the specified input hf, the hellinger sq map embedding conclusion holds.
Formal statement
Proof (Lean source)
Replicating a value in a singleton coordinate is a measurable embedding. the measurable embedding singleton coordinate conclusion holds.
Formal statement
Proof (Lean source)
A singleton product is the image of its only coordinate law. Given the specified input P, the pi one eq map constant conclusion holds.
Formal statement
Proof (Lean source)
One-coordinate product experiments have the original Hellinger distance. Given the specified input B, the specified input C, the hellinger sq pi one conclusion holds.
Formal statement
Proof (Lean source)
Mixing singleton experiments commutes with their constant-coordinate encoding. Given the specified input Z, the specified input K, the bind pi one eq map conclusion holds.
Formal statement
Proof (Lean source)
The cited fuzzy-testing result applies to one entire data block and every measurable decision on that block, without an additional independence assumption. Given the specified input Z, the specified input B, the specified input C, the specified input Model, the specified input hB, the specified input hC, the specified input s, the specified input u, the specified input hs, the specified input hu, the specified input hu2, the specified input hsep, the specified input hhell, the specified input T, the specified input hT, the published fuzzy testing block conclusion holds.
Formal statement
Proof (Lean source)
A testing bound on the image of an indexed model class bounds its original minimax risk when the target is well defined on the experiment laws. Given the specified input Z, the specified input B, the specified input C, the specified input E, the specified input target, the specified input hTarget, the specified input hB, the specified input hC, the specified input s, the specified input u, the specified input hs, the specified input hu, the specified input hu2, the specified input hsep, the specified input hhell, the published fuzzy testing minimax conclusion holds.
Formal statement
Proof (Lean source)
At the certificate's Hellinger budget, the testing overlap is at least three quarters. the fuzzy testing overlap sixteenth conclusion holds.
Formal statement
The prescribed finite marked mixture has unit mass. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the marked mixture probability conclusion holds.
Formal statement
Proof (Lean source)
Appending the same randomizer commutes with the marked finite prior. Given the specified input d, the specified input n, the specified input m, the specified input H, the specified input theta, the marked mixture prod randomizer conclusion holds.
Formal statement
Proof (Lean source)
The marked information bound holds unchanged on randomized original records. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the marked mixture randomized hellinger conclusion holds.
Formal statement
Proof (Lean source)
The first family under the product prior has exactly its own prior mixture. Given the specified input Z, the specified input W, the specified input K, the bind product prior fst conclusion holds.
Formal statement
Proof (Lean source)
The second family under the product prior has exactly its own prior mixture. Given the specified input Z, the specified input W, the specified input K, the bind product prior snd conclusion holds.
Formal statement
Proof (Lean source)
Each prescribed finite sign prior is a probability measure. Given the specified input d, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the sign prior marked probability conclusion holds.
Formal statement
Proof (Lean source)
A finite atomic prior mixed through a kernel is its weighted sum of laws. Given the specified input d, the specified input H, the specified input theta, the specified input K, the sign prior bind kernel conclusion holds.
Formal statement
Proof (Lean source)
The finite family of full original-record experiments is a measurable kernel. Given the specified input d, the specified input H, the specified input theta, the specified input n, the specified input m, marked experiment kernel is the corresponding construction.
Definition (Lean source)
Every member of the full randomized experiment kernel is a probability law. Given the specified input d, the specified input H, the specified input theta, the specified input n, the specified input m, the marked experiment kernel markov conclusion holds.
Formal statement
Proof (Lean source)
Mixing the full experiment kernel appends exactly the common randomizer to its original-record marked mixture. Given the specified input d, the specified input H, the specified input theta, the specified input n, the specified input m, the sign prior bind marked experiment conclusion holds.
Formal statement
Proof (Lean source)
The product of the two prescribed sign priors is one common probability prior for the two full-block families in the cited testing theorem. Given the specified input d, the specified input h, the specified input delta, the specified input a, the specified input b, the marked common prior probability conclusion holds.
Formal statement
Proof (Lean source)
Both families under the common product prior have precisely the randomized marked mixtures prescribed by the lower-bound construction. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the marked common prior mixtures conclusion holds.
Formal statement
Proof (Lean source)
The common product prior preserves the exact marked Hellinger distance, including the independent randomizer. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the marked common prior hellinger conclusion holds.
Formal statement
Proof (Lean source)
Once the causal target is represented on the full experiment laws, the cited fuzzy test gives a minimax bound for the unchanged primitive class. Only values on the two marked families are needed from that representation. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input ha, the specified input hb, the specified input hMembers, the specified input hTargets, the target representation Ψ, its agreement on the marked families, the specified input hhell, the marked fuzzy testing minimax conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.Likelihood 35 declarations Two-channel point-CATE annotation frontier: Lower/Likelihood constructions and obligations.
Lower/Likelihood
Two-channel point-CATE annotation frontier: Lower/Likelihood constructions and obligations.
Given the specified input P, the specified input x, conditional observed is the corresponding construction.
Given the specified input H, the specified input theta, the specified input x, singleton mixture is the corresponding construction.
Definition (Lean source)
Given the specified input H, the specified input theta, the specified input k, auxiliary mixture is the corresponding construction.
Given the specified input H, the specified input theta, the specified input k, the specified input x, conditional auxiliary mixture is the corresponding construction.
fair observed is the corresponding construction.
Given the specified input P, the specified input x, the specified input s, label likelihood is the corresponding construction.
Given the specified input P, the specified input x, the specified input s, auxiliary likelihood is the corresponding construction.
Definition (Lean source)
Given the specified input n, the specified input m, record spins is the corresponding construction.
Given the specified input x, the specified input xt, record covariates is the corresponding construction.
Given the specified input P, the specified input x, the specified input s, record likelihood is the corresponding construction.
Definition (Lean source)
Given the specified input H, the specified input theta, the specified input x, the specified input s, mixed density is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input h, the specified input delta, the specified input theta, the marked prior mass conclusion holds.
Formal statement
Proof (Lean source)
Flip every outcome sign while retaining every propensity sign. Given the specified input d, the specified input h, the specified input delta, flip outcome signs is the corresponding construction.
Definition (Lean source)
The sign flip transports the positive prior weights to the negative weights. Given the specified input d, the specified input h, the specified input delta, the specified input sigma, the marked weight flip outcome signs conclusion holds.
Formal statement
Proof (Lean source)
The designated propensity ignores outcome signs and the hypothesis index. Given the specified input d, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input sigma, the marked propensity flip outcome signs conclusion holds.
Formal statement
Proof (Lean source)
The treatment-record law depends only on the propensity, with the same uniform design. Given the specified input d, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input sigma, the marked xa law flip outcome signs conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input k, the auxiliary only equality conclusion holds.
Formal statement
Proof (Lean source)
Finite product weights turn expectations of coordinate products into products of scalar sums. Given the specified input S, the specified input w, the specified input f, the finite product weighted sum conclusion holds.
Formal statement
Proof (Lean source)
A normalized finite product prior has the prescribed scalar marginal at a coordinate. Given the specified input S, the specified input w, the specified input hw, the specified input z, the specified input f, the finite product coordinate sum conclusion holds.
Formal statement
Proof (Lean source)
Each propensity or outcome sign has mean zero under the prescribed sign-pair prior. Given the specified input d, the specified input h, the specified input delta, the specified input theta, the specified input control, the specified input z, the marked sign mean zero conclusion holds.
Formal statement
Proof (Lean source)
Sign-pair correlation is one half the hypothesis sign at matching indices and zero otherwise. Given the specified input d, the specified input h, the specified input delta, the specified input theta, the specified input z, the specified input w, the marked sign cross moment conclusion holds.
Formal statement
Proof (Lean source)
Both signed frame fields have zero prior mean. Given the specified input d, the specified input h, the specified input delta, the specified input theta, the specified input control, the specified input x, the marked field mean zero conclusion holds.
Formal statement
Proof (Lean source)
The frame partition identifies the prior cross moment of the two signed fields. Given the specified input d, the specified input h, the specified input delta, the specified input hd, the specified input hdh, the specified input hh, the specified input theta, the specified input x, the marked field cross moment conclusion holds.
Formal statement
Proof (Lean source)
Compensation cancels the cross moment in the raw singleton likelihood, including its cubic term. Given the specified input d, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input hd, the specified input hdh, the specified input hh, the specified input theta, the specified input u, the specified input v, the specified input x, the marked raw singleton cancellation conclusion holds.
Formal statement
Proof (Lean source)
The zero-order partial in the Hölder norm bounds the function on the design cube. Given the specified input d, the specified input f, the specified input s, the specified input K, the specified input hK, the specified input hf, the specified input x, the specified input hx, the holder norm sup bound conclusion holds.
Formal statement
Proof (Lean source)
A scale-controlled amplitude cancels the inverse scale in a Hölder supremum bound. Given the specified input r, the specified input s, the specified input c, the specified input K, the specified input a, the specified input f, the specified input hr, the specified input hc, the specified input hK, the specified input ha0, the specified input ha, the specified input hf, the holder scaled amplitude bound conclusion holds.
Formal statement
Proof (Lean source)
The frame field vanishes outside the design cube for an admissible localization window. Given the specified input h, the specified input delta, the specified input hh0, the specified input hh, the specified input sigma, the specified input control, the specified input x, the specified input hx, the sign field zero outside cube conclusion holds.
Formal statement
Proof (Lean source)
The macro bump vanishes outside the design cube for an admissible localization window. Given the specified input h, the specified input hh0, the specified input hh, the specified input x, the specified input hx, the macro bump zero outside cube conclusion holds.
Formal statement
Proof (Lean source)
A public positive amplitude constant keeps the raw propensity and arm means in the unit interval. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the marked raw probability bounds conclusion holds.
Formal statement
Proof (Lean source)
A valid Bernoulli atom equals its affine fair-spin likelihood divided by two. Given the specified input p, the specified input hp, the specified input s, the bern singleton to real spin conclusion holds.
Formal statement
For valid raw probabilities the marked label likelihood is the compensated two-spin product. Given the specified input d, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input sigma, the specified input x, the specified input hp, the specified input hm, the specified input s, the marked label likelihood spin conclusion holds.
Formal statement
Proof (Lean source)
The conditional observed atom factors into its treatment and selected outcome atoms. Given the specified input d, the specified input P, the specified input x, the specified input s, the conditional observed singleton conclusion holds.
Formal statement
Proof (Lean source)
Each Bernoulli atom has finite mass, including for total raw inputs. Given the specified input p, the specified input s, the bern singleton ne top conclusion holds.
Proof (Lean source)
The fair-spin density of a singleton mixture is its prior-weighted label likelihood. Given the specified input d, the specified input H, the specified input theta, the specified input hw, the specified input x, the specified input s, the singleton mixture density conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the singleton cancellation conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.MarkedHandle 41 declarations Two-channel point-CATE annotation frontier: Lower/MarkedHandle constructions and obligations.
Lower/MarkedHandle
Two-channel point-CATE annotation frontier: Lower/MarkedHandle constructions and obligations.
Total Bernoulli probability parametrization; equal to its argument on [0,1]. Given the specified input x, probability clip is the corresponding construction.
Given the specified input e, the specified input mu0, the specified input mu1, independent full law is the corresponding construction.
Definition (Lean source)
Given the specified input f, the specified input hf, the measurable probability clip conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input x, the probability clip mem conclusion holds.
Formal statement
Proof (Lean source)
Probability clipping fixes every valid Bernoulli parameter. Given the specified input x, the specified input hx, the probability clip eq of mem conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the measurable cube conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the uniform law probability conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input p, the specified input hp, the bern probability conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input e, the specified input mu0, the specified input mu1, the specified input he, the specified input h0, the specified input h1, the measurable independent record kernel conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input e, the specified input mu0, the specified input mu1, the specified input he, the specified input h0, the specified input h1, the independent full law probability conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input e, the specified input mu0, the specified input mu1, the specified input he, the specified input h0, the specified input h1, the independent full law support conclusion holds.
Formal statement
Proof (Lean source)
Given the measure μ, the kernel κ, the map f, kernel measurability, and map measurability, mapping a bind equals binding the mapped kernels.
Proof (Lean source)
Given the specified input d, the specified input e, the specified input mu0, the specified input mu1, the specified input he, the specified input h0, the specified input h1, the independent full law covariates conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input p, the specified input hp, the measurable bern record conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input p, the specified input hp, the specified input hprob, the bern record bind eq comp prod conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input x, the specified input e, the specified input p, the specified input q, the specified input he, the specified input hp, the specified input hq, the independent record margins conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input e, the specified input mu0, the specified input mu1, the specified input he, the specified input h0, the specified input h1, the independent full law margin conclusion holds.
Formal statement
Proof (Lean source)
Explicit independent potential-outcome extension, total even for inadmissible raw inputs. Given the specified input e, the specified input mu0, the specified input mu1, the specified input he, the specified input h0, the specified input h1, independent primitive is the corresponding construction.
Definition (Lean source)
Concrete finite sign-pair prior data. No certificate fields are assumed.
Given the specified input h, the specified input a, the specified input b, the specified input theta, the specified input x, marked contrast is the corresponding construction.
Given the specified input h, the specified input delta, the specified input a, the specified input sigma, the specified input x, marked propensity is the corresponding construction.
Given the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input arm, the specified input sigma, the specified input x, marked mean is the corresponding construction.
The marked arm functions differ by the prescribed contrast before probability clipping. Given the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input sigma, the specified input x, the marked mean difference conclusion holds.
Formal statement
Proof (Lean source)
The contrast is bounded by twice the product of the nuisance amplitudes. Given the specified input h, the specified input a, the specified input b, the specified input theta, the specified input x, the specified input ha, the specified input hb, the abs marked contrast le conclusion holds.
Formal statement
Proof (Lean source)
The target value is exact, since the macro bump is one at the center. Given the specified input h, the specified input a, the specified input b, the specified input theta, the marked contrast at x0 conclusion holds.
Formal statement
Proof (Lean source)
The two hypotheses have target separation four times the amplitude product. Given the specified input h, the specified input a, the specified input b, the specified input ha, the specified input hb, the marked contrast separation conclusion holds.
Formal statement
Proof (Lean source)
The contrast vanishes off the localization cube. Given the specified input h, the specified input a, the specified input b, the specified input theta, the specified input hh, the specified input x, the specified input hx, the marked contrast zero outside conclusion holds.
Formal statement
Proof (Lean source)
A uniformly small propensity amplitude guarantees overlap for every sign array. Given the specified input h, the specified input delta, the specified input a, the specified input sigma, the specified input ha, the specified input hsmall, the specified input x, the marked propensity overlap conclusion holds.
Formal statement
Proof (Lean source)
Uniform field and contrast bounds put both marked arms in the required interior band. Given the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input arm, the specified input sigma, the specified input ha, the specified input hb, the specified input hsmall, the specified input x, the marked mean interior conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input h, the specified input delta, the specified input a, the specified input sigma, the measurable marked propensity conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input arm, the specified input sigma, the measurable marked mean conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input sigma, marked law is the corresponding construction.
Definition (Lean source)
Under the overlap amplitude condition the law's treatment margin is the prescribed field. Given the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input sigma, the specified input ha, the specified input hsmall, the specified input x, the marked law propensity eq conclusion holds.
Formal statement
Proof (Lean source)
Under the interior amplitude condition both law margins are the prescribed arm functions. Given the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input sigma, the specified input ha, the specified input hb, the specified input hsmall, the specified input x, the marked law means eq conclusion holds.
Formal statement
Proof (Lean source)
The independent primitive's effect is the compensated contrast when clipping is inactive. Given the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input sigma, the specified input ha, the specified input hb, the specified input hsmall, the marked law raw contrast eq conclusion holds.
Formal statement
Proof (Lean source)
The constructed primitive satisfies the overlap condition at level eps and the two mean-range conditions at small amplitudes. Given the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input sigma, the specified input ha, the specified input hb, the specified input he, the specified input hm, the overlap level eps, its positivity, the overlap amplitude bound, the marked law probability bands conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input h, the specified input delta, the specified input theta, the specified input sigma, marked weight is the corresponding construction.
Given the specified input d, the specified input h, the specified input delta, the specified input a, the specified input b, marked handle is the corresponding construction.
Definition (Lean source)
Given the specified input H, prior sign is the corresponding construction.
Definition (Lean source)
Given the specified input H, the specified input theta, sign prior is the corresponding construction.
Given the specified input H, the specified input theta, the specified input n, the specified input m, marked mixture is the corresponding construction.
Definition (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.MarkedMembership 3 declarations Membership of the finite marked priors and identification of their canonical contrasts.
Membership of the finite marked priors and identification of their canonical contrasts.
An admissible raw witness has the same contrast as the canonical continuous versions. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input hu, the specified input h0, the specified input ht, the specified input hi0, the specified input hi1, the tau eq raw contrast of admissible conclusion holds.
Formal statement
Proof (Lean source)
Amplitude restrictions cancel the inverse Hölder scale. Given the specified input x, the specified input s, the specified input a, the specified input c, the specified input hx, the specified input ha, the amplitude inverse scale bound conclusion holds.
Formal statement
Proof (Lean source)
Every prescribed marked law belongs to the exact primitive class at uniformly small amplitudes. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the marked membership conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.MixtureDensity 22 declarations The independent potential-outcome kernels yield the conditional likelihoods used in the marked-component information calculation.
# Original-record likelihood densities The independent potential-outcome kernels yield the conditional likelihoods used in the marked-component information calculation.
Given the specified input e, the specified input p, the specified input q, the specified input hp, the specified input hq, the observed bern product conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input e, the specified input p, the specified input q, the specified input he, the specified input hp, the specified input hq, the independent obs law conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input X, the specified input S, the reference measure ν, the finite measure μ, the kernel κ, its measurability, the specified input f, the specified input hf, the specified input hf0, the density representation, the finite joint density conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the measurable label likelihood conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input x, the conditional observed density conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input x, the auxiliary likelihood density conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the measurable auxiliary likelihood conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input e, the specified input p, the specified input q, the specified input he, the specified input hp, the specified input hq, the independent obs law density conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input e, the specified input p, the specified input q, the specified input he, the specified input hp, the specified input hq, the independent xa law density conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input p, the specified input hp, the specified input s, the bern atom le one conclusion holds.
Given the specified input d, the specified input e, the specified input p, the specified input q, the specified input he, the specified input hp, the specified input hq, the independent likelihood bounds conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input e, the specified input p, the specified input q, the specified input he, the specified input hp, the specified input hq, the independent likelihood integrable conclusion holds.
Formal statement
Proof (Lean source)
Reference records have the common uniform design and independent fair spins. Given the specified input d, the specified input n, the specified input m, fair dataset is the corresponding construction.
Definition (Lean source)
Concatenate the covariates of the original labeled and auxiliary records. Given the specified input d, the specified input n, the specified input m, the specified input D, dataset covariates is the corresponding construction.
Definition (Lean source)
Retain the two observed bits in labeled records and the treatment bit in auxiliaries. Given the specified input d, the specified input n, the specified input m, the specified input D, dataset spins is the corresponding construction.
Definition (Lean source)
The original-record mixture likelihood is the conditional mixed likelihood. Given the specified input d, the specified input n, the specified input m, the specified input H, the specified input theta, the specified input D, dataset density is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input D, the dataset record product conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input H, the specified input theta, the measurable dataset density conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input H, the specified input theta, the specified input hw, the specified input D, the dataset density nonneg conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input e, the specified input p, the specified input q, the specified input he, the specified input hp, the specified input hq, the independent dataset density conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input S, the specified input Q, the specified input w, the specified input f, the specified input hw, the specified input hf, the specified input hf0, the specified input hQ, the finite prior with density conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the marked mixture density conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.MixtureInformation 16 declarations Reorder the original records into covariates and spins, integrate the conditional component bound, and apply the labeled-root tree series.
# Unconditional marked information Reorder the original records into covariates and spins, integrate the conditional component bound, and apply the labeled-root tree series.
Regroup four blocks by exchanging the middle two. Given the specified input A, the specified input B, the specified input C, the specified input D, regroup four equiv is the corresponding construction.
Definition (Lean source)
Given the specified input A, the specified input B, the specified input C, the specified input D, the specified input a, the specified input b, the specified input c, the specified input d, the regroup four measure preserving conclusion holds.
Formal statement
Proof (Lean source)
Covariate arrays split at the labeled sample size. Given the specified input d, the specified input n, the specified input m, covariate concat equiv is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input n, the specified input m, the covariate concat measure preserving conclusion holds.
Formal statement
Proof (Lean source)
A measurable reordering separates all covariates from all observed spins. Given the specified input d, the specified input n, the specified input m, dataset split equiv is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input D, the dataset split apply conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the dataset split measure preserving conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the fair dataset probability conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the specified input x, the specified input s, the marked mixed density bounds conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input H, the specified input theta, the measurable mixed density conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the marked dataset density integrable conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input theta, the marked mixture finite conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the marked sqrt difference integrable conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input a, the specified input b, the marked mixture hellinger eq integral conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input N, the specified input f, the specified input hf, the sum sizes le shifted range conclusion holds.
Formal statement
Proof (Lean source)
Integrating MC32 and the labeled-root count series proves MC37 for the original records. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the marked information bound conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.NuisanceConverse 1 declarations Two-channel point-CATE annotation frontier: Lower/NuisanceConverse constructions and obligations.
Lower/NuisanceConverse
Two-channel point-CATE annotation frontier: Lower/NuisanceConverse constructions and obligations.
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input hS, the nuisance frontier converse conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.NuisanceScales 9 declarations The prescribed bandwidth, cell side and nuisance amplitudes satisfy the geometric, occupancy and information identities in the converse roadmap.
Scales for the nuisance-frontier converse
The prescribed bandwidth, cell side and nuisance amplitudes satisfy the geometric, occupancy and information identities in the converse roadmap. These identities retain both sample channels and both nuisance amplitudes.
Below the frontier cutoff, the sum of nuisance orders is below the effect order. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input hS, the nuisance order lt gamma conclusion holds.
Formal statement
Proof (Lean source)
The two lower-bound scales are positive, nested and in the localization domain. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input hS, the specified input n, the specified input m, the specified input hn, the specified input ch, the specified input cd, the specified input hch, the specified input hch', the specified input hcd, the specified input hcd', the nuisance scales admissible conclusion holds.
Formal statement
Proof (Lean source)
The cell occupancy is the public constant times a power of the count-boundary ratio. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input n, the specified input N, the specified input cd, the specified input hn, the specified input hN, the specified input hcd, the nuisance occupancy identity conclusion holds.
Formal statement
Proof (Lean source)
In the sparse range the cell occupancy never exceeds the public cell constant. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input n, the specified input N, the specified input cd, the specified input hn, the specified input hN, the specified input hcd, the specified input hboundary, the nuisance occupancy bound conclusion holds.
Formal statement
Proof (Lean source)
The product of the two prescribed amplitudes has exactly the converse rate. Given the specified input alpha, the specified input beta, the specified input gamma, the specified input D, the specified input x, the specified input cd, the specified input rho, the specified input hS, the specified input hD, the specified input hx, the specified input hcd, the nuisance amplitude product conclusion holds.
Formal statement
Proof (Lean source)
Both channels and both nuisance orders cancel in the information monomial. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input x, the specified input ch, the specified input cd, the specified input hx, the specified input hch, the specified input hcd, the nuisance information monomial conclusion holds.
Formal statement
Proof (Lean source)
Raising the bandwidth to the effect order gives exactly its prescribed power. Given the specified input gamma, the specified input D, the specified input x, the specified input ch, the specified input hx, the specified input hch, the nuisance bandwidth bias identity conclusion holds.
Formal statement
Proof (Lean source)
The actual rectangular information term equals the constant monomial after scaling. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input x, the specified input ch, the specified input cd, the specified input rho, the specified input hx, the specified input hch, the specified input hcd, the nuisance scaled information identity conclusion holds.
Formal statement
Proof (Lean source)
A single choice of public constants gives admissible marked priors with the converse-rate separation and small Hellinger distance throughout the sparse range. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input hS, the nuisance scaled marked priors conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.OracleBlockInformation 8 declarations The explicit constant-nuisance bump alternatives have a common auxiliary law.
# Oracle bandwidth and full-block information The explicit constant-nuisance bump alternatives have a common auxiliary law. Their labeled information tensorizes, and the oracle bandwidth cancels the sample size in the resulting Hellinger bound.
The oracle bandwidth is positive, lies below one, and has the prescribed bias and information scaling. Given the specified input d, the specified input n, the specified input gamma, the specified input hg, the specified input hn, the oracle bandwidth identities conclusion holds.
Formal statement
Proof (Lean source)
Both signs of the oracle bump produce exactly the same treatment records. Given the specified input d, the specified input h, the specified input b, the specified input hb, the specified input hbs, the oracle bump common auxiliary conclusion holds.
Formal statement
Proof (Lean source)
A common auxiliary channel and randomizer contribute no information to a pair of primitive laws; only the labeled-record product remains. Given the specified input d, the specified input P, the specified input Q, the specified input n, the specified input m, the specified input haux, the oracle experiment hellinger le conclusion holds.
Formal statement
Proof (Lean source)
The full randomized oracle bump experiment has the paper's fixed-size information bound, uniformly in the auxiliary sample size. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input b, the specified input hh, the specified input hh1, the specified input hb, the specified input hbs, the oracle bump block hellinger conclusion holds.
Formal statement
Proof (Lean source)
At the oracle bandwidth, the full-block information is bounded by sixteen times the squared public bump amplitude. Given the specified input d, the specified input n, the specified input m, the specified input gamma, the specified input eta, the specified input hg, the specified input hn, the specified input heta, the specified input hetas, the oracle bump information at rate conclusion holds.
Formal statement
Proof (Lean source)
A single public amplitude makes the explicit bump laws admissible for every sample size and leaves the full experiment inside the testing budget. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the oracle bump testing family conclusion holds.
Formal statement
Proof (Lean source)
The target of an oracle bump is identified by its full experiment law. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input h, the specified input b, the specified input hn, the specified input hMembers, the specified input theta, the specified input theta', the specified input hE, the oracle bump target eq of experiment conclusion holds.
Formal statement
Proof (Lean source)
The two oracle targets extend to a functional of the full-block law, as required by the cited testing theorem. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input h, the specified input b, the specified input hn, the specified input hMembers, the oracle bump experiment target exists conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.OracleBump 5 declarations The oracle lower-bound roadmap uses a fixed smooth compact profile, with a constant control mean and independent Bernoulli potential outcomes.
# Constant-propensity bump alternatives The oracle lower-bound roadmap uses a fixed smooth compact profile, with a constant control mean and independent Bernoulli potential outcomes.
The unsquared macro bump has the exact scaled Hölder bound on windows up to side one. Given the specified input d, the specified input s, the specified input hs, the oracle macro holder conclusion holds.
Formal statement
Proof (Lean source)
The two oracle alternatives use treatment probability and control mean one half. Given the specified input d, the specified input h, the specified input b, the specified input theta, oracle bump primitive is the corresponding construction.
Definition (Lean source)
Small bump amplitudes keep all three raw margins in their prescribed probability bands. Given the specified input d, the specified input h, the specified input b, the specified input theta, the specified input hb, the specified input hbsmall, the oracle bump primitive margins conclusion holds.
Formal statement
Proof (Lean source)
Canonical representatives coincide with admissible raw propensity and arm means. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input hu, the specified input he, the specified input h0, the specified input ht, the specified input hov, the specified input hi0, the specified input hi1, the oracle admissible raw versions conclusion holds.
Formal statement
Proof (Lean source)
Smoothness and small amplitude make each explicit oracle alternative a member of the exact class. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input h, the specified input b, the specified input hL, the specified input hb, the specified input hbsmall, the specified input hsmooth, the specified input theta, the oracle bump primitive membership conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.OracleBumpInformation 6 declarations The treated outcome cells alone change.
# Information in the oracle bump alternatives The treated outcome cells alone change. Their densities stay bounded away from zero, and the bump's support has volume equal to its side raised to dimension.
Oracle bump likelihoods equal one in control cells and have a signed perturbation in treated cells. Given the specified input d, the specified input h, the specified input b, the specified input theta, the specified input hb, the specified input hbsmall, the specified input x, the specified input s, the oracle bump likelihood conclusion holds.
Formal statement
Proof (Lean source)
Each oracle bump likelihood lies between one half and two. Given the specified input d, the specified input h, the specified input b, the specified input theta, the specified input hb, the specified input hbsmall, the specified input z, the oracle bump likelihood bounds conclusion holds.
Formal statement
Proof (Lean source)
A density floor removes the square-root denominator in the elementary Hellinger identity. Given the specified input a, the specified input b, the specified input ha, the specified input hb, the oracle sqrt difference le conclusion holds.
Formal statement
Proof (Lean source)
The centered localization box has its Euclidean product volume. Given the specified input d, the specified input h, the specified input hh, the oracle loc cube volume conclusion holds.
Proof (Lean source)
Squared bump energy is at most its support volume under the uniform design. Given the specified input d, the specified input h, the specified input hh, the specified input hh1, the oracle bump square energy conclusion holds.
Formal statement
Proof (Lean source)
The one-record Hellinger cost of the two oracle alternatives is of bump-squared times volume order. Given the specified input d, the specified input h, the specified input b, the specified input hh, the specified input hh1, the specified input hb, the specified input hbsmall, the oracle bump hellinger bound conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.TargetIdentification 10 declarations Identification of marked targets from the original-record experiment laws.
Identification of marked targets from the original-record experiment laws.
The conditional observed Bernoulli law is a measurable kernel. Given the specified input d, the specified input P, conditional observed kernel is the corresponding construction.
Definition (Lean source)
Probability-valued margins make the observed conditional kernel Markov. Given the specified input d, the specified input P, the specified input he, the specified input hp, the specified input hq, the conditional observed kernel markov conclusion holds.
Formal statement
Proof (Lean source)
The explicit independent extension has its observed conditional kernel as disintegration. Given the specified input d, the specified input e, the specified input p, the specified input q, the specified input he, the specified input hp, the specified input hq, the independent obs law comp prod conclusion holds.
Formal statement
Proof (Lean source)
Class overlap also holds almost everywhere for any probability-valued raw propensity witness. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input he, the raw propensity overlap ae conclusion holds.
Formal statement
Proof (Lean source)
The four observed cells determine the propensity and both arm means under overlap. Given the specified input d, the specified input P, the specified input Q, the specified input x, the specified input heP, the specified input heQ, the specified input hpP, the specified input hqP, the specified input hpQ, the specified input hqQ, the specified input hobs, the overlap level eps, the conditional observed identifies margins conclusion holds.
Formal statement
Proof (Lean source)
In the overlapping independent Bernoulli subfamily, equality of observed laws identifies the full primitive law, up to null covariates. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input e, the specified input p, the specified input q, the specified input e', the specified input p', the specified input q', the specified input he, the specified input hp, the specified input hq, the specified input he', the specified input hp', the specified input hq', the specified input hP, the specified input hobs, the independent full law eq of obs law conclusion holds.
Formal statement
Proof (Lean source)
The first labeled coordinate has exactly the observed-record law. Given the specified input d, the specified input n, the specified input m, the specified input P, the specified input j, the experiment map labeled conclusion holds.
Formal statement
Proof (Lean source)
Equal full experiments identify the canonical target within the marked subfamily. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input hn, the specified input hMembers, the specified input theta, the specified input theta', the specified input sigma, the specified input sigma', the specified input hE, the marked target eq of experiment conclusion holds.
Formal statement
Proof (Lean source)
A target constant on experiment fibers has a well-defined extension to all laws. Given the specified input A, the specified input B, the specified input E, the specified input t, the specified input ht, the exists function on image conclusion holds.
Formal statement
Proof (Lean source)
The canonical marked target is a functional of the full randomized experiment law. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input hn, the specified input hMembers, the marked experiment target exists conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.TreeCount 5 declarations Two-channel point-CATE annotation frontier: Lower/TreeCount constructions and obligations.
Lower/TreeCount
Two-channel point-CATE annotation frontier: Lower/TreeCount constructions and obligations.
The informative-component count is integrable under the finite uniform covariate experiment. Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input p, the specified input hp, the labeled record count integrable conclusion holds.
Formal statement
Proof (Lean source)
The uniform design mass of the localization cube is its side length to the ambient dimension. Given the specified input d, the specified input h, the specified input hh, the specified input hh', the uniform law loc cube real conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input n, the specified input m, the specified input h, the specified input delta, the specified input hh, the specified input hh', the specified input hd, the specified input hdh, the specified input p, the specified input hp, the labeled root tree count conclusion holds.
Formal statement
Proof (Lean source)
The exponential series bounds the rooted-tree factorial ratio. Given the specified input p, the specified input hp, the factorial tree bound conclusion holds.
Proof (Lean source)
the tree series summable conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.TreeSeries 5 declarations The numerical steps MC34–MC37: a binomial/factorial estimate and a polynomial geometric-series bound under the small-occupancy condition.
Summation of the labeled-root tree envelope
The numerical steps MC34–MC37: a binomial/factorial estimate and a polynomial geometric-series bound under the small-occupancy condition. These estimates do not assert the geometric component count or the Hellinger product assembly, which remain separate obligations.
The binomial coefficient and rooted-parent count have an exponential envelope. Given the specified input N, the specified input p, the specified input hp, the binomial rooted tree bound conclusion holds.
Formal statement
Proof (Lean source)
A finite polynomial-geometric sum has a bound linear in its small ratio. Given the specified input M, the specified input z, the specified input hz, the specified input hzhalf, the finite tree series bound conclusion holds.
Formal statement
Proof (Lean source)
One summand of the tree envelope is controlled by its occupancy ratio. Given the specified input N, the specified input j, the specified input K, the specified input v, the specified input hK, the specified input hv, the tree envelope term bound conclusion holds.
Formal statement
Proof (Lean source)
Small occupancy controls the entire tree envelope uniformly in the truncation and total number of records. This is the numerical content of MC35–MC37. Given the specified input d, the specified input K, the specified input hK, the tree envelope sum bound conclusion holds.
Formal statement
Proof (Lean source)
Applying the geometric count lemma to the numerical envelope gives the labeled-root factor nN, uniformly in the auxiliary-to-labeled ratio. The geometric count itself is a separate, currently unfinished dependency. Given the specified input d, the specified input K, the specified input hK, the labeled component series bound conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Lower.TwoPoint 1 declarations Two-channel point-CATE annotation frontier: Lower/TwoPoint constructions and obligations.
Lower/TwoPoint
Two-channel point-CATE annotation frontier: Lower/TwoPoint constructions and obligations.
Constant-propensity bump alternatives remain members of the exact primitive class. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the oracle bump pair conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.Projection 38 declarations Two-channel point-CATE annotation frontier: Projection constructions and obligations.
Projection
Two-channel point-CATE annotation frontier: Projection constructions and obligations.
Multi-indices of total degree at most two. Given the specified input d, poly idx is the corresponding construction.
Definition (Lean source)
Given the specified input d, the poly idx finite conclusion holds.
Formal statement
Proof (Lean source)
For dimension d, the degree-at-most-two multi-indices form a finite type.
Definition (Lean source)
Given the specified input d, the specified input J, fine idx is the corresponding construction.
Given the specified input d, the poly idx card conclusion holds.
Proof (Lean source)
Given the specified input d, the specified input J, the fine idx card conclusion holds.
Proof (Lean source)
Given the specified input d, the specified input h, loc cube is the corresponding construction.
Definition (Lean source)
Given the specified input h, the specified input x, loc weight is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input h, loc law is the corresponding construction.
Given the specified input k, the specified input u, legendre is the corresponding construction.
Given the specified input h, the specified input x, coarse basis is the corresponding construction.
Given the specified input d, the specified input h, r0 is the corresponding construction.
Definition (Lean source)
Given the specified input h, the specified input v, the specified input x, pv is the corresponding construction.
Definition (Lean source)
Given the specified input h, the specified input J, the specified input z, cell is the corresponding construction.
Given the specified input h, the specified input J, the specified input x, the specified input z, fine basis is the corresponding construction.
Given the specified input d, the specified input h, the specified input J, the specified input x, the specified input xp, fine kernel is the corresponding construction.
Given the specified input d, the specified input h, the specified input J, the specified input f, the specified input x, proj op is the corresponding construction.
Definition (Lean source)
Localization windows are closed boxes. Given the specified input d, the specified input h, the is closed loc cube conclusion holds.
Proof (Lean source)
Given the specified input d, the specified input h, the specified input J, the specified input z, the measurable set cell conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input k, the measurable legendre conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input h, the specified input u, the measurable coarse basis conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input h, the measurable loc weight conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input h, the specified input J, the specified input z, the measurable fine basis conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input h, the specified input J, the measurable fine kernel conclusion holds.
Formal statement
Proof (Lean source)
Direct integration gives orthogonality for degrees zero, one and two on the reference interval. Given the specified input k, the specified input l, the specified input hk, the specified input hl, the legendre interval orthogonality conclusion holds.
Formal statement
Proof (Lean source)
For degree k, the corresponding Legendre polynomial is continuous on the real line.
Formal statement
Proof (Lean source)
Affine rescaling multiplies each one-dimensional orthogonality integral by the side length. Given the specified input h, the specified input hh, the specified input k, the specified input l, the specified input hk, the specified input hl, the scaled legendre orthogonality conclusion holds.
Formal statement
Proof (Lean source)
Integration of a coordinate product over a Euclidean box factors into one-dimensional integrals. Given the specified input d, the specified input a, the specified input b, the specified input f, the euclidean box product integral conclusion holds.
Formal statement
Proof (Lean source)
Euclidean product-set integrals factor across arbitrary coordinate sets. Given the specified input d, the specified input s, the specified input f, the euclidean product set integral conclusion holds.
Formal statement
Proof (Lean source)
A centered cell of any positive side length has the same Legendre orthogonality. Given the specified input c, the specified input t, the specified input ht, the specified input k, the specified input l, the specified input hk, the specified input hl, the centered legendre orthogonality conclusion holds.
Formal statement
Proof (Lean source)
Every cell stays inside the localization box, including its assigned upper face. Given the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input z, the cell subset loc cube conclusion holds.
Formal statement
Proof (Lean source)
Distinct half-open grid cells are disjoint. Given the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input z, the specified input w, the specified input hzw, the cells disjoint conclusion holds.
Formal statement
Proof (Lean source)
Cell face assignments do not change the product Legendre integrals. Given the specified input h, the specified input J, the specified input hh, the specified input hJ, the specified input z, the specified input u, the specified input v, the cell legendre product integral conclusion holds.
Formal statement
Proof (Lean source)
The scaled coarse Legendre basis is orthonormal under localization measure. Given the specified input d, the specified input h, the specified input hh, the specified input hh', the specified input u, the specified input v, the coarse orthonormal conclusion holds.
Formal statement
Proof (Lean source)
The cellwise Legendre basis is orthonormal, including the assigned grid faces. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input u, the specified input v, the fine orthonormal conclusion holds.
Formal statement
Proof (Lean source)
The diagonal orthonormality integral supplies square integrability of each fine basis entry. Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input u, the fine basis mem lp conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input h, the specified input J, the specified input hh, the specified input hh', the specified input hJ, the specified input f, the specified input hf, the projection pythagoras conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input f, the specified input p, the specified input x, taylor poly is the corresponding construction.
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.T_AnnotationThreshold 13 declarations Two-channel point-CATE annotation frontier: T_AnnotationThreshold constructions and obligations.
T_AnnotationThreshold
Two-channel point-CATE annotation frontier: T_AnnotationThreshold constructions and obligations.
Kennedy, Balakrishnan, Robins and Wasserman (2024), Section 3, Theorem 1, has exactly the same numerical supervised exponents and cutoff after substituting the nuisance-average smoothness. This is only a descriptive formula comparison. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input n, the published benchmark eq supervised rate conclusion holds.
Formal statement
Proof (Lean source)
For positive dimension, positive first nuisance smoothness, positive second nuisance smoothness, and effect smoothness at least one, the published point-CATE benchmark's two exponent identities, cutoff equivalence, and piecewise maximum formula all hold.
Formal statement
Proof (Lean source)
The frontier lower bound and its explicit decision give both sample-growth directions. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the annotation acquisition conclusion holds.
Formal statement
Proof (Lean source)
Finite extended-real bounds retain both inequalities after taking real values. Given the specified input R, the specified input a, the specified input b, the specified input ha, the specified input hb, the specified input hl, the specified input hu, the risk to real sandwich conclusion holds.
Formal statement
Proof (Lean source)
In the smooth regime the frontier upper bound divided by the oracle floor is uniform. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input hs, the smooth oracle risk ratio conclusion holds.
Formal statement
Proof (Lean source)
Bounded auxiliary counts change either branch of the maximum rate by only a fixed factor. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input K, the specified input hK, the specified input n, the specified input m, the specified input hn, the specified input hm, the sharp rate bounded auxiliary comparison conclusion holds.
Formal statement
Proof (Lean source)
A bounded auxiliary-to-labeled ratio preserves the supervised minimax order in both directions. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input mseq, the specified input hseq, the bounded auxiliary risk order conclusion holds.
Formal statement
Proof (Lean source)
Uniform positive sandwiches compare ratios in both directions. Given the specified input f, the specified input g, the specified input r, the specified input s, the specified input cF, the specified input CF, the specified input cG, the specified input CG, the specified input hcF, the specified input hCF, the specified input hcG, the specified input hCG, the specified input hr, the specified input hs, the specified input hf, the specified input hg, the positive sandwich ratio bounds conclusion holds.
Formal statement
Proof (Lean source)
Comparable nonnegative sequences have the same boundedness and zero-limit behavior. Given the specified input f, the specified input g, the specified input A, the specified input B, the specified input hA, the specified input hB, the specified input h, the comparable nonnegative sequences conclusion holds.
Formal statement
Proof (Lean source)
Dividing by a positive rate converts a big-O comparison into boundedness. Given the specified input r, the specified input s, the specified input h, the nonnegative rate big o div iff conclusion holds.
Formal statement
Proof (Lean source)
The frontier and supplied-propensity bounds give real-valued uniform sandwiches. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the annotation risk sandwiches conclusion holds.
Formal statement
Proof (Lean source)
Risk and numerical rate comparisons coincide along every auxiliary-size sequence. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the specified input mseq, the annotation risk rate equivalences conclusion holds.
Formal statement
Proof (Lean source)
Oracle attainment, strict benefit, all rate branches, supervised comparison, and necessary and sufficient acquisition requirements for the established frontier. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the annotation threshold conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.T_MarkedComponentCertificate 4 declarations Two-channel point-CATE annotation frontier: T_MarkedComponentCertificate constructions and obligations.
T_MarkedComponentCertificate
Two-channel point-CATE annotation frontier: T_MarkedComponentCertificate constructions and obligations.
Equal treatment-record marginals identify the entire designated propensity on the cube. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input Q, the specified input hP, the specified input hQ, the specified input hxa, the designated propensity eq of xa law conclusion holds.
Formal statement
Proof (Lean source)
The sign involution preserves the law of the designated, continuous propensity function. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input h, the specified input delta, the specified input a, the specified input b, the specified input hMembers, the marked designated propensity marginal conclusion holds.
Formal statement
Proof (Lean source)
The prescribed macro bump equals one at the target, giving the signed contrast. Given the specified input d, the specified input h, the specified input a, the specified input b, the specified input theta, the marked contrast at target conclusion holds.
Formal statement
Proof (Lean source)
The explicit sign-pair construction satisfies membership, exact cancellations, component factorization and the fixed-size information bound. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the marked component certificate conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.T_RectangularUpper 1 declarations Two-channel point-CATE annotation frontier: T_RectangularUpper constructions and obligations.
T_RectangularUpper
Two-channel point-CATE annotation frontier: T_RectangularUpper constructions and obligations.
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the rectangular upper conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.T_SharpAnnotationFrontier 3 declarations Two-channel point-CATE annotation frontier: T_SharpAnnotationFrontier constructions and obligations.
T_SharpAnnotationFrontier
Two-channel point-CATE annotation frontier: T_SharpAnnotationFrontier constructions and obligations.
An original-record rule can be supplied to the oracle while ignoring its extra input. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input n, the specified input m, the oracle risk le minimax risk conclusion holds.
Formal statement
Proof (Lean source)
The oracle floor and the nuisance converse give one constant valid across all branches. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the sharp rate minimax lower conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the sharp annotation frontier conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TwosamplePointcateAnnotationFrontier_Research.T_SuppliedPropensity 7 declarations Two-channel point-CATE annotation frontier: T_SuppliedPropensity constructions and obligations.
T_SuppliedPropensity
Two-channel point-CATE annotation frontier: T_SuppliedPropensity constructions and obligations.
Given the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, constant nuisance is the corresponding construction.
Definition (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input n, the specified input m, oracle subfamily risk is the corresponding construction.
Definition (Lean source)
Restricting to the constant-nuisance subfamily can only decrease oracle minimax risk. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input n, the specified input m, the oracle subfamily risk le oracle risk conclusion holds.
Formal statement
Proof (Lean source)
The supplied function is identical on the whole covariate space for every member of the constant-nuisance subfamily, including its zero extension. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input P, the specified input hP, the specified input hconst, the constant nuisance propensity eq conclusion holds.
Formal statement
Proof (Lean source)
Singleton priors at the two explicit bump laws give an oracle-subfamily lower bound: their supplied input is common, so the cited block test applies. Given the specified input d, the specified input n, the specified input m, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input h, the specified input b, the specified input hb, the specified input hn, the specified input hMembers, the specified input hconst, the specified input htarget, the specified input hhell, the oracle bump testing lower conclusion holds.
Formal statement
Proof (Lean source)
The same-class constant-nuisance subfamily has the irreducible oracle outcome rate, uniformly over every auxiliary sample size. Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the oracle subfamily lower rate conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input alpha, the specified input beta, the specified input gamma, the specified input L, the overlap level eps, the specified input hdom, the supplied propensity conclusion holds.