Formalization: Private Estimation and Honest Inference for Conditional Treatment Effects with Rough Nuisance Functions
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs.
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Basic 51 declarations Concrete causal laws, selected observational versions, private kernels and extended-real minimax criteria.
Concrete causal laws, selected observational versions, private kernels and extended-real minimax criteria. Published inequalities are explicit conditional gates.
The covariate takes values in the closed unit interval.
Definition (Lean source)
Observed records consist of a covariate and two binary marks for treatment and outcome.
Full causal records also carry the two binary potential outcomes.
A dataset is a finite tuple of observed records indexed by the public sample size.
Definition (Lean source)
A binary mark is represented numerically by zero or one.
Definition (Lean source)
The covariate coordinate of a full causal record.
The binary treatment coordinate of a full causal record.
The control and treated potential outcomes of a full causal record.
The observed binary outcome coordinate of a full causal record.
Observation forgets the potential outcomes and retains covariate, treatment and outcome.
Definition (Lean source)
The covariate coordinate is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The public regularity radius is fixed at three.
Definition (Lean source)
The evaluation point one half belongs to the closed unit interval. the asserted conclusion follows.
Formal statement
Proof (Lean source)
The public evaluation point is one half.
Definition (Lean source)
The version identities pin the density and the three observational regressions to the law. The arm means are integrable for their arm-specific covariate measures, without interior bounds.
Definition (Lean source)
The bundled causal law carries its probability-measure instance.
Definition (Lean source)
The observed marginal is the pushforward of the causal law by observation.
The design marginal is the pushforward of the causal law by the covariate coordinate.
The selected observational contrast is the treated regression minus the control regression.
The point target evaluates the selected contrast at one half.
The dataset law is the finite product of the observed marginal.
The sampling hypothesis identifies the dataset distribution with that observed product law.
The observed outcome agrees almost surely with the potential outcome selected by treatment.
The potential-outcome pair and treatment are conditionally independent given the covariate.
Definition (Lean source)
The design marginal is absolutely continuous and its selected density is between one half and three halves almost everywhere for Lebesgue measure.
The selected propensity is between one quarter and three quarters at every covariate.
Definition (Lean source)
The selected propensity obeys the one-tenth Holder modulus with radius three.
Definition (Lean source)
The selected control regression obeys the one-tenth Holder modulus with radius three.
Definition (Lean source)
The selected contrast obeys the Lipschitz modulus with radius three.
Definition (Lean source)
The complete law class bundles consistency, exchangeability, density, overlap and the three specified regularity conditions.
Definition (Lean source)
The Hamming distance counts the records at which two datasets differ.
Definition (Lean source)
Replacement privacy bounds every measurable output event on every adjacent pair of input datasets.
The private-kernel predicate bundles Markov normalization and replacement privacy.
Definition (Lean source)
Total variation is the substrate distance between probability measures on a common measurable space.
Definition (Lean source)
Hamming transport is the extended-real infimum of expected dataset Hamming distance over all couplings.
Connected Borel intervals are represented by extended endpoints and inclusion flags, with a separate empty code.
The empty-or-endpoints representation has the Borel sigma algebra of its sum topology. This representation property is derived locally, rather than assumed by headline consumers. the asserted conclusion follows.
Formal statement
Proof (Lean source)
The interval representation carries its derived Borel-space instance.
Definition (Lean source)
An interval code denotes the corresponding connected subset of the real line.
The length of a coded interval is its possibly infinite Lebesgue measure.
Definition (Lean source)
Absolute risk integrates both the observed dataset distribution and randomized scalar output.
Expected interval length integrates both the observed dataset distribution and randomized interval output.
Definition (Lean source)
Coverage is the probability that the randomized coded interval contains the law-specific point target.
Maximal absolute risk is the extended-real supremum across the complete law class.
Definition (Lean source)
Maximal expected length is the extended-real supremum across the complete law class.
Definition (Lean source)
The same absolute-risk criterion without a privacy restriction.
Definition (Lean source)
Private minimax absolute risk takes the infimum of maximal risk over all total private Markov scalar releases.
Definition (Lean source)
The honest private length frontier takes the infimum of maximal expected length over private Markov interval releases with class-wide coverage at least nine tenths.
Definition (Lean source)
Boucheron, Lugosi and Massart (2013), Theorem 3.1, printed p.54, replacement-copy form. Source: https://math.hse.ru/data/2016/11/24/1113029206/Concentration%20inequalities.pdf DOI: 10.1093/acprof:oso/9780199535255.001.0001. This published claim is an assumed gate.
Definition (Lean source)
Boucheron, Lugosi and Massart (2013), Theorem 6.2, displayed log-mgf bound in the proof, printed p.167. Source: https://math.hse.ru/data/2016/11/24/1113029206/Concentration%20inequalities.pdf . DOI: 10.1093/acprof:oso/9780199535255.001.0001. Positive parameters are exponentiated and the zero parameter is included by equality. This is an assumed gate.
Definition (Lean source)
Keller and Trotter (2017), Applied Combinatorics, Section 5.6, Theorem 5.40. Source: https://appliedcombinatorics.org/book/s_graphs_counting-trees.html . Nat.card counts the finite subtype of undirected labeled trees. This is an assumed gate.
Definition (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.BinaryExchangeability 4 declarations Conditional exchangeability of the explicit independent Bernoulli construction.
Conditional exchangeability of the explicit independent Bernoulli construction.
Density coordinates are sent to full records by selecting the observed outcome.
Definition (Lean source)
The consistency selection map is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The paper's finite conditional law is the pushforward of the library's product density law. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Independent treatment and potential-outcome marks remain conditionally independent when the observed consistency outcome is appended to the record. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.BinaryLaw 26 declarations Uniform-design binary causal laws and their conditional regression identities.
Uniform-design binary causal laws and their conditional regression identities.
The binary probability mass is the specified success probability for one and its complement for zero.
Definition (Lean source)
A valid Bernoulli parameter gives nonnegative mass to either binary outcome. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The two nonnegative Bernoulli masses add to one in extended real arithmetic. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Three independent valid Bernoulli masses have unit total mass. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A uniform covariate draw is followed by independent Bernoulli treatment and potential outcomes and the consistency observation map.
Definition (Lean source)
The finite conditional Bernoulli record law varies measurably with the covariate. the asserted conclusion follows.
Formal statement
Proof (Lean source)
The finite Bernoulli construction is a probability law for measurable probability-valued parameters. the asserted conclusion follows.
Formal statement
Proof (Lean source)
The finite Bernoulli construction has the uniform design density. the asserted conclusion follows.
Formal statement
Proof (Lean source)
The uniform design has the selected constant density one. The displayed conclusion follows.
Formal statement
The selected propensity is integrable under the constructed design marginal. the asserted conclusion follows.
Formal statement
Proof (Lean source)
The selected control mean is integrable under the constructed control-arm covariate measure. the asserted conclusion follows.
Formal statement
Proof (Lean source)
The selected treated mean is integrable under the constructed treated-arm covariate measure. the asserted conclusion follows.
Formal statement
Proof (Lean source)
The constructed propensity satisfies the conditional probability identity on every measurable covariate set. the asserted conclusion follows.
Formal statement
Proof (Lean source)
Integration under the generated record law is integration of the finite conditional masses. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
In each arm, the conditional mean of the observed binary response is its Bernoulli parameter. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The constructed control regression satisfies the conditional mean identity on every measurable covariate set. the asserted conclusion follows.
Formal statement
Proof (Lean source)
The constructed treated regression satisfies the conditional mean identity on every measurable covariate set. the asserted conclusion follows.
Formal statement
Proof (Lean source)
The finite Bernoulli product followed by consistency gives a concrete causal-law bundle.
Definition (Lean source)
Every generated record uses the potential outcome selected by its treatment. the asserted conclusion follows.
Formal statement
Proof (Lean source)
The constructed law's selected density is one and its design is exactly uniform. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Analytic regularity and conditional exchangeability complete the binary law's model certificate; consistency and the uniform density follow from its construction. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
An observed event under the binary construction integrates the four conditional mark masses; the unused potential outcome sums out exactly. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Coordinatewise measure domination is preserved by a finite product. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A common finite domination factor becomes its nth power for an n-record experiment. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every probability-valued binary construction is dominated by eight times the fair full-record law. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Finite domination makes the squared density deviation integrable under a finite reference law. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.CellMoments 30 declarations Positive-mass conditional cell laws, independent binary pair moments and occupancy-certificate assembly.
Positive-mass conditional cell laws, independent binary pair moments and occupancy-certificate assembly.
The observed cell event has exactly the mass of the corresponding design cell. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Density bounded below ensures that conditioning on any public cell gives a probability law. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The bounded binary numerator kernel is integrable under any finite pair measure. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The bounded binary denominator kernel is integrable under any finite pair measure. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The conditional pair numerator cannot exceed the denominator in absolute value. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The normalized cell treatment mean is the selected propensity averaged over that cell. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Averaging the everywhere overlap bounds under a positive-mass cell preserves overlap. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Independent binary treatments have denominator moment twice p times one minus p. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conditional pair denominator satisfies the paper's three-eighths lower bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Conditioning rescales an observed cell integral by its actual design probability. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The arm-response integral equals the design integral of the arm probability times its mean. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Each conditional arm-response moment averages the selected arm regression with its propensity. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conditional treated-response moment is the cell average of propensity times treated mean. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conditional response mean sums the propensity-weighted means in the two treatment arms. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Independent binary records have numerator moment twice the treatment-response covariance. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conditional numerator is the treatment-response covariance within the actual cell law. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conditional numerator uses the actual design-weighted cell moments, with no density approximation. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The observed conditional numerator equals the cross-treatment moment of two actual conditional covariates. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The observed conditional denominator equals the cross-treatment probability for two actual conditional covariates. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The actual conditional cell moments satisfy the paper's complete causal bias bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Two distinct coordinates of an iid array have the product of the record law as their law. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every distinct iid coordinate pair has the same integrable kernel moment. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
At a fixed iid cell count, the count-weighted pair sum has expectation s times the conditional pair moment; empty and singleton samples contribute zero. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Every numerator cell contribution is integrable under a finite dataset law. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Every denominator cell contribution is integrable under a finite dataset law. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Population statistics sum the cell expectations, without independence between cell counts. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Conditional on exact membership labels, the two cell contributions equal the eligible occupancy times their respective conditional pair moments. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Integrating a function over all datasets is summing its integrals on the disjoint exact membership-label events. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Undoing normalization multiplies each conditional integral by the probability of its membership-label event. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The common occupancy weights cancel in the population ratio for every admissible density. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.ComponentAmplitude 27 declarations Free-amplitude conditional mark arrays and their derivative bounds for the second-order component contraction argument.
Free-amplitude conditional mark arrays and their derivative bounds for the second-order component contraction argument.
The Fourier mark mass with a free amplitude and fixed perturbation and bump.
The first amplitude derivative of the four conditional masses.
The second amplitude derivative of the four conditional masses.
A Bernoulli Fourier mark has absolute value one. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Proof (Lean source)
The finite Fourier triangle inequality bounds the sum of absolute mark masses. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
The free-amplitude mass is the product of the treatment and outcome Bernoulli factors. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Summing the four conditional masses gives one at every amplitude. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The mass at zero amplitude is the fair pair mass. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The actual alternative is the free-amplitude array evaluated at the square-root separation. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The polynomial first derivative is valid at every real amplitude. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The polynomial second derivative is valid at every real amplitude. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Legal free amplitudes keep both Bernoulli factors strictly positive. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The four conditional masses have unit ℓ₁ norm on the free-amplitude path. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The Fourier coefficients bound the ℓ₁ norm of the first derivative. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The Fourier coefficients bound the ℓ₁ norm of the second derivative. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The first derivative has ℓ₁ norm at most four throughout the amplitude path. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The second derivative has ℓ₁ norm at most four throughout the amplitude path. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The actual perturbation and bump satisfy all coefficient bounds used by the path. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The actual square-root separation belongs to the path's amplitude interval. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
At zero amplitude each first derivative is linear in the latent perturbation. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Averaging the zero-amplitude derivative cancels the independent fair signs. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Every free-amplitude singleton mixture is exactly the fair mark law. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The finite sign mixture of component mark masses along the amplitude path.
Definition (Lean source)
The amplitude path's endpoint is precisely the existing alternative component array. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
At zero amplitude the component path equals the fair component array. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Differentiation of the finite mixture uses the ordinary finite product rule. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Independent fair signs cancel the entire component path's first derivative at zero. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.ComponentContraction 1 declarations Assembly of the Borel measurable shared-sign coupling and its private contraction bound.
Assembly of the Borel measurable shared-sign coupling and its private contraction bound.
Finite graph factorization yields measurable component couplings and, in the sparse regime, a Hamming bound and its private-output consequence. Both cited gates remain explicit inputs. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.ComponentCounting 18 declarations Component-count expectations as sums over fixed vertex sets, and ordered-tree probability bounds on arbitrary distinct coordinates of the full sample.
Component-count expectations as sums over fixed vertex sets, and ordered-tree probability bounds on arbitrary distinct coordinates of the full sample.
Selecting distinct coordinates of an iid uniform sample preserves the uniform product law. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A Borel event on distinct selected sample coordinates has exactly its smaller product probability. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The event that a fixed vertex set is one of the selected graph components is Borel. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Counting size-s components is exactly summing their indicators over all size-s vertex sets. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Taking expectations of the exact indicator count gives a sum of fixed-component probabilities. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A common probability bound for fixed size-s components gives the binomial component-count bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The component event for any specified two-set is bounded by the corresponding single-edge event. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The actual expected number of two-vertex components satisfies the roadmap's binomial labeled-tree bound, with no assumed probability estimate. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every vertex in a component with another vertex has a neighbor in that component. This uses the first step of a connecting walk, without assuming any graph geometry. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A three-vertex component contains one of the three labeled spanning trees. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A specified two-edge star on three distinct records obeys the tree envelope. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The probability that a specified triple is a component is at most the sum of its three labeled spanning-tree envelopes. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every fixed size-three component obeys the Cayley envelope with three trees. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The expected number of size-three components satisfies the roadmap's binomial Cayley bound with no assumed component probability estimate. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.ComponentCoupling 52 declarations Shared-sign graphs, ordered finite components, explicit common-mass couplings and conditional sparse Hamming/private-output contraction.
Shared-sign graphs, ordered finite components, explicit common-mass couplings and conditional sparse Hamming/private-output contraction.
A graph component contains exactly the vertices reachable from its selected vertex.
Each component is represented by its least vertex.
Components are selected by increasing least vertex, so the construction is deterministic.
Definition (Lean source)
Component size is its vertex cardinality.
Component marks are binary treatment-outcome pairs indexed by the component vertices.
The fair component mark law gives every configuration mass four to the power minus component size.
The alternative component mark mass averages the conditional Bernoulli products over the latent signs.
Definition (Lean source)
The common mass is the pointwise minimum of the alternative and null component masses.
Total overlap sums the common component masses.
The alternative component measure is the finite measure with the specified alternative mark masses.
The null component measure is the finite measure with the specified fair mark masses.
The common-mass coupling combines diagonal common mass with the normalized product of the two residual masses, omitting the residual when overlap is one.
Definition (Lean source)
The finite component coupling measure has the explicit common-mass joint array.
The joint mark array is the product of the common-mass couplings across the ordered graph components.
Definition (Lean source)
The same covariate vector is attached to a vector of treatment-outcome marks.
The conditional dataset coupling attaches the same covariates to both sides of the product component coupling.
Definition (Lean source)
The dataset coupling integrates the ordered product of explicit component couplings over shared uniform covariates.
The full conditional mark mass averages the dataset Bernoulli likelihood product uniformly over all latent signs.
Definition (Lean source)
The four conditional mark masses sum to one at every covariate and sign vector. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Every alternative component mass is nonnegative. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Summing the finite component array gives total mass one, including the empty component. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Every fair component mass is positive. The displayed conclusion follows.
Formal statement
Proof (Lean source)
A singleton alternative array equals the fair array by the exact sign cancellations. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
Singleton component measures coincide pointwise, including at support boundaries. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Common component mass lies between zero and each marginal array. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The total common component mass is a probability overlap between zero and one. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The fair component array sums to one for every finite component. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The first residual array has mass one minus the overlap. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
The second residual array has the same mass one minus the overlap. The displayed conclusion follows.
Formal statement
Proof (Lean source)
At full overlap the alternative array equals the common array. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
At full overlap the null array equals the common array. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The explicit common-mass joint array is nonnegative in both overlap branches. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Summing a row of the explicit coupling recovers the alternative component mass. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Summing a column of the explicit coupling recovers the null component mass. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The explicit finite coupling has the alternative component law as first marginal. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The explicit finite coupling has the fair component law as second marginal. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The fair finite component measure is a probability measure. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The common-mass component construction is a probability coupling of its two mark laws. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
At any mark vector one of the two residual masses is zero. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The diagonal entry of the joint array is exactly the common mass in either branch. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The component coupling's agreement probability is precisely its common mass overlap. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The absolute array difference is twice the mass outside their pointwise overlap. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Singleton components have full common-mass overlap. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The explicit component coupling fails with probability exactly one minus its overlap. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Singleton couplings agree almost surely, including support-boundary singletons. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A component can change at most its cardinality on the coupling's failure event. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The component transport cost is at most half its size times the absolute array difference. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Singleton components contribute no expected changed marks to the dataset coupling. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.ComponentFactorization 12 declarations Pointwise products over the ordered shared-sign partition: fixed-sign conditional likelihoods and fair null masses factor at every covariate vector.
Pointwise products over the ordered shared-sign partition: fixed-sign conditional likelihoods and fair null masses factor at every covariate vector.
The finite union of the ordered components is the whole dataset index set. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The finset underlying the component order is a disjoint partition. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Multiplying vertex factors component by component equals the full dataset product. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Component cardinalities sum to the number of dataset records. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Conditional independence given signs factors its mark likelihood over the graph partition. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A fair component mass is the product of the fair one-record masses. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The fair null factors over components at every covariate vector. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A component uses precisely those active signs nonzero at one of its vertices.
The sign block membership test is the existence of a vertex using that coordinate. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Distinct ordered graph components use disjoint coordinate blocks of the latent signs. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A component mark product is a function only of its selected sign block. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Mixing independent signs preserves the product over distinct shared-sign components. This identity holds pointwise in the covariates, including all support boundaries. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.ComponentJointLaw 30 declarations Finite partition sums, conditional marginals of the product common-mass coupling, and the quadratic component total-variation bound.
Finite partition sums, conditional marginals of the product common-mass coupling, and the quadratic component total-variation bound. The certificates hold at every covariate vector, including support boundaries.
Restriction to the blocks of a finite partition is a bijection of assignment spaces.
Definition (Lean source)
Summing products of independent block arrays factors into their individual sums. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The ordered shared-sign components form a finite partition for any mark alphabet. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every product joint mass is nonnegative. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Summing a row of the joint product recovers the full conditional sign mixture. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Summing a column of the joint product recovers the full fair mark array. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The full conditional alternative array sums to one. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The finite joint product array has unit total mass. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conditional alternative dataset law attaches fixed covariates to the mixed marks.
Definition (Lean source)
The conditional null dataset law attaches fixed covariates to independent fair marks.
The conditional product coupling has the exact mixed dataset law as first marginal. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conditional product coupling has the exact fair dataset law as second marginal. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conditional product coupling is a probability measure at every covariate vector. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The explicit Borel conditional product couples the two full conditional dataset laws. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Integrating the pointwise conditional coupling preserves unit total mass. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conditional alternative dataset law is Borel in the covariates. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The conditional null dataset law is Borel in the covariates. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Integrating the conditional coupling recovers the integrated alternative marginal. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Integrating the conditional coupling recovers the integrated null marginal. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The Borel product construction couples the integrated conditional dataset laws. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A nonnegative finite atomic array evaluates an event by summing its selected entries. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Event gaps of two probability arrays are bounded by their mass outside the common part. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The TV of the finite component laws is bounded by the explicit coupling's failure mass. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The curvature certificate gives the uniform four-times-separation component TV bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Selecting entries where the first array is larger attains its overlap deficit. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Each nonnegative alternative component array defines a probability measure. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The explicit finite common part gives the exact total variation of component laws. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The common-mass component coupling fails with probability exactly its marginal TV. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Component total variation is half the absolute difference of its finite arrays. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The explicit coupling changes at most the component size times its marginal TV. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.ComponentMeasurability 16 declarations Borel regularity of finite common-mass arrays, fixed-component couplings and the full conditional dataset coupling, using finitely many labeled-graph strata.
Borel regularity of finite common-mass arrays, fixed-component couplings and the full conditional dataset coupling, using finitely many labeled-graph strata. These certificates include the overlap-one branch and require no radius restrictions.
Fixing the two marks leaves a Borel conditional likelihood in the covariate. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Each fixed-component alternative mass is Borel in the full covariate vector. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Taking the pointwise common part preserves Borel regularity. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The finite sum of common masses is Borel in the covariates. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The explicit joint mass is Borel, including the branch where overlap is one. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The full sign-mixture conditional mass is Borel for each fixed dataset mark vector. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Attaching fixed marks to covariates is a Borel map into the dataset space. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The alternative finite component measure varies measurably with the covariates. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The common-mass coupling of a fixed component varies measurably with the covariates. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The deterministic ordered components of a fixed graph use increasing least vertices.
A product over any fixed list of components is a Borel joint mark mass. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The varying-graph joint array is Borel by its finite decomposition into graph strata. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The explicit conditional dataset coupling is Borel on every covariate vector. The displayed conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.ComponentPartition 18 declarations The ordered shared-sign components partition the dataset indices.
The ordered shared-sign components partition the dataset indices. Distinct components use disjoint active sign coordinates. Conditional likelihoods depend only on those coordinates.
Component membership is exactly reachability in the shared-sign graph. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every vertex belongs to its own component. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Reachable vertices select the same component. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Two components either coincide or are disjoint. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Component roots are precisely the least vertices of their reachable classes. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every vertex has a component root in its reachable class. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A reachable class has at most one selected least vertex. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Distinct selected roots have disjoint component vertex sets. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The ordered list contains exactly the components of selected roots. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The ordered components cover every dataset index. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Distinct graph components cannot use the same active sign coordinate. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The perturbation depends only on signs with a nonzero envelope-weighted frame. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The entire conditional likelihood, including its quadratic term, uses only active signs. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every component in the ordered list contains its selected root. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Distinct members of the ordered component list are disjoint. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The deterministic component ordering never repeats a component. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Agreement on a component's active signs preserves its entire conditional mark product. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.ComponentProduct 22 declarations Finite tensor product differentiation and second-order integration for the component amplitude path, retaining the sharp finite-array absolute-mass bound.
Finite tensor product differentiation and second-order integration for the component amplitude path, retaining the sharp finite-array absolute-mass bound.
The first product-rule array for a finite collection of scalar paths.
Definition (Lean source)
The second product-rule array, including every ordered pair of distinct factors.
The first product-rule array differentiates to the second product-rule array. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The absolute mass of a tensor array factors as the product of its absolute masses. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Replacing one tensor factor gives its absolute mass times those of the remaining factors. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Unit-mass factors make a one-factor replacement's absolute mass exactly that factor's mass. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Unit-mass factors make two distinct replacements' absolute mass the product of their masses. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The second product derivative has quadratic absolute mass when individual derivatives have absolute masses at most four and the base factors have unit absolute mass. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Free-amplitude component masses sum to one at every real amplitude. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
On the legal path every component mark mass is nonnegative. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The component probability array has unit absolute mass on the legal path. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The averaged first product-rule array along the component path.
Definition (Lean source)
The averaged second product-rule array along the component path.
Definition (Lean source)
The named slope is the derivative of the component mass path. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The named curvature is the derivative of the component slope path. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The named component slope vanishes at zero amplitude by fair-sign cancellation. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Averaging over signs preserves the quadratic bound on the component second derivative. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A vanishing initial slope and a bounded second derivative give the quadratic remainder by the mean-value inequality followed by integration of the first derivative. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Applying the scalar second-order bound to a signed projection controls the whole finite array without multiplying the bound by the number of its coordinates. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Integrating the component curvature twice gives the sharp second-order array bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The absolute-array bound gives the component coupling's failure-probability bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A nonsingleton component's expected number of changed marks is at most four times separation times the cube of its size, as required by the component-counting argument. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.ComponentSpanning 11 declarations General labeled spanning-tree assembly for the shared-sign component count.
General labeled spanning-tree assembly for the shared-sign component count.
A component induces a connected graph. Enumerating its vertices identifies a spanning tree
on Fin s; a finite union bound then applies the published Cayley count.
The induced graph on any selected component is connected, with no size restriction. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
For any fixed enumeration of a component, a labeled spanning tree exists in that component's graph. The enumeration is fixed before taking probabilities. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The component event is contained in the union over all labeled trees on its fixed vertex enumeration. This inclusion also covers singleton components. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A common probability envelope for specified labeled trees gives the component probability bound by the finite union bound and the explicit Cayley gate. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The general size-s count assembly: a specified-tree envelope, on arbitrary distinct sample coordinates, implies the binomial Cayley estimate for the actual component count. The tree probability estimate remains an explicit input here, rather than a paper-theorem premise. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The roadmap's general component-count bound follows from specified-tree probabilities on their own vertex spaces. Cayley and coordinate selection supply all the assembly factors. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The actual sparse dataset coupling obeys the Hamming-cost bound once each specified labeled tree has its geometric probability envelope. All component-count assembly is proved. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.ComponentTransport 15 declarations Additive transport costs for the finite product of component couplings.
Additive transport costs for the finite product of component couplings.
Pairing two assignments coordinatewise preserves all finite assignments.
Partition restriction factors array sums over any commutative semiring. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A normalized partition product preserves the expectation of any one block observable. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The shared-sign component list partitions any sum over dataset records. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Identical attached covariates make dataset replacements exactly mark replacements. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Hamming cost decomposes over the disjoint ordered components. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Summation over pairs of assignments equals summation over paired coordinates. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Each component's paired-coordinate coupling array has total mass one. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Converting the joint mass to an extended real preserves its component product. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Any component observable has its prescribed marginal under the full product coupling array. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conditional dataset coupling's expected Hamming cost is the sum of component costs. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The product coupling costs at most the sum of the nonsingleton cubic certificates. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Replacement Hamming cost is a Borel function of the two datasets. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Integrating the Borel conditional kernel preserves the exact additive transport cost. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The integrated dataset cost is bounded by the expected nonsingleton cubic component sum. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.Construction 54 declarations Public cells, count-weighted pair statistics and the single Laplace release; scalar, interval, dyadic tuning and inversion postprocessings are defined concretely.
Public cells, count-weighted pair statistics and the single Laplace release; scalar, interval, dyadic tuning and inversion postprocessings are defined concretely.
The equal cell width is twice the public radius divided by the public cell count.
Definition (Lean source)
Public cells partition the localization window with left endpoints included and only the final right endpoint included.
A cell selects the dataset indices whose covariates belong to that public cell.
Cell occupancy is the cardinality of the selected dataset indices.
Definition (Lean source)
The numerator pair kernel multiplies treatment difference by outcome difference.
The denominator pair kernel squares the treatment difference.
The count-weighted pair sum is zero below occupancy two, and otherwise weights the sum over unordered pairs by occupancy divided by the number of pairs.
A cell moment sum adds a record function across the selected dataset indices.
Definition (Lean source)
The numerator cell contribution uses the displayed closed treatment-outcome moment formula, with zero below occupancy two.
Definition (Lean source)
The denominator cell contribution uses the displayed closed treatment moment formula, with zero below occupancy two.
The numerator statistic sums the closed cell contributions.
Definition (Lean source)
The denominator statistic sums the closed cell contributions.
Definition (Lean source)
The sum of pairwise difference products equals the centered finite cross moment. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The pair kernels give the displayed count-weighted moment formulas, including s < 2. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Each public cell is a Borel covariate set, including the final endpoint. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Counting cell members is measurable on the full dataset space. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Summing a measurable record function over a public cell is measurable. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Numerically encoding a binary mark is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Each closed numerator cell contribution is measurable, including occupancies zero and one. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Each closed denominator cell contribution is measurable, including occupancies zero and one. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The numerator statistic is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The denominator statistic is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The public occupancy scale is sample size times radius times the truncated expected cell occupancy.
Definition (Lean source)
The public denominator floor is three sixty-fourths of the occupancy scale.
Definition (Lean source)
The public bias envelope retains the localization and rough-nuisance cell terms.
Definition (Lean source)
The public squared-error envelope retains localization, cell bias, occupancy and the Laplace second-moment terms with the specified multiplier.
The joint query consists of the numerator and denominator statistics.
Both coordinates of the joint query are measurable functions of the dataset. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The joint Laplace release is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The single joint Laplace release adds the specified independent noise to the two count- weighted statistics.
Definition (Lean source)
Clipping truncates a real number to the specified lower and upper endpoints.
The scalar postprocessing floors the noisy denominator and clips the ratio to the target range.
Finite closed endpoints give an interval code with both endpoints included.
Definition (Lean source)
The conservative interval centers the public radius at the clipped ratio and truncates it to the target range.
Definition (Lean source)
The floored clipped ratio is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The conservative interval postprocessing is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The scalar release is measurable postprocessing of the single joint noisy release.
Definition (Lean source)
The interval release is measurable postprocessing of that same single joint noisy release.
Definition (Lean source)
The numerical benchmark is the truncated maximum of the sampling, sparse-privacy and dense- privacy terms.
The public radius is the specified dyadic rounding of the benchmark scale.
The public integer cell count is twice the inverse fourth power of the dyadic radius.
Definition (Lean source)
The benchmark is strictly positive at every positive sample size. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Dyadic rounding brackets the benchmark between the radius and twice the radius. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
The integer conversion is exact on the dyadic branch; its radius, cell count and cell width obey the public construction constraints. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Public tuning returns zero in the constant branch and otherwise uses the specified dyadic pair-ratio release.
Public tuning returns the entire target range in the constant branch and otherwise uses the conservative pair-ratio interval.
Definition (Lean source)
The population cell mass is the real measure of the cell under the design marginal.
The population weight is expected occupancy multiplied by the probability of another record in the same cell.
The total occupancy weight sums the population cell weights.
Definition (Lean source)
The conditional record law is the observed marginal restricted to the cell and normalized by its mass.
The conditional numerator moment integrates the pair kernel under two independent draws from the conditional cell law.
Definition (Lean source)
The conditional denominator moment integrates its pair kernel under those independent draws.
Definition (Lean source)
The population numerator is the expectation of the count-weighted numerator under the dataset law.
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.CosineCertificate 24 declarations Assembly of complete sign-family membership and the fixed-sample chi-square certificate.
Assembly of complete sign-family membership and the fixed-sample chi-square certificate.
The micro radius is positive and no larger than the macro radius. the asserted conclusion follows.
Formal statement
Proof (Lean source)
Active centers lie in the integer interval between the two macro endpoint roundings. the asserted conclusion follows.
Formal statement
Proof (Lean source)
Counting the active centers costs at most the macro interval length plus three micro cells. the asserted conclusion follows.
Formal statement
Proof (Lean source)
The number of active signs is at most five times the macro-to-micro radius ratio. the asserted conclusion follows.
Formal statement
Proof (Lean source)
Updating one latent sign changes only its localized frame contribution. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A sign update has pointwise oscillation at most twice its envelope-weighted frame. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Outside the updated frame's support the perturbation is unchanged. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The roadmap's coordinate oscillation constants have the required total squared budget. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The Fourier overlap integrand is unchanged outside a replaced sign's frame support. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The centered overlap stays in a fixed bounded interval after covariate integration. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The boundedness hypothesis of the bounded-differences gate holds for each fixed second sign. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
A coordinate replacement in the overlap is exactly the integral of its localized change. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Only the two neighboring lattice frames can be nonzero, including at grid boundaries. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The two-frame Cauchy-Schwarz bound keeps every squared perturbation below twice the bump. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The centered quadratic Fourier coefficient is bounded by the local bump. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Replacing one sign changes the squared perturbation by at most twice the bump. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The sharp square bound gives a convenient rational sup-norm envelope. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The effect amplitude lies between zero and one for every legal macro radius. the asserted conclusion follows.
Formal statement
Proof (Lean source)
A coordinate replacement changes the Fourier overlap integrand by at most eight amplitudes. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
Restricting a micro support to the unit interval can only decrease its length. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Integrating the localized pointwise change gives the roadmap's sixteen-amplitude coordinate bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
For a fixed second sign vector, the centered overlap obeys the roadmap's mgf bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Averaging the fixed-second-sign mgf estimate gives the joint exponential bound. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Frame moments, model membership, the Fourier likelihood and fixed-sample chi-square certificate are conditional on the published bounded-differences mgf gate. The certificate records absolute continuity and square-density integrability explicitly, so its real-valued chi-square integral represents the finite divergence used in testing. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.CosineFamily 53 declarations Explicit uniform-design Bernoulli causal laws, overlapping cosine signs, and the conditional published-mgf certificate for the fixed-sample alternative mixture.
Explicit uniform-design Bernoulli causal laws, overlapping cosine signs, and the conditional published-mgf certificate for the fixed-sample alternative mixture.
The latent sign law is uniform on all sign vectors.
Definition (Lean source)
The nuisance perturbation multiplies the signed frame sum by the macro envelope.
Definition (Lean source)
A finite signed sum of Borel frames times the envelope is Borel measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Fair independent signs cancel the nuisance perturbation pointwise, including boundaries. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Off-diagonal frame terms cancel in the exact finite-sign second moment. The remaining geometric sum of squared frames is kept explicit. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The alternative propensity is one half plus the specified shared-sign perturbation.
Definition (Lean source)
The alternative control mean has the negative shared-sign term and negative effect bump.
Definition (Lean source)
The alternative treated mean has the negative shared-sign term and positive effect bump.
Definition (Lean source)
The shared-sign propensity is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The shared-sign control mean is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The shared-sign treated mean is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
A localized frame has absolute value at most one, and is zero outside its support. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
At most three closed frame supports cover a covariate, including support endpoints. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Closed-support counting gives a uniform bound on the signed perturbation, also at boundaries. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every legal macro radius gives valid binary probabilities for every sign vector. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The small public amplitude keeps every sign alternative inside the required overlap interval, uniformly over covariates and signs. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The concrete causal alternative has the specified shared-sign propensity and arm means, independent binary potential outcomes given the covariate, and consistency.
Definition (Lean source)
The fair Bernoulli parameters are valid probabilities. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The full-support null uses a uniform covariate and three conditionally independent fair binary variables, followed by consistency.
Definition (Lean source)
The fixed-sample alternative mixture averages the observed product laws uniformly over all sign vectors.
Definition (Lean source)
The one-record mixture averages the observed marginals uniformly over all sign vectors.
Definition (Lean source)
The treatment Fourier mark maps the binary treatment to minus one or one.
Definition (Lean source)
The conditional mark likelihood is the actual Bernoulli cell mass divided by the fair cell mass.
Definition (Lean source)
The effect bump equals one at the target covariate. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Proof (Lean source)
The shared nuisance terms cancel exactly in the alternative contrast. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
Every sign alternative has the prescribed point target. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The fair null has zero contrast at the target. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The fair null's treatment is independent of its potential outcomes given the covariate. the asserted conclusion follows.
Formal statement
Proof (Lean source)
Each shared-sign law has conditionally independent treatment and potential outcomes. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The fair null satisfies all conditions of the complete causal model. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Expanding the four Bernoulli cells gives the Fourier likelihood relative to fair marks. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Averaging the actual Fourier likelihood cancels both linear sign terms; its only remaining deviation from the fair likelihood is the squared-frame defect. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The uniform sign weight times the number of binary sign vectors is one. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The real-valued uniform sign weight normalizes the finite number of vectors. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Integrating any real function against the sign law is its finite uniform average. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The nuisance perturbation has expectation zero under the actual sign probability law. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The actual sign-law second moment leaves only the squared-frame geometric factor. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Under the actual sign law, the averaged likelihood has exactly the squared-frame defect. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The exact localized frame partition makes the sign second moment equal to the effect bump. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The actual conditional likelihood has sign average one at every covariate and mark. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Summing the four-cell likelihood over all signs gives exactly the number of sign vectors. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The uniform average of every actual conditional Bernoulli mark mass is the fair mass. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Averaging the observed one-record laws gives the fair null measure exactly. the asserted conclusion follows.
Formal statement
Proof (Lean source)
Each observed sign alternative is dominated by eight times the fair observed null. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The finite sign mixture is dominated by eight to the sample-size power times the null dataset law. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The uniform finite sign law is a probability measure. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The sign mixture of observed product laws is a probability measure. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
The dataset sign mixture is absolutely continuous with respect to the fair null experiment. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The squared density deviation of the sign mixture is integrable under the fair null experiment. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The direct treated mean is one half plus the localized effect bump.
Definition (Lean source)
The direct treated mean is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The direct alternative has valid binary parameters at every legal macro radius. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The direct localized causal law has fair treatment and control potential outcome and the specified perturbed treated potential outcome, followed by consistency.
Definition (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.CosineRegularity 14 declarations Global Lipschitz and Holder certificates for the shared-sign causal alternatives.
Global Lipschitz and Holder certificates for the shared-sign causal alternatives.
The micro radius is no larger than the macro radius in the published range. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Only frames supported at one of the two points contribute to the signed-sum difference. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The same support counting bounds the unlocalized signed sum by three. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Multiplication by the macro envelope preserves a uniform micro-scale Lipschitz modulus. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The effect bump satisfies the same coarse micro-scale modulus as the perturbation. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The micro radius to the one-tenth power is exactly the square root of the macro radius. The result uses the stated assumptions and establishes the displayed conclusion.
Proof (Lean source)
The square-root amplitude cancels the micro-scale Holder loss with a small constant. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The small effect amplitude is bounded by the square-root amplitude. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The perturbation's two-scale bounds imply the one-tenth Holder modulus. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The bounded effect bump has the analogous one-tenth Holder modulus. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The actual propensity satisfies the model's radius-three Holder requirement. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The actual control mean satisfies the model's radius-three Holder requirement. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Nuisance cancellation and the effect-bump modulus give the required contrast regularity. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every shared-sign alternative belongs to the complete model, with all three regularity requirements derived from its explicit cosine construction. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.DatasetMarginals 20 declarations Finite atomic product kernels identify the integrated conditional dataset laws with the sign mixture and null product experiment, certifying the coupling marginals.
Finite atomic product kernels identify the integrated conditional dataset laws with the sign mixture and null product experiment, certifying the coupling marginals.
Independent finite atomic laws expand into the array of products of their weights. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conditional observed law for a fixed sign vector at one covariate.
Definition (Lean source)
The fixed-sign conditional record law varies measurably with the covariate. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Each fixed-sign conditional record law is a probability measure. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The fixed-sign observation kernel attaches the covariate to its conditional marks.
Definition (Lean source)
The fixed-sign observation kernel is everywhere probability-valued. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Integrating a fixed-sign conditional record reproduces the observed causal law. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Given fixed signs, the conditional dataset law has independent mark weights.
Definition (Lean source)
The conditional fixed-sign dataset array equals the coordinatewise product kernel. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The fixed-sign conditional dataset array is Borel measurable. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Integrating a fixed-sign dataset kernel yields the observed product law. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conditional alternative law is the uniform mixture of the fixed-sign dataset kernels. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Integrating the alternative conditional law gives the specified mixture of product laws. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The constructed dataset coupling's first marginal is the actual sign-mixture experiment. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The fair observation kernel attaches independent uniform binary marks to its covariate.
Definition (Lean source)
The fair observation kernel is a Markov kernel.
Definition (Lean source)
The fair conditional observation integrates to the observed null law. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The fair conditional dataset array equals the coordinatewise fair observation kernel. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Integrating the fair conditional dataset law yields the null observed product law. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The Borel common-mass construction couples the two specified dataset experiments. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.DesignPairMoments 10 declarations Actual conditional design laws and cross-treatment pair moments.
Actual conditional design laws and cross-treatment pair moments.
The actual design distribution conditioned on a public cell.
Every admissible public cell has a normalized conditional design law. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Conditional design integrals retain the actual within-cell density. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Two independent conditional covariates belong to their conditioning cell almost surely. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Cross-treatment numerator at two selected covariates.
Cross-treatment probability at two selected covariates.
The propensity, arm means, and arm-response regressions are integrable under any finite covariate measure, because the complete model gives everywhere binary-mean bounds. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Factorization of independent design pairs gives the exact numerator formula. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Factorization of independent design pairs gives the exact denominator formula. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Integration of the pointwise causal certificate preserves the density-weighted cell bias. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.DirectCoupling 17 declarations The shared-threshold direct experiment coupling and its independent-record transport cost.
The shared-threshold direct experiment coupling and its independent-record transport cost.
The localized bump has integrated mass at most the length of its macro support. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The crossing probability includes the fair treatment probability.
Definition (Lean source)
The crossing mass fits within the fair treated-zero atom. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Integrating the shared thresholds leaves four common atoms and one crossing atom.
Definition (Lean source)
The finite shared-threshold law is a measurable conditional measure. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Conditional shared thresholds have total mass one. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Only the crossing atom contributes to the conditional disagreement cost. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Integrate the conditional shared-threshold coupling over the common uniform covariate.
Definition (Lean source)
The common covariate and conditional shared thresholds give a probability coupling law. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The fair marginal of the shared-threshold conditional coupling. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The treated marginal of the shared-threshold conditional coupling. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The first integrated marginal is the observed fair null law. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The second integrated marginal is the observed direct alternative law. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The integrated disagreement cost is bounded by the crossing probability and macro support. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Independent copies of the shared-threshold record pair are regrouped into two datasets.
The independent-record construction has the two prescribed product marginals. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Hamming cost adds the identical one-record crossing costs over all independent records. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.FrameGeometry 20 declarations Localized cosine frames and their exact squared partition identity, including lattice and macro support boundaries.
Localized cosine frames and their exact squared partition identity, including lattice and macro support boundaries.
The lower-family micro radius is the fifth power of its macro radius.
Definition (Lean source)
The amplitude constant is two to the power minus twelve.
Definition (Lean source)
The target separation is the amplitude constant times the macro radius.
Definition (Lean source)
The macro envelope is the squared cosine inside the localization window and zero outside.
The effect bump squares the macro envelope.
Definition (Lean source)
Each overlapping cosine frame element is supported within one micro radius of its integer center.
The localized macro envelope is Borel measurable, including its boundary convention. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Squaring the macro envelope preserves measurability. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Each localized cosine frame is Borel measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The squared-cosine envelope takes values between zero and one. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The effect bump also takes values between zero and one. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Proof (Lean source)
The finite active integer indices have frame interiors intersecting the interior of the macro window.
The latent signs are binary encodings of minus one and one on the active index set.
Definition (Lean source)
The finite index construction selects exactly the strict support intersections for every legal macro radius. The displayed conclusion follows.
Formal statement
Proof (Lean source)
A frame vanishes at either support endpoint and beyond it. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The macro envelope vanishes at its endpoints as well as outside its support. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
An index omitted from the active frame set contributes zero after localization. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
On a lattice interval the two neighboring frame squares sum to one. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
All frames except the two neighboring indices vanish on a lattice interval. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Localizing the finite frame square sum gives exactly the effect bump everywhere. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.FrameRegularity 7 declarations Global moduli of the localized cosine envelope and effect bump, including support boundaries.
Global moduli of the localized cosine envelope and effect bump, including support boundaries.
Clamping the displacement to the support interval realizes a zero-extended cosine exactly. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A zero-extended cosine has its global cosine Lipschitz bound across both support endpoints. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Squaring values in the unit interval at most doubles their absolute difference. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The macro envelope has a global Lipschitz modulus, with no exception at support boundaries. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The squared envelope has a global Lipschitz modulus inherited from the envelope. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Each micro-frame has the global modulus of its zero-extended cosine. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A bounded oscillation and a Lipschitz modulus give the one-tenth Holder modulus by splitting distances at the public radius. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.IntervalEvents 1 declarations Borel point-containment events for the shared interval representation.
Borel point-containment events for the shared interval representation.
Point containment is Borel for every empty, finite, or unbounded interval code. The displayed conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.Inversion 11 declarations Explicit endpoints and measurability for the affine acceptance-set inversion.
Explicit endpoints and measurability for the affine acceptance-set inversion.
Positive denominators turn the affine acceptance inequality into two explicit endpoints. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Clipping places the center inside the target range, so the truncated endpoints are ordered. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A nonpositive denominator gives the full range at zero, a singleton at zero radius, or an empty acceptance set. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The inversion accepts exactly the target-range candidates satisfying the specified floored and clipped affine inequality.
The inversion returns the closed interval hull of the accepted set, with the prescribed full- range fallback.
Definition (Lean source)
The interval hull inversion has explicit endpoints on every denominator branch. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The explicit inversion is measurable, including the zero and negative denominator cases. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The publicly tuned inversion uses the same single joint release and returns the full target range in the constant branch.
Definition (Lean source)
The numerical interval scale output is the benchmark.
Definition (Lean source)
The fixed interval lower constant is two to the power minus twenty.
Definition (Lean source)
The fixed interval upper constant is two to the power twenty-two.
Definition (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.MixtureOverlap 31 declarations Exact iid likelihood-overlap expansion of the shared-sign mixture and its reduction to a finite exponential average.
Exact iid likelihood-overlap expansion of the shared-sign mixture and its reduction to a finite exponential average. All domination and integrability conditions are derived.
Every observed causal law is a probability measure. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The finite sign weight is the reciprocal of the number of sign vectors. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The dataset sign mixture is exactly the library's uniform finite iid mixture. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Finite domination bounds the real density under the reference measure. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Products of the alternative one-record densities are integrable, with bound sixty-four. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The one-record density overlap is the nonnegative likelihood inner product.
Definition (Lean source)
Each one-record density overlap is nonnegative. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
One plus the dataset mixture divergence is exactly the uniform average of nth powers of one-record overlaps; the iid product and finite-mixture identities come from Causalean. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Nonnegative likelihood overlaps raised to n are dominated by the exponential of the centered overlap times n, as used in the fixed-sample roadmap. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The exact iid mixture identity reduces its divergence bound to a finite exponential average, without any additional integrability or absolute-continuity assumptions. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The centered conditional likelihood inner product in the paper's Fourier expansion.
Definition (Lean source)
Orthogonality of the four fair marks leaves exactly the two terms of the centered overlap integrand, pointwise in the covariate. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The centered overlap integrand is Borel measurable in the covariate. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The finite sign second moment is exactly the number of signs times the bump, including macro endpoints and lattice boundaries. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Averaging the centered integrand over the first sign vector gives zero for every fixed second sign vector and every covariate, exactly as required by the mgf step. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The actual sign probability law gives the centered integrand mean zero pointwise. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The fair observed null integrates four equally weighted mark cells at each covariate. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The actual conditional likelihood is measurable on the full observed record space. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Every actual conditional mark likelihood is nonnegative for legal macro radii. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conditional four-cell likelihood is the actual observed density relative to the fair null. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The real observed density is the stated likelihood almost everywhere under the null. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Nonnegative real functions under the fair null integrate their four-cell average. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Each actual conditional likelihood is at most four, since a Bernoulli cell mass is a product of two probabilities at most one. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The centered Fourier overlap integrand lies between minus one and fifteen. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The covariate overlap integral is integrable by its measurable bounded construction. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The paper's centered likelihood inner product integrates the Fourier overlap terms.
Definition (Lean source)
The observed density overlap equals one plus the explicit Fourier covariate integral. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Finite averaging commutes with the bounded covariate integrals; the centered overlap has sum zero in its first sign vector for every fixed second vector. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The centered likelihood overlap has expectation zero under the actual sign law. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The exact fixed-sample chi-square identity uses the paper's centered Fourier overlap. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The dataset divergence is bounded by the uniform exponential average of the explicit centered Fourier overlap; only the bounded-differences estimate remains to be assembled. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.Occupancy 27 declarations Occupancy cancellation and design-uniform population bias and denominator bounds.
Occupancy cancellation and design-uniform population bias and denominator bounds.
Density bounds compare every design-event mass with its Lebesgue mass. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Each cell's endpoints lie in the unit interval and differ by the public width. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Including the final right endpoint does not change the Lebesgue mass of a cell. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The complete model supplies both cellwise mass estimates without design smoothness. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Summing equal-cell mass bounds gives the local-window mass bounds. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every population cell mass lies between zero and one. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The probability of no partner has the usual exponential envelope. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The union bound controls the probability that a cell has a partner. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The exponential partner probability dominates a rational envelope. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The rational envelope controls both sparse and dense occupancies uniformly. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The lower cell-mass bound gives a uniform partner-probability lower bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The upper cell-mass bound gives a uniform partner-probability upper bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Summing the partner envelopes gives both design-uniform occupancy comparisons. The premises are the cell-mass estimates supplied by the model's density bounds. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The density bounds imply both occupancy comparisons for every law in the complete model. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The common occupancy weights are nonnegative, even without model assumptions. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The public information and denominator floor are strictly positive on the public domain. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A common nonnegative weight preserves the cellwise denominator lower bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Common nonnegative weights preserve the conditional cell bias certificate. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Dividing a weighted bias certificate by a positive denominator gives the ratio bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The independent cross-treatment probability is at least three eighths under overlap. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The pointwise conditional numerator identity gives the paper's cellwise bias envelope. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every point of a public cell lies within the public radius of the target covariate. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Two covariates in one cell are separated by at most the public cell width, including the right endpoint of the final cell. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The two one-tenth Holder remainders multiply to the one-fifth cell-width term. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Expanding the two cross-treatment cases separates nuisance variation from the contrast. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
At any two covariates in one cell, the independent binary cross-treatment moments satisfy both the denominator lower bound and the paper's complete bias envelope. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The population identities and cellwise certificates imply the floor and ratio bias bounds. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.PartnerProbability 13 declarations Product-law probabilities of a record having another record in a specified cell.
Product-law probabilities of a record having another record in a specified cell.
The observed probability of a covariate cell equals its design probability. The displayed conclusion follows.
Formal statement
Proof (Lean source)
A product rectangle has real mass equal to the product of its coordinate real masses. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Under iid sampling, none of the other records belongs to a fixed measurable event with probability p with probability (1-p)^(n-1). the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The probability that the distinguished record belongs to an event and all other records avoid it is p(1-p)^(n-1). the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Avoidance by all records except the distinguished one is a measurable event. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The real mass of a single iid coordinate event is the observed marginal mass. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The old record has a partner in a measurable event with probability p[1-(1-p)^(n-1)]. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
An independent replacement has a partner among the unreplaced records with the same probability p[1-(1-p)^(n-1)]. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Having a partner in a measurable event is itself a measurable dataset event. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Counting members with a distinct partner discards exactly the empty and singleton counts. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The eligible cell occupancy is the sum of record-level partner indicators. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Eligible occupancy is integrable under every finite dataset measure. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The binomial occupancy identity follows by summing iid record-partner probabilities, without requiring independence between different cell counts. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.PartnerVariance 23 declarations Partner-sensitive replacement increments and the occupancy-weighted Efron--Stein assembly.
Partner-sensitive replacement increments and the occupancy-weighted Efron--Stein assembly.
Inserting one record into an arbitrary selected set changes each scalar causal contribution by at most three, at every count. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Without a remaining selected record, both scalar contributions before and after insertion are zero. With a partner, the scalar insertion bound is three. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The partner indicator records whether a proposed record shares a public cell with any record other than the replaced index.
Definition (Lean source)
Partner indicators take only the values zero and one. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The two datasets in a replacement have identical cell selections after erasing its index. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A scalar cell replacement is bounded by the old and new partner indicators in that cell. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Disjointness reduces the sum of cellwise partner envelopes to the single partner indicator. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Each scalar replacement increment vanishes without partners and is at most three times the sum of its old and new partner indicators. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Squared scalar replacement increments are bounded by eighteen times the two partner indicators, exactly the deterministic envelope in the variance roadmap. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Partner indicators are Borel functions of the dataset and proposed record. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Partner indicators are bounded by one and integrable under every finite measure. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The squared replacement differences of the bounded statistics are integrable under every finite measure on dataset and replacement pairs. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Disjoint public cells express the partner indicator as a sum of cell event indicators. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Existence of an unreplaced record in an event is measurable. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Old and independent-copy cell partner indicators both have the Bernoulli occupancy mean. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The old-record partner indicator is Borel on the dataset and independent-copy space. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The old-record partner indicator is integrable under any finite pair measure. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Cellwise partner indicators are integrable for any finite pair measure. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Each of the two partner indicators has mean W/n under the iid law and its independent copy. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The old-plus-new partner expectation is exactly twice W/n. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Integrating the deterministic squared replacement bound reduces both second moments to the common old-plus-new partner expectation. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Efron--Stein converts the two occupancy-weighted replacement second-moment estimates into the asserted variance bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Sensitivity includes every input and every occupancy; iid variance on the complete model is controlled by the population occupancy weight. The replacement-copy inequality is an explicit assumed gate. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.PointVersion 26 declarations Continuity selects the uniquely identified point-CATE representative from the observed law.
Continuity selects the uniquely identified point-CATE representative from the observed law.
The model's contrast modulus is an ordinary Lipschitz bound. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The selected contrast is continuous under the complete model. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The positive design density transfers design-null sets to Lebesgue-null sets. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Continuous functions on the unit interval that agree Lebesgue-almost everywhere agree at every point, including the two boundary points. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Positive design density makes the continuous representative of the contrast unique. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The treatment coordinate is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The observed outcome coordinate is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Each treatment-arm event is measurable. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The arm-specific design measure evaluates a covariate set as its joint arm event. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
The selected propensity and its complement integrate to the two arm probabilities. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Overlap transfers arm-specific null sets to design null sets. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The control Holder modulus gives continuity of the selected control mean. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Continuity of the control mean and contrast gives continuity of the treated mean. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The observed binary response bounds each selected arm mean almost everywhere. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Continuity and positive arm support extend the binary mean bounds to every covariate. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The difference of the two binary arm means bounds the point target between minus one and one. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The observation map is measurable. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The observed marginal determines each arm-specific covariate measure. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The observed marginal determines the response integral on every joint covariate-arm event. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Equal observed laws have identical continuous arm-mean versions at every covariate. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The observed law identifies the point target through uniqueness of the continuous arm means. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Each arm-specific design measure has the selected arm probability as its density relative to the design. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A measurable binary response is integrable under any finite measure. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Exchangeability factors the arm-potential product; consistency and overlap identify its conditional mean. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Conditional-expectation linearity identifies the selected contrast with the conditional causal effect. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Model regularity selects a unique continuous contrast, bounds the target, and identifies both the conditional causal contrast and its point value from the observed marginal. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.PrivateComparison 9 declarations Private Hamming comparison, unrestricted Markov contraction, and finite-chi-square TV bounds.
Private Hamming comparison, unrestricted Markov contraction, and finite-chi-square TV bounds.
A composed probability kernel evaluates an event by averaging its row probabilities. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Proof (Lean source)
Averaging a Markov kernel contracts total variation, by the bounded-function dual bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Finite squared density deviation supplies the integrability needed for the chi-square TV bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Convexity on the unit interval bounds the privacy exponential increment. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Privacy in both directions bounds the event-probability change on an adjacent pair. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A one-coordinate oscillation bound sums along the finite Hamming replacement path. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Pure privacy controls every event along the Hamming path, including out-of-model datasets. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Integrating the Hamming event bound against any coupling controls output total variation. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Replacement privacy contracts expected Hamming transport. Ordinary Markov contraction needs no privacy, and finite chi-square divergence gives the square-root TV bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.RateRegimes 13 declarations Exact comparisons of the benchmark terms and the four public budget regimes.
Exact comparisons of the benchmark terms and the four public budget regimes.
The sparse-privacy term meets the sampling term at the fourth-root budget. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The dense-privacy term meets the sampling term at the square-root budget. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The two privacy terms meet at the three-fifths budget. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Reversing the budget comparison reverses the order of the two privacy terms. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
In the large-budget regime both privacy terms are below the sampling term. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
In the intermediate sparse regime the sparse-privacy term is the maximum and below one. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
In the dense regime the dense-privacy term is the maximum and below one. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Below the inverse-sample-size budget the dense term reaches the cap. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Unit budget gives exactly the nonprivate sampling benchmark. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The capped dense-privacy term is always a lower bound for the benchmark. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
Divergence of sample size times budget makes all three benchmark terms vanish. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
A vanishing benchmark forces sample size times budget past every finite bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The numerical benchmark vanishes exactly for diverging sample size times budget. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.ReleaseMoments 3 declarations Exact centered Laplace release moments and the uniform density-free squared-error guarantee.
Exact centered Laplace release moments and the uniform density-free squared-error guarantee.
The constructed pair release is the measurable Laplace kernel. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The released coordinate squares add exactly two independent Laplace variances to the input variances, with no inflation of the noise coefficient. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Integrating the pointwise floored-ratio bound and exact release moments proves the public second-moment envelope throughout the complete model. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.SelectionLaw 11 declarations Membership-label rectangles and their normalized iid product laws.
Membership-label rectangles and their normalized iid product laws.
Specifying every cell membership label is a rectangle in the iid sample space. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every exact membership-label event is measurable. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Restricting the iid sample law to specified labels factors coordinate by coordinate. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Normalizing any positive-mass restriction gives a probability law. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Dividing a positive rectangle restriction by its mass preserves the product structure. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Given a specified positive-probability label pattern, all records are independent with coordinate laws conditioned on their own labels. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
On an exact label event, two selected coordinates have the independent conditional cell law, irrespective of the membership of the other records. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Every selected pair on a fixed label event has the same kernel expectation. This is the conditional pair identity needed before summing the unordered pairs and then the label events. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The complete density model gives positive probability to either membership label. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A normalized exact label event is a probability measure. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Summing the selected unordered pairs at fixed membership labels gives occupancy times the common conditional pair moment. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.SignBlockFactorization 4 declarations Finite fair-sign averages factor over disjoint coordinate blocks, by iterating Causalean's two-block expectation identity.
Finite fair-sign averages factor over disjoint coordinate blocks, by iterating Causalean's two-block expectation identity.
A single latent sign is a fair bit.
Definition (Lean source)
The independent fair-bit design expectation is the uniform finite sign average. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
An arbitrary finite family of functions using pairwise disjoint coordinate blocks has factorized product expectation under an independent coordinate design. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
Uniform fair-sign averaging commutes with a product of functions of disjoint sign blocks. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.SignProduct 3 declarations Uniform finite sign averages as independent fair-bit product integrals, and the published bounded-differences gate transported to arbitrary finite sign indices.
Uniform finite sign averages as independent fair-bit product integrals, and the published bounded-differences gate transported to arbitrary finite sign indices.
Every atom of the independent fair-bit product has the same reciprocal-cardinality mass. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Integrating a function of independent fair bits is exactly its uniform finite average. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The published independent-coordinate mgf gate bounds a centered uniform finite-sign average on any finite index type, after reindexing its coordinates by Fin. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.Stability 31 declarations All-count sensitivity and Efron--Stein-conditional iid variance stability.
All-count sensitivity and Efron--Stein-conditional iid variance stability.
Appending a last index adds exactly its pairs with the existing indices. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The number of ordered index pairs with the first strictly smaller is the binomial count. The displayed conclusion follows.
Formal statement
Proof (Lean source)
A unit-bounded kernel has a pair sum bounded by the number of pairs. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Count-weighted pair contributions are bounded by the occupancy, at every count. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
At occupancy at least two, insertion equals twice the new-pair average minus the old pair average, as in the all-count stability roadmap. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The new pairs have total absolute value at most the old occupancy. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Inserting into a cell with at least two records changes a scalar contribution by at most three, using the exact pair identity rather than a count-specific approximation. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A singleton contributes zero, and the first pair contributes twice its kernel value. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The insertion bound includes empty and singleton cells as well as all larger occupancies. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Both causal pair kernels are symmetric, and their joint absolute mass is at most two. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The causal numerator and denominator satisfy the scalar unit-kernel bound. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Proof (Lean source)
The two causal contributions have joint insertion sensitivity at most six at every count. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
A replacement through a common deleted dataset has joint sensitivity at most twelve. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The insertion indicator bound yields the squared replacement bound used by Efron--Stein. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Reindexing the selected record set by any finite enumeration preserves its moment sums. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every enumeration of the records in a cell realizes its closed numerator and denominator as count-weighted pair contributions. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Each scalar cell contribution is bounded by its occupancy, including empty and singleton cells. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Distinct public cells are disjoint, including the final right endpoint. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Disjoint cell selection counts each dataset record at most once. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Both scalar statistics are bounded by the sample size on every input dataset. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The bounded measurable statistics belong to every finite-measure Lp space, in particular the square-integrability class needed for Efron--Stein. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The closed numerator moment formula on an arbitrary finite selected record set.
The closed denominator moment formula on an arbitrary finite selected record set.
An arbitrary finite record selection has the same closed moments as its enumerated pair contributions. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Inserting one record into an arbitrary selected set changes the joint causal contribution by at most six, at every count. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Selected contributions depend only on records at the selected indices. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Erasing one selected record has joint sensitivity at most six; erasing an absent record has zero effect. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A replacement changes only its old and new cells, using their common erased selection. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A covariate belongs to at most one public cell, so its summed insertion envelope is at most six. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Deletion followed by insertion bounds the joint statistic change by twelve, including replacements between different cells. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Hamming-distance-one datasets satisfy the asserted joint sensitivity bound on the entire input space. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.TestingPriors 12 declarations Two finite, class-supported priors with fixed target separation and uniformly close outputs under every private Markov kernel.
Two finite, class-supported priors with fixed target separation and uniformly close outputs under every private Markov kernel.
A finite prior uniformly averages the observed product laws of its constituent causal laws.
The direct alternative has the localized contrast prescribed by the construction. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The direct alternative has exactly the common target required by the testing prior. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Scaling the bump cancels its inverse-radius modulus, giving radius-three regularity. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The explicit direct law satisfies every condition of the complete unknown-density model. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A singleton uniform prior is the observed product law itself. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Enumerating all sign vectors gives exactly the uniform sign mixture. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The sampling-radius sign experiment remains close after every Markov release. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The proof selects signs when the sampling scale is a maximum, or when the sparse scale strictly dominates both other scales. At sample size times budget at most one it selects the direct family; otherwise ties favor sampling, then direct, then sparse.
Definition (Lean source)
In every branch selecting the direct experiment, the benchmark is the capped square-root privacy scale, including ties with the sparse scale. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The selected direct radius has the uniformly small privacy-transport scale computed in the testing-prior roadmap. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The proof-selected uniform sign mixture or direct product law at one quarter of the benchmark has the stated separation and TV bound after every private standard-Borel release. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.TreeGeometry 10 declarations Geometric support restrictions and rooted integration bounds for shared-sign trees.
Geometric support restrictions and rooted integration bounds for shared-sign trees. Each child is integrated in its parent's micro neighborhood; the root is in the macro window.
A nonzero localized frame is strictly inside both the macro and micro supports. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Any subset of a real-radius neighborhood in the unit interval has volume at most its length. The displayed conclusion follows.
Formal statement
Proof (Lean source)
The potential child region of a frozen parent has length at most four micro radii. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The root region has length at most two macro radii. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The exact rooted-order integral for successive children constrained to their parent's neighborhood. The parent selector reads only the already sampled covariates.
Definition (Lean source)
Each newly integrated child costs at most four micro radii, regardless of the previous covariates or the choice of its parent among them. The displayed conclusion follows.
Formal statement
Proof (Lean source)
Integrating the root and then the children gives the roadmap's specified-tree envelope. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.TreeOrdering 6 declarations Parent-before-child enumerations of finite connected graphs and the resulting specified labeled-tree probability bound.
Parent-before-child enumerations of finite connected graphs and the resulting specified labeled-tree probability bound. This closes the geometric input to the general Cayley component-count estimate and sparse common-mass Hamming-cost bound.
Every finite connected graph has an ordering in which each non-root vertex has an earlier neighbor. Removing a non-cut vertex constructs the ordering inductively. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Every specified labeled tree has the roadmap probability envelope, without an assumed enumeration or probability bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The actual size-s component count has the binomial Cayley expectation bound under iid uniform design. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The constructed common-mass coupling has expected Hamming cost at most 1024 times separation, squared sample size, macro radius, and micro radius in the sparse regime. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.TreeProbability 8 declarations Product-measure bounds for rooted trees enumerated in parent-before-child order.
Product-measure bounds for rooted trees enumerated in parent-before-child order.
Appending an independent uniform child multiplies any prefix event's probability by at most four micro radii. The selector can be any measurable function of the prefix. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
An independent last coordinate obeys the child-extension bound in the original finite product space, without introducing a conditional probability version. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The rooted geometric event obtained by successively adding a child whose parent is a function of the earlier covariates. Coordinate projections give ordinary ordered labeled trees.
Definition (Lean source)
The ordered rooted-tree event is Borel whenever each parent selector is Borel. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Under iid uniform design, any parent-before-child rooted tree has probability bounded by its root length times one child length per edge. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.TreeSeries 17 declarations Numerical summation of the labeled-tree envelope for sparse shared-sign components.
Numerical summation of the labeled-tree envelope for sparse shared-sign components.
In the sparse regime, the differentiated geometric envelope is at most three. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Each tree-series coefficient is bounded by the differentiated geometric majorant. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Summing the tree coefficients under the sparse cap gives the roadmap's constant thirty-two. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The sample sparsity cap places the exponential tree-series argument below one eighth. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The finite numerical tree series is uniformly bounded in the sparse sample regime. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Each cubic component-count envelope factors into the numerical tree coefficient. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The full labeled-tree cubic envelope is at most the transport constant in the roadmap. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The number of shared-sign components with a specified size, counted without repeated roots.
Definition (Lean source)
Every ordered component has between one and the sample size many vertices. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Empty components never contribute to the component-size count. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Grouping a component observable by size is an exact finite counting identity. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Component counts are Borel because they are constant on each finite labeled-graph stratum. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The expected nonsingleton cubic sum is exactly the sum of the expected component counts. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Removing sizes zero and one reindexes any vanishing observable by nonsingleton sizes. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The expected nonsingleton cubic component cost is indexed by sizes two through n. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Component-count expectations bounded by the labeled-tree envelope give the claimed cubic cost. This implication leaves the geometric spanning - tree probability estimate as an explicit input, without inserting it into a frozen paper theorem. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
For the actual dataset coupling, the remaining tree-count probability estimate implies its full sparse Hamming cost certificate. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.TunedLength 4 declarations Uniform expected interval length under the public tuning, including its fallback branch.
Uniform expected interval length under the public tuning, including its fallback branch.
The tuned variance envelope bounds twice the conservative interval radius. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The public full-range fallback has length two under every model law. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The tuned interval obeys the stated expected-length rate at every law, from the deterministic radius bound on the active branch and the full-range length on the fallback branch. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Taking the supremum over the full model preserves the public interval-length bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.TunedRisk 4 declarations Absolute risk from the squared-error envelope under public tuning.
Absolute risk from the squared-error envelope under public tuning.
Young's quadratic inequality converts a second moment to an absolute first moment. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The data-independent zero release has absolute risk at most one throughout the model. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The active tuned scalar release attains the absolute-risk rate from its second moment. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The fallback and active tuning branches give the uniform scalar-risk rate once the uniform statistical second moment has been proved. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.TuningEnvelope 7 declarations The benchmark constraints and the dyadic public tuning variance envelope.
The benchmark constraints and the dyadic public tuning variance envelope.
A reciprocal-root lower bound is equivalent to the corresponding polynomial constraint. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Below the public fallback threshold the cap is inactive, so each candidate scale bounds its polynomial information constraint. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Dyadic rounding loses at most a factor of sixty-four in the occupancy scale. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The three candidate rate constraints imply the two scaled information lower bounds used by the public variance envelope. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The scaled information bounds control the inverse occupancy and inverse privacy scales. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
At the tuned cell width, the roughness term equals the squared macro radius. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The public tuning puts the entire second-moment envelope below the roadmap's squared-rate constant, independently of the law or the statistical second-moment proof. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.Helpers.UpperGuarantees 35 declarations Uniform private scalar-risk, coverage and length guarantees for the total single-release construction and its public tuning, over the full unknown measurable-density model.
Uniform private scalar-risk, coverage and length guarantees for the total single-release construction and its public tuning, over the full unknown measurable-density model.
The positive public budget normalizes the everywhere-defined noisy pair release. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The all-count sensitivity bound gives pure privacy for the single joint release. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Measurable postprocessing preserves normalization and replacement privacy for any output carrier. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The clipped, floored ratio inherits pure privacy on all datasets. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The conservative interval inherits pure privacy from the same joint release. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A data-independent probability release is private at every nonnegative budget. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Public tuning preserves privacy, including its data-independent fallback. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The tuned interval remains private in both public branches. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Finite closed endpoint codes denote the usual real closed interval. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The length of a finite closed interval is its nonnegative endpoint difference. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The ratio center always belongs to the target range, even on arbitrary datasets. The displayed conclusion follows.
Formal statement
Proof (Lean source)
A nonnegative radius around a center in the target range has ordered truncated endpoints. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The released conservative interval is nonempty and contains its clipped center. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Truncation bounds each interval by the target diameter and twice its public radius. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Integrating the deterministic interval-length bound gives the finite-sample guarantee. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Projection to the target range cannot increase distance to a target in that range. the asserted conclusion follows. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The denominator floor fixes the population denominator and contracts its perturbation. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The raw floored ratio is controlled by the two coordinate perturbations over the floor. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Bias plus the two released coordinate perturbations controls the clipped estimator error. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Nonnegative occupancy weights preserve the binary pair numerator domination. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The population comparison ratio belongs to the target range. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Two applications of the quadratic sum bound give the roadmap's pointwise squared error. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
For each model law, only the public bias and released centered coordinate squares are needed. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Squaring the roughness term converts its fifth-root power to the two-fifths power. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The quadratic sum inequality bounds the two contributions to the public bias. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Substitution of the public floor converts the occupancy and noise terms to inverse scales. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The roadmap's bias, occupancy variance and independent Laplace variance fit the public envelope. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Truncation retains any target in the model range within the public radius of the center. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
The public variance envelope is strictly positive on admissible radii and cell counts. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Markov's inequality turns a second-moment envelope into a one-tenth radius-tail bound. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The truncated interval misses a model-range target only on the radius-tail event. The result uses the stated assumptions and establishes the displayed conclusion.
Formal statement
Proof (Lean source)
Scalar postprocessing expresses the mean-square error as an integral over the joint release. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The finite-sample second-moment guarantee implies coverage for the interval from the same joint release, including targets on the boundary of the model range. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The public fallback interval covers every law in the complete model with probability one. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Coverage of the tuned interval follows from the tuned second moment on its active branch and full-range coverage on its fallback branch. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.TMatchedRiskFrontier 6 declarations Matched private absolute-risk frontier over all total randomized mechanisms in the same observation experiment, attained above by the explicit publicly tuned release.
Matched private absolute-risk frontier over all total randomized mechanisms in the same observation experiment, attained above by the explicit publicly tuned release.
A nonempty finite uniform prior is a probability measure. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Kernel composition distributes over a finite sum of input laws. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Prior-averaged loss at a common target is bounded by the maximal class risk, including when the latter is infinite. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A real error event of probability at least three eighths forces absolute loss. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Le Cam's two-error inequality and finite-prior averaging give the scalar converse. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The minimax risk lies between the specified fixed multiples of the benchmark. The total publicly tuned kernel attains the upper bound across the entire complete model. The public parameters and their domains and the Efron--Stein gate, bounded-differences gate, and Cayley gate specify the conditional scope.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.TRegimeAndSanity 5 declarations Exact public-budget regimes, the unrestricted nonprivate order, and the exact condition for consistency along budget sequences.
Exact public-budget regimes, the unrestricted nonprivate order, and the exact condition for consistency along budget sequences.
The matched risk frontier transfers the benchmark's exact consistency criterion to risk. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The unit-budget release also attains the sampling upper bound without privacy constraints. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The explicit sign mixture at one quarter of the sampling radius gives the unrestricted nonprivate lower bound, through chi-square comparison and Le Cam testing. the theorem's stated inputs and assumptions, and the asserted conclusion follows.
Formal statement
Proof (Lean source)
Given the Efron--Stein gate, bounded-differences gate, and Cayley gate, the unrestricted minimax risk at every sample size at least two lies between the explicit constants 2⁻²⁰ and 2¹⁸ times the fourth-root rate.
Formal statement
Proof (Lean source)
The benchmark has four exact regimes, its unit-budget scale is exactly the nonprivate fourth-root order, and private minimax consistency holds exactly when sample size times the privacy budget diverges. The Efron--Stein gate, bounded-differences gate, and Cayley gate specify the conditional scope.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.TSharpIntervalFrontier 9 declarations Honest private expected-length frontier, explicit inversion identity, and uniform equivalence to the scalar absolute-risk frontier.
Honest private expected-length frontier, explicit inversion identity, and uniform equivalence to the scalar absolute-risk frontier.
Clipping a numerator commutes with division by a positive denominator. the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
At legal public parameters the acceptance hull is the released interval. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Public tuning uses the same interval on both release branches. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
An interval containing two ordered points contains the open span between them. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Simultaneous containment forces Lebesgue length even for unbounded codes. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
A finite class prior inherits honesty at its common target. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Prior expected length is no greater than maximal class expected length. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
Two honest finite priors force simultaneous containment under the null output law. the theorem's stated inputs and assumptions, and the asserted conclusion follows. the theorem's stated inputs and assumptions.
Formal statement
Proof (Lean source)
The explicit inversion kernel equals the conservative tuned interval and attains honest coverage and optimal maximal expected length. The scalar and interval frontiers are uniformly comparable with the stated numerical constants. The public parameters and their domains and the Efron--Stein gate, bounded-differences gate, and Cayley gate specify the conditional scope.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_PrivateCateRoughdesignFrontier_Research.TUniformPrivateUpper 1 declarations Assembly of the uniform private scalar-risk, coverage and length guarantees.
Assembly of the uniform private scalar-risk, coverage and length guarantees.
The constructed kernels are Markov and pure private on every input. Their second moments, coverage and interval lengths obey the public envelopes throughout the complete model, and public tuning attains the stated scalar-risk and interval-length constants. The public parameters and their domains and published substrate gates specify the conditional scope.