Formalization: Minimax Estimation of Budgeted Treatment Value Curves 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. Note: this index was generated at a different commit than the paper's audited pin (c4f4de3) — statements may have moved since the audit.
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Basic 63 declarations The finite observed and potential-outcome carriers reuse the earlier finite-PMF development.
Discrete budget value curves
The finite observed and potential-outcome carriers reuse the earlier finite-PMF development. The causal restrictions and budget functional are paper-specific.
the cell definition specifies the stated object.
Definition (Lean source)
the obs definition specifies the stated object.
Definition (Lean source)
the discrete law definition specifies the stated object.
Definition (Lean source)
For d, the potential atom definition specifies the stated object.
For d, the observed from potential definition specifies the stated object.
Definition (Lean source)
For d, Q, the canonical observed outcome definition specifies the stated object.
Definition (Lean source)
The canonical observed outcome of consistency result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The potential law structure records the data and laws for d.
Definition (Lean source)
For d, Q, the pmf definition specifies the stated object.
Definition (Lean source)
The property result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
For d, this instance provides the stated structure.
Definition (Lean source)
the full obs definition specifies the stated object.
Definition (Lean source)
For d, P, j, a, the joint mass definition specifies the stated object.
Definition (Lean source)
For d, Q, z, the full mass definition specifies the stated object.
Definition (Lean source)
For d, P, j, the cell vector definition specifies the stated object.
Definition (Lean source)
For d, P, j, the cell mass definition specifies the stated object.
Definition (Lean source)
For d, P, a, j, the arm mass definition specifies the stated object.
Definition (Lean source)
For d, P, j, the propensity definition specifies the stated object.
Definition (Lean source)
For d, P, n, the product law definition specifies the stated object.
Definition (Lean source)
For d, Q, the observed marginal definition specifies the stated object.
Definition (Lean source)
For d, Q, j, the po cell mass definition specifies the stated object.
Definition (Lean source)
For d, Q, a, j, the po regression definition specifies the stated object.
Definition (Lean source)
The finite observation carrier.
Definition (Lean source)
A finite observed sample.
Definition (Lean source)
The four nonnegative observed cell masses.
Definition (Lean source)
For d, P, mu, the iid sampling definition specifies the stated object.
Definition (Lean source)
A four-variable potential-outcome law with its derived observed outcome.
Definition (Lean source)
For d, Q, the consistency definition specifies the stated object.
Definition (Lean source)
Joint atom mass for the two potential outcomes, after marginalizing observed Y.
Treatment atom mass within a covariate cell.
Joint treatment and potential-outcome atom.
Definition (Lean source)
For d, Q, the conditional exchangeability definition specifies the stated object.
Definition (Lean source)
For d, epsilon, P, the overlap definition specifies the stated object.
Definition (Lean source)
The causal model class structure records the data and laws for epsilon, d, Q.
Definition (Lean source)
@realizes \epsilon(model overlap parameter in (0,1/2))
Cell effect, totalized to zero on null cells.
Definition (Lean source)
Cell potential-outcome regression.
Definition (Lean source)
For d, Q, b, the budget policy class definition specifies the stated object.
Definition (Lean source)
Value of the never-treat policy.
Definition (Lean source)
For d, Q, b, the budget value definition specifies the stated object.
Definition (Lean source)
The po regression unit interval budget result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The po cell mass sum one budget result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The budget value unit interval result. Under the hb premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The budget value order lipschitz result. Under the horder premise, It proves the stated conclusion. The argument assumes the two ordered-budget premises.
Formal statement
Proof (Lean source)
The mass of treatment arm a in a generic four-vector.
Definition (Lean source)
Total mass of a generic four-vector.
Globally extended arm value.
Cellwise threshold functional.
Zero extension used by intermediate polynomial calculations at real arguments.
Definition (Lean source)
For d, epsilon, P, lambda, the dual process definition specifies the stated object.
Definition (Lean source)
Zero extension of the dual process for real-indexed auxiliary processes.
Definition (Lean source)
Bounded measurable curve estimators on the stated interval.
Causal laws in the stated model class.
Definition (Lean source)
Squared supremum curve risk at a single causal law.
Definition (Lean source)
For n, epsilon, the curve minimax risk definition specifies the stated object.
Definition (Lean source)
The logarithmic alphabet scale log(e d).
A probability simplex represented by real coordinates.
Definition (Lean source)
Contrasts on the stated cube.
Bernoulli atom mass.
Definition (Lean source)
Full-data atom mass in the paired construction.
Definition (Lean source)
The finite masses sum to one. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
For k, r, theta, the paired law definition specifies the stated object.
Definition (Lean source)
A completion may couple the two potential outcomes arbitrarily, but their joint law is independent of treatment conditional on the covariate cell.
Definition (Lean source)
All admissible causal completions of the paired cell marginals.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.BVLipschitz 21 declarations Bounded-variation Lipschitz estimate for the threshold process.
Bounded-variation Lipschitz estimate for the threshold process.
Total-variation norm on the unit shadow-price interval.
Definition (Lean source)
The arm value agrees on nonnegative cells with the predecessor's totalized extension. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Each arm value is Lipschitz in the four masses on the nonnegative cone. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The total mass changes by at most the coordinatewise L1 distance. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Perturbing both arm values and the total mass perturbs a threshold hinge. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
At each shadow price, the threshold process inherits a cellwise L1 bound. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The hinge height is a nonnegative fraction of the cell mass. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The positive treatment gain inherits the two arm-value perturbation bounds. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Subtracting a nonnegative threshold commutes with taking positive gain. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
On the unit interval the threshold cell functional is a constant plus a hinge. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The positive hinge changes formula at its mass-normalized cutoff. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
An affine path has variation equal to its endpoint displacement. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A three-piece affine path has variation bounded by six times its sup norm. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The normalized breakpoint of a nonnegative hinge.
Definition (Lean source)
The hinge breakpoint lies in the unit interval. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A hinge agrees with its affine branch before the breakpoint. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A hinge vanishes after the breakpoint. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Two hinges are uniformly close under parameter perturbations. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The difference of two hinges has controlled total variation. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Adding a constant does not change the variation of a real path. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The threshold fun bv lipschitz result. Under the he premise, the he' premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.BVMaximal 29 declarations Good-pilot and bad-pilot centered continuum processes.
Good-pilot and bad-pilot centered continuum processes.
Cell statistic restricted to good or bad pilot draws.
Definition (Lean source)
Sum of the good-pilot or bad-pilot cell statistics.
Definition (Lean source)
Joint data/auxiliary mean of one pilot part.
Definition (Lean source)
Expected squared supremum of the centered good or bad pilot contribution.
Definition (Lean source)
Good pilot event in the ideal, uncapped count experiment.
Definition (Lean source)
On a good pilot draw, the true cell mass lies in the truncated pilot rectangle, equivalently within one pilot radius of its midpoint. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise.
Formal statement
Proof (Lean source)
Flattened-rate form of good-pilot rectangle containment, matching the hcenter premise of localJacksonFourPoissonFactorialPath_sq_bound. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise.
Formal statement
Proof (Lean source)
On a good pilot draw, every evaluation Poisson coordinate satisfies the normalized variance-to-radius condition used by the factorial-path bound. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise.
Formal statement
Proof (Lean source)
The paper's good or bad summand includes the cellwise target subtraction.
Definition (Lean source)
The contribution of one cell to the good or bad ideal pilot error process.
Definition (Lean source)
On the nonnegative cone, a fixed-threshold cell functional is continuous. This is the local regularity needed on every pilot rectangle. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Every point in the affine image of a pilot rectangle has nonnegative coordinates when the Poisson scale and alphabet are positive. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Every coordinate of a positive-scale pilot rectangle has strictly positive radius. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The threshold pullback to every positive-scale pilot rectangle is continuous, discharging the regularity premise of the Jackson construction. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
One positive constant depending only on the overlap level bounds every pilot-local Jackson coefficient BV envelope by the paper's radius sum and exp (12 K) factor. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Conditional on a fixed good flattened pilot table, the promoted four-Poisson factorial-path theorem gives the complete measurable BV and square-path-size package for one evaluation cell. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise.
Formal statement
Proof (Lean source)
Equation (21), conditionally on a fixed good pilot table: the evaluation factorial path has squared path-size bounded by the pilot radius sum squared, the structural d^(1/16) loss, and a coefficient-envelope constant. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise, the positive envelope constant, and the coefficient envelope.
Formal statement
Proof (Lean source)
The epsilon-dependent coefficient estimate instantiates the conditional equation (21) bound for every good pilot table. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise.
Formal statement
Proof (Lean source)
The ideal cell-error summand is continuous in the threshold whenever its pilot-local threshold pullbacks satisfy the Jackson construction regularity. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Positive sample size and nonempty alphabet automatically supply the pilot rectangle pullback regularity for an ideal cell-error path. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The ideal good or bad error process is the sum of its cell contributions. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A continuous cell contribution, restricted to the threshold interval, as a bounded-variation maximal-inequality path.
Definition (Lean source)
The uniform norm of a continuous real path restricted to [0,1] is the real supremum of its absolute values in the paper's sSup notation. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Norm identification for the paper's ideal good or bad cell-error path. With the specified inputs and conditions, the stated relationship holds. The argument assumes path continuity.
Formal statement
Proof (Lean source)
The abstract bounded-variation maximal theorem specialized to the ideal Poisson cell-error paths. Its hypotheses isolate the remaining paper-specific work: continuity in the threshold, measurability and integrability in the counts, the cellwise path-size moment, and independence across cells. With the specified inputs and conditions, the stated relationship holds. The argument assumes the probability-law premise, path continuity, measurability, Bochner integrability, the bounded-variation control, the path moment bound, and cross-cell independence.
Formal statement
Proof (Lean source)
Mean of the uncapped good or bad error part.
Definition (Lean source)
Centered risk of the paper's good or bad cellwise error sum.
Definition (Lean source)
The clipped cell path from the common Jackson polynomial.
Definition (Lean source)
The uncentered bad-pilot cell envelope in proof (28).
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.BadPilotAggregate 7 declarations Aggregate centered risk of the bad-pilot cell paths.
Aggregate centered risk of the bad-pilot cell paths.
A bad-pilot cell path is Bochner integrable once its squared norm is integrable. With the specified inputs and conditions, the stated relationship holds. The argument assumes the probability-law premise.
Formal statement
Proof (Lean source)
The scalar centered bad-pilot risk is the squared norm risk of the centered sum of continuous bad-pilot cell paths. With the specified inputs and conditions, the stated relationship holds. The argument assumes the probability-law premise.
Formal statement
Proof (Lean source)
The centered aggregate bad-pilot error is continuous in the shadow price. With the specified inputs and conditions, the stated relationship holds. The argument assumes the probability-law premise.
Formal statement
Proof (Lean source)
Centering and summing finitely many bad-pilot paths costs at most four times the alphabet size times the sum of their uncentered squared norms. With the specified inputs and conditions, the stated relationship holds. The argument assumes the probability-law premise.
Formal statement
Proof (Lean source)
Equations (28) and (32) give the centered bad-pilot aggregate bound before the final elementary exponential absorption. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The exponential bad-event factor absorbs the residual alphabet and logarithmic powers on the large-alphabet branch. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Equation (34): the centered bad-pilot aggregate has the advertised rate. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.BadPilotEnvelope 9 declarations Deterministic clipping bounds for bad pilot cells.
Deterministic clipping bounds for bad pilot cells.
Truncating the pilot interval at zero moves its midpoint from the empirical center by at most the original half-width. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
At every shadow price, clipping bounds a cell error by the empirical center score and the clipping scale. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The continuum supremum of one clipped-cell error is bounded by the same four-coordinate empirical score as every pointwise error. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
In the one-cell pilot/evaluation experiment, the squared bad-pilot continuum envelope is controlled by the promoted four-coordinate moment. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The local bad-pilot envelope estimate transports to the paper's full curried ideal count experiment. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Equation (28): one epsilon-dependent constant controls every bad-pilot cell envelope in the full ideal count experiment. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Equation (28) also supplies the squared-norm integrability of each bad-pilot cell Path required by later Bochner arguments. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The finite sum of bad-pilot cell squared Path norms is integrable. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
For an arbitrary discrete law, the unrestricted squared supremum error of one clipped ideal cell is integrable; no overlap estimate is needed. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.BadPilotMoment 10 declarations Coordinatewise empirical-radius estimates for bad pilot cells.
Coordinatewise empirical-radius estimates for bad pilot cells.
The paper's one-coordinate bad pilot event has the promoted exponential probability bound. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
On its bad event, the squared paper coordinate score satisfies the promoted empirical-radius moment bound. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
On its bad event, the fourth power of the paper coordinate score satisfies the promoted empirical-radius moment bound. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The universal four-coordinate bad-score moment specializes to one pilot cell with total intensity m * cellMass. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The promoted empirical-radius product theorem, specialized to the four pilot counts of one paper cell. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The squared empirical aggregate score restricted to the union of the four bad-radius events is integrable under independent Poisson coordinates. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Without restricting to the bad event, the squared empirical aggregate score is still integrable under four Poisson coordinates. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The four paper pilot coordinates have an exponentially small squared aggregate score on failure of the good-pilot rectangle. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The paper's squared four-coordinate bad score is integrable under its one-cell product Poisson law. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The unrestricted squared four-coordinate pilot score has a finite moment under its one-cell product Poisson law. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.CapCoupling 9 declarations Finite auxiliary weights and the capped marked-count coupling interface.
Finite auxiliary weights and the capped marked-count coupling interface.
The finite nonoverflow auxiliary experiment, augmented by one atom for Poisson overflow.
Auxiliary weight, with the missing Poisson tail assigned to the overflow atom.
Definition (Lean source)
Every augmented finite auxiliary weight is nonnegative. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The overflow atom completes the subprobability cap weights to a finite probability vector. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The paired table read from one nonoverflow auxiliary draw.
Definition (Lean source)
On the cap event, the paper's permuted marked table is the table component of the established uncapped finite-Poisson prefix construction. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The established uncapped marked finite-Poisson experiment has exactly the ideal paired table law used in this paper. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The paper's fair marking law is the fair Boolean law used by the capped prefix theorem. The stated relationship holds.
Formal statement
Proof (Lean source)
The finite auxiliary mixture in auxiliaryAverage equals the nonoverflow part of the established uncapped marked Poisson experiment. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.CapTransfer 19 declarations Capped, conditional-averaged threshold-process risk.
Capped, conditional-averaged threshold-process risk.
The true dual curve, restricted to the shadow-price interval, is a continuous Path.
Definition (Lean source)
On a nonnegative four-vector, each arm value lies between zero and the total mass. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The true dual threshold lies between zero and one after summing the cell masses of a discrete law. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The true dual target Path has unit supremum norm. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
One auxiliary Jackson estimate, restricted to the shadow-price interval, as a continuous path.
Definition (Lean source)
The ideal Jackson estimate is a continuous path for every count table.
Definition (Lean source)
The promoted quarter-mean Poisson cap estimate implies the weaker exponential remainder used in equation (37) of the paper. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The uncapped shadow-price process in the ideal Poisson experiment.
Definition (Lean source)
The ideal path error has exactly the paper's scalar supremum loss. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The squared supremum loss of the full uncapped ideal process is integrable for every discrete law; this coarse fact uses no overlap assumption. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The good and bad pilot events partition the ideal cell error exactly. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The structural Jackson degree leaves a fixed power of the alphabet to absorb the coefficient envelope. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Constants completing the common-polynomial handle. One constant works for all sample sizes, alphabets, observed laws, cells, and shadow prices.
Definition (Lean source)
Squared supremum error in the ideal, uncapped count experiment.
Definition (Lean source)
The expected squared continuum error of the deterministic averaged process.
Definition (Lean source)
The finite auxiliary estimator path, with the overflow atom assigned the zero path exactly as in the capped construction.
Definition (Lean source)
The weighted finite auxiliary path evaluates to the deterministic averaged threshold process. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The finite auxiliary average of error paths is the averaged estimator error path pointwise. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Transfer from ideal uncapped Poisson error to the capped, averaged fixed-sample estimator; the cap penalty is stated separately. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.CapacityAlphabetPadding 17 declarations Zero-mass padding of the paper's full-data causal laws.
Zero-mass padding of the paper's full-data causal laws.
Embed an observed record along an enlargement of its covariate alphabet.
Definition (Lean source)
Embed a full-data record along an enlargement of its covariate alphabet.
Extend a full-data causal law by zero mass on the new covariate cells.
Definition (Lean source)
Padded full atom masses agree with the original masses on embedded cells. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Every atom in a newly added covariate cell has zero padded mass. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Padded cell masses agree with the original masses on embedded cells. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Padded regressions agree with the original regressions on embedded cells. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Newly added cells have zero padded mass. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Newly added cells have totalized regression and effect zero. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Padding preserves effects on embedded cells. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Padding preserves the never-treat value. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Zero-mass alphabet padding preserves the budget-constrained value. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Zero-mass padding preserves all restrictions defining the capacity hard class and its binding half-budget certificate. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The observed PMF of a padded potential law is the pushforward of the original observed PMF. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Coordinatewise padding transports the iid observed sample law exactly. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Pulling an estimator back along coordinatewise alphabet padding preserves its squared risk, including the half-budget target. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A paired lower bound on an even subalphabet transfers to any larger paper alphabet by zero-mass padding. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.CapacityLowerTransport 5 declarations Fixed-sample transport from paired L1 estimation to half-budget value.
Fixed-sample transport from paired L1 estimation to half-budget value.
The parameter-free paired randomization as a Mathlib Markov kernel.
For n, this instance provides the stated structure.
Definition (Lean source)
The paired Markov kernel sends the fixed two-sample law exactly to the observed iid law of the normalized paired causal construction. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Any positive paired-L1 minimax lower bound transfers, with the exact 1/32 affine scale, to an even-alphabet capacity-active causal instance. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The same transport uses any supplied sampling-law family satisfying the paper's IidSampling equality, rather than a definitionally chosen product. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.CitedGates 10 declarations The cited known-reference lower bound used by the two-sample reduction.
The cited known-reference lower bound used by the two-sample reduction.
A simplex vector has total ENNReal mass one. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The PMF of a probability-simplex vector.
Definition (Lean source)
The fixed-sample law from a simplex vector.
Definition (Lean source)
Discrete L1 distance.
Definition (Lean source)
The simplex l1 nonneg le two result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The simplex l1 self result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The simplex l1 symm result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
All measurable scalar estimators using the first sample and a known reference vector.
Definition (Lean source)
Fixed-reference L1 squared risk.
Definition (Lean source)
Jiao, Han, and Weissman (2018), Minimax estimation of the L1 distance, Theorem 3, equation (24), and the discussion following Theorem 6; arXiv:1705.00807v7. The known-reference large-alphabet bound in its stated regime.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.CoefficientEnvelope 1 declarations The coefficient-process bounded-variation quantity.
The coefficient-process bounded-variation quantity.
Sum of the bounded-variation norms of normalized polynomial coefficients.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.Estimator 10 declarations The deterministic, auxiliary-randomization-averaged curve estimator.
The deterministic, auxiliary-randomization-averaged curve estimator.
The empirical observed four-mass vector.
Definition (Lean source)
The plug-in threshold process used below the alphabet cutoff.
Definition (Lean source)
The uncapped pilot/evaluation threshold process for one auxiliary draw.
Definition (Lean source)
The cap event contributes the zero threshold process.
Exact finite average over Poisson count, permutation, and fair marks.
Definition (Lean source)
The process used by the two nonconstant estimator branches.
Definition (Lean source)
The projected dual minimum, with no optimizer choice.
For n, epsilon, sample, the jf estimator definition specifies the stated object.
Definition (Lean source)
Measurability and global boundedness of the clipped curve estimator. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The estimator packaged for the minimax infimum.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.FactorialMoments 11 declarations Products of centered factorial lifts for the four coordinates.
Products of centered factorial lifts for the four coordinates.
A bounded monomial coefficient of the local Jackson polynomial, packaged as a continuous threshold path.
Definition (Lean source)
Every local Jackson coefficient path has finite total variation. This is the paper-side regularity premise required by the clipped Poisson factorial path moment theorem. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The clipped four-count factorial polynomial driven by the paper's local Jackson coefficient paths.
Definition (Lean source)
Pointwise, the paper-specific factorial path is exactly the symmetric clip of the Jackson coefficient polynomial in the normalized factorial monomials. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Adding back the center threshold identifies the generic clipped factorial path with the paper's complete clipped Jackson cell statistic. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The paper-specific local Jackson factorial path inherits measurability, samplewise bounded variation, integrability, and the promoted exponential square path-size estimate. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The paper's centered falling-factorial coordinate is exactly the generic Poisson factorial lift. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A monomial's centered factorial lift on the pilot rectangle.
Definition (Lean source)
A paper factorial monomial is the generic normalized four-coordinate factorial monomial after reindexing the four cells. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Under independent Poisson evaluation counts, the mean of a paper factorial monomial is the corresponding normalized product of powers. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The paper's normalized four-coordinate factorial monomial inherits the generic exponential square-moment envelope. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.GoodPilotAggregate 5 declarations Identification and simplification of the aggregate good-pilot path risk.
Identification and simplification of the aggregate good-pilot path risk.
The paper's scalar centered good-pilot risk is exactly the squared norm risk of the centered sum of its continuous cell paths. With the specified inputs and conditions, the stated relationship holds. The argument assumes the probability-law premise.
Formal statement
Proof (Lean source)
The centered aggregate good-pilot error is continuous in the shadow price. With the specified inputs and conditions, the stated relationship holds. The argument assumes the probability-law premise.
Formal statement
Proof (Lean source)
Equations (21), (32), and (33), before the final elementary rate simplification, bound the exact scalar good-pilot risk. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The logarithmic cell-scale expression in the raw equation (33) bound is absorbed by the advertised d /(m log(ed)) rate on the paper's main branch. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Equation (33) in its advertised rate form. The constant depends only on the fixed overlap level through the preceding Jackson envelope. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.GoodPilotCellMoment 9 declarations Deterministic target correction and full good-pilot cell moments.
Deterministic target correction and full good-pilot cell moments.
The promoted measurability of total variation makes the paper's path-size functional Borel measurable on the continuous-path space. The stated relationship holds.
Formal statement
Proof (Lean source)
Adding a fixed continuous path preserves measurability of squared path size for a measurable random path. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Path size is subadditive on bounded-variation paths. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The deterministic threshold discrepancy between a pilot midpoint and the true cell vector, viewed as a path on the threshold interval.
Definition (Lean source)
The deterministic threshold correction always has finite variation. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
On a good pilot cell, the deterministic target correction has path size at most an epsilon-dependent constant times the sum of pilot radii. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
With a fixed good pilot table, the complete ideal cell-error path is the sum of its factorial evaluation path and deterministic target correction. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise.
Formal statement
Proof (Lean source)
Pointwise on a good pilot cell, the complete ideal error path is bounded by the factorial path size plus an epsilon-dependent radius-sum correction. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise.
Formal statement
Proof (Lean source)
Conditional on a fixed good pilot table, the full cell-error path has the paper's equation (21) squared path-size scale. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.GoodPilotCellOuterMoment 21 declarations Block-local composition and unconditional good-pilot cell moments.
Block-local composition and unconditional good-pilot cell moments.
Boolean reflection of the paper's cellwise good-pilot event.
Definition (Lean source)
The Boolean good-pilot event reflects the propositional definition. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Embed four counts into one cell of a flattened count table.
Extracting the embedded cell recovers its four counts. The cell extraction identity follows.
Formal statement
Proof (Lean source)
At the selected cell, currying a table depends only on its extracted four-count block. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The paper's good-pilot predicate is local to the selected four-count pilot block. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Replacing both flattened tables by their selected-cell embeddings leaves the selected ideal cell-error path unchanged. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Under the two flattened Poisson table laws, the indicator-weighted full good-pilot cell path has the unconditional equation (21) moment scale. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Pushing the flattened product experiment through the count-table equivalence gives the unconditional full good-pilot cell moment under the paper's idealCountLaw. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Outside the good-pilot event, the good = true cell path is the zero path; hence its squared path size equals its indicator-weighted version. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A sum of two finite-variation continuous paths again has finite extended variation. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Every realization of the good-pilot cell path has finite variation: it is zero off the good event and factorial path plus correction on that event. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The pointwise finite-variation result supplies the almost-everywhere BV hypothesis used by the centered maximal theorem. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
For a fixed cell, the ideal good-pilot error is a measurable random continuous path under the count-table sigma algebra. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The unconditional equation (21) theorem exports square-path-size integrability in the exact form required by the maximal inequality. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Square-path-size integrability implies Bochner integrability of the good-pilot random path. With the specified inputs and conditions, the stated relationship holds. The argument assumes the probability-law premise.
Formal statement
Proof (Lean source)
Cellwise good-pilot error paths are mutually independent under the ideal count law because each is a measurable function of its paired pilot/evaluation four-count block. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The abstract centered maximal inequality applies to the complete family of good-pilot cell paths under the ideal count experiment. With the specified inputs and conditions, the stated relationship holds. The argument assumes the probability-law premise.
Formal statement
Proof (Lean source)
The marginal masses of a discrete observed law sum to one. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Equation (32): the squared local mass scales sum to a linear mass term plus the uniform four-count remainder. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Combining equations (21), (32), and the BV maximal inequality gives a single quantitative bound for the centered sum of all good-pilot paths. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.IdealCountTransport 7 declarations Transport between flattened Poisson tables and the paper's curried count tables.
Transport between flattened Poisson tables and the paper's curried count tables.
Flatten a paper count table using the fixed four-cell equivalence.
Curry a flattened four-coordinate table back into the paper representation.
Definition (Lean source)
Flattening and currying are inverse table representations.
Definition (Lean source)
The flattened rate corresponding to one pool in idealCountLaw.
Definition (Lean source)
One flattened ideal Poisson pool pushes forward to the paper's curried pool. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Both flattened ideal pools push forward to idealCountLaw. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Selecting a cell after currying a flat table returns its four-count block. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.JacksonBias 5 declarations Cellwise expectation and scalar bias of the capped Jackson statistic.
Cellwise expectation and scalar bias of the capped Jackson statistic.
The ideal, uncapped Poisson pilot and evaluation counts.
Definition (Lean source)
Uncapped cellwise expectation in the ideal Poisson count experiment.
Definition (Lean source)
Scalar bias before the finite-sample Poisson cap transfer.
Definition (Lean source)
Mean of a single capped cell statistic under data and auxiliary randomization.
Definition (Lean source)
Absolute cellwise scalar bias of the same polynomial used by the estimator.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.JacksonCoefficientEnvelope 11 declarations Jackson coefficient bounded-variation envelopes and their Poisson path consequences.
Jackson coefficient bounded-variation envelopes and their Poisson path consequences.
A finite-variation continuous path is controlled by its value at the left endpoint and its total variation. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Summing the deterministic endpoint/variation bound over a finite family costs only the universal numerical factor four after squaring. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Restricting a real function to the ordered interval [0,1] preserves exactly its extended variation. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A normalized-cube affine perturbation moves from its center by at most the sum of its nonnegative coordinate radii in cellwise L1 distance. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Averaging paths against the normalized positive tensor Jackson kernel does not increase a common path-size bound. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The centered local Jackson polynomial has a uniform cube path-size envelope obtained from the spatial BV Lipschitz constant and the radius sum. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The explicit four-dimensional Chebyshev conversion factor is absorbed by the paper's exp (12 K) budget. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The finite four-coordinate factorial index set, together with the degree exponential from equation (21), is absorbed by the structural d^(1/16) budget. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A uniform path-size bound for every normalized-cube evaluation of the local Jackson polynomial implies the paper's coefficient BV envelope. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The squared path sizes of all local Jackson coefficient paths are bounded by four times the paper's coefficient bounded-variation envelope squared. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The four-Poisson factorial path square moment is controlled directly by the paper's Jackson coefficient bounded-variation envelope. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.JacksonPolynomial 33 declarations The polynomial is chosen from its normalized cosine representation.
Pilot-local Jackson polynomial and factorial lift
The polynomial is chosen from its normalized cosine representation. This lets the estimator use its actual monomial coefficients without choosing a minimizer.
the cell four equiv definition specifies the stated object.
Definition (Lean source)
Restricted to the unit threshold interval, the extended threshold functional is continuous in the threshold. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
At a fixed cell vector, the threshold functional is Lipschitz in the threshold with constant equal to the absolute total cell mass. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The threshold functional at a fixed cell vector is a Lipschitz function of the threshold on the unit interval. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The fixed pilot-radius multiplier.
Definition (Lean source)
The fixed inverse degree multiplier.
Definition (Lean source)
The bounded-alphabet cutoff.
Definition (Lean source)
The paper's structural Jackson degree.
Definition (Lean source)
Poisson pilot or evaluation count for a permuted and marked sample.
Definition (Lean source)
Coordinatewise pilot center.
Definition (Lean source)
Coordinatewise pilot half-width.
Definition (Lean source)
The lower endpoint, truncated at zero.
Definition (Lean source)
The upper endpoint.
Definition (Lean source)
Midpoint of the truncated pilot interval.
Definition (Lean source)
Radius of the truncated pilot interval.
Definition (Lean source)
The exact tensor convolution of the cell threshold on its pilot rectangle.
Definition (Lean source)
If every fixed-threshold pullback is continuous on the normalized cube, the local Jackson convolution is Lipschitz, hence continuous, in the threshold. The proof uses only thresholdwise continuity in the integration coordinate. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The local Jackson convolution is continuous in the threshold under the same pointwise pullback regularity used to construct its polynomial. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The normalized tensor convolution has a monomial polynomial representative when its pullback is continuous on the normalized cube. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A canonical normalized polynomial obtained by choice from the Jackson construction. It defaults to zero outside the degree and continuity domain of that construction.
Definition (Lean source)
On the Jackson construction domain, the chosen local polynomial has the required coordinatewise degree. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
On the Jackson construction domain, evaluating the chosen polynomial on the cosine cube recovers the centered tensor convolution. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
At each fixed point of the normalized cube, the chosen local Jackson polynomial has a continuous evaluation path in the threshold. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
At every fixed point of the normalized cube, evaluation of the chosen local Jackson polynomial is Lipschitz in the threshold. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The normalized monomial coefficient.
Definition (Lean source)
A bounded multi-index Jackson coefficient is the corresponding fixed tensor-basis coefficient of the local polynomial. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Continuous fixed-grid evaluations remove the apparent incoherence of the pointwise chosen Jackson representatives: every bounded coefficient then varies continuously with the threshold. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Every bounded coefficient of the local Jackson polynomial varies continuously with the threshold. The proof recovers it from a fixed finite tensor grid lying inside the normalized cube. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Every fixed evaluation of the degree-bounded local Jackson polynomial is continuous in the threshold. In particular, this supplies the integer-grid premise used by the generic tensor coefficient path API. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Centered factorial polynomial for a single count and monomial degree.
Definition (Lean source)
The uncapped polynomial statistic for one cell and one shadow price.
Definition (Lean source)
The clipped cellwise Jackson-factorial statistic.
Definition (Lean source)
Under the same fixed-threshold cube regularity used by the Jackson construction, the complete clipped cell statistic is continuous in the threshold. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.LowerSplice 1 declarations Sparse, dense, and finite-alphabet lower-bound splice.
Sparse, dense, and finite-alphabet lower-bound splice.
The matched lower-rate scale.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.MomentMatchingPriors 1 declarations The local absolute-moment prior composition.
The local absolute-moment prior composition.
Source match: cite:cailow2011, Lemma 1 (p. 10) and the Bernstein-limit discussion defining (p. 8). T. Tony Cai and Mark G. Low (2011), arXiv:1105.3039, DOI 10.1214/10-AOS849. The stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.PairedKernel 1 declarations Fixed-sample paired-kernel reduction substrate for the lower proof.
Fixed-sample paired-kernel reduction substrate for the lower proof.
The hard capacity-active subclass, including the binding requirement.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.PairedObservedAtom 29 declarations Real atom sums for the observed margin of the explicit paired law.
Real atom sums for the observed margin of the explicit paired law.
Summing out both potential outcomes gives the paired observed atom mass. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Every atom of the paired full-data construction has nonnegative mass. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The real mass of an explicit paired-law atom is its defining mass. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
An observed paired-law atom has the stated Bernoulli mass. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Conditional mass of one generated record from one draw of each input law.
Definition (Lean source)
The one-record kernel mass is nonnegative. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The conditional record masses sum to one. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The conditional distribution of one record given a draw from each input law.
Definition (Lean source)
Independent conditional randomization at each sample coordinate.
The conditional sample law factors over record coordinates. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Mixing the conditional atom over independent input labels gives the target atom. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Mixing the conditional atom over independent input labels gives the target atom. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Pairing the two input samples coordinatewise is an equivalence.
Definition (Lean source)
Finite product sums factor coordinatewise for paired samples. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The fixed-sample kernel mixture factors into its one-record marginals. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The explicit paired law has the prescribed mass in each covariate cell. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Both arms of a paired cell have equal treatment mass. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Joint potential-outcome and treatment atoms factor under the paired law. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The paired potential-outcome atom is twice either arm's joint atom. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The explicit paired law obeys consistency and joint exchangeability. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The numerator of a paired cell's conditional potential-outcome mean. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Weighted conditional means of the explicit paired law match its parameters. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The explicit paired law is one of the admissible causal completions. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The fixed-sample observed law factors into its one-record atom masses. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The normalized contrast has the exact signed mass needed by the sampling kernel. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The treated outcome atom is a fixed mixture of the two input-label atoms. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Every observed atom of the normalized pair is an equal mixture of the corresponding atoms produced from the two input labels. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The kernel mixture is exactly each normalized paired observed atom. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The parameter-free fixed-sample kernel reproduces the normalized observed law. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.PilotEvents 1 declarations Good-pilot event for each observed cell.
Good-pilot event for each observed cell.
All four pilot coordinates fall within one quarter of their local radii.
Definition (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.PilotRadiusMoment 5 declarations Ordinary second moments of the paper's pilot rectangle radii.
Ordinary second moments of the paper's pilot rectangle radii.
The paper's pilot half-width is exactly the promoted empirical Poisson radius with multiplier 4096 and logarithmic level logAlphabet d. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The local mass scale v_j with L = log(ed) and m = n/8.
Definition (Lean source)
Truncating the lower endpoint of a nonnegative pilot interval can only decrease its radius below the untruncated half-width. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A single squared pilot radius is bounded by an affine function of its Poisson count. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Under the flattened pilot Poisson table law, the squared sum of the four pilot radii has the ordinary second-moment bound required in equation (21). With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.PoissonSplit 2 declarations Exact finite auxiliary weights for the capped Poisson split.
Exact finite auxiliary weights for the capped Poisson split.
The probability weight of one Poisson count, permutation, and marking.
Finite expectation over the nonzero cap-event outcomes.
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.ScalarBias 18 declarations Boundary-adaptive Jackson approximation and scalar cell bias.
Boundary-adaptive Jackson approximation and scalar cell bias.
The paper's canonical normalized polynomial, after affine substitution, inherits the promoted physical-coordinate boundary-adaptive estimate. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
On a good pilot cell, the promoted boundary-adaptive estimate applies at the true four-cell vector, including coordinates of zero mass. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise.
Formal statement
Proof (Lean source)
The boundary-adaptive Jackson remainder on a good pilot cell is bounded by the pilot radius sum times the usual first and second degree factors. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise.
Formal statement
Proof (Lean source)
Projection onto a symmetric interval differs from its input by at most the input square divided by the positive clipping radius. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A centered normalized factorial lift has a finite first absolute moment under every Poisson law. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A finite product of centered factorial lifts is integrable under independent Poisson coordinates. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A product of two falling factorials has a finite Poisson first moment. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A finite sum is square integrable when every pair of summands has an integrable product. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The square of a centered normalized factorial lift is Poisson integrable. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A finite product of centered factorial lifts has an integrable square under independent Poisson coordinates. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The unprojected centered Jackson factorial polynomial has an integrable square under independent Poisson evaluation counts. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
On a pilot rectangle containing the true normalized rate, the conditional second moment of the raw Jackson factorial polynomial is controlled by the coefficient BV envelope and the promoted factorial-product envelope. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The paper's choice of Jackson degree absorbs the factorial index count, coefficient growth, and factorial square moment into d^(1/16). With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Equation (23)'s raw conditional second-moment input, for a fixed good pilot table and one evaluation cell. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise, the shadow-price range, the positive envelope constant, and the coefficient envelope.
Formal statement
Proof (Lean source)
Conditional clipping changes the mean of the Jackson factorial polynomial by at most its centered second moment divided by the clipping radius. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
On a fixed good pilot table, clipping changes the conditional cell mean by the raw second-moment envelope divided by the paper's clipping scale. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise, the shadow-price range, the positive envelope constant, and the coefficient envelope.
Formal statement
Proof (Lean source)
Independent Poisson evaluation counts make the unprojected paper factorial polynomial exactly unbiased for the canonical Jackson polynomial. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Conditional on a fixed good pilot table, the cell mean bias is the sum of the clipping correction and the boundary-adaptive Jackson remainder. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise, the shadow-price range, the positive envelope constant, and the coefficient envelope.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.ScalarBiasOuter 15 declarations Outer pilot expectation bounds for the scalar Jackson cell bias.
Outer pilot expectation bounds for the scalar Jackson cell bias.
The ideal two-pool count law is a probability measure. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
On a probability space, the square of the mean of a nonnegative square-integrable scalar is at most its second moment. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The first moment of the sum of the four pilot radii is controlled by the square root of the equation-(21) cell scale. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Linear first-moment form of the pilot-radius estimate. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Integrating the conditional good-pilot scalar bias costs one first moment of the sum of the four pilot radii. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
At a fixed shadow price, the ideal clipped cell error is integrable. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The paper's ideal cell expectation is the iterated flattened pilot and evaluation Poisson expectation. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The absolute bad-pilot contribution to a fixed scalar cell mean is bounded by the existing equation-(28) cell envelope. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The good-pilot contribution to the ideal scalar cell mean inherits the flattened conditional bias bound. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The scalar cell bias is the sum of its good-pilot conditional clipping contribution and the bad-pilot envelope contribution. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The logarithmic factor times the negative three-sixteenths power is uniformly bounded on the paper's large-alphabet branch. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The logarithm divided by the paper's Jackson degree is uniformly bounded. With the specified inputs and conditions, the stated relationship holds.
Proof (Lean source)
The complete good-pilot clipping coefficient loses one logarithmic factor uniformly in the alphabet size. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Boundary adaptivity removes the additive empirical-radius floor: inside the truncated nonnegative confidence interval, the product of the distances to its endpoints is controlled by the true intensity times the radius level. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
On a paper good-pilot draw, each physical Jackson boundary product has the sharp true-rate scale, including at a null coordinate. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.ScalarBiasSharp 14 declarations Sharp boundary-product bounds for the scalar Jackson bias.
Sharp boundary-product bounds for the scalar Jackson bias.
Each coordinate of a cell vector is bounded by the total cell mass. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The sum of the four good-pilot physical boundary products has the sharp true cell-mass scale. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise.
Formal statement
Proof (Lean source)
The good-pilot Jackson approximation keeps the boundary-adaptive term separate from the second-order radius term. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise.
Formal statement
Proof (Lean source)
Conditional good-pilot scalar bias with the physical boundary term kept separate from the second-order radius term. With the specified inputs and conditions, the stated relationship holds. The argument assumes the good-pilot premise, the shadow-price range, the positive envelope constant, and the coefficient envelope.
Formal statement
Proof (Lean source)
Integrating the sharp conditional bias over the pilot table costs only the first moment of the radius sum; the boundary product is deterministic. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Any flattened good-pilot scalar bound transports unchanged to the paper's curried ideal count law. With the specified inputs and conditions, the stated relationship holds. The argument assumes the flattened-law bound.
Formal statement
Proof (Lean source)
The sharp flattened good-pilot bias bound under the ideal count law. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Two logarithmic factors are absorbed by the negative power supplied by the factorial clipping term. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The cell scale is at most two logarithmic factors times the scalar target rate. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The bad-pilot exponential envelope absorbs the two logarithmic factors needed to convert the cell scale to the scalar target rate. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Splitting the ideal scalar error by the pilot event bounds its bias by the absolute good mean plus the existing bad-pilot envelope. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The boundary square-root term divided by the Jackson degree has the frozen scalar rate. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The second-order radius term divided by the squared Jackson degree also has the frozen scalar rate. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A single epsilon-dependent constant controls the uncapped scalar cell bias at the paper's square-root rate. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.SmallCapacityLower 1 declarations A two-cell parametric lower bound inside the capacity-active paired family.
A two-cell parametric lower bound inside the capacity-active paired family.
On every alphabet containing two cells, a binary paired submodel gives a uniform parametric capacity-active lower bound. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.TwoSampleL1 23 declarations The fixed two-sample L1 reduction conditional on the cited known-reference gate.
The fixed two-sample L1 reduction conditional on the cited known-reference gate.
Product law of two independent fixed samples.
Every measurable real-valued statistic of the paired samples.
Definition (Lean source)
Squared risk in the normalized two-sample L1 experiment.
Definition (Lean source)
The exact fixed two-sample minimax risk.
Definition (Lean source)
Atom probabilities of the two independent fixed samples factor coordinatewise. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Conditional Jensen for the known-reference reduction: averaging over the second sample cannot increase squared loss at a fixed first sample. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Integrating conditional Jensen gives the risk comparison used when the reference distribution is revealed to the estimator. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
At each fixed reference distribution, the two-sample worst-case risk dominates the known-reference minimax risk. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The two sample l1 risk bdd above all result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The two sample l1 risk bdd above fixed result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The two sample l1 known reference le result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The fixed-reference minimax lower bound transfers to the experiment where both distributions are sampled and unknown. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The known-reference cited bound applies unchanged to two fixed samples through conditional averaging over the reference sample. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The cited dense-regime bound with the alphabet logarithm used by the two-sample theorem. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A finite sample can be read as the initial coordinates of a longer sample. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Discarding observations shows that the two-sample minimax risk decreases with the sample size. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The known-reference gate supplies the claimed two-sample rate throughout the dense range of large alphabets. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The two fixed hypotheses used to handle finitely many small alphabets.
Definition (Lean source)
For k, hk, the two sample l1 half mass definition specifies the stated object.
Definition (Lean source)
The two sample l1 fixed targets result. Under the hk premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The two sample l1 common atom result. Under the hk premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The two sample l1 atom risk le result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
A common observation atom gives a positive two-point squared-risk bound at every finite sample size, uniformly over alphabets with two labels. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.Helpers.TwoSampleL1Splice 3 declarations Sparse and finite-alphabet completion of the two-sample L1 lower bound.
Sparse and finite-alphabet completion of the two-sample L1 lower bound.
At large alphabets the cited dense result also controls samples below k / log k, by comparing with the first dense sample size. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The two sample l1 lower result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The paper's small-sample bound and the generic large-sample theorem give the matched two-sample lower bound for every positive sample size. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.TCapacityActiveLower 2 declarations The capacity-active minimax converse, conditional on the known-reference gate.
The capacity-active minimax converse, conditional on the known-reference gate.
Measurable scalar estimators of the half-budget value.
Definition (Lean source)
The capacity active lower result. Under the he premise, the he' premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.TCurveUpper 19 declarations Uniform risk bound for the explicit total curve estimator.
Uniform risk bound for the explicit total curve estimator.
The four-mass plug-in coordinate is the ordinary empirical mass of its atom. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Each plug-in four-mass coordinate has mean-square error at most 1/n. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Cellwise Lipschitz control of the empirical threshold process. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The empirical threshold process has uniform squared risk of order d²/n. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The empirical threshold path is bounded on the price interval. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The averaged threshold path is bounded on the price interval. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Projection to the unit interval contracts distance to a unit-interval target. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
A bounded threshold path gives a lower-bounded dual objective. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Dual minimization and clipping transfer a uniform price-path error to curve loss. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The nonconstant estimator branch inherits the threshold-process loss. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
In the empirical branch, curve risk is bounded by the empirical process risk. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
In the Jackson branch, curve risk is bounded by the averaged process risk. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The logarithmic scale lies between one and the alphabet size. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The empirical bound has the required logarithmic rate below the cutoff. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The total curve estimator takes values in the unit interval on every branch. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The clipped estimator has squared uniform loss at most one. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Every model has unit-bounded curve risk under the clipped estimator. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The unit risk bound is uniform over the causal model class. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The curve upper result. Under the he premise, the he' premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.TDualRepresentation 16 declarations Fractional-knapsack duality and contraction of the dual minimum.
Fractional-knapsack duality and contraction of the dual minimum.
The observed cell mass is the corresponding full-data covariate marginal. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Joint conditional independence of both potential outcomes implies armwise independence. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The budget cell mass as total mass result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The budget arm mass as arm mass fn result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The budget cell success mass result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
Under causal identification and overlap, the extended arm value is cell mass times mean. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The observed threshold term is the causal baseline plus the positive effect hinge. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The threshold process equals control value plus the sum of positive effect hinges. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The minimum of an indexed shadow-price process on [0,1].
The dual minimum lipschitz result. Under the hF premise, the hG premise, the hM premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The weighted budget weak duality result. Under the hp premise, the hpi premise, the hbudget premise, the hlambda premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The dual minimum uniform lipschitz result. Under the hF premise, the hG premise, the hM premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The dual minimum uniform contraction result. Under the hF premise, the hG premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The dual process real bounded result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
Every feasible policy lies below every nonnegative shadow-price objective. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The dual representation result. Under the hd premise, the hQ premise, the he premise, the he' premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.TFixedAlphabetReduction 4 declarations Parametric fixed-alphabet specialization and linear budget curves.
Parametric fixed-alphabet specialization and linear budget curves.
The po cell mass nonneg budget result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The po cell mass sum budget result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The constant effect budget value result. Under the hcpos premise, the hc premise, the hb premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The fixed alphabet reduction result. Under the he premise, the he' premise, the hd premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.TIntegratedProcessCertificate 1 declarations Uniform Jackson-factorial threshold-process certificate.
Uniform Jackson-factorial threshold-process certificate.
The integrated process certificate result. Under the he premise, the he' premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.TMatchedCurveFrontier 12 declarations The matched all-procedure budget-curve frontier.
The matched all-procedure budget-curve frontier.
The curve coordinate in budget interval result. Under the hb0 premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The curve loss pointwise bound result. Under the hb0 premise, the hB premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The curve loss sup bound result. Under the hb0 premise, the hB premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The curve risk bdd above result. Under the hb0 premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The curve risk nonneg result. Under the hb0 premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
For n, b0, hb0, est, the scalar coordinate of curve estimator definition specifies the stated object.
Definition (Lean source)
The scalar coordinate risk le curve risk result. Under the hb0 premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The curve rate nonneg result. Under the hn premise, the hd premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
The full budget cell mass nonneg result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The full budget cell mass sum result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The full budget value result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
The matched curve frontier result. Under the he premise, the he' premise, It proves the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_DiscreteBudgetvalueCurve_Research.TPairedCapacityIdentity 16 declarations The positive-effect paired family and its exact fixed-sample reduction.
The positive-effect paired family and its exact fixed-sample reduction.
The observed arm mass is the corresponding full-data treatment marginal. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Binding capacity with an attaining randomized policy.
Definition (Lean source)
The two sampled simplex vectors give valid pair masses and contrasts. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The normalized embedding converts the paired capacity term to L1 distance. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Occupied cells of a paired completion have the specified positive effects. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The paired family has a fixed control-policy value. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Pairwise cancellation makes the value of treating every cell constant. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
Every paired completion obeys the causal model restrictions. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The paired completion budget value one result. It proves the stated conclusion.
Formal statement
Proof (Lean source)
Select exactly the better member of each cell pair, including at ties.
Definition (Lean source)
The sign-selecting policy treats exactly half the population. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The sign-selecting feasible policy realizes the paired value formula. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The shadow price one quarter evaluates to the paired capacity value. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The sign policy attains the shadow-price bound and uses the full half budget. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The normalized pair's half-budget value is an affine copy of L1 distance. With the specified inputs and conditions, the stated relationship holds.
Formal statement
Proof (Lean source)
The paired capacity identity result. Under the hk premise, the he premise, the he' premise, It proves the stated conclusion.