Formalization: Minimax Estimation and Honest Inference in Randomized Experiments with Missing Outcomes
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs. Note: this index was generated at a different commit than the paper's audited pin (d07574d) — statements may have moved since the audit.
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Basic 64 declarations The full law retains observed and potential coordinates separately, making consistency a substantive condition.
Finite randomized MAR experiment
The full law retains observed and potential coordinates separately, making consistency a substantive condition. The finite PMF model is used because the paper's risks range over explicit observed-data laws, rather than regime-indexed potential-outcome kernels.
Baseline and potential coordinates.
Potential-data atoms have decidable equality for the given covariate dimension.
Definition (Lean source)
Potential-data atoms have a finite enumeration for the given covariate dimension.
Definition (Lean source)
Full-data atom with separate observed and potential outcomes.
Full-data atoms have decidable equality for the given covariate dimension.
Definition (Lean source)
Full-data atoms have a finite enumeration for the given covariate dimension.
Definition (Lean source)
The baseline covariate of a full-data atom is inherited from the supplied atom.
The control-arm arrival indicator of a full-data atom is inherited from the supplied atom.
The treated-arm arrival indicator of a full-data atom is inherited from the supplied atom.
The control potential outcome of a full-data atom is inherited from the supplied atom.
The treated potential outcome of a full-data atom is inherited from the supplied atom.
The record visible to the statistician; the last coordinate is R Y.
Definition (Lean source)
Observed-data atoms have decidable equality for the given covariate dimension.
Definition (Lean source)
Observed-data atoms have a finite enumeration for the given covariate dimension.
Definition (Lean source)
The measurable structure on observed atoms is the discrete structure for the given covariate dimension.
Definition (Lean source)
Every singleton observed atom is measurable for the given covariate dimension.
Definition (Lean source)
Superpopulation distribution on full-data atoms.
Deterministic observation, with a zero outcome mark when the outcome does not arrive.
Definition (Lean source)
Observed-data marginal of the superpopulation law.
Real mass of a full-data atom.
Probability of a full-data event.
Probability of an observed atom.
Marginal mass of a treatment arm.
Mass of an occupied (X,A,S) cell.
The arrival probability, totalized to zero on null cells.
Arrived-outcome regression calculated solely from the observed distribution.
Superpopulation ATE.
Randomization factors the treatment from all baseline and potential coordinates. Given the specified input P, the stated mathematical conclusion holds.
Definition (Lean source)
Balanced Bernoulli treatment allocation. Given the specified input P, the stated mathematical conclusion holds.
Observed outcomes equal their treatment-selected potential outcomes almost surely. Given the specified input P, the stated mathematical conclusion holds.
Cross-multiplied conditional independence of arrival and realized outcome. Given the specified input P, the stated mathematical conclusion holds.
Definition (Lean source)
Uniform arrival floor on occupied cells. Given the specified input q, the specified input P, the stated mathematical conclusion holds.
Definition (Lean source)
The randomized finite-cell MAR law class. Given the specified input d, the specified input q, the specified input P, the stated mathematical conclusion holds.
Definition (Lean source)
A law with its certificate of membership in the MAR class.
Treatment-conditional (X,S) mass computed from the observed law.
Observed-data MAR identifying functional, with totalized null-cell terms. Given the specified input d, the stated mathematical conclusion holds. Given the specified input p.
Definition (Lean source)
The missingness envelope.
Definition (Lean source)
Logarithmic moment scale.
Half-separation scale.
Near-complete minimax squared-error rate. Given the specified input n, the specified input d, the specified input q, the stated mathematical conclusion holds.
Definition (Lean source)
Canonical iid law of the observed sample.
A supplied sample law equals the iid observed-data product law. Given the specified input d, the specified input P, the specified input n, the stated mathematical conclusion holds. Given the specified input μ.
Total measurable observed-data estimator with range in [-1,1].
Definition (Lean source)
An estimator acts as its sample-to-real function for the sample size and covariate dimension.
All-procedure finite-sample minimax squared risk. Given the specified input n, the specified input d, the specified input q, the stated mathematical conclusion holds.
A measurable closed interval inside [-1,1].
Definition (Lean source)
Uniform coverage over the legal law class.
Definition (Lean source)
Honest connected confidence intervals at noncoverage level α. Given the specified input n, the specified input d, the specified input q, the stated mathematical conclusion holds. Given the specified input α.
Definition (Lean source)
Minimax worst-law expected interval length. Given the specified input n, the specified input d, the specified input q, the stated mathematical conclusion holds. Given the specified input α.
Definition (Lean source)
Observed event masses are the pushforwards of their full-data preimages. Given the specified input d, the specified input P, the specified input E, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input a, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input q, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the specified input hc, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input q, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the specified input hc, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input q, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input a, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.Converse.Interpolation 3 declarations Lagrange moment cancellation for the paired latent distribution
Lagrange moment cancellation for the paired latent distribution
Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
For a positive moment order below the number of interpolation nodes, the signed interpolation weights have zero moment of that order.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.Converse.PairTV 2 declarations Nonnegative eight-atom Poisson intensity obligations
Nonnegative eight-atom Poisson intensity obligations
All four possible observed coefficients of an oriented pair are nonnegative. Given the specified input q, the specified input z, the specified input u, the specified input o, the specified input hz, the specified input hu, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq.
Formal statement
Proof (Lean source)
Every observed count atom has a nonnegative unnormalized intensity. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input o, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ, the specified input hσ. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.Converse.SmallN 1 declarations Small-sample two-point comparison
Small-sample two-point comparison
The Bernoulli perturbation dominates the requested scale at bounded sample sizes. Given the specified input a, the specified input c, the specified input N, the specified input n, the specified input d, the specified input q, the specified input ha, the specified input hc, the specified input hcn, the specified input hn, the specified input hN, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.Converse.Target 1 declarations ATE target properties of the normalized pair
ATE target properties of the normalized pair
A binary-outcome ATE is in the unit interval for every full law. Given the specified input d, the specified input P, the stated mathematical conclusion holds.
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.Estimator 26 declarations All Poisson and four-stream randomization is averaged out by a finite sum.
Missing-membership estimator and clipped interval
All Poisson and four-stream randomization is averaged out by a finite sum. The N > n
Poisson tail has value zero, so the displayed finite sum is the unconditional auxiliary
expectation. The polynomial coefficients are taken from the exact Chebyshev quotient.
Projection onto the estimator and estimand range.
The degree used in the light-cell correction.
The polynomial threshold.
Definition (Lean source)
The Chebyshev quotient Q_k, with removable value one at zero.
Definition (Lean source)
Coefficient a_v of 1-Q_k.
Definition (Lean source)
Falling factorial (C-1)_{v-1} for a positive index v.
Definition (Lean source)
A record belongs to the specified observed cell.
Count observations in an auxiliary stream satisfying a given condition.
Definition (Lean source)
Light-cell factorial-polynomial correction.
Definition (Lean source)
Heavy-cell plug-in correction.
Definition (Lean source)
One cell's missing-membership correction using streams two through four.
Definition (Lean source)
One four-stream randomized estimate, already clipped to [-1,1].
Definition (Lean source)
Auxiliary Poisson probability for the uncapped count.
Definition (Lean source)
Averaging all iid uniform four-stream assignments at a fixed count.
Definition (Lean source)
Projected complete-outcome Horvitz--Thompson randomized difference.
Projected centered arrived-outcome fallback.
The total missing-membership estimator for sample size, baseline dimension, known arrival floor, and observed sample. On the full Cartesian record space, Yobs is the supplied fifth coordinate RY. Stream four's U count uses the supplied mark RY=true; on the observation-map support this is the arrived-success count. The estimator averages the clipped four-stream estimate over Poisson(n/2) counts and uniform stream labels, returning zero for N>n. Its q=1 branch is the projected complete-outcome difference using Yobs; the small-logarithm or large-dimension fallback is the projected centered arrived-outcome difference using R(Yobs-1/2).
Definition (Lean source)
For a sample size, a covariate dimension, and an arrival floor, the missing-membership estimator is measurable as a function of the observed sample.
Formal statement
Proof (Lean source)
For an observed sample, the missing-membership estimate lies in the treatment-effect interval from minus one to one.
Formal statement
Proof (Lean source)
A numerical constant certifying the estimator's uniform upper risk.
The upper-risk constant is an explicit input to the confidence radius.
For the specified sample size, dimension, arrival floor, confidence level, and risk constant, the confidence-interval radius is nonnegative.
Formal statement
Proof (Lean source)
For the specified sample size, dimension, arrival floor, confidence level, and risk constant, the lower endpoint of the confidence interval is measurable.
Formal statement
Proof (Lean source)
For the specified sample size, dimension, arrival floor, confidence level, and risk constant, the upper endpoint of the confidence interval is measurable.
Formal statement
Proof (Lean source)
When the interval radius is nonnegative, every resulting confidence interval is ordered and contained in the feasible treatment-effect interval.
Formal statement
Proof (Lean source)
Clipped connected interval around the total estimator. Given the specified input n, the specified input d, the specified input q, the specified input CU, the stated mathematical conclusion holds. Given the specified input α.
Definition (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.Identification 8 declarations Finite-law randomization and MAR identification.
Finite-law randomization and MAR identification.
Given the specified input d, the specified input P, the specified input E, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input hR, the specified input a, the specified input F, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the stated mathematical conclusion holds.
Proof (Lean source)
Given the specified input d, the specified input P, the specified input hB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input hC, the specified input a, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the stated mathematical conclusion holds.
Formal statement
Given the specified input d, the specified input P, the specified input hR, the specified input hB, the specified input hC, the specified input a, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Randomization, consistency and MAR identify the original superpopulation ATE. Given the specified input d, the specified input q, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.CountMixture.AssembledTail 8 declarations Split a count vector into its disjoint pair blocks and its common residual block.
Assembly of independent count blocks
Split a count vector into its disjoint pair blocks and its common residual block. This injection transfers the normalized product L1 bound to the original count alphabet without counting any atom twice.
Given the specified input n, the specified input d, the specified input hd, the specified input counts, the specified input o, the stated mathematical conclusion holds. Given the specified input j.
Given the specified input n, the specified input d, the specified input hd, the specified input counts, the specified input o, the stated mathematical conclusion holds.
Given the specified input n, the specified input d, the specified input hd, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Restricting the count vector to its pair does not alter the local factor. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Formal statement
Proof (Lean source)
The residual restriction carries the filler likelihood and all forced zeros on unused labels, exactly the common factor in the full experiment. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
The singleton-mass ℓ¹ discrepancy of the two count mixtures is bounded by twice the pair count times the unmatched factorial-series tail. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
The two count mixtures differ only through unmatched pair-block degrees; their total variation is bounded by the pair count times the exponential series tail from paper equation (35). Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.CountMixture.Basic 18 declarations Basic for the paired count-mixture comparison
Basic for the paired count-mixture comparison
The random count normalizer is uniformly at least one half. Given the specified input n, the specified input d, the specified input hn, the stated mathematical conclusion holds. Given the specified input θ.
Formal statement
Proof (Lean source)
The conditional total-count Poisson rate generated by the paired prior has a uniformly small lower tail. Given the specified input n, the specified input d, the specified input hn, the stated mathematical conclusion holds. Given the specified input θ.
Formal statement
Proof (Lean source)
Uniformly over every latent parameter and dimension, the conditional short-count probability is eventually below any positive tolerance. the stated mathematical conclusion holds. Given the specified input β, the specified input hβ.
Formal statement
Proof (Lean source)
Averaging over the latent prior preserves the uniform 8 / n short-count bound required by random-scale transfer. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
At any fixed baseline label, the filler observed coefficients have total mass one. Given the specified input d, the specified input q, the specified input x, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
At any fixed baseline label, each oriented pair's observed coefficients have total mass one. Given the specified input d, the specified input q, the specified input z, the specified input u, the specified input x, the stated mathematical conclusion holds. Given the specified input σ.
Formal statement
Proof (Lean source)
The unnormalized count-cell intensities sum exactly to the random normalizer, independently of the sign parameter. Given the specified input n, the specified input d, the specified input q, the specified input hd, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ.
Formal statement
Proof (Lean source)
Flipping the experiment sign is exactly the same as flipping the latent sign in every oriented pair coefficient. Given the specified input q, the specified input z, the specified input u, the specified input o, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
After averaging the two opposite orientations, every degree-one observed coefficient is independent of the experiment sign. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input o, the stated mathematical conclusion holds. Given the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
Explicit averaging over the base orientation removes every degree-one experiment-sign dependence. Given the specified input q, the specified input z, the specified input target, the specified input o, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
At the treated observed-failure mark, the orientation-averaged quadratic coefficient has a nonzero signed-latent gap. This is the first term for which moment cancellation is needed. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input o, the specified input hA, the specified input hS, the specified input hR, the specified input hRY, the stated mathematical conclusion holds. Given the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
Every legal oriented-pair observed coefficient is at most one. Given the specified input q, the specified input z, the specified input u, the specified input o, the specified input hz, the specified input hu, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq.
Formal statement
Proof (Lean source)
The singleton likelihood of a conditional count vector is the finite product of its scalar Poisson probabilities. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ.
Formal statement
Proof (Lean source)
In the legal sign regime, the conditional count-vector likelihood has one shared exponential factor determined by normalizationJ. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ, the specified input θ. Given the specified input hq.
Formal statement
Proof (Lean source)
The mixed count-vector likelihood is the finite latent average of the conditional product likelihood, with a sign-independent exponential factor. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq.
Formal statement
Proof (Lean source)
At a paired baseline label, exactly one pair component contributes to the unnormalized observed-atom mass. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input o, the specified input side, the specified input ho, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
At the filler baseline label, every paired component vanishes. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input o, the specified input ho, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ.
Formal statement
Proof (Lean source)
A finite product over observed atoms factors into products over baseline labels. Given the specified input f, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.CountMixture.CountDegree 10 declarations The multinomial identity sums all observed marks before bounding the latent mass.
Summing marked likelihoods at a fixed count degree
The multinomial identity sums all observed marks before bounding the latent mass. This preserves the pair's total intensity and avoids a factor depending on the number of mark configurations in the unmatched Taylor tail.
For a sample multiplier, alphabet size, total count degree, arrival parameter, sign, latent orientation, latent mass, positive-alphabet witness, pair index, and base orientation, summing the factorial-normalized products of the marked intensities over all count vectors of that degree gives the corresponding Poisson-series coefficient.
Formal statement
Proof (Lean source)
Fairly averaging the orientations leaves the same fixed-degree mass. Given the specified input n, the specified input d, the specified input r, the specified input q, the specified input z, the specified input p, the specified input hd, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Formal statement
Proof (Lean source)
The fixed-degree signed orientation average is bounded in total absolute mass by the sum of its two nonnegative marked likelihoods. Given the specified input n, the specified input d, the specified input r, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input hz, the specified input hp, the stated mathematical conclusion holds. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
For a positive covariate dimension and a count vector supported on the selected pair, the full marked factorial likelihood equals the label-restricted local likelihood.
Formal statement
Proof (Lean source)
A positive count outside both labels of the pair makes its full marked likelihood zero. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input base, the specified input counts, the specified input o, the specified input ho, the specified input hc, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Formal statement
Proof (Lean source)
For a positive covariate dimension and a count vector supported on the selected pair, the pair block count equals the total observed count.
Formal statement
Proof (Lean source)
The signed fair-orientation likelihood on the full observed alphabet, with zero rates enforcing zero counts outside the selected pair. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input j.
Definition (Lean source)
For a positive covariate dimension and a count vector supported on the selected pair, the signed marked likelihood has its local scalar-power representation.
Formal statement
Proof (Lean source)
The latent-averaged signed Taylor coefficient on the full observed alphabet, including the count-support constraint outside the selected pair. Given the specified input n, the specified input d, the specified input t, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input j.
Definition (Lean source)
Summing the absolute signed Taylor coefficient over all marks of degree r gives the two-factor factorial envelope at the maximal latent intensity. This is the marked multinomial step in the one-pair tail comparison. Given the specified input n, the specified input d, the specified input r, the specified input t, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.CountMixture.Eventual 3 declarations Eventual for the paired count-mixture comparison
Eventual for the paired count-mixture comparison
Exponential tilting bounds the unmatched factorial tail, without needing an asymptotic approximation to the factorial. Given the specified input K, the specified input z, the specified input hz, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The prior's logarithmic matched degree makes the whole pair-count tail at most the reciprocal sample size, uniformly in the dimension. Given the specified input n, the specified input d, the specified input hn, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Count-mixture half of the large-sample comparison. Moment cancellation in latent_signed_power_moment_zero removes degrees two through priorK; the remaining Poisson likelihood tail must be summed over the independent pairs. the stated mathematical conclusion holds. Given the specified input β, the specified input hβ.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.CountMixture.Factorization 16 declarations Factorization for the paired count-mixture comparison
Factorization for the paired count-mixture comparison
Product of count factorials at one paired baseline label. Given the specified input n, the specified input d, the specified input hd, the specified input side, the specified input counts, the stated mathematical conclusion holds. Given the specified input j.
The full power/factorial contribution at one paired label separates into its scalar pair mass, observed-mark monomial, and count factorials. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the specified input side, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input j.
Definition (Lean source)
Multiplying the two labels of one pair combines their scalar mass powers to pairBlockCount and their marks to the pair-block monomial. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
Factorial likelihood contribution restricted to the two labels of one marked pair. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input base, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Definition (Lean source)
The local marked-pair factorial likelihood is the scalar pair-count power times its observed-mark monomial divided by the block factorial. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input base, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Formal statement
Proof (Lean source)
The fair orientation-averaged raw block likelihood is exactly the fair average of the two fixed-base marked local factors. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Formal statement
Proof (Lean source)
The normalized Poisson factor on one side of a marked pair is its raw marked likelihood times the exponential of the side's total rate. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input hz, the specified input hp, the specified input base, the specified input side, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
Multiplying the two normalized side factors yields the normalized marked pair likelihood with total exponential rate 8 * n * p. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input hz, the specified input hp, the specified input base, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
One pair's latent-and-orientation averaged marked-Poisson likelihood factor. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Definition (Lean source)
Every legal one-pair averaged marked-Poisson likelihood factor is nonnegative. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
Averaging the product of conditional pair-block likelihoods under thetaLaw gives the product of the one-pair mixture factors. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input hq.
Formal statement
Proof (Lean source)
The sign-independent filler and forced-zero contribution to a count-vector likelihood. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds.
Definition (Lean source)
Every fixed choice of pair masses, signs, and base orientations gives a normalized full observed count-vector likelihood. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input hp, the specified input hz, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq, the specified input p, the specified input z, the specified input base.
Formal statement
Proof (Lean source)
The fixed latent component used by the paired prior is a normalized full count-vector likelihood. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ, the specified input θ. Given the specified input hq.
Formal statement
Proof (Lean source)
A conditional likelihood splits into a common filler/zero-rate factor and one marked-Poisson factor for each active pair. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.CountMixture.MarkedRates 24 declarations MarkedRates for the paired count-mixture comparison
MarkedRates for the paired count-mixture comparison
The filler-label local Poisson factor of a partitioned family uses only the supplied filler rate. Given the specified input n, the specified input d, the specified input hd, the specified input fillerRate, the specified input counts, the stated mathematical conclusion holds. Given the specified input pairRate.
Formal statement
Proof (Lean source)
Each active pair-label local Poisson factor of a partitioned family uses only its supplied pair-side rate. Given the specified input n, the specified input d, the specified input hd, the specified input fillerRate, the specified input side, the specified input counts, the stated mathematical conclusion holds. Given the specified input pairRate, the specified input j.
Formal statement
Proof (Lean source)
At an unused label, the local Poisson factor is exactly the indicator that all counts at that label vanish. Given the specified input n, the specified input d, the specified input hd, the specified input fillerRate, the specified input x, the specified input hx, the specified input counts, the stated mathematical conclusion holds. Given the specified input pairRate.
Formal statement
Proof (Lean source)
Filler, pair-side, and unused-zero local factors jointly normalize over the full observed count-vector space. Given the specified input n, the specified input d, the specified input hd, the specified input fillerRate, the stated mathematical conclusion holds. Given the specified input pairRate.
Formal statement
Proof (Lean source)
A zero-rate Poisson factorial factor forces its count coordinate to zero. Given the specified input k, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Any product over observed atoms splits exactly into the filler block, one block for every pair and side, and blocks over unused baseline labels. Given the specified input n, the specified input d, the specified input hd, the specified input g, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Marked count intensity for one pair at a fixed base orientation. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input base, the specified input o, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Definition (Lean source)
Legal pair marked intensities are nonnegative. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input hz, the specified input hp, the specified input base, the specified input o, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
At one of the pair's two labels, the marked intensity is its scalar mass times the corresponding observed-mark coefficient. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input base, the specified input side, the specified input o, the specified input ho, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Formal statement
Proof (Lean source)
The marked intensities of one pair have total rate 8 * n * p. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input base, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Formal statement
Proof (Lean source)
Nonnegative-real packaging of one pair's marked intensity. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input base, the specified input o, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Definition (Lean source)
Under the legal parameter restrictions, coercing pairMarkedRate back to the reals recovers the marked intensity. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input hz, the specified input hp, the specified input base, the specified input o, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
The packaged pair marked rate also has total mass 8 * n * p. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input hz, the specified input hp, the specified input base, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
The raw factorial count series for one oriented marked pair sums to the exponential of its total rate. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input hz, the specified input hp, the specified input base, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
Nonnegative marked rate carried by one side label of a pair. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input base, the specified input side, the specified input o, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Definition (Lean source)
A legal pair-side marked rate coerces to its explicit real intensity. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input hz, the specified input hp, the specified input base, the specified input side, the specified input o, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
One pair-side marked rate has total mass 4 * n * p. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input p, the specified input hd, the specified input hz, the specified input hp, the specified input base, the specified input side, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
A finite Poisson product separates into its common exponential and raw power/factorial factors, even when restricted to a decidable subset. Given the specified input rate, the specified input counts, the specified input keep, the stated mathematical conclusion holds. Given the specified input α.
Formal statement
Proof (Lean source)
The filler mass is nonnegative at every positive sample size. Given the specified input n, the specified input d, the specified input hn, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Every legal filler observed-mark coefficient is nonnegative. Given the specified input q, the specified input o, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Nonnegative-real packaging of the filler-label marked rate. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input o, the stated mathematical conclusion holds.
Definition (Lean source)
A legal filler marked rate coerces to its explicit real intensity. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input o, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Filler marked rates have total mass 4 * n * fillerMass. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
The normalized local filler Poisson factor equals its raw likelihood times the exponential of the negative filler rate. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.CountMixture.PairMarks 22 declarations PairMarks for the paired count-mixture comparison
PairMarks for the paired count-mixture comparison
Polynomial likelihood monomial contributed by the observed marks at one paired baseline label. Given the specified input q, the specified input z, the specified input u, the specified input x, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ.
Definition (Lean source)
The likelihood powers at one paired label split into a latent-mass power and the observed-mark monomial. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the specified input side, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
Every one-label likelihood monomial transforms by latent-sign reflection when the experiment sign is flipped. Given the specified input q, the specified input z, the specified input u, the specified input x, the specified input counts, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Orientation averaging preserves the exact latent-sign reflection of a one-label likelihood monomial. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input x, the specified input counts, the stated mathematical conclusion holds. Given the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
Under legal signs, every one-label pair likelihood monomial lies in the unit interval. Given the specified input q, the specified input z, the specified input u, the specified input x, the specified input counts, the specified input hz, the specified input hu, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq.
Formal statement
Proof (Lean source)
Total observed count in the two labels belonging to one latent pair. Given the specified input n, the specified input d, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input j.
A finite family of natural numbers summing to one has a unique unit entry. Given the specified input f, the stated mathematical conclusion holds. Given the specified input α. Given the specified input h.
Formal statement
Proof (Lean source)
Orientation-averaged observed-mark monomial for one pair block, written without reference to the other latent coordinates. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
A block with no observations has the same orientation-averaged mark monomial under both experiment signs. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input hd, the specified input counts, the specified input hzero, the stated mathematical conclusion holds. Given the specified input j.
Formal statement
Proof (Lean source)
If one specified observed atom is the unique record in a pair block, the block mark monomial reduces to its orientation-averaged scalar coefficient. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input hd, the specified input counts, the specified input target, the specified input o₀, the specified input ho₀, the specified input hone, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j, the specified input hother.
Formal statement
Proof (Lean source)
A block with exactly one observation has the same orientation-averaged mark monomial under both experiment signs. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input hd, the specified input counts, the specified input hone, the stated mathematical conclusion holds. Given the specified input j.
Formal statement
Proof (Lean source)
For legal overlap and latent signs, the absolute orientation-averaged mark gap of one pair block is at most two. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input hd, the specified input counts, the specified input hz, the stated mathematical conclusion holds. Given the specified input j, the specified input hq.
Formal statement
Proof (Lean source)
Flipping the experiment sign is exactly reflection of the scalar latent sign in the orientation-averaged block monomial. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input j.
Formal statement
Proof (Lean source)
On the two-point latent-sign support, the signed block gap factors as the latent sign times its value at positive sign. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input hd, the specified input counts, the specified input hz, the stated mathematical conclusion holds. Given the specified input j.
Formal statement
Proof (Lean source)
The signed tail after truncating the power series of exp (-x) through the displayed degree. Given the specified input degree, the specified input x, the stated mathematical conclusion holds.
Definition (Lean source)
Exact Taylor decomposition of the random-normalizer exponential. Given the specified input degree, the specified input x, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The signed Taylor remainder is dominated by the ordinary positive exponential-series tail. Given the specified input degree, the specified input x, the specified input hx, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The factorial-normalized Cauchy coefficient of two exponential series is the corresponding coefficient at the sum of their arguments. Given the specified input a, the specified input b, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The unmatched bidegrees of two factorial series regroup into the ordinary exponential tail at the sum of the two arguments. Given the specified input degree, the specified input a, the specified input b, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input z, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input z, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
The full latent-and-orientation law factors coordinatewise for arbitrary per-pair real statistics. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq, the specified input f.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.CountMixture.ProductSummation 4 declarations The one-pair factorial tail is combined across independent blocks using normalized nonnegative likelihoods, as in equation (14) of the converse.
Normalization and L1 telescoping for independent paired counts
The one-pair factorial tail is combined across independent blocks using normalized nonnegative likelihoods, as in equation (14) of the converse.
For a sample multiplier, alphabet size, arrival parameter, sign, latent orientation, latent mass, positive-alphabet witness, admissible-arrival witness, admissible-sign witness, admissible-orientation witness, nonnegative-mass witness, pair index, base orientation, and observed count vector, the marked component likelihood equals the product of its coordinatewise Poisson masses.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
Averaging the normalized marked components preserves their total mass. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
Two summable nonnegative likelihoods have a summable absolute gap. Given the specified input A, the specified input a, the specified input b, the specified input ha, the specified input hb, the specified input ha0, the specified input hb0, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.CountMixture.Taylor 13 declarations Taylor for the paired count-mixture comparison
Taylor for the paired count-mixture comparison
The full mixed singleton likelihood is the common filler/zero-rate factor times the product of the independently averaged pair factors. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq.
Formal statement
Proof (Lean source)
The factorized mixed likelihood normalizes over every observed count vector; this is the aggregate Tonelli target for the later Taylor envelope. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq.
Formal statement
Proof (Lean source)
The product gap between the two experiment signs is bounded by the weighted pair telescope, retaining all non-target pair likelihood factors. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
The signed latent mass cancels every power from degree two through the interpolation-node count. The nonzero first moment is the target signal. Given the specified input n, the specified input t, the specified input ht, the specified input hK, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input z, the stated mathematical conclusion holds.
Proof (Lean source)
A one-pair signed likelihood coefficient vanishes whenever its observed degree plus exponential Taylor degree lies in the matched-moment range. Given the specified input n, the specified input d, the specified input r, the specified input t, the specified input q, the specified input hd, the specified input counts, the specified input hlo, the specified input hhi, the stated mathematical conclusion holds. Given the specified input j.
Formal statement
Proof (Lean source)
Every Taylor/observed coefficient through the matched degree vanishes: degrees zero and one use direct mark cancellation, while higher degrees use the signed latent moments. Given the specified input n, the specified input d, the specified input r, the specified input t, the specified input q, the specified input hd, the specified input counts, the specified input hr, the specified input hhi, the stated mathematical conclusion holds. Given the specified input j.
Formal statement
Proof (Lean source)
Given the specified input n, the stated mathematical conclusion holds. Given the specified input i.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input z, the stated mathematical conclusion holds.
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Every one-pair Taylor coefficient has the uniform absolute envelope used for the unmatched factorial tail. Given the specified input n, the specified input d, the specified input r, the specified input t, the specified input q, the specified input hn, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
The absolute Taylor coefficient is dominated by a positive envelope that retains both legal marked likelihoods. This form can be summed by the marked component normalization without paying for the number of observed marks. Given the specified input n, the specified input d, the specified input r, the specified input t, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
After factorial normalization, a pair Taylor coefficient is dominated by positive normalized marked-pair factors times the compensating positive Taylor weight. Given the specified input n, the specified input d, the specified input t, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.CountMixture.TaylorRemainder 12 declarations The exponential expansion is summed before taking absolute values.
Convergent unmatched Taylor remainder for one paired count block
The exponential expansion is summed before taking absolute values. All matched coefficients cancel by the latent signed moments and the low-degree mark identities.
The factorial-normalized signed coefficient of one paired count block. Given the specified input n, the specified input d, the specified input t, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input j.
Definition (Lean source)
The coefficient on the full marked alphabet agrees with the original block coefficient whenever the count vector is supported on that pair. For a positive covariate dimension and a count vector supported on the selected pair, the marked Taylor coefficient equals the local block coefficient.
Formal statement
Proof (Lean source)
For a positive covariate dimension, if an observed atom lies outside the selected pair and has positive count, its signed marked Taylor coefficient is zero.
Formal statement
Proof (Lean source)
The signed pair likelihood has a convergent exponential Taylor expansion, with the finite latent average interchanged with the series. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input j.
Formal statement
Proof (Lean source)
Every coefficient whose combined count and Taylor degree is matched is zero. Given the specified input n, the specified input d, the specified input t, the specified input q, the specified input hd, the specified input counts, the specified input hmatch, the stated mathematical conclusion holds. Given the specified input j.
Formal statement
Proof (Lean source)
After including the zero-rate support constraint, every coefficient of matched total observed and Taylor degree vanishes on the full alphabet. For a positive covariate dimension, if the total count plus Taylor degree is within the matching range, the signed marked Taylor coefficient is zero.
Formal statement
Proof (Lean source)
The full signed pair likelihood is exactly its unmatched Taylor remainder; no absolute-value relaxation is made until after the moment cancellations. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input j.
Formal statement
Proof (Lean source)
The absolute pair likelihood gap is bounded by the absolutely convergent unmatched coefficient series. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input j.
Formal statement
Proof (Lean source)
Each normalized coefficient has a factorial envelope, uniform over the legal arrival floor and over all latent nodes. Given the specified input n, the specified input d, the specified input t, the specified input q, the specified input hn, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
For a fixed observed block, only Taylor terms above the matched combined degree contribute to the signed likelihood gap. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
At each combined degree, the matched coefficients vanish and the unmatched marked coefficients have the factorial envelope at twice the maximal pair intensity. Given the specified input n, the specified input d, the specified input s, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
The absolutely summed marked Taylor coefficients are bounded by twice the unmatched exponential-series tail. Matched degrees have been removed using the signed latent moments before this summation. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.CountMixture.TaylorSummation 9 declarations Reindex the Taylor degree and observed counts by their combined degree.
Absolute summation of the marked Taylor series
Reindex the Taylor degree and observed counts by their combined degree. This turns the finite multinomial coefficient bounds into an absolutely convergent series on the full count alphabet.
For a sample size, alphabet size, arrival parameter, positive-sample witness, positive-alphabet witness, admissible-arrival witness, and pair index, the sequence of absolute marked Taylor coefficients grouped by combined Taylor and count degree is summable.
Formal statement
Proof (Lean source)
The marked coefficients are absolutely summable jointly over Taylor degree and all observed count vectors. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
The full absolute Taylor/count sum obeys the same unmatched factorial tail as the finite combined-degree sums. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
The one-pair mixture likelihood on the full observed count alphabet, including the zero rates outside that pair. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Definition (Lean source)
For a positive covariate dimension and a count vector supported on the selected pair, the full-alphabet pair mixture likelihood equals its local counterpart.
Formal statement
Proof (Lean source)
A count at a zero-rate atom makes the full pair likelihood vanish. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the specified input o, the specified input ho, the specified input hc, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input j.
Formal statement
Proof (Lean source)
The full marked likelihood gap is the sum of its Taylor coefficients; unsupported count vectors have both sides zero. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input j.
Formal statement
Proof (Lean source)
The one-pair likelihood gap is bounded by the absolute coefficient series. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input counts, the stated mathematical conclusion holds. Given the specified input j.
Formal statement
Proof (Lean source)
Summing every count vector yields the paper's one-pair L1 bound. The matched moments have already canceled before any absolute summation. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.CountMixture.Telescope 16 declarations Telescope for the paired count-mixture comparison
Telescope for the paired count-mixture comparison
Product-Poisson likelihood factor restricted to one baseline label. Given the specified input rate, the specified input x, the specified input counts, the stated mathematical conclusion holds.
Multiplying all baseline-label-local Poisson factors recovers the full observed-coordinate product likelihood. Given the specified input rate, the specified input counts, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The product of all local baseline-label Poisson factors sums to one over the full observed count-vector space. Given the specified input rate, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Global observed-coordinate rate assembled from one local rate family per baseline label. Given the specified input localRate, the specified input o, the stated mathematical conclusion holds.
Definition (Lean source)
Poisson factor at one baseline label using that label's member of a local rate family. Given the specified input localRate, the specified input x, the specified input counts, the stated mathematical conclusion holds.
At each label, the local-family factor agrees with the corresponding factor of the globally assembled rate. Given the specified input localRate, the specified input x, the specified input counts, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Arbitrary nonnegative local rate families normalize jointly after their disjoint baseline-label supports are assembled. Given the specified input localRate, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The fair-orientation average of a legal pair-block mark likelihood lies in the unit interval, as required by the product telescoping bound. Given the specified input n, the specified input d, the specified input q, the specified input z, the specified input hd, the specified input counts, the specified input hz, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input j, the specified input hq.
Formal statement
Proof (Lean source)
Baseline labels carrying nonzero construction mass: the filler and the two labels of every active latent pair. Given the specified input n, the specified input d, the specified input hd, the stated mathematical conclusion holds.
Every baseline label outside the filler and paired-label image has exactly zero conditional atom mass for all observed marks. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input o, the specified input hf, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hp.
Formal statement
Proof (Lean source)
Local rate family assembled from one filler rate, one rate for every pair side, and zero on unused baseline labels. Given the specified input n, the specified input d, the specified input hd, the specified input fillerRate, the specified input x, the specified input o, the stated mathematical conclusion holds. Given the specified input pairRate.
Definition (Lean source)
At the filler label, the partitioned local family selects the filler rate. Given the specified input n, the specified input d, the specified input hd, the specified input fillerRate, the specified input o, the stated mathematical conclusion holds. Given the specified input pairRate.
Formal statement
Proof (Lean source)
At an active pair label, the partitioned local family selects exactly its corresponding pair-side rate. Given the specified input n, the specified input d, the specified input hd, the specified input fillerRate, the specified input side, the specified input o, the stated mathematical conclusion holds. Given the specified input pairRate, the specified input j.
Formal statement
Proof (Lean source)
The partitioned local family vanishes at every unused baseline label. Given the specified input n, the specified input d, the specified input hd, the specified input fillerRate, the specified input x, the specified input hx, the specified input o, the stated mathematical conclusion holds. Given the specified input pairRate.
Formal statement
Proof (Lean source)
A product over active baseline labels reindexes exactly into the filler factor followed by one factor for each pair and side. Given the specified input n, the specified input d, the specified input hd, the specified input f, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Every baseline-label product splits exactly into filler, active pair labels, and the complement of unused zero-rate labels. Given the specified input n, the specified input d, the specified input hd, the specified input f, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.Decision 3 declarations Decision theoretic reductions for the one cell lower bound
Decision theoretic reductions for the one cell lower bound
A hard separated pair gives a uniform squared risk lower bound. Given the specified input n, the specified input d, the specified input q, the specified input u, the specified input P₀, the specified input P₁, the specified input hu, the specified input htau₀, the specified input htau₁, the stated mathematical conclusion holds. Given the specified input htv.
Formal statement
Proof (Lean source)
A fixed legal law transfers a length lower bound through the minimax extrema. Given the specified input n, the specified input d, the specified input q, the specified input c, the specified input P, the stated mathematical conclusion holds. Given the specified input α, the specified input hα. Given the specified input h.
Formal statement
Proof (Lean source)
Coverage under a TV close pair forces expected interval length. Given the specified input n, the specified input d, the specified input q, the specified input u, the specified input P₀, the specified input P₁, the specified input hu, the specified input htau₀, the specified input htau₁, the stated mathematical conclusion holds. Given the specified input α, the specified input hα. Given the specified input htv.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.NormalizedGlue 4 declarations Glue interface for the two branches of the normalized converse
Glue interface for the two branches of the normalized converse
The paired-prior conclusion at fixed parameters and separation constant. Given the specified input n, the specified input d, the specified input q, the specified input c, the stated mathematical conclusion holds. Given the specified input β.
Definition (Lean source)
The exact remaining large-sample obligation: a uniform certificate after a threshold depending only on the fixed testing tolerance. the stated mathematical conclusion holds. Given the specified input β.
Definition (Lean source)
A certificate remains valid after decreasing its separation constant. Given the specified input n, the specified input d, the specified input q, the specified input c, the specified input c', the specified input hc, the specified input hcc, the specified input h, the stated mathematical conclusion holds. Given the specified input β. Given the specified input hq.
Formal statement
Proof (Lean source)
An eventual uniform certificate and the parametric finite branch imply the full normalized converse. Given the specified input hlarge, the stated mathematical conclusion holds. Given the specified input β. Given the specified input hβ.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.NormalizedLagrange 2 declarations Exterior Lagrange mass for the normalized paired prior
Exterior Lagrange mass for the normalized paired prior
The qid's Lagrange normalization is exactly its calibrated exterior Chebyshev value. Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Uniform exterior mass bound for the normalized paired prior. Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.NormalizedLargeN 5 declarations Remaining large-sample normalized certificate
Remaining large-sample normalized certificate
A minus-prior event is the corresponding latent event under thetaLaw. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input E, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
A plus-prior event is the corresponding latent event under thetaLaw. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input E, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
The concentration certificate transfers to both target events of the legal pushed-forward priors. the stated mathematical conclusion holds. Given the specified input β, the specified input hβ.
Formal statement
Proof (Lean source)
Remaining parameter-independent prefix-transfer leaf. Eventually, transfer from the random-scale count experiment costs at most half the requested TV budget, uniformly over the exact normalized paired construction. the stated mathematical conclusion holds. Given the specified input β, the specified input hβ.
Formal statement
Proof (Lean source)
The count-mixture comparison and random-scale prefix transfer imply the eventual fixed-size predictive TV bound. the stated mathematical conclusion holds. Given the specified input β, the specified input hβ.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.NormalizedScale 10 declarations Scale arithmetic for normalized paired concentration
Scale arithmetic for normalized paired concentration
Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input hd, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input x, the specified input hx, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input hd, the specified input n, the stated mathematical conclusion holds. Given the specified input hnell.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input n, the stated mathematical conclusion holds. Given the specified input hq, the specified input hreg.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input n, the stated mathematical conclusion holds. Given the specified input hq, the specified input hreg.
Formal statement
Proof (Lean source)
the stated mathematical conclusion holds. Given the specified input ε, the specified input hε.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input n, the stated mathematical conclusion holds. Given the specified input hq, the specified input hreg.
Formal statement
Proof (Lean source)
the stated mathematical conclusion holds. Given the specified input η, the specified input hη.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.NormalizedSmallN 3 declarations Parametric finite-sample branch of the normalized converse
Parametric finite-sample branch of the normalized converse
The predictive mixture of a point prior is its iid sample law. Given the specified input n, the specified input d, the specified input q, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A point prior assigns unit mass to every event containing its support point. Given the specified input d, the specified input q, the specified input P, the specified input E, the specified input hE, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The one-cell pair proves the normalized-converse certificate below any fixed positive sample-size threshold. For a positive tolerance, a positive separation, a scale budget valid at every positive integer, a positive sample size below the threshold, a positive dimension, and an admissible arrival floor, the normalized converse certificate holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.NormalizedTarget 7 declarations Exact target identity for the normalized paired prior
Exact target identity for the normalized paired prior
The signed latent mass in the paired construction.
Given the specified input n, the specified input d, the stated mathematical conclusion holds. Given the specified input θ.
Formal statement
Proof (Lean source)
The filler component contributes its normalized mass times the filler mean. Given the specified input n, the specified input d, the specified input q, the specified input hd, the stated mathematical conclusion holds. Given the specified input θ.
Formal statement
Proof (Lean source)
One oriented paired label contributes its normalized mass times its treated mean. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input side, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
Opposite orientations have the exact filler-centered signed mean shift. Given the specified input q, the specified input z, the specified input u, the specified input hz, the specified input hu, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ. Given the specified input hq.
Formal statement
Proof (Lean source)
Summing the two random orientations removes the orientation sign exactly. Given the specified input n, the specified input d, the specified input q, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ, the specified input θ. Given the specified input hq, the specified input j.
Formal statement
Proof (Lean source)
The normalized paired law has exactly the filler target plus the signed latent mass shift; normalization creates no additional sign-dependent term. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input σ, the specified input hσ, the specified input θ. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.NormalizedTargetConcentration 22 declarations Target concentration leaves for the normalized paired prior
Target concentration leaves for the normalized paired prior
The cardinal Lagrange coefficients at zero sum to one. Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The normalized signed interpolation coefficients retain total mass 1 / lagrangeNorm. Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The absolute normalized interpolation coefficients have total mass one. Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The one-pair signed mass has the exact mean used in equation (18). Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Every interpolation node is at most the right endpoint one. Given the specified input n, the stated mathematical conclusion holds. Given the specified input i.
Formal statement
Proof (Lean source)
The one-pair signed latent mass has the scale-squared second-moment bound. Given the specified input n, the specified input hn, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The one-pair latent mass has mean priorH * priorB. Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The one-pair latent mass has the same scale-squared second-moment envelope. Given the specified input n, the specified input hn, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Every scalar latent weight is nonnegative. Given the specified input n, the specified input z, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The real mass function of the scalar latent PMF is latentWeight. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input z, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
For a sample size, every singleton latent state is measurable.
Definition (Lean source)
Integrating a statistic of the latent coordinates under thetaLaw reduces to the corresponding finite product-weighted sum. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq, the specified input f.
Formal statement
Proof (Lean source)
A lower bound on the normalized signed latent mass gives the two pointwise target inequalities for the opposite prior signs. Given the specified input n, the specified input d, the specified input q, the specified input c, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input θ. Given the specified input hq, the specified input hshift.
Formal statement
Proof (Lean source)
Equation (18), first part: the signed latent mass has the displayed mean. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Equation (18), second part: the signed latent mass has the required variance bound. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Equation (19): the random normalizer has mean one and controlled variance. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input n, the stated mathematical conclusion holds. Given the specified input hq, the specified input hreg.
Formal statement
Proof (Lean source)
Given the specified input Q, the specified input F, the stated mathematical conclusion holds. Given the specified input α.
Formal statement
Proof (Lean source)
the stated mathematical conclusion holds. Given the specified input β, the specified input hβ.
Formal statement
Proof (Lean source)
the stated mathematical conclusion holds. Given the specified input β, the specified input hβ.
Formal statement
Proof (Lean source)
Equations (20)--(24): beyond a tolerance-dependent threshold, the normalized signed latent mass dominates a universal multiple of gScale with prior probability at least 1-β. the stated mathematical conclusion holds. Given the specified input β, the specified input hβ.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.ObservedAtoms 4 declarations The full-data construction marginalizes to the displayed count-experiment coefficients divided by the shared normalizer.
Exact observed-atom masses of the normalized paired construction
The full-data construction marginalizes to the displayed count-experiment coefficients divided by the shared normalizer.
An oriented pair marginalizes to its displayed observed coefficient. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input side, the specified input o, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input j, the specified input hq, the specified input hσ.
Formal statement
Proof (Lean source)
The filler marginalizes to its common observed coefficient. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input o, the stated mathematical conclusion holds. Given the specified input θ.
Formal statement
Proof (Lean source)
The normalized observed atom mass is the unnormalized count mass divided by the shared scale. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input o, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ.
Formal statement
Proof (Lean source)
The paper's conditional count experiment is the histogram law of the normalized observed distribution at intensity four n times the shared scale. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.OneCell 16 declarations This module gives the explicit Bernoulli submodel used for the parametric point-risk and honest-interval floors.
Complete-arrival one-cell submodel
This module gives the explicit Bernoulli submodel used for the parametric point-risk and honest-interval floors.
The full-data atom generated from a fair treatment bit and one treated-potential bit.
Bernoulli PMF written with real-valued success probability.
Definition (Lean source)
Complete-arrival one-cell Bernoulli law with treated mean p.
Definition (Lean source)
For a probability in the unit interval and a binary outcome, the Bernoulli point mass equals its usual real-valued probability.
Formal statement
Proof (Lean source)
For a valid treated success probability and a full-data atom, the one-cell law's atom mass is the sum of its fair-treatment and outcome weights over generating pairs.
Formal statement
Proof (Lean source)
For a valid treated success probability and a decidable event, the one-cell event probability reduces to the four generating treatment-outcome pairs.
Formal statement
Proof (Lean source)
For a valid treated success probability and an outcome function, the one-cell expectation reduces to the four generating treatment-outcome pairs.
Formal statement
Proof (Lean source)
For a valid treated success probability, if a full-data atom is not one of the generated treatment-outcome atoms, the one-cell law assigns it zero mass.
Formal statement
Proof (Lean source)
The one-cell family has deterministic outcome arrival. Given the specified input d, the specified input x, the specified input p, the specified input hp, the specified input w, the specified input hR, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The one-cell family obeys consistency. Given the specified input d, the specified input x, the specified input p, the specified input hp, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The one-cell family is balanced. Given the specified input d, the specified input x, the specified input p, the specified input hp, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Treatment is independent of the fixed baseline and potential vector. Given the specified input d, the specified input x, the specified input p, the specified input hp, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The target of the one-cell family is its treated success probability. Given the specified input d, the specified input x, the specified input p, the specified input hp, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
For a valid treated success probability and an observed atom, the one-cell law's observed point mass has the displayed explicit form.
Formal statement
Proof (Lean source)
Every one-cell observed law is dominated by the central one. Given the specified input d, the specified input x, the specified input p, the specified input hp, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The central one-record chi-square divergence of the one-cell family. Given the specified input d, the specified input x, the specified input p, the specified input hp, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.PairedPrefixTransfer 1 declarations The exact observed-atom identity identifies the conditional count law with independent Poisson counts from the normalized marks.
Fixed-size predictive comparison for the normalized paired priors
The exact observed-atom identity identifies the conditional count law with independent Poisson counts from the normalized marks. The shared normalizer is at least one half, so the four-n experiment loses at most sixteen over n when converted to its fixed-size ordered prefix.
The exact normalized paired predictives are compared by their count mixtures with a uniform prefix-transfer loss of sixteen divided by n. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.LowerBound.PrefixTransfer 1 declarations Histogram reconstruction retains the ordered experiment.
Random-scale prefix comparison through independent Poisson counts
Histogram reconstruction retains the ordered experiment. The shared latent scale need not be constant: only its uniform lower bound enters the short-count loss. These lemmas implement the transfer in equations (15)--(16) of the normalized-converse roadmap.
Integrating a measure-valued map against a finite PMF is its finite weighted mixture. Given the specified input X, the specified input f, the stated mathematical conclusion holds. Given the specified input Θ, the specified input π.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.PairedPrior 44 declarations Normalized paired prior and count experiment
Normalized paired prior and count experiment
Full legal law generated by one latent vector and one prior sign.
Definition (Lean source)
The normalized full-law mass is the displayed atom weight. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input w, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ.
Formal statement
Proof (Lean source)
All atoms inconsistent with the treatment-selected potential outcomes have zero mass. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ.
Formal statement
Proof (Lean source)
The constructed control potential outcome is identically zero. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input w, the specified input hy, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ.
Formal statement
Proof (Lean source)
Treatment remains a fair coin after the random cell masses are normalized. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ.
Formal statement
Proof (Lean source)
At fixed potential outcomes, the filler weight is equal in both arms. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input v, the specified input a, the stated mathematical conclusion holds. Given the specified input θ.
Formal statement
Proof (Lean source)
At fixed potential outcomes, an oriented pair weight is equal in both arms. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input side, the specified input v, the specified input a, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
The complete constructed law has equal arm masses at each potential atom. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input v, the specified input a, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ.
Formal statement
Proof (Lean source)
The normalized construction is randomized independently of all potential coordinates. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ.
Formal statement
Proof (Lean source)
At a fixed oriented label and fixed nonarrival coordinates, the arrived atom carries at least the fraction q of the two arrival possibilities. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input side, the specified input v, the specified input a, the specified input s, the specified input y, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ, the specified input j.
Formal statement
Proof (Lean source)
All filler mass has an arrived outcome. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input v, the specified input a, the specified input s, the specified input y, the stated mathematical conclusion holds. Given the specified input θ. Given the specified input hq.
Formal statement
Proof (Lean source)
The normalized atom weights retain the arrival floor after summing labels. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input v, the specified input a, the specified input s, the specified input y, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ.
Formal statement
Proof (Lean source)
Coordinates arranged with arrival last, for finite-sum calculations. Given the specified input d, the stated mathematical conclusion holds.
Definition (Lean source)
Rewrite a full-atom sum as nested sums, with arrival the innermost bit. Given the specified input d, the specified input f, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The pointwise arrival inequality gives the conditional arrival floor. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ.
Formal statement
Proof (Lean source)
If each observed cell has an arrival factor depending only on the observed record, the full-data law satisfies missing at random.
Formal statement
Proof (Lean source)
One oriented pair has an arrival factor independent of its outcome bit. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input side, the specified input v, the specified input a, the specified input s, the specified input y, the specified input r, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
The filler component always arrives, independently of its outcome bit. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input v, the specified input a, the specified input s, the specified input y, the specified input r, the stated mathematical conclusion holds. Given the specified input θ.
Formal statement
Proof (Lean source)
Only the filler component contributes at the filler label. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input w, the specified input hw, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ.
Formal statement
Proof (Lean source)
Only its own oriented component contributes at a paired label. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input side, the specified input w, the specified input hw, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
For a sample size of at least one, a positive dimension, an admissible arrival floor, an admissible sign, and a latent configuration, the paired construction is a legal law in the model class.
Formal statement
Proof (Lean source)
The normalized law, bundled with its MAR-class certificate.
Definition (Lean source)
The pair of priors on legal normalized MAR laws, indexed by prior sign.
Definition (Lean source)
Finite prior-predictive iid mixture for either sign.
For a covariate dimension and an arrival floor, the class of legal laws is equipped with the discrete measurable structure.
Definition (Lean source)
For a covariate dimension and an arrival floor, every singleton legal law is measurable.
Definition (Lean source)
The complete observed-sample mixture induced by any prior on legal laws.
Prior probability of a target event.
the stated mathematical conclusion holds. Given the specified input α, the specified input π.
Formal statement
Proof (Lean source)
For a sample size of at least one, a positive dimension, and an admissible arrival floor, the negative-sign paired predictive law equals the predictive law of the first paired prior.
Formal statement
Proof (Lean source)
For a sample size of at least one, a positive dimension, and an admissible arrival floor, the positive-sign paired predictive law equals the predictive law of the second paired prior.
Formal statement
Proof (Lean source)
Unnormalized observed atom coefficient of an oriented pair.
Fixed filler observed-atom coefficient.
Definition (Lean source)
Unnormalized mass at an observed atom in the count experiment.
Definition (Lean source)
Independent Poisson counts with rate 4n times each unnormalized atom mass.
Definition (Lean source)
Latent mixture of the unnormalized count experiment.
Definition (Lean source)
The number of records in a finite count vector.
Definition (Lean source)
An ordering has exactly the specified multiset of records.
Definition (Lean source)
For observed-cell counts, the collection of all orderings with exactly those counts is defined.
Definition (Lean source)
Given the specified input counts, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Uniform ordering of the finite counted multiset.
Definition (Lean source)
Uniform ordering followed by first-n truncation, independent of sign and latent draws.
Definition (Lean source)
The public handle for the normalized paired-prior construction and its associated predictive and count experiments.
Definition (Lean source)
The normalized same-experiment paired-prior handle, including the induced sample mixtures, Poisson count experiments, and the fixed-record truncation kernel used to transfer between them. Given the specified input n, the specified input d, the specified input q, the specified input o_circle, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input hq.
Definition (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.PairedPrior.Atoms 49 declarations The latent support, legal full laws, observed mixtures, independent Poisson count experiment and parameter-independent count-ordering kernel are defined here.
Normalized paired prior and count experiment
The latent support, legal full laws, observed mixtures, independent Poisson count experiment and parameter-independent count-ordering kernel are defined here. All normalization and law-class obligations are separately named proof obligations.
The interpolation degree is the logarithmic degree selected for the sample size.
The interpolation lower endpoint is determined by the sample size.
Definition (Lean source)
The prior scale is determined by the sample size.
Definition (Lean source)
The number of paired coordinates is determined by the sample size and the covariate dimension.
The residual filler mass is determined by the sample size and the covariate dimension.
The baseline Bernoulli mean is calibrated to the arrival-floor parameter.
Definition (Lean source)
Interpolation nodes on [h,1].
Cardinal Lagrange coefficient evaluated at zero.
Definition (Lean source)
Total variation of the interpolation coefficients.
Definition (Lean source)
Signed normalized interpolation weights.
Definition (Lean source)
One latent pair is either an interpolation node or the residual zero atom.
The latent probability coordinate assigns each atom in the sample-size-dependent support its interpolation value or zero.
Definition (Lean source)
The latent sign coordinate assigns each atom in the sample-size-dependent support its signed interpolation orientation.
Definition (Lean source)
The latent mixing weight assigns each atom in the sample-size-dependent support its normalized mass.
Definition (Lean source)
Given the specified input n, the stated mathematical conclusion holds. Given the specified input i.
Formal statement
Proof (Lean source)
Given the specified input n, the stated mathematical conclusion holds. Given the specified input i.
Formal statement
Proof (Lean source)
Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
For a sample size of at least one, a positive dimension, and an admissible arrival floor, the latent weights sum to one.
Formal statement
Proof (Lean source)
Probability law of one latent pair, including the residual atom.
Definition (Lean source)
Latent draws and independent fair orientation signs for all pairs.
Product weight of all independent pair draws and fair signs.
Definition (Lean source)
For a sample size of at least one, a positive dimension, and an admissible arrival floor, the joint weights of latent draws and orientations sum to one.
Formal statement
Proof (Lean source)
For a sample size, a positive dimension, and an admissible arrival floor, the probability law of all latent draws and orientations is defined.
Definition (Lean source)
Exact random total mass of the unnormalized filler and pair labels.
Definition (Lean source)
The two orientations at a pair are opposite.
Treatment arrival probability in one oriented pair under sign σ.
Definition (Lean source)
Treatment outcome mean at one pair label.
Definition (Lean source)
For a sample size and a positive dimension, the pair labels and filler label fit within the available covariate labels.
Formal statement
Proof (Lean source)
The filler has label zero.
Definition (Lean source)
For a pair index, a side of that pair, and a positive dimension, the corresponding pair label is strictly below the dimension.
Formal statement
Proof (Lean source)
Pair labels occupy the next 2M positions.
Definition (Lean source)
A pair index and orientation determine a unique baseline label. Given the specified input n, the specified input d, the specified input hd, the specified input side, the specified input side', the specified input h, the stated mathematical conclusion holds. Given the specified input j, the specified input k.
Formal statement
Proof (Lean source)
The filler label is disjoint from every paired label. Given the specified input n, the specified input d, the specified input hd, the specified input side, the stated mathematical conclusion holds. Given the specified input j.
Formal statement
Proof (Lean source)
Bernoulli factor, totalized by the real arithmetic of the displayed model.
Definition (Lean source)
Given the specified input p, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input p, the specified input hp, the specified input b, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input q, the specified input z, the specified input u, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input hq, the specified input ht.
Formal statement
Given the specified input q, the specified input z, the specified input u, the stated mathematical conclusion holds. Given the specified input σ. Given the specified input hq, the specified input hu, the specified input ht.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input z, the stated mathematical conclusion holds.
Proof (Lean source)
Given the specified input side, the stated mathematical conclusion holds. Given the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input side, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hσ, the specified input j.
Formal statement
Proof (Lean source)
Full atom mass at an oriented pair label, before normalization.
Definition (Lean source)
A paired component puts no mass on another pair's baseline label. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input side, the specified input side', the specified input w, the specified input hw, the specified input hne, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input j, the specified input k.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input z, the stated mathematical conclusion holds.
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input hJ, the specified input side, the specified input w, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ, the specified input j.
Formal statement
Proof (Lean source)
Full atom mass at the fixed filler label, before normalization.
Definition (Lean source)
The filler component puts no mass on a paired baseline label. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input side, the specified input w, the specified input hw, the stated mathematical conclusion holds. Given the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
Every paired component puts no mass on the filler baseline label. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input side, the specified input w, the specified input hw, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
Exact mass of a normalized causal full-data atom.
Definition (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.PairedPrior.Normalization 16 declarations Exact normalization and positivity of constructed full laws
Exact normalization and positivity of constructed full laws
Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the stated mathematical conclusion holds. Given the specified input i.
Formal statement
Proof (Lean source)
For positive sample size, positive covariate dimension, and an arrival floor in the admissible range, the normalization constant is strictly positive.
Formal statement
Proof (Lean source)
For an arrival floor in the admissible range, the associated baseline mean lies between zero and one.
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input w, the stated mathematical conclusion holds. Given the specified input θ. Given the specified input hq.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input w, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ.
Formal statement
Proof (Lean source)
Given the specified input d, the stated mathematical conclusion holds.
Given the specified input d, the stated mathematical conclusion holds.
Definition (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hd, the stated mathematical conclusion holds. Given the specified input θ.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input side, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
Each treatment arm receives half the normalized filler mass. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input a, the stated mathematical conclusion holds. Given the specified input θ.
Formal statement
Proof (Lean source)
Each treatment arm receives half the normalized mass of an oriented pair label. Given the specified input n, the specified input d, the specified input q, the specified input hd, the specified input side, the specified input a, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input j.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the stated mathematical conclusion holds. Given the specified input σ, the specified input θ. Given the specified input hq, the specified input hσ.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.BiasVariance 4 declarations Risk integrability for the finite observed-sample experiment
Risk integrability for the finite observed-sample experiment
When the target lies in the feasible treatment-effect interval, clipping an estimate to that interval cannot increase its squared error.
Formal statement
Proof (Lean source)
The cellwise quadratic missing-mass term in equation (16) is absorbed by its linear missing mass whenever the arrival-floor comparison w ≤ 2 * δ * t holds. Given the specified input w, the specified input t, the specified input m, the specified input hm, the specified input hw, the specified input ht, the specified input hwt, the stated mathematical conclusion holds. Given the specified input δ, the specified input hδ.
Formal statement
Proof (Lean source)
For a law in the model class, an admissible arrival floor, and a positive scale, the cellwise quadratic missing-mass terms are bounded by total missing mass and the arrival floor.
Formal statement
Proof (Lean source)
The missing-cell terms in the heavy-branch variance sum are bounded by one inverse stream intensity, uniformly over the alphabet. Given the specified input d, the specified input q, the specified input P, the specified input h, the specified input m, the specified input hm, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.CellBounds 12 declarations This module formalizes equations (1)--(2): arrived and missing cell masses, their arrival-floor bounds, and the exact centered target decomposition.
Cell decomposition for the upper-risk proof
This module formalizes equations (1)--(2): arrived and missing cell masses, their arrival-floor bounds, and the exact centered target decomposition.
Probability mass in an arrived (X,A,S) cell.
Probability mass in the missing part of an (X,A,S) cell.
Definition (Lean source)
Centered arrived-outcome regression in a cell.
Definition (Lean source)
Signed treatment contrast multiplier.
Definition (Lean source)
Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input q, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input a, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input q, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input q, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.ChebyshevBounds 1 declarations Light-cell Chebyshev calibration obligations
Light-cell Chebyshev calibration obligations
For a positive sample size and a nonzero evaluation point, the polynomial quotient equals its displayed Chebyshev formula.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.ChebyshevCoefficients 1 declarations This module isolates the shifted Chebyshev recurrence and coefficient bound behind equation (6) of the upper-risk proof.
Coefficient growth of the light-cell Chebyshev correction
This module isolates the shifted Chebyshev recurrence and coefficient bound behind equation (6) of the upper-risk proof.
The coefficient budget of the light-cell correction is bounded by the paper's exponential degree factor. Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.ChebyshevRiskBounds 4 declarations These leaves isolate the direct interval consequences of the quotient formula in equation (6) of the upper-risk proof.
Chebyshev quotient bounds for the light-cell correction
These leaves isolate the direct interval consequences of the quotient formula in equation (6) of the upper-risk proof.
The removable value of the Chebyshev quotient at zero is one. Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The Chebyshev quotient is nonnegative at a positive rate below the polynomial threshold. Given the specified input n, the specified input hn, the specified input z, the specified input hz, the specified input hzB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
On the light-cell range, rate times the Chebyshev quotient is bounded by the threshold divided by the square of its polynomial degree. Given the specified input n, the specified input hn, the specified input z, the specified input hz, the specified input hzB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The Chebyshev quotient is at most one at a positive rate below the polynomial threshold. Given the specified input n, the specified input hn, the specified input z, the specified input hz, the specified input hzB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.CompleteArrivalRisk 21 declarations The complete-outcome score is unbiased at arrival floor one.
Complete-arrival and fallback risk branches
The complete-outcome score is unbiased at arrival floor one. Its iid variance bound and projection close that endpoint independently of the main frontier.
Unprojected complete-outcome randomized difference. Given the specified input n, the specified input d, the specified input sample, the stated mathematical conclusion holds.
The complete-arrival one-record randomized score. Given the specified input d, the specified input o, the stated mathematical conclusion holds.
Definition (Lean source)
Given the specified input d, the specified input o, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input sample, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input h, the specified input w, the specified input hw, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input h, the specified input a, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input P, the specified input h, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input P, the specified input hn, the stated mathematical conclusion holds. Given the specified input hmean.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input sample, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input sample, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input z, the specified input t, the stated mathematical conclusion holds. Given the specified input ht.
Proof (Lean source)
Given the specified input n, the specified input d, the specified input P, the specified input sample, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
At complete arrival, the projected estimator has risk at most four over n. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input h, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
All complete-arrival and fallback regimes share a universal risk constant. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input P, the specified input h, the specified input n, the stated mathematical conclusion holds. Given the specified input hq, the specified input hb.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.Fallback 1 declarations Complete-arrival and small-scale estimator branches
Complete-arrival and small-scale estimator branches
If arrival is incomplete and the scale is in the fallback regime, the missing-membership estimator equals the fallback estimator.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.FallbackBias 6 declarations The fallback score averages the arrived centered cell contributions.
Population bias and large-dimension fallback risk
The fallback score averages the arrived centered cell contributions. The omitted missing contributions have absolute sum at most the missingness envelope.
The arrived regression times its cell mass is the arrived outcome mass, including null arrived cells. Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The population fallback score is the arrived part of the centered target. Given the specified input d, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The missing part of the centered contrast has magnitude at most delta. Given the specified input d, the specified input q, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
The population bias of the fallback estimator is bounded by delta. Given the specified input d, the specified input q, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
The fallback branch has risk at most twice the sampling and missingness budgets. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
When dimension exceeds n log(e+n), the fallback risk is at most twice the rate. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input P, the specified input h, the specified input hneq, the specified input n, the stated mathematical conclusion holds. Given the specified input hq, the specified input hd.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.FallbackRisk 7 declarations The centered arrived score has second moment at most one.
Sampling risk and the small-log fallback regime
The centered arrived score has second moment at most one. Its empirical mean therefore has parametric sampling error; projection preserves the resulting bias-and-sampling bound. Bounded loss closes the small-log regime uniformly.
The centered arrived-outcome score used by the fallback branch. Given the specified input d, the specified input o, the stated mathematical conclusion holds.
Definition (Lean source)
Every fallback score has squared magnitude at most one. Given the specified input d, the specified input o, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The fallback formula is the projection of the empirical score mean. Given the specified input n, the specified input d, the specified input sample, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The iid empirical fallback score mean has sampling error at most one over n. Given the specified input n, the specified input d, the specified input hn, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Projection and the sampling bound control fallback risk by twice sampling error plus twice its population bias squared. Given the specified input n, the specified input d, the specified input hn, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The bounded estimator and target have squared loss at most four. Given the specified input n, the specified input d, the specified input q, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
When the logarithmic scale is small, bounded loss is already a universal multiple of the inverse-sample-size component of the frontier rate. Given the specified input n, the specified input d, the specified input hn, the specified input q, the specified input P, the specified input hL, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.LightExponentialBounds 8 declarations The numerical degree and threshold choices turn equation (8) into the small-cell bound (9) and pilot-weighted large-cell decay (11).
Exponential bounds for the light correction
The numerical degree and threshold choices turn equation (8) into the small-cell bound (9) and pilot-weighted large-cell decay (11).
Above the fallback cutoff, the degree is at most the logarithmic scale divided by sixty-four. Given the specified input n, the specified input hL, the stated mathematical conclusion holds.
Proof (Lean source)
The logarithms of the two fixed numerical bases have simple rational upper bounds. the stated mathematical conclusion holds.
Proof (Lean source)
The exponential degree factor in equation (8) is at most exp(6k). Given the specified input k, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
In a small cell, the power-growth factor in equation (8) costs at most exp(k); the numerical threshold is much larger than the degree. Given the specified input n, the specified input hL, the specified input z, the specified input hz, the specified input hzB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Equation (9), with universal constant one, for the actual fourth-stream light correction. Given the specified input n, the specified input d, the specified input hL, the specified input P, the specified input x, the specified input a, the specified input s, the specified input hzB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The large-cell polynomial growth is dominated by exp(z/8). This leaves ample decay after multiplying by the pilot lower-tail probability. Given the specified input n, the specified input hL, the specified input z, the specified input hzB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The actual light correction's second moment grows slowly enough beyond the threshold to be suppressed by the pilot selection probability. Given the specified input n, the specified input d, the specified input hL, the specified input P, the specified input x, the specified input a, the specified input s, the specified input hzB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Equation (11) for the actual light statistic: pilot weighting changes large-cell polynomial growth into exponential decay. Given the specified input n, the specified input d, the specified input hL, the specified input P, the specified input x, the specified input a, the specified input s, the specified input hzB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.LightSecondMoment 10 declarations Descending factorials and the coefficient budget bound the light correction by a count-power envelope.
Pointwise light-correction second-moment bounds
Descending factorials and the coefficient budget bound the light correction by a count-power envelope. The square envelope holds almost surely for the actual fourth-stream statistic, providing the integrand bound for equation (8).
A centered success count bounded by its containing count yields a coefficient-sum bound for the light correction. Given the specified input n, the specified input C, the specified input U, the specified input hC, the specified input hU0, the specified input hUC, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Squaring the coefficient-sum bound controls a single light correction's second-moment integrand. Given the specified input n, the specified input C, the specified input U, the specified input hC, the specified input hU0, the specified input hUC, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A centered success count times the shifted product is at most half the count's descending factorial, including the zero-count case. Given the specified input k, the specified input v, the specified input hv, the specified input U, the specified input hU0, the specified input k, the stated mathematical conclusion holds. Given the specified input hUk.
Formal statement
Proof (Lean source)
The light correction is bounded by half its absolute-coefficient-weighted sum of descending factorials. Given the specified input n, the specified input k, the specified input U, the specified input hU0, the specified input k, the stated mathematical conclusion holds. Given the specified input hUk.
Formal statement
Proof (Lean source)
Bounding descending factorials by powers gives the count-power envelope used before taking Poisson moments in equation (8). Given the specified input n, the specified input k, the specified input U, the specified input hU0, the specified input k, the stated mathematical conclusion holds. Given the specified input hUk.
Formal statement
Proof (Lean source)
Powers below a fixed degree are bounded by the larger of one and the highest power of a nonnegative ratio. Given the specified input r, the specified input hr, the specified input v, the specified input K, the specified input hv, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The coefficient budget turns the light correction into a single count-to-threshold power envelope with exponential degree factor. Given the specified input n, the specified input k, the specified input U, the specified input hU0, the specified input k, the stated mathematical conclusion holds. Given the specified input hUk.
Formal statement
Proof (Lean source)
Squaring the count-power envelope produces the exponential-degree and power-growth factors of the light second-moment bound. Given the specified input n, the specified input k, the specified input U, the specified input hU0, the specified input k, the stated mathematical conclusion holds. Given the specified input hUk.
Formal statement
Proof (Lean source)
Almost surely the arrived count is a natural number and the success count lies between zero and that count. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The actual light-stream statistic obeys the count-power square envelope almost surely under the ideal experiment. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.PilotTails 2 declarations The exponential tilt by log 4 gives the light-selection lower tail and the complementary heavy-selection upper tail used in the upper-risk proof.
Poisson tails for pilot selection
The exponential tilt by log 4 gives the light-selection lower tail and the
complementary heavy-selection upper tail used in the upper-risk proof.
The light-branch selection probability obeys the Poisson lower-tail estimate at the arrived-cell rate. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The heavy-branch selection probability obeys the Poisson upper-tail estimate at the arrived-cell rate. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamAggregateVariance 3 declarations Independence of distinct cells turns the selected cell variance sum into the variance of the signed correction aggregate.
Aggregate correction variance and nonfallback risk
Independence of distinct cells turns the selected cell variance sum into the variance of the signed correction aggregate. This finishes the nonfallback risk budget.
Independence across cells identifies aggregate signed correction variance with the sum of individual selected-product variances. Given the specified input n, the specified input d, the specified input hn, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The signed aggregate satisfies the universal selected-cell variance budget. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input d, the specified input n, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hd, the specified input hq.
Formal statement
Proof (Lean source)
The nonfallback estimator has a universal risk constant after the cross-cell variance, projection, capping, and averaging budgets are combined. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input P, the specified input h, the specified input hqne, the specified input d, the specified input n, the stated mathematical conclusion holds. Given the specified input hq, the specified input hreg.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamBiasAlgebra 4 declarations The signed treatment contrast in equation (14) is controlled by a weighted sum of cellwise correction biases.
Deterministic aggregation of the pilot correction bias
The signed treatment contrast in equation (14) is controlled by a weighted sum of cellwise correction biases.
A centered Bernoulli outcome regression has absolute value at most one half. Given the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The light-branch pilot selection probability lies in the unit interval. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The absolute bias of one pilot-selected correction is bounded by its light Chebyshev remainder and heavy empty-count remainder. Given the specified input n, the specified input d, the specified input q, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The signed aggregate pilot bias is bounded by the missing-mass-weighted sum of the absolute cell biases. Given the specified input n, the specified input d, the specified input q, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamBiasRates 5 declarations The arrival-floor comparison converts the Chebyshev quotient rate bound into a missing-mass-weighted cell estimate for equation (13).
Small-cell pilot bias rate bounds
The arrival-floor comparison converts the Chebyshev quotient rate bound into a missing-mass-weighted cell estimate for equation (13).
In a light-rate cell, missing mass times the Chebyshev remainder is controlled by the arrival floor and the quotient rate bound. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the specified input hzB, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
In the nonfallback regime the polynomial degree is at least one hundred twenty-eighth of the logarithmic sample scale. Given the specified input n, the specified input hL, the stated mathematical conclusion holds.
Proof (Lean source)
The threshold-to-squared-degree ratio has the inverse logarithmic rate used in the light-cell bias calculation. Given the specified input n, the specified input hL, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The light-cell remainder bound also holds in absolute value, including null arrived cells where the missing mass vanishes. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the specified input hzB, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
The light-rate cells' pilot-weighted Chebyshev remainders sum to a universal multiple of delta times alphabet size divided by n log(e+n). Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamCellIndependence 15 declarations Singleton histogram counts are independent within each Poisson stream and across the four streams.
Independence of Poisson stream histograms across cells
Singleton histogram counts are independent within each Poisson stream and across the four streams. Disjoint cell coordinates therefore supply independent missing-membership corrections.
The singleton counts in each of the four finite Poisson streams. Given the specified input d, the specified input i, the specified input o, the stated mathematical conclusion holds. Given the specified input streams.
Definition (Lean source)
Every histogram coordinate is a measurable count statistic. Given the specified input d, the specified input i, the specified input o, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A stream histogram has the independent singleton Poisson count law. Given the specified input n, the specified input d, the specified input P, the specified input i, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The entire family of stream-by-atom counts is independent. This combines Poisson splitting within each stream with independence of the four streams. Given the specified input n, the specified input d, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Coordinates belonging to one observed covariate-treatment-surrogate cell. Given the specified input d, the specified input j, the stated mathematical conclusion holds.
Distinct cells use disjoint singleton histogram coordinates. Given the specified input d, the specified input j, the specified input k, the specified input hjk, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The complete count vectors for two distinct cells are independent. Given the specified input n, the specified input d, the specified input P, the specified input j, the specified input k, the specified input hjk, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
An event count is the sum of its singleton histogram counts. Given the specified input d, the specified input E, the stated mathematical conclusion holds. Given the specified input sample.
Formal statement
Proof (Lean source)
Extend a cell's count vector by zero outside that cell. Given the specified input d, the specified input j, the specified input v, the specified input i, the specified input o, the stated mathematical conclusion holds.
Definition (Lean source)
Counts formed from the zero extension of a cell histogram. Given the specified input d, the specified input j, the specified input v, the specified input i, the specified input E, the stated mathematical conclusion holds.
Definition (Lean source)
Any event supported on a cell can be counted from that cell's histogram. Given the specified input d, the specified input j, the specified input i, the specified input E, the specified input hE, the stated mathematical conclusion holds. Given the specified input streams.
Formal statement
Proof (Lean source)
The selected correction is a function of just one cell's count vector. Given the specified input d, the specified input n, the specified input j, the specified input v, the stated mathematical conclusion holds.
Definition (Lean source)
A cell correction agrees exactly with its histogram representation. Given the specified input n, the specified input d, the specified input j, the stated mathematical conclusion holds. Given the specified input streams.
Formal statement
Proof (Lean source)
The histogram representation of a cell correction is measurable. Given the specified input n, the specified input d, the specified input j, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Corrections from distinct cells are independent, even though their pilot and outcome branches within a cell can be dependent. Given the specified input n, the specified input d, the specified input P, the specified input j, the specified input k, the specified input hjk, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamCorrectionVariance 11 declarations The independent missing-count and fourth-stream correction moments bound the pilot-selected difference from the heavy branch, as in equation (17).
Small-cell correction variance budget
The independent missing-count and fourth-stream correction moments bound the pilot-selected difference from the heavy branch, as in equation (17).
The normalized missing stream is independent of every measurable statistic of the fourth stream. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the specified input hf, the stated mathematical conclusion holds. Given the specified input f.
Formal statement
Proof (Lean source)
The difference between light and heavy corrections is square integrable. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Squaring the branch difference costs twice the light second moment and one half for the bounded heavy branch. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Independence supplies both integrability and the exact unselected product second moment needed to dominate the pilot-selected correction. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Pilot selection only removes the branch difference, so its square is bounded by the unselected product square. Given the specified input n, the specified input d, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds. Given the specified input streams.
Formal statement
Proof (Lean source)
The pilot-selected correction is measurable. Given the specified input n, the specified input d, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The selected product square is integrable by domination, without additional regularity hypotheses on the estimator. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Dropping pilot selection and factoring the independent product bounds the actual correction second moment by the two branch moments. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A small cell has a uniformly small missing-count second moment, using the arrival floor rather than any extra moment premise. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the specified input hzB, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Equation (17), cellwise: pilot-selected correction squares in small cells have the exponential light-moment envelope times the missing-count budget. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the specified input hzB, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Equation (17), aggregated over the at most four times d small cells. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamCorrections 2 declarations This module proves the light polynomial and heavy ratio branch identities for the four-stream estimator.
Correction branch means for the upper-risk proof
This module proves the light polynomial and heavy ratio branch identities for the four-stream estimator.
Equation (5), light branch: the mean polynomial correction is the centered cell outcome mean times one minus the Chebyshev quotient. Given the specified input n, the specified input d, the specified input P, the specified input q, the specified input h, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Equation (5), heavy branch: the plug-in correction has mean equal to the centered cell outcome mean times its nonempty-count probability. Given the specified input n, the specified input d, the specified input P, the specified input q, the specified input h, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamCorrectionsBase 6 declarations This module contains the scalar factorial identities, the joint arrived-success moment, and the integrability result used by the correction branch means.
Factorial corrected stream moments
This module contains the scalar factorial identities, the joint arrived-success moment, and the integrability result used by the correction branch means.
The paper's shifted product becomes the usual falling factorial after including the leading count. Given the specified input k, the specified input v, the specified input hv, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The scalar factorial moment needed after conditioning on the arrived count. Given the specified input rate, the specified input v, the specified input hv, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
For an observed-data probability mass function and a decidable event, the event probability equals its explicit sum of point masses.
Formal statement
Proof (Lean source)
In one arrived cell, the success count weighted by a function of the total arrived count has the same mean as the total count weighted by that function, times the totalized arrived-success probability. This is the joint-count step used in equation (4). Given the specified input n, the specified input d, the specified input v, the specified input hv, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Equation (4): the centered success count times a shifted falling factorial has expectation equal to the centered cell mean times the corresponding Poisson-rate power. Given the specified input n, the specified input d, the specified input v, the specified input hv, the specified input P, the specified input q, the specified input h, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
For a positive factorial order, a full-data law, a covariate cell, and treatment and arrival indicators, the centered factorial stream statistic is integrable under the four-stream law.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamHeavyBias 7 declarations The second remainder in equation (12) is exponentially small uniformly in the arrived-cell rate.
Heavy-branch empty-count bias
The second remainder in equation (12) is exponentially small uniformly in the arrived-cell rate. Summing against missing mass gives its contribution to equation (14), without a factor depending on the alphabet size.
The logarithmic tilt used for pilot selection is at least one. the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Splitting at one sixteenth of the threshold makes the heavy-branch empty-count remainder uniformly exponentially small. Given the specified input B, the specified input z, the specified input p, the specified input hB, the specified input hp, the stated mathematical conclusion holds. Given the specified input htail.
Formal statement
Proof (Lean source)
The heavy empty-count part of the selected correction bias is uniformly bounded at every cell, including null cells. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Summing the heavy empty-count remainder against missing cell mass costs at most delta times exp of minus sixteen logarithmic sample scales. Given the specified input n, the specified input d, the specified input q, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Multiplying a half-sum cell bias bound by twice the nonnegative missing mass removes the one-half factor. Given the specified input w, the specified input b, the specified input u, the specified input v, the specified input hw, the stated mathematical conclusion holds. Given the specified input hb.
Formal statement
Proof (Lean source)
The signed correction bias is controlled by the pilot-weighted polynomial remainder plus the now-bounded heavy empty-count remainder. Given the specified input n, the specified input d, the specified input q, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
In the nonfallback regime the only unbounded part of the signed bias is the polynomial remainder on cells above the threshold. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamHeavyVariance 6 declarations Square integrability and independent stream moments give the cellwise variance bound and its alphabet-uniform sum in equation (16) of the upper-risk proof.
Heavy correction product variance
Square integrability and independent stream moments give the cellwise variance bound and its alphabet-uniform sum in equation (16) of the upper-risk proof.
The ideal four-stream experiment is a probability measure. Given the specified input n, the specified input d, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The normalized missing-cell count is square integrable, including at zero sample size under the totalized division convention. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The missing-count times heavy-correction statistic is square integrable: the heavy factor has absolute value at most one half almost surely. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The mean of the heavy correction has squared absolute size at most one quarter under its almost-sure centered Bernoulli range. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Independent stream moments and the inverse-rate heavy variance bound give the cellwise product-variance budget in equation (16). Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The sum of the actual heavy product variances is bounded by 34 divided by the sample size, uniformly over the alphabet and the legal arrival floors. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamLargeBias 8 declarations The light mean identity and its second moment suppress the large-cell Chebyshev remainder, completing equation (14) of the upper-risk proof.
Large-cell pilot bias and the aggregate bias rate
The light mean identity and its second moment suppress the large-cell Chebyshev remainder, completing equation (14) of the upper-risk proof.
The square of the light correction's mean is bounded by its second moment. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
In a large cell, the pilot lower tail decays at least as exp(-z/4). Given the specified input n, the specified input d, the specified input hL, the specified input P, the specified input x, the specified input a, the specified input s, the specified input hzB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Pilot weighting makes the absolute light mean decay at exp(-z/16), by the mean-square inequality and equation (11). Given the specified input n, the specified input d, the specified input hL, the specified input P, the specified input x, the specified input a, the specified input s, the specified input hzB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Equation (5) turns the light mean bound into a bound for the actual centered Chebyshev remainder, without division by the centered regression. Given the specified input n, the specified input d, the specified input q, the specified input hL, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the specified input hzB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The absolute branch bias retains the centered regression in the polynomial term, so the large-cell mean identity can be used directly. Given the specified input n, the specified input d, the specified input q, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Large-cell branch bias is exponentially small, including the empty-count heavy remainder. Given the specified input n, the specified input d, the specified input q, the specified input hL, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the specified input hzB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Each missing-mass-weighted bias has a small-cell polynomial budget and an exponentially small residual, completing the cellwise split in (14). Given the specified input n, the specified input d, the specified input q, the specified input hL, the specified input P, the specified input h, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Equation (14) for the actual pilot-selected correction: the signed aggregate bias has the desired logarithmic rate plus exponential residual. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamLargeVariance 9 declarations Pilot selection is retained in the independent three-stream product, so the large-cell light moment decays exponentially as required by equation (18).
Large-cell correction second moments
Pilot selection is retained in the independent three-stream product, so the large-cell light moment decays exponentially as required by equation (18).
Three distinct ideal streams factor integrable coordinate products. Given the specified input n, the specified input d, the specified input P, the specified input hf, the specified input hg, the specified input hh, the stated mathematical conclusion holds. Given the specified input f, the specified input g, the specified input h, the specified input hfi, the specified input hgi, the specified input hhi.
Formal statement
Proof (Lean source)
The pilot-retained correction square factors into the missing-count second moment, pilot probability, and branch-difference second moment. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Retaining the pilot improves the branch-moment bound by its selection probability, which is essential for large cells. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Equation (18), cellwise: both the light and bounded heavy contributions are exponentially suppressed by the large-cell pilot tail. Given the specified input n, the specified input d, the specified input hn, the specified input hL, the specified input P, the specified input x, the specified input a, the specified input s, the specified input hzB, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The missing-count second moments sum to a dimension-free budget, using nonnegative cell masses and their total missing-mass bound. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Equation (18), summed over all large cells, costs only the total missing-mass budget times the exponential pilot decay. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
The large-cell exponential residual is at most inverse sample size. Given the specified input n, the specified input hn, the specified input hL, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Equation (18) has a universal inverse-sample-size budget, with explicit constant 25 and no dimension dependence. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
The entire selected correction second moment is the sum of the small-cell budget in (17) and the dimension-free large-cell budget in (18). Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamLightSecondMoment 9 declarations The arrived-count law transports the raw Poisson moment bound to the actual fourth stream.
Expected light-correction square envelope
The arrived-count law transports the raw Poisson moment bound to the actual fourth stream. Integrating the pointwise envelope proves equation (8).
Real-valued finite-stream event counts are measurable. Given the specified input d, the specified input hE, the stated mathematical conclusion holds. Given the specified input E.
Formal statement
Proof (Lean source)
The fourth-stream arrived count is measurable. Given the specified input d, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The fourth-stream light correction is measurable. Given the specified input n, the specified input d, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
All arrived-count powers are integrable under the ideal experiment. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the specified input r, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Equation (7) transferred through the actual arrived-count marginal. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the specified input r, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Replacing the maximum by one plus the nonnegative count power gives an integrable envelope for the light correction's square. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The coefficient and count-power envelope makes the actual light correction square integrable without adding regularity premises. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Integrating the envelope and applying the Poisson power moment bound gives the growth factor in equation (8). Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Equation (8) for the actual light-stream statistic, with explicit universal constant one half. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamLinear 14 declarations The linear arrived score is a difference of two thinned Poisson counts.
Moments of the linear first stream
The linear arrived score is a difference of two thinned Poisson counts. Their exact moments give square integrability and an inverse-sample-size variance budget for the linear term in equations (1) and (20).
Count a Boolean event in an auxiliary stream. Given the specified input d, the specified input i, the specified input E, the stated mathematical conclusion holds. Given the specified input streams.
Stream event counts are measurable. Given the specified input d, the specified input i, the specified input E, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Thinning any of the four streams gives the Poisson law at intensity n/8 times the event probability. Given the specified input n, the specified input d, the specified input P, the specified input i, the specified input E, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Real event counts have finite second moments. Given the specified input n, the specified input d, the specified input P, the specified input i, the specified input E, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The mean of an event count is its thinned intensity. Given the specified input n, the specified input d, the specified input P, the specified input i, the specified input E, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The variance of an event count is its thinned intensity. Given the specified input n, the specified input d, the specified input P, the specified input i, the specified input E, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The normalized arrived score from the first auxiliary stream. Given the specified input n, the specified input d, the stated mathematical conclusion holds. Given the specified input streams.
Definition (Lean source)
The linear term is the difference of positive and negative arrived counts. Given the specified input n, the specified input d, the stated mathematical conclusion holds. Given the specified input streams.
Formal statement
Proof (Lean source)
The first-stream linear term is square integrable. Given the specified input n, the specified input d, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The linear term in the raw estimator agrees with the named first-stream score. Given the specified input n, the specified input d, the stated mathematical conclusion holds. Given the specified input streams.
Formal statement
Proof (Lean source)
The linear-stream variance is bounded by a universal multiple of 1/n. The two event probabilities are each at most one; no cell-count factor enters. Given the specified input n, the specified input d, the specified input hn, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The arrived score mean is the difference of its positive and negative event probabilities. Given the specified input d, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Normalizing the first Poisson stream leaves the population arrived-score mean unchanged. Given the specified input n, the specified input d, the specified input hn, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The linear-stream mean is exactly the arrived part of the identified centered target decomposition (1). Given the specified input n, the specified input d, the specified input hn, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamMoments 10 declarations These leaves isolate equations (3)--(5) of the upper-risk proof.
Paper-local four-stream moment targets
These leaves isolate equations (3)--(5) of the upper-risk proof. They expose the exact independent Poisson stream law and the estimator's named cell statistics.
The ideal independent four-stream law for one full-data distribution.
Definition (Lean source)
Mean count of arrived records in a cell of one auxiliary stream.
Definition (Lean source)
Nonnegative Poisson rate for an arrived cell in one auxiliary stream.
Equation (3), first moment: the normalized missing count has mean equal to the missing cell mass. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input X, the specified input Y, the specified input P, the specified input f, the specified input hf, the specified input lambda, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input X, the specified input E, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
An event count in a finite Poisson sample has the corresponding Poisson law. Given the specified input X, the specified input Q, the specified input lam, the specified input E, the specified input hE, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input d, the specified input E, the stated mathematical conclusion holds. Given the specified input z.
Formal statement
Proof (Lean source)
Equation (3), second moment: a scaled Poisson missing count has its mean squared plus its Poisson variance. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Equation (3), count law: the pilot and correction arrived counts each have the Poisson law with rate given by the arrived cell mass. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamPilot 4 declarations These paper-local identities combine the proved branch means using independence of the third pilot stream from the fourth correction stream.
Pilot selection of the light and heavy correction branches
These paper-local identities combine the proved branch means using independence of the third pilot stream from the fourth correction stream.
Probability that the third stream selects the light correction in a cell.
Definition (Lean source)
The pilot light-selection probability is the Poisson probability that the arrived-cell pilot count is below its threshold. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Independence of the pilot and correction streams mixes their light and heavy expected corrections with the pilot selection probability. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The selected correction's cellwise bias is the sum of its light Chebyshev remainder and heavy empty-count remainder. Given the specified input n, the specified input d, the specified input P, the specified input q, the specified input h, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamProduct 2 declarations These identities isolate the independence step in the heavy-cell variance calculation of the upper-risk proof.
Product moments of the independent missing and correction streams
These identities isolate the independence step in the heavy-cell variance calculation of the upper-risk proof.
The mean of a cell's missing-count times heavy correction factors across the independent second and fourth Poisson streams. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The second moment of a cell's missing-count times heavy correction factors across the independent second and fourth Poisson streams. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamRawMean 5 declarations Independence of the missing-count stream from the pilot and outcome streams turns the correction mean into the missing-mass-weighted mean in equation (14).
Mean and bias of the unprojected four-stream estimator
Independence of the missing-count stream from the pilot and outcome streams turns the correction mean into the missing-mass-weighted mean in equation (14).
The missing-count statistic is independent of the jointly selected pilot and outcome correction, since their stream coordinates are disjoint. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Independence factors the mean of the actual selected cell product. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The finite sum defining the unprojected estimator is square integrable. Given the specified input n, the specified input d, the specified input hn, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The exact raw-estimator bias is the signed aggregate selected-correction bias; identification cancels the first-stream arrived component. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
The raw-estimator bias inherits equation (14), with no extra regularity premises or independence gates. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamRiskAssembly 9 declarations Bias, projection, capping and averaging reduce the nonfallback upper bound to one remaining quantity: the variance of the aggregate signed cell correction.
Squared-risk assembly for the four-stream estimator
Bias, projection, capping and averaging reduce the nonfallback upper bound to one remaining quantity: the variance of the aggregate signed cell correction. The aggregate is retained explicitly until cross-cell independence is proved.
The uncapped estimator's squared risk is its variance plus squared bias. Given the specified input n, the specified input d, the specified input hn, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Projection cannot increase squared risk, since the target is in the projection interval and the raw estimator has a finite second moment. Given the specified input n, the specified input d, the specified input hn, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Below the dimension fallback threshold the rate has the untruncated squared-bias scale used in equations (19)--(20). Given the specified input n, the specified input d, the specified input hn, the specified input hL, the specified input q, the specified input d, the specified input n, the stated mathematical conclusion holds. Given the specified input hd.
Formal statement
Proof (Lean source)
The exponentially small pilot-bias remainder has a squared inverse-sample-size budget. Given the specified input n, the specified input q, the specified input hn, the specified input hL, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
The raw estimator's squared bias has the claimed nonfallback rate, using the established pilot-bias bound and its exponential remainder. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input d, the specified input n, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hd, the specified input hq.
Formal statement
Proof (Lean source)
The aggregate signed correction is square integrable by the finite sum of the already established cell product moments. Given the specified input n, the specified input d, the specified input hn, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The raw estimator variance is controlled by the first stream and the aggregate correction; this step does not require independence between them. Given the specified input n, the specified input d, the specified input hn, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
In the nonfallback regime, projection and the proved bias and linear variance budgets leave only the aggregate correction variance to control. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input d, the specified input n, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hd, the specified input hq.
Formal statement
Proof (Lean source)
Capping and averaging preserve the risk reduction to aggregate correction variance, paying only the already proved inverse-sample-size cap penalty. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input P, the specified input h, the specified input hqne, the specified input d, the specified input n, the stated mathematical conclusion holds. Given the specified input hq, the specified input hreg.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamRiskVariance 5 declarations The heavy product and pilot-selected remainder decomposition combines equation (16) with equations (17)--(19), without assuming independence of the branches.
Variance budget for the selected cell correction
The heavy product and pilot-selected remainder decomposition combines equation (16) with equations (17)--(19), without assuming independence of the branches.
The variance of a sum is at most twice the sum of its variances, even when the two square-integrable terms are dependent. Given the specified input X, the specified input Y, the specified input hX, the specified input hY, the stated mathematical conclusion holds. Given the specified input Ω, the specified input μ.
Proof (Lean source)
The pilot-selected remainder is square integrable by the previously proved product-square domination. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The full selected missing-membership correction is square integrable, since it is the sum of the heavy product and selected remainder. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Splitting off the heavy branch bounds the selected cell variance by twice the heavy variance plus twice the selected remainder's second moment. Given the specified input n, the specified input d, the specified input hn, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The sum of selected cell variances has the squared-bias scale and a universal inverse-sample-size budget obtained from equations (16)--(19). Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamStatistic 16 declarations This module identifies the run's explicit count-and-label formula with the finite-partition Rao--Blackwell API.
Four-stream form of the missing-membership estimator
This module identifies the run's explicit count-and-label formula with the finite-partition Rao--Blackwell API.
Count observations in a finite stream satisfying a condition.
Definition (Lean source)
Missing-cell count from the second stream divided by its Poisson intensity.
Definition (Lean source)
Pilot arrived-cell count from the third stream.
Definition (Lean source)
Arrived-cell count from the fourth stream.
Definition (Lean source)
Arrived-success count from the fourth stream.
Definition (Lean source)
Light-cell polynomial correction for a fourth-stream cell.
Definition (Lean source)
Heavy-cell plug-in correction for a fourth-stream cell.
Definition (Lean source)
Pilot-selected correction for one cell.
Definition (Lean source)
One cell's missing-membership correction written as a statistic of four streams.
The raw, unprojected missing-membership estimate of four streams.
Definition (Lean source)
The projected missing-membership estimate as a statistic of four independent streams.
Definition (Lean source)
Uniform masses for the four auxiliary labels.
Definition (Lean source)
the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input N, the specified input sample, the specified input hN, the specified input labels, the specified input stream, the specified input E, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input N, the specified input sample, the specified input hN, the specified input labels, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the specified input n, the specified input d, the specified input q, the specified input sample, the specified input hq, the specified input d, the specified input n, the stated mathematical conclusion holds. Given the specified input hreg.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamSupport 3 declarations The observed outcome mark can be true only when the outcome arrived.
Support of the observed success count
The observed outcome mark can be true only when the outcome arrived. These helpers express that support condition for one observed record and for the fourth ideal Poisson stream.
Count arrived successes in one cell of the fourth stream.
Definition (Lean source)
Under the observed-data law, a true recorded outcome mark almost surely implies that the outcome arrived. Given the specified input d, the specified input P, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Under the ideal four-stream law, the fourth-stream success count agrees almost surely with the count of successes whose outcomes arrived. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamTransfer 7 declarations The actual nonfallback estimator is the finite-partition conditional average.
Capping and averaging the ideal four-stream estimator
The actual nonfallback estimator is the finite-partition conditional average. Conditional Jensen and the Poisson cap coupling transfer its squared risk from the projected ideal experiment, with a universal inverse-sample-size penalty.
Singleton finite samples are measurable, by checking each fixed-size slice. Given the specified input d, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
For a sample size and a covariate dimension, the ideal four-stream estimate is measurable.
Formal statement
Proof (Lean source)
Projection confines every ideal estimate to the feasible target interval. Given the specified input n, the specified input d, the stated mathematical conclusion holds. Given the specified input streams.
Formal statement
Proof (Lean source)
Exponential Markov at tilt log two bounds the count-cap overflow for an auxiliary Poisson count of mean half the sample size. Given the specified input n, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The exponential cap penalty is bounded by eight inverse observations. Given the specified input n, the specified input hn, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Conditional averaging and cap coupling bound the actual nonfallback risk by projected independent-stream risk plus four times the overflow tail. Given the specified input n, the specified input d, the specified input q, the specified input P, the specified input hq, the specified input d, the specified input n, the stated mathematical conclusion holds. Given the specified input hreg.
Formal statement
Proof (Lean source)
The fully implemented nonfallback estimator pays at most a universal inverse-sample-size cost for its cap and auxiliary averaging. Given the specified input n, the specified input d, the specified input hn, the specified input q, the specified input P, the specified input hq, the specified input d, the specified input n, the stated mathematical conclusion holds. Given the specified input hreg.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamVariance 6 declarations This module isolates the self-normalized heavy correction variance needed in the paper's upper-risk aggregation.
Cellwise variance bounds for the four-stream correction
This module isolates the self-normalized heavy correction variance needed in the paper's upper-risk aggregation.
The heavy correction lies in the centered Bernoulli range almost surely. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The totalized heavy correction is measurable as a function of the streams. Given the specified input d, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The centered heavy correction has mean squared size at most one quarter, by its almost-sure centered Bernoulli range. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The heavy correction satisfies the required inverse-rate bound whenever the arrived-cell Poisson rate is at most fifteen. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the specified input hz, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Splitting the containing event into successes and failures splits its zero-safe empirical fraction as well. Given the specified input X, the specified input A, the specified input B, the specified input hAB, the specified input z, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The fourth-stream heavy correction has variance at most a constant divided by one plus its arrived-cell Poisson rate. Given the specified input n, the specified input d, the specified input P, the specified input x, the specified input a, the specified input s, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamVarianceAlgebra 2 declarations These bounds turn a within-stream heavy-correction variance estimate into the cellwise and aggregate product-variance budget in equation (16).
Deterministic heavy-cell variance assembly
These bounds turn a within-stream heavy-correction variance estimate into the cellwise and aggregate product-variance budget in equation (16).
Product-moment algebra bounds one heavy-cell correction variance from its within-stream variance and centered-mean bounds. Given the specified input w, the specified input m, the specified input z, the specified input hw, the specified input hm, the specified input hz, the stated mathematical conclusion holds. Given the specified input ν, the specified input μ, the specified input hμ. Given the specified input hν.
Formal statement
Proof (Lean source)
Summing the heavy-cell product-variance bounds costs at most a universal multiple of the inverse stream intensity. Given the specified input d, the specified input q, the specified input P, the specified input h, the specified input m, the specified input hm, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.Helpers.UpperRisk.StreamVarianceRates 6 declarations Equation (19) follows from the sixth Taylor term of the exponential and Young's inequality.
Absorbing the correction variance into the frontier rate
Equation (19) follows from the sixth Taylor term of the exponential and Young's inequality. These bounds retain the exact exponential logarithmic scale of equation (17), avoiding an unnecessary approximation by n^(1/8).
The sixth logarithmic power is dominated by an exponential with exponent three quarters, with a fixed numerical constant. Given the specified input L, the specified input hL, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The exponential of the sample logarithm is at most a fixed multiple of sample size, including the smallest positive sample size. Given the specified input n, the specified input hn, the stated mathematical conclusion holds.
Proof (Lean source)
Squaring the factor paired with the bias scale in equation (19) costs only a universal multiple of inverse sample size. Given the specified input n, the specified input hn, the specified input hL, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Young's inequality absorbs any fixed multiple of the nonparametric correction term into squared bias and inverse sample size. Given the specified input n, the specified input hn, the specified input hL, the specified input A, the specified input x, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The explicit small-cell envelope in equation (17) factors into the bias scale times the logarithmic factor controlled by equation (19). Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
Combining equations (17)--(19) bounds the full correction second-moment budget by squared bias scale plus a universal inverse-sample-size term. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hL, the specified input P, the specified input h, the stated mathematical conclusion holds. Given the specified input hq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.TCompleteArrival 1 declarations At q=1 the estimator uses only the observed primary outcomes and the rate loses its many-cell term.
Complete-arrival endpoint
At q=1 the estimator uses only the observed primary outcomes and the rate
loses its many-cell term. The point and interval constants remain uniform in d.
Complete arrival gives the projected HT estimator and uniform parametric frontiers. the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.THonestInterval 1 declarations The radius uses a certified uniform risk constant.
Honest clipped interval from the risk certificate
The radius uses a certified uniform risk constant. Its large-radius branch covers deterministically, and its smaller branch uses Markov's inequality.
The clipped interval is honest and has the stated pointwise and expected length. Given the specified input n, the specified input d, the specified input q, the specified input CU, the specified input hn, the specified input hd, the specified input hCU, the stated mathematical conclusion holds. Given the specified input α. Given the specified input hq, the specified input hα.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.TIntervalFrontier 1 declarations Exact honest connected-interval length frontier
Exact honest connected-interval length frontier
Fixed-coverage expected length is uniformly comparable to the square-root rate. the stated mathematical conclusion holds. Given the specified input α. Given the specified input hα.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.TNormalizedConverse 3 declarations Both priors are on the legal full-data class.
Normalized same-experiment converse
Both priors are on the legal full-data class. Their predictive laws retain the entire observed record, including membership on nonarrival.
Paired legal priors have close complete-sample mixtures and separated ATEs. the stated mathematical conclusion holds. Given the specified input β. Given the specified input hβ.
Formal statement
Proof (Lean source)
Separation constant extracted from the proved converse at a fixed tolerance.
Definition (Lean source)
The selected separation constant retains the complete paired-prior certificate. the stated mathematical conclusion holds. Given the specified input β. Given the specified input hβ.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.TParametricFloor 18 declarations The point-risk constant is universal.
One-cell parametric minimax floors
The point-risk constant is universal. The interval constant may depend only on its fixed noncoverage level.
Lowering the required arrival floor preserves membership in the MAR class. Given the specified input d, the specified input q, the specified input q', the specified input hqq', the specified input P, the specified input hP, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A law with deterministic outcome arrival satisfies MAR on every cell. Given the specified input d, the specified input P, the specified input hR, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
An event has the same mass after intersecting with certain arrival. Given the specified input d, the specified input P, the specified input hR, the specified input E, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Certain arrival meets every arrival floor at most one. Given the specified input d, the specified input P, the specified input q, the specified input hq, the specified input hR, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A randomized, balanced and consistent law with certain arrival is legal. Given the specified input d, the specified input P, the specified input q, the specified input hq, the specified input hrandom, the specified input hbalanced, the specified input hconsistent, the specified input hR, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The complete-arrival one-cell Bernoulli family belongs to every required floor class. Given the specified input d, the specified input x, the specified input p, the specified input q, the specified input hp, the specified input hq, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The one-record chi-square expression of the one-cell Bernoulli submodel is at most sixteen times the squared half-separation. Given the specified input u, the specified input hu0, the specified input hu1, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The two treated-atom contributions in the paper's one-record calculation. Given the specified input u, the specified input hu0, the specified input hu1, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Equation (45), ready for the product chi-square comparison. Given the specified input u, the specified input hu0, the specified input hu1, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The product chi-square identity and Cauchy--Schwarz give equation (46) once the one-record divergence is bounded by 16u². Given the specified input d, the specified input n, the specified input hac, the specified input u, the specified input hchi, the stated mathematical conclusion holds. Given the specified input μ, the specified input ν.
Formal statement
Proof (Lean source)
A logarithmic chi-square budget makes the two product laws hard to test. Given the specified input d, the specified input n, the specified input hac, the specified input u, the specified input hchi, the specified input n, the stated mathematical conclusion holds. Given the specified input μ, the specified input ν, the specified input hbudget.
Formal statement
Proof (Lean source)
A single positive perturbation scale meets the product testing budget at every sample size. the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
For absolutely continuous observed laws, a positive sample size, a radius budget valid at every positive integer, and the stated chi-square bound, the product laws have total variation distance at most one half.
Formal statement
Proof (Lean source)
A chi-square budget calibrated to an arbitrary positive testing tolerance. Given the specified input d, the specified input n, the specified input hac, the specified input u, the specified input b, the specified input hb, the specified input hchi, the specified input n, the stated mathematical conclusion holds. Given the specified input μ, the specified input ν, the specified input hbudget.
Formal statement
Proof (Lean source)
The one-cell perturbation can be scaled to any positive interval-testing tolerance. Given the specified input b, the specified input hb, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
For absolutely continuous observed laws, a nonnegative tolerance, a positive sample size, a tolerance radius budget, and the stated chi-square bound, the product laws have total variation distance at most half the tolerance.
Formal statement
Proof (Lean source)
The central and perturbed one-cell laws form a legal pair with controlled divergence. Given the specified input d, the specified input q, the specified input u, the specified input hd, the specified input hq, the specified input hu, the specified input huquarter, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
One-cell Bernoulli submodels give the standard parametric floors. the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.TPointFrontier 1 declarations Exact all-procedure point-risk frontier
Exact all-procedure point-risk frontier
Universal constants sandwich the finite-sample minimax MSE at the stated rate. the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.TPriorReduction 7 declarations This module converts prior separation and parametric floors into interval and combined minimax bounds.
Interval reduction and combined lower frontiers
This module converts prior separation and parametric floors into interval and combined minimax bounds.
A high-probability event on the concentrated part of a prior remains likely in its mixture. Given the specified input n, the specified input d, the specified input q, the specified input Good, the specified input hgood, the stated mathematical conclusion holds. Given the specified input α, the specified input β, the specified input hα. Given the specified input π, the specified input E, the specified input hE.
Formal statement
Proof (Lean source)
Integration under a predictive mixture is integration under the prior of sample integrals. Given the specified input n, the specified input d, the specified input q, the stated mathematical conclusion holds. Given the specified input π, the specified input f.
Formal statement
Proof (Lean source)
The bounded interval length is integrable over any legal-law prior. Given the specified input n, the specified input d, the specified input q, the specified input I, the stated mathematical conclusion holds. Given the specified input π.
Formal statement
Proof (Lean source)
A lower bound on every honest interval's prior-average length passes to minimax length. Given the specified input n, the specified input d, the specified input q, the specified input c, the stated mathematical conclusion holds. Given the specified input α, the specified input hα. Given the specified input π, the specified input h.
Formal statement
Proof (Lean source)
Length on a predictive sample event bounds its mixture expectation. Given the specified input n, the specified input d, the specified input q, the specified input I, the specified input a, the specified input hE, the stated mathematical conclusion holds. Given the specified input π, the specified input E.
Formal statement
Proof (Lean source)
The normalized converse gives the stated 5/4 interval-length coefficient. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input n, the stated mathematical conclusion holds. Given the specified input α. Given the specified input hα, the specified input hq, the specified input hlarge.
Formal statement
Proof (Lean source)
Explicit fuzzy-prior constants, parametric floors and combined lower rates. the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.TPriorReductionPoint 27 declarations This is the paper's reduction from the normalized paired prior and one-cell parametric floor to the combined point and interval lower frontiers.
Fuzzy-prior and interval lower-bound reduction
This is the paper's reduction from the normalized paired prior and one-cell parametric floor to the combined point and interval lower frontiers.
Mixing the legal iid sample laws under a prior gives a probability law. Given the specified input n, the specified input d, the specified input q, the stated mathematical conclusion holds. Given the specified input π.
Formal statement
Proof (Lean source)
A predictive event has probability equal to its prior-averaged sample probability. Given the specified input n, the specified input d, the specified input q, the stated mathematical conclusion holds. Given the specified input π, the specified input E.
Formal statement
Proof (Lean source)
Total variation transfers any sample-event lower bound between the two mixtures. Given the specified input n, the specified input d, the specified input q, the stated mathematical conclusion holds. Given the specified input β. Given the specified input πminus, the specified input πplus, the specified input htv, the specified input E.
Formal statement
Proof (Lean source)
Two high-probability hits under the fuzzy priors overlap under the plus mixture. Given the specified input n, the specified input d, the specified input q, the stated mathematical conclusion holds. Given the specified input α, the specified input β. Given the specified input πminus, the specified input πplus, the specified input htv, the specified input Eleft, the specified input Eright, the specified input hleft, the specified input hright.
Formal statement
Proof (Lean source)
Fixed fuzzy-hypothesis tolerance for point risk.
Definition (Lean source)
The fixed point-risk tolerance lies strictly between zero and one quarter.
Tolerance used in the honest-interval reduction.
Definition (Lean source)
For a confidence level strictly between zero and one half, the interval-risk tolerance lies strictly between zero and one quarter.
Formal statement
Proof (Lean source)
The missingness scale is nonnegative on the model's arrival-floor range. Given the specified input n, the specified input d, the specified input q, the stated mathematical conclusion holds. Given the specified input hq.
Proof (Lean source)
The parametric floor and the separation bound combine into the point-risk rate. Given the specified input n, the specified input d, the specified input q, the specified input c0, the specified input cSep, the specified input R, the specified input hn, the specified input hc0, the specified input hcSep, the specified input n, the specified input n, the stated mathematical conclusion holds. Given the specified input hfloor, the specified input hsep.
Formal statement
Proof (Lean source)
The parametric floor and separated-prior bound combine into the interval rate. Given the specified input n, the specified input d, the specified input q, the specified input c0, the specified input cSep, the specified input R, the specified input hn, the specified input hc0, the specified input hcSep, the specified input hfloor, the specified input n, the stated mathematical conclusion holds. Given the specified input hsep, the specified input hq.
Formal statement
Proof (Lean source)
Prior mass of a target failure is the complement of target success. Given the specified input d, the specified input q, the specified input E, the stated mathematical conclusion holds. Given the specified input π.
Formal statement
Proof (Lean source)
A prior concentration certificate bounds the complementary target event. Given the specified input d, the specified input q, the specified input E, the specified input hgood, the stated mathematical conclusion holds. Given the specified input β. Given the specified input π.
Formal statement
Proof (Lean source)
A test that selects the right hypothesis incurs the separation loss on a left target. Given the specified input t, the specified input m, the specified input a, the specified input ha, the specified input ht, the stated mathematical conclusion holds. Given the specified input θ, the specified input hθ.
Formal statement
Proof (Lean source)
A test that selects the left hypothesis incurs the separation loss on a right target. Given the specified input t, the specified input m, the specified input a, the specified input ha, the specified input ht, the stated mathematical conclusion holds. Given the specified input θ, the specified input hθ.
Formal statement
Proof (Lean source)
A pointwise nonnegative loss bound on a sample event passes to its probability. Given the specified input n, the specified input d, the specified input P, the specified input a, the specified input hf, the specified input hE, the stated mathematical conclusion holds. Given the specified input E, the specified input f.
Formal statement
Proof (Lean source)
A right decision costs the squared separation on every left-target law. Given the specified input n, the specified input d, the specified input P, the specified input T, the specified input m, the specified input a, the specified input ha, the stated mathematical conclusion holds. Given the specified input hτ.
Formal statement
Proof (Lean source)
A left decision costs the squared separation on every right-target law. Given the specified input n, the specified input d, the specified input P, the specified input T, the specified input m, the specified input a, the specified input ha, the stated mathematical conclusion holds. Given the specified input hτ.
Formal statement
Proof (Lean source)
A concentrated prior turns a sample-event loss into a Bayes-risk bound. Given the specified input n, the specified input d, the specified input q, the specified input Good, the specified input loss, the specified input a, the specified input ha, the specified input hgood, the specified input hlossint, the specified input hloss_nonneg, the stated mathematical conclusion holds. Given the specified input β. Given the specified input π, the specified input E, the specified input hloss_good.
Formal statement
Proof (Lean source)
The bounded squared loss can be averaged under any legal-law prior. Given the specified input n, the specified input d, the specified input q, the specified input T, the stated mathematical conclusion holds. Given the specified input π.
Formal statement
Proof (Lean source)
Two concentrated target priors force the sum of their Bayes squared risks. Given the specified input n, the specified input d, the specified input q, the specified input T, the specified input m, the specified input a, the specified input ha, the stated mathematical conclusion holds. Given the specified input β. Given the specified input πminus, the specified input πplus, the specified input htv, the specified input hminus, the specified input hplus.
Formal statement
Proof (Lean source)
A connected interval hitting both separated target regions has length at least 2a. Given the specified input n, the specified input d, the specified input I, the specified input o, the specified input m, the specified input a, the specified input xL, the specified input xR, the specified input hleft, the specified input hright, the stated mathematical conclusion holds. Given the specified input hL, the specified input hR.
Formal statement
Proof (Lean source)
A two-law risk bound passes through the supremum and estimator infimum. Given the specified input n, the specified input d, the specified input q, the specified input c, the specified input Pminus, the specified input Pplus, the stated mathematical conclusion holds. Given the specified input h.
Formal statement
Proof (Lean source)
A fixed legal law gives a lower bound on every honest interval's worst-law length. Given the specified input n, the specified input d, the specified input q, the specified input c, the specified input P, the stated mathematical conclusion holds. Given the specified input α, the specified input hα. Given the specified input h.
Formal statement
Proof (Lean source)
A pointwise risk bound also bounds its average under any legal-law prior. Given the specified input d, the specified input q, the specified input f, the specified input R, the specified input hf, the specified input hR, the stated mathematical conclusion holds. Given the specified input π.
Formal statement
Proof (Lean source)
A Bayes-risk lower bound under two legal priors passes to minimax risk. Given the specified input n, the specified input d, the specified input q, the specified input c, the stated mathematical conclusion holds. Given the specified input πminus, the specified input πplus, the specified input h.
Formal statement
Proof (Lean source)
The normalized converse gives the stated 13/32 point-risk coefficient. Given the specified input n, the specified input d, the specified input q, the specified input hn, the specified input hd, the specified input n, the stated mathematical conclusion holds. Given the specified input hq, the specified input hlarge.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_MarNearcompleteFrontier_Research.TUpperRisk 1 declarations The constant is outside all sample-size, alphabet-size and arrival-floor quantifiers.
Uniform risk of the missing-membership estimator
The constant is outside all sample-size, alphabet-size and arrival-floor quantifiers.
A universal constant controls the estimator's risk on the complete MAR class. the stated mathematical conclusion holds.