Formalization: Minimax Estimation of Optimal Treatment Values with Discrete Covariates
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs.
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Basic 40 declarations Finite-PMF substrate for the observed and full-data experiments.
Discrete optimal-value minimax model
Finite-PMF substrate for the observed and full-data experiments. The general regime-indexed potential-outcome API is intentionally bypassed because all variables here are coordinates of a finite product.
The treatment-outcome coordinate set.
One observed unit.
A probability law on the observed finite alphabet.
Definition (Lean source)
For the specified discrete law, the observed-data law is the probability measure associated with the discrete probability mass function.
Definition (Lean source)
For the specified discrete law, the observed-data law induced by a discrete law is a probability measure.
Definition (Lean source)
An observed atom mass.
Definition (Lean source)
The four observed masses in one covariate cell.
Definition (Lean source)
The mass of a covariate cell.
Definition (Lean source)
The mass of one treatment arm within a covariate cell.
Definition (Lean source)
The totalized propensity.
Definition (Lean source)
The totalized binary outcome regression.
Definition (Lean source)
Canonical finite product law.
Definition (Lean source)
For the specified discrete law, the finite observed-data product law is a probability measure.
Definition (Lean source)
The supplied sample law equals the canonical product law.
Definition (Lean source)
Every occupied cell has propensity in the fixed overlap interval.
Definition (Lean source)
A full-data atom (X,A,Y,Y(0),Y(1)).
A probability law on the full-data alphabet.
For the specified rectangle or law, data point or sample, the full-data atom mass is the real-valued probability assigned by the potential-outcome law to that atom.
Definition (Lean source)
Observed outcomes equal the selected potential outcome almost surely.
Definition (Lean source)
For the specified rectangle or law, cell, treatment arm, y0, y1, the potential-outcome atom mass marginalizes the full-data law over the observed outcome while fixing covariate, treatment, and both potential outcomes.
Definition (Lean source)
The (Y(r),A,X) atom obtained by marginalizing the other potential outcome.
Armwise finite conditional independence Y(r) ⟂ A | X, separately for each arm.
Push a full-data law to its observed margin.
Definition (Lean source)
The unrestricted observed finite-law class, restricted only by overlap.
Definition (Lean source)
Consistent, exchangeable causal completions with an overlapping observed margin.
Definition (Lean source)
If the potential-outcome law satisfies the stated causal restrictions, then the observed marginal belongs to the observed model class.
Formal statement
Proof (Lean source)
The observed-law factorization using the canonical cell mass, propensity, and regressions. This uses the observed law satisfies the stated model restrictions. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The formula underlying the observed optimal-regression value.
Definition (Lean source)
The optimal-regression value, defined only on the published observed model class.
Definition (Lean source)
Full-data cell mass.
Totalized conditional potential-outcome mean.
Definition (Lean source)
The full-data unrestricted oracle value.
Definition (Lean source)
Measurable estimators for the fixed-sample experiment.
Definition (Lean source)
Observed laws packaged with model-class membership.
Definition (Lean source)
Statewise squared-error risk.
Definition (Lean source)
Thin paper-local notation for the reused generic minimax value.
Definition (Lean source)
For the specified alphabet size, overlap level, the causal model law is a potential-outcome law belonging to the causal completion class at the chosen overlap level.
Definition (Lean source)
For the specified overlap level, sample size, estimator, rectangle or law, the causal risk is the squared-error risk of the estimator under the observed marginal, with the potential-outcome oracle value as target.
Definition (Lean source)
For the specified sample size, alphabet size, overlap level, the causal minimax risk is the minimax squared-error risk over the causal model class.
Definition (Lean source)
The logarithmic alphabet scale.
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.AlphabetPadding 9 declarations Zero-mass alphabet padding for the paired fixed-sample L1 experiment.
Zero-mass alphabet padding for the paired fixed-sample L1 experiment.
extending a function by zero along an injection preserves its finite sum.
Formal statement
Proof (Lean source)
For the specified alphabet embedding certificate, discrete law, the padded simplex point extends a smaller probability vector by zero on the added alphabet cells.
Definition (Lean source)
If the stated sd condition holds, then the stated pad simplex l1 distance relation holds.
Formal statement
Proof (Lean source)
If the stated sd condition holds, then the stated simplex probability mass pad simplex relation holds.
Formal statement
Proof (Lean source)
If the stated sd condition holds, then the stated map fixed pair single pad simplex relation holds.
Formal statement
Proof (Lean source)
For the specified alphabet embedding certificate, data point or sample, the padded paired sample embeds both coordinates of every smaller-alphabet observation into the larger alphabet.
If the stated sd condition holds, then zero-padding both distributions and the paired sample preserves fixed-sample L1 risk.
Formal statement
Proof (Lean source)
For the specified smaller alphabet size, nonempty-alphabet certificate, the simplex point mass places all probability on the first cell of a nonempty alphabet.
Definition (Lean source)
If the stated support condition holds, and the stated sd condition holds, then fixed-sample L1 minimax risk cannot decrease when the alphabet is enlarged.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.CitedGates 2 declarations Explicit cited logical gates.
Explicit cited logical gates. These are propositions, not proved declarations.
Cai and Low (2011), Lemma 1 and Section 3.1, arXiv:1105.3039. Symmetric probability measures on [-1,1] match moments through every positive even degree and attain twice the best absolute-value approximation error; that error is bounded above and below by universal multiples of the reciprocal degree.
Definition (Lean source)
Jiao, Han, and Weissman (2018), Theorem 3, equation (24), DOI 10.1109/TIT.2018.2846245. The two-sample Poissonized L1 minimax risk has the stated large-alphabet lower rate in the displayed sample-size regime.
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.ConeExtension 7 declarations Four-cell overlap geometry and the global optimal-value extension.
Four-cell overlap geometry and the global optimal-value extension.
Treatment-arm mass of a four-vector.
Total mass of a four-vector.
Definition (Lean source)
Nonnegative four-vectors whose treated mass is in the overlap band.
Definition (Lean source)
The arm-specific totalized global extension.
Definition (Lean source)
Totalized implementation of the optimal-value cell extension on ambient real vectors.
Definition (Lean source)
The nonnegative four-vector domain appearing in the paper.
Definition (Lean source)
The paper-facing global extension on the nonnegative four-vector cone.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.DenseConstruction 42 declarations Dense sign submodel and the quantities used in its fuzzy-hypothesis lower bound.
Dense sign submodel and the quantities used in its fuzzy-hypothesis lower bound.
For the specified alphabet size, the dense contrast is a coordinate vector whose alphabet has at least two cells and whose entries all lie between minus one half and one half.
For the specified contrast, data point or sample, the dense full-data mass is the consistency-compatible product mass with the two outcome means shifted symmetrically by the contrast, and is zero off the consistency event.
Definition (Lean source)
the dense full-data masses are nonnegative and sum to one.
Formal statement
Proof (Lean source)
For the specified contrast, the dense law is the potential-outcome probability law induced by the dense full-data masses.
Definition (Lean source)
the positive even degree is a positive integer that is even.
Definition (Lean source)
For the specified degree, the best even-degree approximation error is the infimum uniform error for approximating absolute value on minus one to one by a polynomial of degree at most K.
Definition (Lean source)
For the specified alphabet size, the lower approximation degree is twice the ceiling of four times the logarithmic alphabet size.
Definition (Lean source)
the lower approximation degree is even.
Formal statement
Proof (Lean source)
In the paper's nontrivial alphabet regime, the dense lower-bound degree is positive. This uses the alphabet size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The lower-bound degree, packaged in the positive-even carrier in its stated alphabet regime.
Definition (Lean source)
Rounding the logarithmic degree to the next even integer changes it by less than two. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
For the specified sample size, alphabet size, the dense regime holds when the alphabet has at least two cells and its squared size is smaller than the sample size. The alphabet contains at least two cells, and its squared size is below the sample size.
Definition (Lean source)
For the specified sample size, alphabet size, the Poisson cell intensity is twice the sample size divided by the alphabet size.
Definition (Lean source)
For the specified sample size, alphabet size, the dense amplitude is the square root of the lower approximation degree divided by sixty-four times the Poisson cell intensity.
Definition (Lean source)
Squaring the dense amplitude removes the square root and gives the paper's exact scale. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The intrinsic domain on which the scaled priors are laws on the stated contrast cube. The stronger inequality d ^ 2 < n belongs to the lower-bound lemma, not to the construction itself.
Definition (Lean source)
the dense sign-count pair records the two nonnegative integer counts in a cell.
Definition (Lean source)
The actual likelihood ratio for the two independent sign counts in one dense cell, relative to independent baseline Pois(lambda/2) counts. The exponential factors cancel between the two signs.
Definition (Lean source)
For the specified lambda, the dense sign baseline is the product of two independent Poisson laws with equal half-intensity.
Definition (Lean source)
The probability generating function of a scalar Poisson count, in the real-valued form needed by the dense likelihood calculation. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The two independent Poisson sign counts have the exponential likelihood Gram kernel used by the moment-matching substrate. This uses the Poisson intensity is nonnegative. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
the stated dense amplitude range relation holds.
Formal statement
Proof (Lean source)
The dense sample-size regime and overlap inequalities discharge the construction domain. This uses the sample size and alphabet lie in the dense regime, and the overlap parameter satisfies its stated range restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
For the specified sample size, alphabet size, the dense prior separation is the dense amplitude times the best even-polynomial approximation error.
Definition (Lean source)
If the stated e condition holds, then the stated dense prior separation range relation holds.
Formal statement
Proof (Lean source)
For the specified sample size, alphabet size, overlap level, domain certificate, coordinate prior, the scaled dense product prior is the coordinatewise product prior, restricted to the unit cube, scaled by the dense amplitude, and mapped into the contrast class.
Definition (Lean source)
For the specified alphabet size, the dense Poisson sample is a finite marked Poisson sample on the observed-data space.
Definition (Lean source)
For the specified alphabet size, the dense Poisson estimator is a measurable real-valued statistic of the dense Poisson sample.
Definition (Lean source)
For the specified Poisson mean, estimator, discrete law, the Poisson observed risk is squared-error risk of the clipped dense estimator under the finite Poisson observed-sample law.
Definition (Lean source)
Minimax squared risk in the genuine experiment with an independent Poisson sample size having the displayed mean.
Definition (Lean source)
If the alphabet size satisfies its stated restriction, then the stated dense observation kernel exists relation holds.
Proof (Lean source)
For the specified sample size, alphabet size, alphabet-size certificate, the dense observation kernel sends each contrast to its finite Poisson observed-sample law.
Definition (Lean source)
Observation mixture induced by a scaled product prior and an independent Pois(2n) sample.
Definition (Lean source)
For the specified contrast, the dense target is one half plus the average absolute contrast divided by two.
Definition (Lean source)
For the specified sample size, alphabet size, overlap level, domain certificate, coordinate prior, the dense prior target mean is the expectation of the dense target under the scaled product prior.
Definition (Lean source)
Under a supported probability prior, the dense target mean is the baseline one half plus the scaled sum of the one-coordinate absolute moments. This uses the dense construction domain conditions hold, and the prior is supported on the unit interval. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The probability, support, symmetry, moment-matching, and absolute-gap clauses stated for the two dense priors at the fixed lower-bound degree.
Definition (Lean source)
An exact characterization of the Hahn--Banach prior pair at every even degree, before the lower-bound construction specializes the family.
Definition (Lean source)
The complete dense moment-matching construction at one even degree, including the hard submodel, two scaled priors and mixtures, the Poissonized experiment, and the prior target-mean separation.
Definition (Lean source)
For the specified sample size, alphabet size, overlap level, domain certificate, moment-matching prior family, the dense submodel is the moment-matching construction assembled from the dense law, approximation degree, scaled priors, mixtures, target separation, and their certificates. Its components are the domain certificate, the dense law, the approximation error, the approximation degree, the Poisson intensity, the dense amplitude, the first coordinate prior, the second coordinate prior, the first scaled product prior, the second scaled product prior, the first observation mixture, the second observation mixture, the Poissonized risk, the prior target separation, the prior conditions, the degree identity, the target-separation identity.
Definition (Lean source)
Difference of the two target means for the priors bundled by the constructed dense experiment, rather than for arbitrary measures.
Definition (Lean source)
For the specified sample size, alphabet size, the dense likelihood tail is the exponential-series remainder above the lower approximation degree.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.DenseDepoissonization 7 declarations Exact prefix-law substrate for the dense fixed/Poisson risk transfer.
Exact prefix-law substrate for the dense fixed/Poisson risk transfer.
The first n observations of a finite sample, totalized by a fallback array when the sample contains fewer than n points.
Definition (Lean source)
The totalized fixed-prefix map is measurable. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
On the event that a finite Poisson sample contains at least n points, its first n observations have the unnormalised n-fold product law. This uses the stated lam condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
A fixed-sample estimator applied to the first n points of a Poisson sample, with zero output when the Poisson sample is too short.
Definition (Lean source)
Projection to the unit interval cannot increase squared distance from a point already in that interval. This uses the target or contrast satisfies the stated unit-range restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Applying a fixed-sample estimator to a successful Poisson prefix costs at most its fixed-sample risk; the short-sample event costs at most its probability. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The first-n prefix construction transfers the genuine mean-2n Poisson minimax lower bound to the fixed-sample experiment, losing only the Poisson lower-tail probability. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.DenseLowerAssembly 12 declarations Assembly of the dense fuzzy-hypothesis and de-Poissonization certificate.
Assembly of the dense fuzzy-hypothesis and de-Poissonization certificate.
The chosen dense observation kernel is the genuine Poisson sample law at each contrast. This uses the alphabet size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The paper's dense observation mixture is exactly the prior predictive law of its genuine Poisson observation kernel. This uses the alphabet size satisfies its stated restriction, and the dense construction domain conditions hold. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The standard two-fuzzy-hypotheses theorem converts the paper's dense observation-mixture and target-concentration bounds into an ENNReal minimax lower bound for the dense Poisson experiment. This uses the dense construction domain conditions hold, and the stated delta condition holds, and the two experiments have the stated total-variation bound, and the stated prior-tail bound holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Every observed-model target is in the unit interval. This uses the observed law satisfies the stated model restrictions. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The dense fuzzy minimax problem is a restriction of the genuine clipped Poisson observed-law problem. This also converts its ENNReal risk to the paper's real-valued minimax convention. This uses the dense construction domain conditions hold. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
A probability experiment with a target in the unit interval has finite minimax squared risk: the constant-zero estimator has risk at most one. This uses the approximation degree satisfies its stated restriction, and the target lies in the unit interval. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The fuzzy-hypothesis lower bound transfers, with its exact numerical constant, to the paper's genuine Poissonized observed-law minimax risk. This uses the dense construction domain conditions hold, and the stated delta condition holds, and the two experiments have the stated total-variation bound, and the stated prior-tail bound holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The reciprocal-degree Cai--Low bound and logarithmic degree choice make the product-prior concentration scale valid above a universal alphabet cutoff. This uses the Cai--Low moment-matching prior result is available. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The reciprocal Cai--Low approximation bound gives the exact squared separation scale needed by the fuzzy-hypothesis lower bound. This uses the Cai--Low moment-matching prior result is available. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The complete dense fuzzy-hypothesis certificate: construction identities, moment matching, likelihood/tensorization control, concentration, and both Poissonized and fixed-sample risk conclusions.
Definition (Lean source)
The already-localized analytic ingredients assemble into the complete construction and supported-prior portion of the dense lower-bound argument. This isolates the remaining observation-regrouping and minimax-transfer work. This uses the sample size and alphabet lie in the dense regime, and the overlap parameter satisfies its stated range restriction, and the Cai--Low moment-matching prior result is available, and the stated scale inequality holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
If the product experiment has the stated independent-sampling law, and the Cai--Low moment-matching prior result is available, then in the dense regime, the minimax risk is bounded below by a positive constant times .
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.DenseMomentMatchingLower 28 declarations Conditional dense moment-matching lower bound.
Conditional dense moment-matching lower bound.
The Poisson sign-count likelihood is jointly measurable in its contrast parameter and the two observed counts. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
On the prior support, both sign factors in the Poisson likelihood are nonnegative. This uses the target or contrast satisfies the stated unit-range restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The likelihood ratio integrates to one under the zero-contrast sign-count law. This uses the Poisson intensity is nonnegative. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The two independent Poisson sign counts at contrast theta.
Definition (Lean source)
On the contrast interval, the exact sign-count experiment has the paper's likelihood ratio with respect to the zero-contrast law. This uses the Poisson intensity is nonnegative, and the target or contrast satisfies the stated unit-range restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The likelihood family after scaling the Cai--Low support to the dense amplitude.
Definition (Lean source)
The scaled one-cell hard experiment has the likelihood density required by the support-localized moment-matching theorem. This uses the sample size and alphabet lie in the dense regime, and the argument satisfies the stated support or positivity restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The scaled dense likelihood remains jointly measurable. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The scaled likelihood is nonnegative on the Cai--Low support. This uses the sample size and alphabet lie in the dense regime, and the argument satisfies the stated support or positivity restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
On the prior support, the scaled likelihood has the exponential Gram kernel with interaction parameter lambda * amplitude². This uses the sample size and alphabet lie in the dense regime, and the stated t condition holds, and the stated t' condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
the dense observed law has the four stated symmetric atom masses in every cell.
Formal statement
Proof (Lean source)
The zero contrast is the common reference point of the dense experiment.
Definition (Lean source)
Relative to the zero-contrast law, one observed atom contributes the positive or negative likelihood factor according as treatment and outcome agree or disagree. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
If the overlap parameter satisfies its stated range restriction, then the dense law is an overlapping observed model with uniform cell masses, propensity one half, shifted outcome means, and the stated optimal value.
Formal statement
Proof (Lean source)
Every contrast in the scaled dense cube gives the required observed hard-submodel law. This uses the dense construction domain conditions hold, and the target or contrast satisfies the stated unit-range restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Cai--Low supplies the exact supported, symmetric moment-matched pair at the chosen dense degree. This uses the Cai--Low moment-matching prior result is available, and the alphabet size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Cai--Low's positive-even-degree prior pairs assemble into the family used by the dense construction.
Definition (Lean source)
Scaling a supported probability product prior into the dense contrast cube produces a probability measure. This uses the dense construction domain conditions hold, and the prior is supported on the unit interval. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The dense target is measurable on the finite contrast cube. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Under either supported coordinate prior, the dense target has the required 1 / d variance gain from the independent product coordinates. This uses the dense construction domain conditions hold, and the prior is supported on the unit interval. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Chebyshev turns the product-prior variance bound into the one-eighth concentration clause used by the standard fuzzy-hypothesis theorem. This uses the dense construction domain conditions hold, and the prior is supported on the unit interval, and the stated e condition holds, and the stated scale inequality holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The cited reciprocal approximation lower bound makes the chosen error strictly positive. This uses the Cai--Low moment-matching prior result is available, and the alphabet size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The paper's likelihood tail is exactly the tail used by the generic moment-matched-mixture substrate. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
In the dense regime the exponential-tail argument is the chosen degree divided by sixty-four. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
A probability prior whose complement of [-1,1] is null has unit mass on the support set, in the form expected by the mixture substrate. This uses the prior is supported on the unit interval. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
A globally probability-valued version of the scaled sign-count experiment. Outside the prior support it falls back to the zero-contrast baseline; on the support it is exactly the scaled Poisson sign-count law.
Definition (Lean source)
The promoted support-localized mixture theorem gives the paper's product sign-count total-variation bound directly from the Cai--Low prior conditions. This uses the sample size and alphabet lie in the dense regime, and the two priors satisfy the moment-matching certificate. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The deterministic construction part of the dense certificate follows from the degree, amplitude, observed-law, and one-cell likelihood identities. This uses the dense construction domain conditions hold, and the sample size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.DenseNumerics 3 declarations Numerical exponential-tail estimates for the dense moment-matching lower bound.
Numerical exponential-tail estimates for the dense moment-matching lower bound.
The factorial tail at the calibrated dense intensity is dominated by the geometric series with ratio exp(1) / 64 used in the paper. This uses the sample size and alphabet lie in the dense regime. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The geometric likelihood-tail envelope is uniformly small after a universal alphabet cutoff. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
In the dense regime the mean-2n Poisson lower tail is eventually absorbed by any fixed positive multiple of the target dense rate. This uses the stated c condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.DenseObservationRegrouping 7 declarations Measure-theoretic tools for regrouping the dense Poisson observation experiment.
Measure-theoretic tools for regrouping the dense Poisson observation experiment.
The baseline conditional law given the dense sign statistic reconstructs every member of the dense Poisson family from its sign-count pushforward. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
On the Cai--Low support, the totalized supported sign kernel is the scaled one-cell Poisson sign law. This uses the sample size and alphabet lie in the dense regime, and the argument satisfies the stated support or positivity restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The supported sign kernel is probability-valued both on and off the Cai--Low support. This uses the sample size and alphabet lie in the dense regime. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Pushing the genuine dense observation mixture through its sufficient sign statistic gives exactly the supported product prior-predictive law. This uses the sample size and alphabet lie in the dense regime, and the dense construction domain conditions hold, and the prior is supported on the unit interval. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The same baseline conditional kernel reconstructs the full observation mixture from the supported product sign-count predictive law. This uses the sample size and alphabet lie in the dense regime, and the dense construction domain conditions hold, and the prior is supported on the unit interval. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Passing two probability laws through the same Markov kernel cannot increase their total-variation distance. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Dense full-observation prior mixtures are no farther apart than their product sign-count prior predictives. This uses the sample size and alphabet lie in the dense regime, and the dense construction domain conditions hold, and the first prior is supported on the unit interval, and the second prior is supported on the unit interval. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.DenseObservationStatisticLaw 9 declarations
For the specified data point or sample, the dense sign cell records the alphabet cell and whether treatment and outcome agree.
the stated measurable dense sign cell relation holds.
Formal statement
Proof (Lean source)
If the alphabet size satisfies its stated restriction, then under the zero contrast, every dense sign cell has mass .
Formal statement
Proof (Lean source)
For the specified count table, the regrouped dense counts pair the two sign-category counts within each alphabet cell.
Definition (Lean source)
the stated measurable dense regroup counts relation holds.
Formal statement
Proof (Lean source)
the dense sign statistic equals the regrouped observation histogram.
Formal statement
Proof (Lean source)
the stated map dense regroup counts product poisson relation holds.
Formal statement
Proof (Lean source)
If the alphabet size satisfies its stated restriction, then the stated map dense sign statistic baseline relation holds.
Formal statement
Proof (Lean source)
the stated map dense sign statistic dense law relation holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.DenseObservationSufficiency 14 declarations
each dense observed atom has mass when treatment and outcome agree and otherwise.
Formal statement
Proof (Lean source)
If the stated lam condition holds, then the stated finite poisson sample law singleton dense sufficiency relation holds.
Formal statement
Proof (Lean source)
each dense observed atom equals its zero-contrast mass times the corresponding one-observation likelihood factor.
Formal statement
Proof (Lean source)
For the specified contrast, smaller alphabet size, the dense sample likelihood is the product of the observation-level likelihood factors relative to the zero contrast.
Definition (Lean source)
each dense Poisson sample probability equals its zero-contrast probability times the dense sample likelihood.
Formal statement
Proof (Lean source)
For the specified smaller alphabet size, the dense sign statistic counts, in each cell, observations where treatment and outcome agree and disagree.
Definition (Lean source)
the stated measurable dense sign statistic relation holds.
Formal statement
Proof (Lean source)
the dense sample likelihood factors across alphabet cells into one-cell likelihoods.
Formal statement
Proof (Lean source)
the stated measurable dense sample likelihood enn relation holds.
Formal statement
Proof (Lean source)
the dense Poisson sample law is the zero-contrast law tilted by the dense sample likelihood.
Formal statement
Proof (Lean source)
If the stated stat condition holds, and the stated g condition holds, then the stated map with density composition singleton relation holds.
Formal statement
Proof (Lean source)
If the stated stat condition holds, and the stated g condition holds, and the stated g condition holds, and the stated support condition holds, and the stated base condition holds, then at every supported statistic value with positive baseline mass, tilting by a statistic-measurable density leaves the conditional distribution unchanged.
Formal statement
Proof (Lean source)
almost every point has nonzero singleton mass.
Formal statement
Proof (Lean source)
If the stated stat condition holds, and the stated g condition holds, and the stated g condition holds, then the baseline conditional kernel, mixed against the tilted statistic law, reconstructs the tilted distribution.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.DensePriorConcentration 1 declarations Pairwise assembly of the dense priors' variance and concentration bounds.
Pairwise assembly of the dense priors' variance and concentration bounds.
Both members of a Cai--Low prior pair satisfy the variance and one-eighth target-concentration clauses needed by the dense fuzzy-hypothesis argument. This uses the dense construction domain conditions hold, and the two priors satisfy the moment-matching certificate, and the stated scale inequality holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.DensePriorSetup 1 declarations Assembly of the supported Cai--Low product priors used by the dense lower bound.
Assembly of the supported Cai--Low product priors used by the dense lower bound.
In the dense regime, the cited Cai--Low pair gives supported product priors with the required separation, sign-count mixture bound, variance, and target concentration. This uses the sample size and alphabet lie in the dense regime, and the overlap parameter satisfies its stated range restriction, and the Cai--Low moment-matching prior result is available, and the stated scale inequality holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.EmpiricalRatioRisk 26 declarations The bounded-alphabet empirical-ratio branch of the upper bound.
The bounded-alphabet empirical-ratio branch of the upper bound.
For the specified observed datum, the observed binary mark is one for a successful outcome and zero otherwise.
Definition (Lean source)
under the observed-data law, a category has probability equal to its cell mass.
Formal statement
Proof (Lean source)
under the observed-data law, an arm-and-cell category has probability equal to its arm mass.
Formal statement
Proof (Lean source)
the stated category count identity sample cell count relation holds.
Formal statement
Proof (Lean source)
the stated category arm count identity sample arm count relation holds.
Formal statement
Proof (Lean source)
the stated arm mark sum identity sample success count relation holds.
Formal statement
Proof (Lean source)
the stated totalized arm mean identity sample ratio relation holds.
Formal statement
Proof (Lean source)
the stated fixed stratum arm score singleton identity relation holds.
Formal statement
Proof (Lean source)
the stated integral observed binary mark arm category relation holds.
Formal statement
Proof (Lean source)
the stated outcome mean mem unit interval empirical relation holds.
Formal statement
Proof (Lean source)
the stated integral observed binary residual identity zero relation holds.
Formal statement
Proof (Lean source)
the stated observed arm residual mem lp two relation holds.
Formal statement
Proof (Lean source)
the stated integral observed binary residual squared upper bound relation holds.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, and the stated x condition holds, then the stated observed overlap arm mass lower relation holds.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, then the stated fixed stratum arm target singleton identity relation holds.
Formal statement
Proof (Lean source)
If the stated u condition holds, and the stated p condition holds, then the stated nonnegativity product exp neg upper bound reciprocal relation holds.
Formal statement
Proof (Lean source)
If the sample size satisfies its stated restriction, and the overlap parameter satisfies its stated range restriction, then the stated missing arm envelope singleton upper bound relation holds.
Formal statement
Proof (Lean source)
every cell mass is at most one.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, and the sample size satisfies its stated restriction, then the stated fixed stratum arm score singleton mse upper bound relation holds.
Formal statement
Proof (Lean source)
the empirical-ratio estimator equals the sum across strata of the larger empirical arm score.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, then the stated observed optimal value identity max arm targets relation holds.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, then the squared empirical-ratio error is bounded by twice the sum of the two arm-score errors.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, and the sample size satisfies its stated restriction, then the empirical-ratio estimator has the stated uniform squared-risk upper bound.
Formal statement
Proof (Lean source)
the stated sample success count upper bound sample arm count relation holds.
Formal statement
Proof (Lean source)
sample cell counts sum to the total sample size.
Formal statement
Proof (Lean source)
If the sample size satisfies its stated restriction, then the stated empirical ratio estimator mem unit interval relation holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.Estimator 18 declarations Empirical-ratio fallback and the all-data Jackson--factorial estimator.
Empirical-ratio fallback and the all-data Jackson--factorial estimator.
For the specified observed sample, cell, the sample cell count is the number of observations in the specified alphabet cell.
For the specified observed sample, cell, treatment arm, the sample arm count is the number of observations in the specified cell and treatment arm.
For the specified observed sample, cell, treatment arm, the sample success count is the number of successful observations in the specified cell and treatment arm.
For the specified observed sample, the empirical-ratio estimator sums empirical cell shares times the larger of the two totalized within-arm success ratios.
Definition (Lean source)
The named universal tuning constants whose admissible values are chosen by the risk theorem.
Definition (Lean source)
For the specified tuning rule, alphabet size, the Jackson degree is the larger of two and the integer part of the tuning constant times the logarithmic alphabet size.
Definition (Lean source)
the stated jackson degree lower bound two relation holds.
Formal statement
Proof (Lean source)
Count one observed four-cell coordinate among the first M units carrying a given fair mark.
Definition (Lean source)
Coordinatewise pilot center c_j = N'_j/m.
Coordinatewise pilot radius h_j from the frozen estimator definition.
Definition (Lean source)
Pilot-local rectangle constructed from the marked pilot counts.
Definition (Lean source)
If the Poisson intensity is positive, then the stated pilot rectangle valid relation holds.
Formal statement
Proof (Lean source)
the stated pilot rectangle nonnegativity relation holds.
Formal statement
Proof (Lean source)
In the paper's nontrivial alphabet regime, every pilot rectangle has a strictly positive radius, including coordinates whose pilot count is zero. This uses the Poisson intensity is positive, and the alphabet size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The clipped pilot-local cell statistic built from the Jackson polynomial and its factorial lift.
Definition (Lean source)
The fair product law of the Bernoulli marks.
Randomized projected statistic before Rao--Blackwellization.
Definition (Lean source)
For the specified tuning rule, overlap level, observed sample, the Jackson factorial estimator uses the empirical ratio for small alphabets, one half in the saturated regime, and otherwise averages the randomized Jackson statistic over Poisson truncation and fair marks.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.FactorialLift 14 declarations Centered falling-factorial lifts for Poisson counts.
Centered falling-factorial lifts for Poisson counts.
Linearization of a product of two falling-factorial basis polynomials, classified by the size of the overlap between the two ordered selections. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Exact overlap expansion for the product of two descending factorials. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Falling factorial (N)_t.
Definition (Lean source)
The paper's product definition of a falling factorial agrees with Mathlib's descending factorial. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Shifting a Poisson falling-factorial summand by its order cancels the factorial denominator. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Every falling factorial is summable against a Poisson mass function. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The order-t falling factorial of a Poisson count has expectation equal to the t-th power of its mean. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Every falling factorial of a Poisson count is integrable. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
A product of two falling factorials is integrable under every Poisson law. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The joint Poisson moment of two falling factorials is the exact finite overlap expansion. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Centered factorial lift of a monomial.
Definition (Lean source)
A centered factorial lift is unbiased for the corresponding centered power under a Poisson count with mean m*q. This uses the Poisson intensity is positive, and the cell masses satisfy their stated restrictions. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Two centered factorial lifts have an integrable product under every Poisson law. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Expanding both lifts and classifying the overlap gives the raw finite-sum form of their joint Poisson moment. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.FactorialProductRisk 8 declarations Product-Poisson L² control for normalized centered-factorial monomials.
Product-Poisson L² control for normalized centered-factorial monomials.
A pointwise normalized-coordinate expansion identifies the actual centered polynomial used by the factorial lift. This uses the stated r condition holds, and the stated exp condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The coefficient envelope in a normalized pointwise expansion bounds the coefficient ℓ1 norm of the centered polynomial actually lifted by the estimator. This uses the stated r condition holds, and the stated exp condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The chosen Jackson polynomial has the explicit normalized coefficient envelope needed by the factorial-risk calculation. This uses the overlap parameter satisfies its stated range restriction, and the approximation degree satisfies its stated restriction, and the potential-outcome law satisfies the stated causal restrictions, and the stated q0 condition holds, and the stated qr condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The tensor monomial obtained by multiplying normalized centered-factorial coordinates with the exponents in alpha.
Definition (Lean source)
Every normalized centered-factorial tensor monomial is square-integrable under a product of scalar Poisson laws when all normalization radii are nonzero. This uses the stated r condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Coordinatewise Poisson noise-to-radius bounds tensorize: the normalized monomial's second moment is bounded by the exponential of the sum of squared coordinate degrees. This uses the Poisson intensity is positive, and the cell masses satisfy their stated restrictions, and the stated r condition holds, and the centering parameters satisfy the stated bounds, and the intensity-to-center ratio satisfies the stated bound. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
If every coordinate degree is at most K, the four-coordinate tensor monomial has the uniform exponential second-moment bound used by the Jackson coefficient envelope. This uses the Poisson intensity is positive, and the cell masses satisfy their stated restrictions, and the stated r condition holds, and the centering parameters satisfy the stated bounds, and the intensity-to-center ratio satisfies the stated bound, and the exponential-moment parameter is below one, and the multi-index degree satisfies the stated bound. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
A centered polynomial lift inherits a product-Poisson L² bound from its normalized coefficient ℓ1 norm and a common coordinate-degree bound. This uses the Poisson intensity is positive, and the cell masses satisfy their stated restrictions, and the stated r condition holds, and the centering parameters satisfy the stated bounds, and the intensity-to-center ratio satisfies the stated bound, and the exponential-moment parameter is below one, and the multi-index degree satisfies the stated bound. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.FactorialRisk 11 declarations Generic risk bounds and exact moments for centered factorial polynomials.
Generic risk bounds and exact moments for centered factorial polynomials.
Translate a polynomial to normalized coordinates around a center and subtract its value at that center.
Definition (Lean source)
Centered factorial lift of every monomial of a normalized polynomial.
Definition (Lean source)
Under independent Poisson coordinates, the centered factorial lift is unbiased for the original polynomial minus the declared center value. This uses the Poisson intensity is positive, and the cell masses satisfy their stated restrictions, and the stated r condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The binomial-overlap sum occurring in a centered factorial second moment is bounded by its exponential generating function. This uses the exponential-moment parameter is below one. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Clip a real number to the interval of radius t around c.
Clipping around a center cannot increase distance from that center. This uses the argument satisfies the stated support or positivity restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Clipping to the interval centered at c with nonnegative radius t stays within distance t of its center. This uses the argument satisfies the stated support or positivity restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The clipping displacement is controlled by squared distance divided by the radius. This uses the argument satisfies the stated support or positivity restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
A finite linear combination whose summands have a common L² bound is controlled by the coefficient ℓ₁ norm. This uses the stated r condition holds, and the stated x condition holds, and the stated x2 condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
If the Poisson intensity is positive, and the cell masses satisfy their stated restrictions, then the stated integral centered factorial product poisson relation holds.
Formal statement
Proof (Lean source)
If the true mean lies within radius r of the centering point and the Poisson noise-to-radius ratio is at most rho, the normalized centered factorial monomial has the exponential L² bound used by the Jackson lift. This uses the Poisson intensity is positive, and the cell masses satisfy their stated restrictions, and the stated r condition holds, and the stated z condition holds, and the intensity-to-center ratio satisfies the stated bound. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.FinitePoissonHistogram 4 declarations Exact histogram law for an unmarked finite Poisson sample.
Exact histogram law for an unmarked finite Poisson sample.
Counts the observations assigned to each cell by a finite classifier.
Definition (Lean source)
If the stated cell condition holds, then the stated measurable finite poisson histogram relation holds.
Formal statement
Proof (Lean source)
Mapping every point of a finite Poisson sample maps its base law. This uses the target function is continuous. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
A measurable finite classifier turns a Poisson sample into independent Poisson cell counts with the corresponding thinned means. This uses the stated cell condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.GlobalLipschitz 12 declarations
For the specified first cell vector, second cell vector, the cellwise L1 distance is the sum of absolute coordinate differences across the four cells.
Definition (Lean source)
If the overlap parameter satisfies its stated range restriction, and the stated u condition holds, then the stated arm cell value bounds relation holds.
Formal statement
Proof (Lean source)
If the overlap parameter satisfies its stated range restriction, and the stated u condition holds, then the stated global cell value bounds relation holds.
Formal statement
Proof (Lean source)
If the target function is continuous, and the stated z condition holds, and the stated f' condition holds, and the stated z' condition holds, and the argument satisfies the stated support or positivity restriction, and the stated t' condition holds, then the stated unit ratio diff bound relation holds.
Formal statement
Proof (Lean source)
For the specified overlap level, first failure mass, data point or sample, third cell mass, smaller alphabet size, the scalar arm value is zero at zero total mass and otherwise equals total mass times the success-cell mass divided by the larger of arm mass and overlap-truncated total mass.
Definition (Lean source)
If the overlap parameter satisfies its stated range restriction, and the stated s condition holds, and the stated low condition holds, then the stated scalar arm value of low relation holds.
Formal statement
Proof (Lean source)
If the stated s condition holds, and the stated high condition holds, then the stated scalar arm value of high relation holds.
Formal statement
Proof (Lean source)
If the overlap parameter satisfies its stated range restriction, and the target function is continuous, and the stated z condition holds, and the stated r condition holds, and the stated support condition holds, and the stated f' condition holds, and the stated z' condition holds, and the stated r' condition holds, and the stated s' condition holds, and the stated s condition holds, and the stated s' condition holds, then the stated scalar arm value lipschitz of pos relation holds.
Formal statement
Proof (Lean source)
If the stated u condition holds, and the stated mass condition holds, then a nonnegative cell vector with zero total mass vanishes in every coordinate.
Formal statement
Proof (Lean source)
If the stated u condition holds, and the stated v condition holds, then the stated l1 cell distance zero left relation holds.
Formal statement
Proof (Lean source)
If the overlap parameter satisfies its stated range restriction, and the stated u condition holds, and the stated v condition holds, then arm value is Lipschitz in cellwise L1 distance with constant .
Formal statement
Proof (Lean source)
If the overlap parameter satisfies its stated range restriction, and the stated u condition holds, and the stated v condition holds, then global cell value is Lipschitz in cellwise L1 distance with constant .
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.JacksonCertificate 6 declarations Simultaneous pointwise and coefficient control for the tensor Jackson approximant.
Simultaneous pointwise and coefficient control for the tensor Jackson approximant.
For the specified rectangle or law, second cell vector, the rectangle-membership condition requires every cell coordinate to lie between its lower and upper endpoints. In each cell, the coordinate is at least the lower endpoint and at most the upper endpoint.
For the specified rectangle or law, degree, second cell vector, the Jackson pointwise scale sums the local square-root boundary widths and second-order rectangle radii across the four cells.
Definition (Lean source)
A tensor Jackson convolution inherits a coordinatewise first/second-order modulus. This uses the approximation degree satisfies its stated restriction, and the Lipschitz scale is positive, and the target function is continuous, and the linear weights are nonnegative, and the quadratic weights are nonnegative, and the target function obeys the stated weighted increment bound. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
A cosine shift has the first/second-order bound used at rectangle faces. The displayed identity or bound is the asserted conclusion.
Proof (Lean source)
A finite centered, radius-scaled monomial expansion of a physical polynomial.
Definition (Lean source)
one universal exponential coefficient constant yields, for every overlap level, simultaneous degree, approximation, and centered-coefficient bounds for the Jackson polynomial.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.JacksonKernel 11 declarations The order-four Jackson kernel and its tensor-convolution representation.
The order-four Jackson kernel and its tensor-convolution representation.
A pilot rectangle represented by lower and upper endpoints.
The endpoint condition required of a genuine rectangle.
Definition (Lean source)
For the specified rectangle or law, cell index, the rectangle center is the midpoint of the lower and upper endpoint in the selected cell.
For the specified rectangle or law, cell index, the rectangle radius is half the difference between the upper and lower endpoint in the selected cell.
The canonical enumeration of the four treatment--outcome coordinates.
The cell functional, reindexed on the four-coordinate type used by the Jackson substrate.
Definition (Lean source)
The affine tensor Jackson convolution after enumerating the four cell coordinates.
Definition (Lean source)
One polynomial together with the normalized-coordinate representative used for its coefficient envelope.
Definition (Lean source)
If the approximation degree satisfies its stated restriction, and the stated q0 condition holds, and the overlap parameter satisfies its stated range restriction, and the stated qr condition holds, then the stated jackson tensor polynomial data exists relation holds.
Formal statement
Proof (Lean source)
On a rectangle with at least one zero-radius coordinate, the tensor convolution still has a physical-coordinate polynomial representative. Zero-radius coordinates are frozen at their singleton endpoint rather than causing the whole polynomial to vanish. This uses the approximation degree satisfies its stated restriction, and the potential-outcome law satisfies the stated causal restrictions, and the stated q0 condition holds, and the overlap parameter satisfies its stated range restriction, and the stated deg condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The physical-coordinate polynomial induced by the four-dimensional Jackson convolution.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.L1Depoissonization 5 declarations This file specializes the reusable paired-histogram Rao--Blackwell theorem to the two simplex laws used by the paper.
Fixed/Poisson transfer for the paired L1 experiment
This file specializes the reusable paired-histogram Rao--Blackwell theorem to the two simplex laws used by the paper.
the L1 distance between two probability vectors lies between zero and two.
Formal statement
Proof (Lean source)
the family of fixed-sample L1 risks is bounded above.
Formal statement
Proof (Lean source)
the risk of the paired-histogram estimator in the Poisson experiment is no greater than its fixed-sample counterpart plus the stated tail.
Formal statement
Proof (Lean source)
fixed-sample L1 minimax risk is at least the Poissonized risk minus the stated exponential tail.
Formal statement
Proof (Lean source)
If the Jiao--Han--Weissman Poisson L1 lower bound is available, and the stated c0 condition holds, and the stated c0 condition holds, then the stated jhw fixed l1 lower sub exp tail relation holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.L1Embedding 20 declarations Equal-propensity embedding of the normalized two-sample L1 experiment.
Equal-propensity embedding of the normalized two-sample L1 experiment.
For the specified alphabet size, the probability simplex consists of nonnegative weights on the alphabet that sum to one.
Definition (Lean source)
For the specified success probability, binary value, the Bernoulli mass assigns probability p to success and one minus p to failure.
Definition (Lean source)
For the specified first probability vector, second probability vector, data point or sample, the L1 embedding full-data mass is the consistency-compatible product mass formed from the two simplex weights and their normalized outcome means, and is zero off the consistency event.
Definition (Lean source)
the L1 embedding masses are nonnegative and sum to one.
Formal statement
Proof (Lean source)
For the specified first probability vector, second probability vector, the L1 embedding is the potential-outcome law induced by the embedding full-data masses.
Definition (Lean source)
The explicit embedding has the four required atom identities, fair propensity, armwise exchangeability, and consistency. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
For the specified first probability vector, second probability vector, the L1 distance is the sum of absolute differences between the two probability vectors.
Definition (Lean source)
the simplex weights, viewed as extended nonnegative reals, sum to one.
Formal statement
Proof (Lean source)
For the specified discrete law, the simplex probability mass function assigns each alphabet point its simplex weight.
Definition (Lean source)
A single paired draw is randomized into one of the four displayed observed atoms.
Definition (Lean source)
The explicit fixed-n product Markov kernel used in the reduction.
Definition (Lean source)
For the specified sample size, pair of probability vectors, the fixed paired-sample law is the product law of independent draws from the two categorical distributions at every sample index.
Definition (Lean source)
For the specified sample size, alphabet size, the fixed-sample L1 estimator is a measurable real-valued statistic of paired categorical samples.
Definition (Lean source)
For the specified sample size, estimator, pair of probability vectors, the fixed-sample L1 risk is squared-error risk for estimating the L1 distance between two categorical distributions.
Definition (Lean source)
For the specified sample size, alphabet size, the fixed-sample L1 minimax risk is the minimax squared-error risk for the paired categorical experiment.
Definition (Lean source)
Two independent vectors of Poisson counts with means 2n P_x and 2n Q_x.
Definition (Lean source)
For the specified alphabet size, the Poissonized L1 estimator is a measurable real-valued statistic of two categorical histograms.
Definition (Lean source)
For the specified sample size, estimator, pair of probability vectors, the Poissonized L1 risk is squared-error risk for estimating L1 distance from the paired Poisson histograms.
Definition (Lean source)
Measurable Poisson-histogram estimators whose squared loss is integrable at every pair of simplex laws and whose worst-case risk is finite. This scopes ordinary real-valued Bochner risk to the finite-risk estimators represented by the cited minimax theorem.
Definition (Lean source)
The two-sample Poissonized L1 minimax risk over measurable estimators with finite worst-case risk. The finite-risk scope prevents both the Bochner integral and the real supremum from taking junk values.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.LowerSplice 6 declarations Numerical and statistical assembly for the lower-bound regime splice.
Numerical and statistical assembly for the lower-bound regime splice.
If the alphabet size satisfies its stated restriction, then the logarithmic alphabet size is positive.
Formal statement
Proof (Lean source)
If the alphabet size satisfies its stated restriction, then the logarithmic alphabet size is at least one.
Formal statement
Proof (Lean source)
for all sufficiently large alphabets, is at most .
Formal statement
Proof (Lean source)
If the stated c condition holds, then beyond a finite sample-size cutoff, the paired Poisson tail is absorbed by the stated constant bounds.
Formal statement
Proof (Lean source)
For the specified sample size, the saturated alphabet size is the ceiling of sample size times its logarithmic scale.
If the sample size satisfies its stated restriction, and the alphabet size satisfies its stated restriction, and the stated sat condition holds, then the saturated alphabet is at least two, fits inside the original alphabet, meets the L1 lower-bound gate, and has the stated logarithmic ratio bounds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.PilotControl 30 declarations Moment, bias, and variance control for the pilot-local factorial construction.
Moment, bias, and variance control for the pilot-local factorial construction.
A concrete universal tuning with the promoted self-normalized Poisson radius and a cutoff strictly above the smallest admissible alphabet.
Definition (Lean source)
the canonical bounded-alphabet cutoff is strictly greater than two.
Formal statement
Proof (Lean source)
Independent pilot and evaluation Poisson counts in all four coordinates.
Definition (Lean source)
A complete table of pilot and evaluation counts, before the fixed-sample cap is imposed.
The fair mark law used in the uncapped Poisson comparison experiment.
Definition (Lean source)
the fair uncapped mark law is a probability measure.
Definition (Lean source)
Read the total count and the pilot/evaluation cell-count tables from a marked finite sample.
Definition (Lean source)
The full marked count-table readout is measurable on the finite-sample space. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The uncapped experiment induced by M ~ Pois(n/4), i.i.d. observations, and fair marks.
Definition (Lean source)
The total coordinate of the uncapped marked experiment retains its original Poisson count law. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Independent pilot and evaluation count tables, each having mean scale m.
Definition (Lean source)
The table component of the uncapped marked experiment is the full product of independent pilot and evaluation Poisson count tables at scale n / 8. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Each cell projection of the full independent count table is exactly the four-coordinate pilot/evaluation product law used by the cell statistic. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Conditional expectation over evaluation counts after fixing the pilot table.
Definition (Lean source)
Conditional on any pilot table, a coordinatewise centered factorial lift has the centered-power expectation under the independent evaluation law. This uses the Poisson intensity is positive, and the cell masses satisfy their stated restrictions. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Conditional on any pilot table, the product of two centered factorial lifts has the raw finite overlap expansion inherited from its scalar Poisson coordinate. This is the pre-collapse form of the paper's second moment identity. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Conditional on the pilot table, the product of two centered factorial lifts has the collapsed overlap expansion from the paper. This uses the Poisson intensity is positive, and the cell masses satisfy their stated restrictions. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
For the specified tuning rule, overlap level, alphabet size, Poisson intensity, cell-mass vector, positive-intensity certificate, the cell-statistic expectation is the mean of the Jackson cell statistic under the pilot-evaluation law.
Definition (Lean source)
For the specified tuning rule, overlap level, alphabet size, Poisson intensity, cell-mass vector, positive-intensity certificate, the cell-statistic variance is the mean squared deviation of the Jackson cell statistic from its expectation under the pilot-evaluation law.
Definition (Lean source)
The estimator's nested maximum/minimum is exactly clipping around the pilot-center target at the declared random radius. This bridge lets the generic clipping-risk inequalities apply without unfolding the estimator. This uses the Poisson intensity is positive. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The paper's good-pilot event G_x = ⋂_j {|N'_{j,x}/m - q_{j,x}| ≤ h_{j,x}/4}. This is deliberately stronger than mere membership of q_x in the (radius-h) pilot rectangle.
Definition (Lean source)
On the coordinatewise good-pilot event, the true cell vector belongs to the random pilot rectangle. This includes zero coordinates because the lower endpoint is truncated at zero. This uses the cell masses satisfy their stated restrictions, and the pilot sample lies in the good event. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The radius of the zero-truncated pilot interval lies between one half and one times the untruncated radius. This uses the Poisson intensity is positive, and the alphabet size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
For the canonical tuning, the promoted normalized aggregate score is exactly the sum of the pilot deviations and the untruncated pilot radii. This uses the Poisson intensity is positive, and the cell masses satisfy their stated restrictions. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The center displacement and the sum of the actual (zero-truncated) rectangle radii are pointwise dominated by the promoted aggregate score. This uses the Poisson intensity is positive, and the alphabet size satisfies its stated restriction, and the cell masses satisfy their stated restrictions. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
For the canonical radius constant, failure of the paper's pilot event is exactly the promoted self-normalized Poisson bad event. This uses the Poisson intensity is positive, and the cell masses satisfy their stated restrictions. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The promoted four-coordinate Poisson theorem applies directly to a pilot array with independent coordinate laws. This uses the Poisson intensity is positive, and the argument satisfies the stated support or positivity restriction, and the Lipschitz scale is positive. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
On a good pilot, every coordinate's Poisson noise-to-radius ratio is at most the reciprocal logarithmic level required by the factorial L² bound. This uses the Poisson intensity is positive, and the alphabet size satisfies its stated restriction, and the pilot sample lies in the good event. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Pilot-failure contribution, restricted to the complement of the paper's coordinatewise good-pilot event.
Definition (Lean source)
Squared pilot-failure contribution, at the local second-moment scale.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.PilotControlIntegration 6 declarations Integrated good-pilot and pilot-failure bounds for the cellwise factorial risk.
Integrated good-pilot and pilot-failure bounds for the cellwise factorial risk.
Conditional on a good pilot, clipping and the product-factorial bound give the stated local second-moment scale. This uses the overlap parameter satisfies its stated range restriction, and the Poisson intensity is positive, and the alphabet size satisfies its stated restriction, and the cell masses satisfy their stated restrictions, and the pilot sample lies in the good event. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The normalized four-coordinate pilot score is square-integrable under the independent product-Poisson pilot law. This uses the Poisson intensity is positive, and the alphabet size satisfies its stated restriction, and the cell masses satisfy their stated restrictions. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Integrating the pointwise clipping bound on the bad-pilot event gives the promoted exponentially small local first- and second-moment contributions. This uses the overlap parameter satisfies its stated range restriction, and the Poisson intensity is positive, and the alphabet size satisfies its stated restriction, and the cell masses satisfy their stated restrictions. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The logarithmic factors left by approximation and bad-pilot integration are absorbed by the fixed fractional powers of the alphabet size. This uses the alphabet size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Two coarse logarithmic bounds used to absorb the squared localized pilot radius into fixed powers of the alphabet size. This uses the alphabet size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Cauchy--Schwarz over the four cell coordinates controls the sum of local square-root scales by twice the aggregate square-root scale. This uses the cell masses satisfy their stated restrictions, and the stated tau condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.PilotControlPointwise 8 declarations Final pilot-failure estimate and assembly of the cellwise factorial risk theorem.
Final pilot-failure estimate and assembly of the cellwise factorial risk theorem.
The clipped cell estimator's pointwise error is controlled by the promoted self-normalized aggregate pilot score, uniformly in the evaluation counts. This uses the overlap parameter satisfies its stated range restriction, and the Poisson intensity is positive, and the alphabet size satisfies its stated restriction, and the cell masses satisfy their stated restrictions. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The first-moment pilot-failure integrand is bounded pointwise by the promoted bad-event aggregate score. This uses the overlap parameter satisfies its stated range restriction, and the Poisson intensity is positive, and the alphabet size satisfies its stated restriction, and the cell masses satisfy their stated restrictions. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The squared pilot-failure integrand is bounded pointwise by the square of the promoted bad-event aggregate score. This uses the overlap parameter satisfies its stated range restriction, and the Poisson intensity is positive, and the alphabet size satisfies its stated restriction, and the cell masses satisfy their stated restrictions. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The deliberately small canonical Jackson constant still gives a degree large enough, up to a universal factor, to absorb one logarithmic level. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
On a good pilot, the sum of the four random rectangle radii has the local square-root-plus-linear scale, uniformly down to zero cell masses. This uses the Poisson intensity is positive, and the alphabet size satisfies its stated restriction, and the cell masses satisfy their stated restrictions, and the pilot sample lies in the good event. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The chosen degree constant makes the squared coefficient envelope and factorial-moment exponential fit strictly inside the stated d^(1/16) loss. This uses the alphabet size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
On a good pilot, the centered factorial lift of the chosen Jackson polynomial has the required local product-Poisson second moment. This uses the overlap parameter satisfies its stated range restriction, and the Poisson intensity is positive, and the alphabet size satisfies its stated restriction, and the cell masses satisfy their stated restrictions, and the pilot sample lies in the good event. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Conditional on a good pilot, Jackson approximation plus clipping gives the local bias bound before averaging over the pilot. This uses the overlap parameter satisfies its stated range restriction, and the Poisson intensity is positive, and the alphabet size satisfies its stated restriction, and the cell masses satisfy their stated restrictions, and the stated cj condition holds, and the polynomial has the stated approximation guarantee, and the pilot sample lies in the good event. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.PilotControlTheorem 1 declarations Final assembly of the cellwise factorial risk theorem.
Final assembly of the cellwise factorial risk theorem.
If the product experiment has the stated independent-sampling law, then the canonical Jackson tuning simultaneously provides the stated pilot/evaluation laws, factorial moment identities, and uniform bias, variance, and pilot-failure bounds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.PilotExperimentCore 1 declarations Exact marked-Poisson laws and conditional factorial moments used by pilot control.
Exact marked-Poisson laws and conditional factorial moments used by pilot control.
The uncapped marked experiment has the required Poisson total, joint cell-product law, and coordinatewise conditional factorial-moment identities. This uses the sample size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.PilotLocalizedScale 1 declarations Localized geometry of the canonical pilot rectangle.
Localized geometry of the canonical pilot rectangle.
On a good pilot, the Jackson endpoint weight vanishes at a null coordinate and otherwise has the local square-root scale. This uses the Poisson intensity is positive, and the alphabet size satisfies its stated restriction, and the cell masses satisfy their stated restrictions, and the pilot sample lies in the good event. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.RegularLower 9 declarations A regular parametric submodel for the bounded-alphabet lower bound.
A regular parametric submodel for the bounded-alphabet lower bound.
For the specified validity certificate, the regular null law is the discrete observed law generated by the valid null parametric data-generating process.
For the specified validity certificate, the regular perturbed law is the discrete observed law generated by the valid perturbed parametric data-generating process.
If the stated v condition holds, then the stated regular null law joint mass relation holds.
Formal statement
Proof (Lean source)
If the stated v condition holds, then the stated regular perturbed law joint mass relation holds.
Formal statement
Proof (Lean source)
If the alphabet size satisfies its stated restriction, and the overlap parameter satisfies its stated range restriction, and the stated v condition holds, then the stated regular null law model relation holds.
Formal statement
Proof (Lean source)
If the alphabet size satisfies its stated restriction, and the overlap parameter satisfies its stated range restriction, and the stated v condition holds, then the stated regular perturbed law model relation holds.
Formal statement
Proof (Lean source)
If the stated v condition holds, and the observed law satisfies the stated model restrictions, then the stated regular null law value relation holds.
Formal statement
Proof (Lean source)
If the stated delta condition holds, and the stated v condition holds, and the observed law satisfies the stated model restrictions, then the stated regular perturbed law value relation holds.
Formal statement
Proof (Lean source)
If the overlap parameter satisfies its stated range restriction, and the sample size satisfies its stated restriction, and the alphabet size satisfies its stated restriction, then every admissible model has minimax risk at least .
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.TwoPointLower 1 declarations A reusable two-model testing lower bound for the observed minimax problem.
A reusable two-model testing lower bound for the observed minimax problem.
Two observed models separated by 2s in target value and at total variation at most one half force minimax squared risk at least s²/4. This uses the stated support condition holds, and the two target values have the stated separation, and the two experiments have the stated total-variation bound. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.UpperRiskAggregation 9 declarations
If the alphabet size satisfies its stated restriction, and the stated c condition holds, and the Poisson intensity is positive, and the Lipschitz scale is positive, and the stated p condition holds, and the stated sump condition holds, and the quadratic weights are nonnegative, then the stated sum cell bias squared upper bound relation holds.
Formal statement
Proof (Lean source)
If the overlap parameter satisfies its stated range restriction, and the Poisson intensity is positive, and the alphabet size satisfies its stated restriction, and the cell masses satisfy their stated restrictions, then the stated canonical jackson cell statistic mem lp two relation holds.
Formal statement
Proof (Lean source)
If the stated t condition holds, then the stated sum independent cell risk upper bound relation holds.
Formal statement
Proof (Lean source)
Regrouping the independent pilot and evaluation tables by cells gives a product of the cellwise pilot--evaluation laws. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The uncapped statistic's risk is the squared-error integral of the cellwise sum under the independent product of cell laws. This uses the sample size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Projection onto the unit interval does not increase squared loss from a target in that interval. This uses the target or contrast satisfies the stated unit-range restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Cellwise bias and variance bounds aggregate under Poisson splitting into the projected uncapped risk bound. This uses the sample size satisfies its stated restriction, and the alphabet size satisfies its stated restriction, and the overlap parameter satisfies its stated range restriction, and the stated c condition holds, and the target or contrast satisfies the stated unit-range restriction, and the target lies in the unit interval, and the stated cellwise bias bound holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The two logarithmic variance factors are uniformly absorbed by the fractional alphabet power left by the factorial coefficient envelope. This uses the alphabet size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
In the nontrivial Jackson regime, the summed cell bounds yield the target d /(n log(ed)) risk rate. This uses the sample size satisfies its stated restriction, and the alphabet size satisfies its stated restriction, and the overlap parameter satisfies its stated range restriction, and the stated c condition holds, and the target or contrast satisfies the stated unit-range restriction, and the target lies in the unit interval, and the stated scale inequality holds, and the stated cellwise bias bound holds, and the stated cellwise variance bound holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.Helpers.UpperRiskCoupling 19 declarations The marked finite-Poisson statistic and its capped fixed-sample Rao--Blackwell coupling.
The marked finite-Poisson statistic and its capped fixed-sample Rao--Blackwell coupling.
The projected Jackson cell sum on an uncapped marked finite sample.
Definition (Lean source)
The uncapped projected statistic is measurable. This uses the sample size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Projection places the uncapped statistic in the unit interval. This uses the sample size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Extending a prefix indicator by zero preserves its finite sum. This uses the stated m condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The uncapped count table of a fixed-array prefix is exactly the table used by the randomized estimator. This uses the stated m condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
On nonoverflow, the generic prefix statistic is the paper's randomized statistic. This uses the sample size satisfies its stated restriction, and the stated m condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The inner Poisson average in the estimator is the generic capped Rao--Blackwell statistic associated with the uncapped marked statistic. This uses the sample size satisfies its stated restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The capped randomized statistic always belongs to the unit interval. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
In its Jackson regime, the explicit estimator is the fair-mark average of the generic capped Rao--Blackwell statistic. This uses the sample size satisfies its stated restriction, and the alphabet exceeds the bounded-alphabet cutoff, and the stated scale inequality holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The fixed marked-sample risk is bounded by the uncapped finite-Poisson risk plus the exact overflow probability. This uses the sample size satisfies its stated restriction, and the target or contrast satisfies the stated unit-range restriction. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
The explicit uniform law on all mark arrays is the independent product of the one-coordinate fair mark laws. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Adjoin one independent fair Boolean mark to an observation.
Definition (Lean source)
The fair observation-marking kernel preserves total probability one.
Definition (Lean source)
Pointwise, adjoining a fair mark is the pushforward of the fair law by pairing. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Conditional on an observation array, the coordinatewise marking kernel is the pushforward of the explicit fair array law. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Averaging a statistic through the coordinatewise marking kernel is exactly integration over the paper's fair mark array. This uses the stated t condition holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Marking a single observation produces its product with the fair mark law. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
Coordinatewise fair marking of an iid observation array gives the iid law of independently marked observations. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
In the Jackson regime, outer Rao--Blackwellization over the fair marks cannot increase risk relative to the marked fixed-array statistic. This uses the sample size satisfies its stated restriction, and the alphabet exceeds the bounded-alphabet cutoff, and the stated scale inequality holds. The displayed identity or bound is the asserted conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.OpenQuestions 2 declarations Nonassertive carriers for the unresolved sharp-constant route and question.
Nonassertive carriers for the unresolved sharp-constant route and question.
For the specified overlap level, the sharp-constant handle is the three-step research program of local Poisson rescaling, sharp polynomial bias-variance optimization, and dual moment-matching.
Definition (Lean source)
For the specified overlap level, the sharp-overlap-constant question asks whether the normalized nonsaturated minimax risk converges to a positive finite limit and whether the sharp-constant program yields an attaining estimator.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.TAllEstimatorLower 1 declarations Conditional minimax lower bound over all measurable estimators.
Conditional minimax lower bound over all measurable estimators.
If the product experiment has the stated independent-sampling law, and the Cai--Low moment-matching prior result is available, and the Jiao--Han--Weissman Poisson L1 lower bound is available, then there is a positive constant, depending only on overlap, for which every estimator has risk at least that constant times the minimum of one and .
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.TCausalOptimalValueCorollary 8 declarations Causal interpretation of the observed optimal-regression value.
Causal interpretation of the observed optimal-regression value.
each observed-marginal atom equals the sum of compatible full-data atoms.
Formal statement
Proof (Lean source)
the cell mass of the observed marginal equals the corresponding covariate mass of the potential-outcome law.
Formal statement
Proof (Lean source)
under consistency, each observed atom equals the compatible selected potential-outcome atom.
Formal statement
Proof (Lean source)
the stated potential-outcome regression identity potential-outcome arm atom ratio relation holds.
Formal statement
Proof (Lean source)
under consistency, observed arm mass equals the total compatible potential-outcome arm mass.
Formal statement
Proof (Lean source)
summing the compatible potential-outcome arm atoms over arm and outcome gives cell mass.
Formal statement
Proof (Lean source)
If the stated cons condition holds, and the stated exch condition holds, and the stated cell condition holds, and the stated arm condition holds, then the stated potential-outcome regression identity outcome mean of pos relation holds.
Formal statement
Proof (Lean source)
If the potential-outcome law satisfies the stated causal restrictions, then the causal oracle value equals the optimal value identified from the observed marginal.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.TConsistencyParametricBoundaries 7 declarations Consistency and parametric-rate boundaries along arbitrary alphabet sequences.
Consistency and parametric-rate boundaries along arbitrary alphabet sequences.
For the specified risk sequence, the parametric-rate property says that the risk is eventually bounded above and below by positive constant multiples of one over sample size. There are constants such that the lower constant is positive, it does not exceed the upper constant, and the risk eventually lies between those constants divided by sample size.
Definition (Lean source)
For the specified alphabet-size sequence, the bounded-alphabet sequence is an alphabet-size sequence that remains uniformly bounded asymptotically.
Definition (Lean source)
If the alphabet size satisfies its stated restriction, then the phase scale converges to zero exactly when .
Formal statement
Proof (Lean source)
If the alphabet size satisfies its stated restriction, and the stated c condition holds, and the stated c condition holds, and the stated bounds condition holds, then a risk sequence satisfying the stated two-sided phase-scale bounds converges to zero exactly when the phase scale does.
Formal statement
Proof (Lean source)
If the alphabet size satisfies its stated restriction, and the stated c condition holds, and the stated lower condition holds, and the stated param condition holds, then a two-sided parametric risk bound forces the alphabet-size sequence to be uniformly bounded.
Formal statement
Proof (Lean source)
a bounded-alphabet sequence admits a single finite upper bound at every sample size.
Formal statement
Proof (Lean source)
If the Cai--Low moment-matching prior result is available, and the Jiao--Han--Weissman Poisson L1 lower bound is available, then observed and causal minimax risks are consistent exactly when , and attain the parametric rate exactly for uniformly bounded alphabets.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.TEqualPropensityL1Reduction 11 declarations Equal-propensity L1 identities and minimax transfer.
Equal-propensity L1 identities and minimax transfer.
the stated l1 source singleton relation holds.
Formal statement
Proof (Lean source)
the stated l1 kernel singleton relation holds.
Formal statement
Proof (Lean source)
the stated l1 kernel atoms relation holds.
Formal statement
Proof (Lean source)
the stated l1 kernel atom formula relation holds.
Formal statement
Proof (Lean source)
the stated l1 single kernel composition pair relation holds.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, then the stated observed optimal value mem unit interval relation holds.
Formal statement
Proof (Lean source)
every real-valued function on a finite set is uniformly bounded.
Formal statement
Proof (Lean source)
the family of observed squared-error risks is bounded above.
Formal statement
Proof (Lean source)
If the alphabet size satisfies its stated restriction, and the overlap parameter satisfies its stated range restriction, then the L1 embedding is an admissible equal-propensity observed model whose optimal value is one half plus one quarter of the L1 distance.
Formal statement
Proof (Lean source)
If the alphabet size satisfies its stated restriction, and the overlap parameter satisfies its stated range restriction, then observed optimal-value minimax risk is at least one sixteenth of the paired-distribution L1 minimax risk.
Formal statement
Proof (Lean source)
If the product experiment has the stated independent-sampling law, and the alphabet size satisfies its stated restriction, and the overlap parameter satisfies its stated range restriction, then the equal-propensity embedding transfers the paired-distribution L1 minimax lower bound to observed optimal-value estimation.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.TIdentificationAndExtension 27 declarations Identification, global extension bounds, and equivalence of observed and causal experiments.
Identification, global extension bounds, and equivalence of observed and causal experiments.
For the specified success probability, binary value, the completion Bernoulli mass assigns probability p to success and one minus p to failure.
Definition (Lean source)
For the specified discrete law, data point or sample, the completion full-data mass equals the observed joint mass times the counterfactual Bernoulli mass when consistency holds, and zero otherwise.
Definition (Lean source)
the stated joint mass nonnegativity relation holds.
Formal statement
Proof (Lean source)
the stated cell mass nonnegativity relation holds.
Formal statement
Proof (Lean source)
the stated outcome mean mem unit interval relation holds.
Formal statement
Proof (Lean source)
the completion masses are nonnegative and their extended-real sum is one.
Formal statement
Proof (Lean source)
For the specified discrete law, the Bernoulli completion is the potential-outcome law obtained from the completion masses.
Definition (Lean source)
the total mass of a cell vector equals the observed cell mass.
Formal statement
Proof (Lean source)
the arm mass of a cell vector equals the observed arm mass.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, then every observed cell vector belongs to the overlap cone.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, then the arm value of a cell vector equals cell mass times the corresponding outcome mean.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, then the global cell value equals cell mass times the larger of the two outcome means.
Formal statement
Proof (Lean source)
each full-data atom of the Bernoulli completion has its prescribed completion mass.
Formal statement
Proof (Lean source)
the real-valued atom probability of the Bernoulli completion equals its completion mass.
Formal statement
Proof (Lean source)
converting a completion mass to an extended nonnegative real and back leaves it unchanged.
Formal statement
Proof (Lean source)
the Bernoulli completion satisfies consistency.
Formal statement
Proof (Lean source)
each potential-outcome atom of the Bernoulli completion factors into the observed joint mass and the missing-outcome Bernoulli mass.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, then each potential-outcome atom factors into cell mass, treatment propensity, and the two Bernoulli outcome masses.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, then the Bernoulli completion satisfies conditional exchangeability.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, then treatment is conditionally independent of the pair of potential outcomes given the covariate.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, then the two potential outcomes are conditionally independent given the covariate.
Formal statement
Proof (Lean source)
the observed marginal of the Bernoulli completion recovers the original observed law.
Formal statement
Proof (Lean source)
The particular completion used for observed-margin surjectivity: potential outcomes are conditionally independent Bernoulli variables, treatment is independent of their joint vector given X, and the observed outcome is selected by treatment.
Definition (Lean source)
If the observed law satisfies the stated model restrictions, then the Bernoulli completion supplies a valid completion of the observed law.
Formal statement
Proof (Lean source)
If the observed law satisfies the stated model restrictions, then the Bernoulli completion belongs to the causal completion class.
Formal statement
Proof (Lean source)
If the alphabet size satisfies its stated restriction, and the overlap parameter satisfies its stated range restriction, and the observed law satisfies the stated model restrictions, then the Bernoulli construction extends every admissible observed law to a causal model with the identified optimal value.
Formal statement
Proof (Lean source)
If the alphabet size satisfies its stated restriction, and the overlap parameter satisfies its stated range restriction, and the observed law satisfies the stated model restrictions, then the observed optimal-value functional is identified and every admissible observed law has a causal completion with the same oracle value.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.TJacksonFactorialUpper 1 declarations Uniform upper risk bound for the explicit Jackson--factorial estimator.
Uniform upper risk bound for the explicit Jackson--factorial estimator.
If the product experiment has the stated independent-sampling law, then the stated jackson factorial upper relation holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.TMatchedMinimaxFrontier 2 declarations Matched minimax frontier and its causal transfer.
Matched minimax frontier and its causal transfer.
For the specified tuning rule, sample size, alphabet size, overlap level, the Jackson worst-case risk is the supremum squared-error risk of the Jackson factorial estimator over the observed model class.
Definition (Lean source)
If the Cai--Low moment-matching prior result is available, and the Jiao--Han--Weissman Poisson L1 lower bound is available, then the observed minimax risk is bounded above and below by positive constants times the minimum of one and , with the stated causal and fallback comparisons.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteOptimalValueMinimaxMatched_Research.TParentReduction 2 declarations Deterministic comparison with the predecessor rates and bounded-alphabet branch.
Deterministic comparison with the predecessor rates and bounded-alphabet branch.
Eventual two-sided parametric risk bounds along a bounded alphabet sequence.
Definition (Lean source)
If the Cai--Low moment-matching prior result is available, and the Jiao--Han--Weissman Poisson L1 lower bound is available, then the parent observed and causal minimax problems inherit the matched frontier, bounded-alphabet equivalence, and fallback comparisons.