Formalization: Honest Confidence Intervals for Transported Complier Effects with Rough Nuisance Functions
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs. Note: this index was generated at a different commit than the paper's audited pin (46d0720) — statements may have moved since the audit.
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Basic 84 declarations The law has a full-data population coordinate and an assigned source overlay.
Rough nuisance transported CACE: law and decision class
The law has a full-data population coordinate and an assigned source overlay. Fixed-size source and target experiments are separate factors. The single-population IV and infinite-sequence iid abstractions in Causalean have different carriers (bypass-justified); restricted volume, affine inversion, and Hölder balls are reused.
The covariate space object is defined without additional inputs.
Definition (Lean source)
The parameter space object is defined without additional inputs.
Definition (Lean source)
The full data object is defined without additional inputs.
The assigned object is defined without additional inputs.
The source obs object is defined without additional inputs.
The two sample object is defined from the supplied inputs.
The population object is defined from the supplied inputs.
The covariate object is defined from the supplied inputs.
Definition (Lean source)
The receipt0 object is defined from the supplied inputs.
The receipt1 object is defined from the supplied inputs.
The outcome0 object is defined from the supplied inputs.
Definition (Lean source)
The outcome1 object is defined from the supplied inputs.
Definition (Lean source)
The bool real object is defined from the supplied inputs.
Definition (Lean source)
The potential receipt object is defined from the supplied inputs.
The potential outcome object is defined from the supplied inputs.
The complier object is defined from the supplied inputs.
The observe source object is defined from the supplied inputs.
The transport law is specified by its full-data, assignment, and sampling laws together with its density, propensity, and arm-mean functions.
The population law object is defined from the supplied inputs.
Definition (Lean source)
The source obs law object is defined from the supplied inputs.
Definition (Lean source)
The source xlaw object is defined from the supplied inputs.
Definition (Lean source)
The target xlaw object is defined from the supplied inputs.
Definition (Lean source)
The data law object is defined from the supplied inputs.
Definition (Lean source)
The arm value object is defined from the supplied inputs.
The assignment mass object is defined from the supplied inputs.
Definition (Lean source)
The arm contrast object is defined from the supplied inputs.
Definition (Lean source)
The transported form object is defined from the supplied inputs.
Definition (Lean source)
The first stage object is defined from the supplied inputs.
Definition (Lean source)
The target cace object is defined from the supplied inputs.
Definition (Lean source)
The holder exponent object is defined without additional inputs.
Definition (Lean source)
The threshold object is defined without additional inputs.
Definition (Lean source)
The holder on object is defined from the supplied inputs.
Definition (Lean source)
The measurable on covariate object is defined from the supplied inputs.
Definition (Lean source)
The source iid object is defined from the supplied inputs.
Definition (Lean source)
The target iid object is defined from the supplied inputs.
Definition (Lean source)
The sample independence object is defined from the supplied inputs.
The source density bounds object is defined from the supplied inputs.
Definition (Lean source)
The target density bounds object is defined from the supplied inputs.
Definition (Lean source)
The source density holder object is defined from the supplied inputs.
Definition (Lean source)
The target density holder object is defined from the supplied inputs.
Definition (Lean source)
The propensity overlap object is defined from the supplied inputs.
Definition (Lean source)
The propensity holder object is defined from the supplied inputs.
Definition (Lean source)
The arm means holder object is defined from the supplied inputs.
Definition (Lean source)
The receipt consistency object is defined from the supplied inputs.
Definition (Lean source)
The outcome consistency object is defined from the supplied inputs.
Definition (Lean source)
The instrument randomization object is defined from the supplied inputs.
Definition (Lean source)
The exclusion object is defined from the supplied inputs.
Definition (Lean source)
The monotonicity object is defined from the supplied inputs.
Definition (Lean source)
The conditional mean object is defined from the supplied inputs.
The transport complier outcome object is defined from the supplied inputs.
The positive strength object is defined from the supplied inputs.
Definition (Lean source)
The model class records that the supplied constants, law, and sample size satisfy the statistical assumptions of the transported CACE experiment.
Definition (Lean source)
@realizes n(common source-target sample size) @realizes \mathcal M_n(full model class)
Bounded arm means imply a contrast in the parameter interval. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The target density is nonnegative on its declared domain. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The one-dimensional Hölder condition supplies continuity on the covariate interval. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The target probability law normalizes its real density to one. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating a bounded arm contrast against the target probability density preserves its range for either observable. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Model membership bounds the positive first stage above by one. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The geometry object is defined without additional inputs.
Definition (Lean source)
The admissible geometry object is defined from the supplied inputs.
The fixed-geometry subclass records that the supplied model and geometry meet the required geometric restrictions.
Definition (Lean source)
The is interval partition object is defined from the supplied inputs.
Definition (Lean source)
The partition object is defined without additional inputs.
The finite-cell subclass records that the supplied model and partition meet the finite-cell restrictions.
Definition (Lean source)
The marked density vector object is defined from the supplied inputs.
Definition (Lean source)
The phi object is defined from the supplied inputs.
The known geometry envelope object is defined from the supplied inputs.
Definition (Lean source)
The known-geometry expected-length constant, computed from the noncoverage level and the density envelopes.
Definition (Lean source)
The known geometry radius object is defined from the supplied inputs.
Definition (Lean source)
The known geometry score object is defined from the supplied inputs.
Definition (Lean source)
The known geometry interval object is defined from the supplied inputs.
Definition (Lean source)
The restricted length object is defined from the supplied inputs.
Definition (Lean source)
Restricted Lebesgue length always lies between zero and two. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The expected length object is defined from the supplied inputs.
Definition (Lean source)
The honest intervals object is defined from the supplied inputs.
Definition (Lean source)
The strength slice object is defined from the supplied inputs.
Definition (Lean source)
The length frontier object is defined from the supplied inputs.
Definition (Lean source)
The unequal data law object is defined from the supplied inputs.
Definition (Lean source)
The unequal model class object is defined from the supplied inputs.
Definition (Lean source)
The unequal honest intervals object is defined from the supplied inputs.
Definition (Lean source)
The unequal sample frontier object is defined from the supplied inputs.
Definition (Lean source)
The unequal sample frontier question object is defined without additional inputs.
Definition (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse 2 declarations Mean-square bound for the exact seven-mark cubic score
Mean-square bound for the exact seven-mark cubic score
Model membership implies square integrability of the concrete estimator error, including the zero-statistic fallback at small sample sizes. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about marked cubic mse holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.Assembly 1 declarations Bias and variance assembly interface
Bias and variance assembly interface
Given the supplied inputs, the stated result about mse envelope positive holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.Blocks 4 declarations Exact deterministic four-block partition
Exact deterministic four-block partition
Given the supplied inputs, the stated result about block card holds.
Proof (Lean source)
Given the supplied inputs, the stated result about block size lower holds.
Formal statement
The training view object is defined from the supplied inputs.
The training sigma object is defined from the supplied inputs.
Definition (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.BoundedLinearScores 7 declarations Roadmap (19) uses bounded observation scores rather than the absolute cell-pair envelope in (15).
Density-free variance bounds for linear marked scores
Roadmap (19) uses bounded observation scores rather than the absolute cell-pair envelope in (15). Keeping the signed covariance sum gives a bound independent of the density envelope and of the number of cells.
A bounded score averaged over an actual iid block has variance at most its squared envelope divided by the block size. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The covariance quadratic form of cell histograms is the variance of the single-record cell score, with the exact iid normalization. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Bounded coefficients on disjoint cells produce a bounded source score, including outside the covariate support where all cell scores vanish. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The target score has the same cell-disjointness bound, with unit marks. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The signed source cell-pair sum retains cancellation and costs only C² / m, with no density or resolution factor. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The target channel obeys the identical density-free variance bound. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The signed covariance bound survives the flattening of the actual source and target experiment, for every marked coordinate. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.Cancellation 3 declarations Exact cancellation of one within-cell projection residual
Exact cancellation of one within-cell projection residual
The cell average object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about one residual cell cancellation holds.
Formal statement
Proof (Lean source)
Any cell-constant Taylor coefficient and any finite collection of cell-constant projected factors can multiply one residual without changing its zero integral. This covers every one-residual quadratic and cubic term. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.CellMoments 37 declarations Product-law and bounded-mark facts for histogram cells
Product-law and bounded-mark facts for histogram cells
The three sampling assumptions identify the full observed-data law with the product of the source and target iid laws. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A single dependent product carrier for the source and target arrays. This is the carrier expected by the conditional independence lemmas for coordinate blocks. For the displayed assumptions and inputs, the stated object is defined.
The flat obs object is defined from the supplied inputs.
The flat obs measurable space object is defined from the supplied inputs.
Definition (Lean source)
The flat law object is defined from the supplied inputs.
Definition (Lean source)
The flatten sample object is defined from the supplied inputs.
Definition (Lean source)
The model assumptions identify the flattened sample with one dependent Measure.pi. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The flat block object is defined from the supplied inputs.
Given the supplied inputs, the stated result about inl mem flat block holds.
Formal statement
Given the supplied inputs, the stated result about inr mem flat block holds.
Formal statement
Given the supplied inputs, the stated result about block idx disjoint holds.
Formal statement
Given the supplied inputs, the stated result about flat block disjoint holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about flat block training disjoint holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about flat block eval pairwise holds.
Formal statement
Proof (Lean source)
The flat mask object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about flatten sample training view holds.
Formal statement
Proof (Lean source)
The flat reconstruct object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about measurable flat reconstruct holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about flat reconstruct proj eq mask holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about proj flat mask eq proj holds.
Formal statement
Proof (Lean source)
The flat training proj object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about flat training proj training view holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about training view eq unflatten reconstruct proj holds.
Formal statement
Proof (Lean source)
The paper's zero-filled training view generates the same sigma algebra as the flattened finite-coordinate projection used by the conditional product library. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The target marginal is a probability measure. Positivity of the conditioning event is forced by the strictly positive density lower envelope. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source obs law is probability measure holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about flat law is probability measure holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about measurable set cell holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about cell subset covariate space holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about volume cell holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about cell disjoint holds.
Formal statement
Proof (Lean source)
Either source or target covariate mass of one regular cell is at most C_f / K. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source cell mass le holds.
Formal statement
Proof (Lean source)
Conditional expectations given the paper's training view are the pullbacks of conditional expectations given block zero in the flattened product experiment. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about measurable channel x holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about measurable channel mark holds.
Formal statement
Proof (Lean source)
Every empirical channel mark is deterministically between zero and one. The outcome channels are clipped in the statistic itself. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.CenteredCubicCells 7 declarations This proves the three-residual member of roadmap (16) for the actual marked histograms, with bounded training-measurable coefficients.
Conditional variance of the fully centered cubic cell component
This proves the three-residual member of roadmap (16) for the actual marked histograms, with bounded training-measurable coefficients. The block covariance factorization is derived from the product experiment, rather than supplied as a premise of the variance bound.
A held-out cell histogram centered at its exact experiment mean. For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
The fully centered three-block product in a single histogram cell. For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
Independence of the three evaluation blocks preserves square integrability of their centered histogram product. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The fully centered cubic histogram cell product has zero training-conditional mean, derived from the disjoint evaluation blocks. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The conditional cross moment of actual centered cubic histogram products is exactly the product of three blockwise histogram covariances. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The three-residual part of the exact cubic histogram sum satisfies the K² / m³ + 1 / m³ conditional variance bound in roadmap (16). The training coefficient can be random; only its measurability and envelope are needed. Covariance factorization is proved above for the actual histograms. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The flattened centered product is precisely the product of the paper's three held-out marked histograms at a cell midpoint, each minus its exact mean. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.CenteredPairCells 3 declarations Roadmap (16) for two actual centered histograms on distinct evaluation blocks.
Two-residual contributions to quadratic and cubic variance
Roadmap (16) for two actual centered histograms on distinct evaluation blocks. The same statement handles all three two-block subsets of the cubic statistic.
The product of two centered cell heights on distinct evaluation blocks. For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
The two-residual member obeys the exact C² V² (K+1)/(n/5)² conditional variance estimate, derived from disjoint-block independence. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The flattened pair is exactly the product of two of the paper's marked histograms at a cell midpoint, centered at their experiment means. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.CenteredSingleCells 1 declarations Roadmap (16) for a single centered histogram factor, with the actual finite product experiment and a bounded training-measurable cell coefficient.
One-residual contributions to quadratic and cubic variance
Roadmap (16) for a single centered histogram factor, with the actual finite product experiment and a bounded training-measurable cell coefficient.
The one-residual member of the subset expansion obeys the exact 2 C² V / (n/5) conditional variance estimate. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.CombinedBias 4 declarations This module proves roadmap (14) for the exact integrated Taylor remainder and the exact quadratic and cubic projection errors, with constant 3(BR+BQ+BC).
Combined spatial Taylor and projection bias
This module proves roadmap (14) for the exact integrated Taylor remainder and the exact quadratic and cubic projection errors, with constant 3(BR+BQ+BC). The identification with the full statistic's conditional bias remains separate.
The integrated exact third-order Taylor remainder. For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
The spatial cubic Taylor term minus its exact projection mean. For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
Three real summands cost at most three times their squared norms. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (14): the exact spatial Taylor remainder plus the quadratic and cubic projection errors has the paper's combined squared-bias bound. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.ConditionalBlockCovariance 4 declarations These adapters derive centering and cross-moment factorization from disjoint blocks of a finite product experiment.
Conditional moments of centered held-out block scores
These adapters derive centering and cross-moment factorization from disjoint blocks of a finite product experiment.
Given the supplied inputs, the stated result about cond exp block score eq integral holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about cond exp centered block score zero holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about cond exp centered block cross eq covariance holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about cond cov centered three block eq prod covariance holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.ConditionalCellSum 5 declarations Roadmap (16) follows by expanding the square under conditional expectation, using the factored block covariances, and counting diagonal and off-diagonal cell pairs.
Conditional second moments of centered cell sums
Roadmap (16) follows by expanding the square under conditional expectation, using the factored block covariances, and counting diagonal and off-diagonal cell pairs. Training coefficients may depend on the conditioned observation.
The conditional second moment of a finite sum is its ordered cross-moment sum. No independence between the cells is needed. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional version of the diagonal/off-diagonal cell-pair bound. The cross-moment identity is supplied by independent evaluation blocks and the training-coefficient pull-out lemma. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A normalized cell sum of conditionally centered summands is conditionally centered, even when its coefficients depend on training. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact normalized diagonal/off-diagonal bound in roadmap (16), for q+1 centered residual blocks. Taking q=0,1,2 gives all nonempty subsets in the quadratic and cubic expansions. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional variance of the normalized cell sum equals its centered second moment and satisfies the factored bound. This joins conditional centering with the cell-pair computation rather than assuming a variance estimate. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.CubicBiasMoments 4 declarations The spatial L1 pilot moments and the exact single-residual cancellation bound give the squared cubic bias, retaining both resolution powers in roadmap (13) before dyadic sample-rate conversion.
Second moment of the exact cubic projection bias
The spatial L1 pilot moments and the exact single-residual cancellation bound give the squared cubic bias, retaining both resolution powers in roadmap (13) before dyadic sample-rate conversion.
Squaring an affine finite-error bound costs twice the squared offset and twice the coordinate count times the sum of coordinate second moments. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Dyadic rounding and the exact block size control every nonnegative power of the inverse cubic resolution, with the constants in roadmap (13). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The squared spatial L1 pilot error is integrable: joint measurability and clipping provide a uniform bound on the unit covariate interval. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact spatial cubic bias has the two second-moment terms of roadmap (13): the squared resolution modulus times the pilot L1 rate, and the sixth power of that modulus. No stochastic content is assumed. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.CubicBiasRate 2 declarations The two terms in roadmap (13) have rates n^(-7/10) and n^(-3/4).
Sample rate of the exact spatial cubic projection bias
The two terms in roadmap (13) have rates n^(-7/10) and n^(-3/4). Dyadic rounding and exponent comparison give the stated BC n^(-2/3) bound.
Convert both resolution powers in the cubic squared-bias bound, keeping exactly the computable constant BC from roadmap (13). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact spatial cubic Taylor term minus the exact cubic projection mean has the sample-size bound (13), with the paper's BC constant. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.CubicBlockCovariance 4 declarations Uniform covariance bounds for flattened histogram blocks
Uniform covariance bounds for flattened histogram blocks
Given the supplied inputs, the stated result about measurable iid block height holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about iid block height mem lp of unit interval holds.
Formal statement
Proof (Lean source)
The covariance of two flattened block heights is bounded uniformly over source and target channels on the same histogram cell. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The covariance of two flattened block heights is bounded uniformly over source and target channels on distinct histogram cells. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.CubicDerivative 21 declarations Second and third coordinate derivative envelopes at the clipped pilot
Second and third coordinate derivative envelopes at the clipped pilot
The density vector object is defined without additional inputs.
Definition (Lean source)
The density coord object is defined from the supplied inputs.
Definition (Lean source)
The cubic ratio term object is defined from the supplied inputs.
Definition (Lean source)
The cubic ratio d1 object is defined from the supplied inputs.
Definition (Lean source)
The cubic ratio d1 apply object is defined from the supplied inputs.
Definition (Lean source)
The cubic ratio d2 apply object is defined from the supplied inputs.
Definition (Lean source)
The cubic ratio d3 apply object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about has fderiv at cubic ratio term holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about cubic ratio d1 apply holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about fderiv cubic ratio d1 apply holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about fderiv cubic ratio d2 apply holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about iterated fderiv one cubic ratio term holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about iterated fderiv two cubic ratio term holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about iterated fderiv three cubic ratio term holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about iterated fderiv three phi holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about iterated fderiv two phi holds.
Formal statement
Proof (Lean source)
The explicit second derivative of one marked ratio has a uniform coordinate bound. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The second coordinate derivative has the same deterministic envelope as orders zero and one. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about cubic ratio d3 basis abs le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about d phi3 abs le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about pilot mem clipping rectangle holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.CubicProjectionBias 6 declarations The cubic Taylor projection error is assembled from the exact cell errors.
Exact spatial cubic projection bias
The cubic Taylor projection error is assembled from the exact cell errors. Nested pilot cells identify it with the spatial Taylor term minus the exact conditional mean, retaining all seven coordinates and the factor one sixth.
The exact cubic projection error summed over coordinates and cells. For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
The midpoint cell sum is the exact cubic Taylor term minus the projection polynomial appearing in the conditional mean. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Nested pilot constancy identifies the cubic cell bias with the true spatial cubic Taylor term minus its exact conditional projection mean. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing midpoint-frozen cellwise pilot errors gives their exact spatial L1 norm. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (12): after exact single-residual cancellation, the global cubic bias retains the pilot L1 error, with the constants C1 and C2 of the paper. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The pilot-sensitive roadmap (12) bound applies to the spatial cubic Taylor term and the exact projection mean, without extra premises. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.CubicResolution 2 declarations Elementary bounds for the cubic dyadic resolution
Elementary bounds for the cubic dyadic resolution
Given the supplied inputs, the stated result about cubic resolution le block size holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about cubic resolution le n holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.CubicVariance 3 declarations Constants for the cubic conditional variance calculation
Constants for the cubic conditional variance calculation
The cubic variance constant object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about cubic conditional variance with mem lp holds.
Formal statement
Proof (Lean source)
The exact cubic correction variance bound. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.ExactBiasAssembly 12 declarations This module turns the exact quadratic and cubic cell projection identities into quantitative bounds.
Cellwise projection-bias assembly for the exact cubic statistic
This module turns the exact quadratic and cubic cell projection identities into quantitative bounds. It isolates the deterministic part of the bias calculation from the conditional-expectation argument for the held-out histogram blocks.
In a decomposition into a conditionally centered fluctuation and a training-measurable shift, the shift is the exact conditional mean. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A normalized finite cell sum remains conditionally centered after multiplication by cellwise training-measurable coefficients. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A single centered held-out histogram cell has zero conditional mean given the training block. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The product of two centered held-out histogram cells from distinct evaluation blocks has zero conditional mean given training. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The training-measurable quadratic projection polynomial: every held-out residual is replaced by its exact cell-mean shift. For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
The training-measurable cubic projection polynomial: every held-out residual is replaced by its exact cell-mean shift. For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
The explicit finite-sum formula defining the quadratic projection mean. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The explicit finite-sum formula defining the cubic projection mean. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The quadratic projection polynomial is measurable with respect to the training sigma algebra. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The cubic projection polynomial is measurable with respect to the training sigma algebra. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A marked-density coordinate differs from its cell average by at most the common Hölder modulus times the cell width. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The integral of a quadratic Taylor monomial loses only the product of two within-cell projection residuals. Its absolute size is bounded explicitly. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.ExactConditionalMeans 1 declarations This module exports the exact training-conditional means of both held-out histogram corrections.
Exact conditional means of the quadratic and cubic corrections
This module exports the exact training-conditional means of both held-out histogram corrections. The quadratic proof is split into its own dependency; this file supplies the cubic identity.
The exact training-conditional mean of the cubic correction is its cellwise projection polynomial. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.ExactConditionalMeansQuadratic 1 declarations This module identifies the training-conditional mean of the held-out quadratic histogram correction with its deterministic cellwise projection polynomial.
Exact conditional mean of the quadratic correction
This module identifies the training-conditional mean of the held-out quadratic histogram correction with its deterministic cellwise projection polynomial.
The exact training-conditional mean of the quadratic correction is its cellwise projection polynomial. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.ExactFluctuation 3 declarations The pilot integral cancels from the fluctuation about the projected mean.
Exact estimator fluctuation and its integrated variance bound
The pilot integral cancels from the fluctuation about the projected mean. The three exact conditional means then identify this fluctuation with the centered corrections in roadmap (20).
The full estimator fluctuation is exactly the sum of the three centered corrections, almost surely under the two-sample experiment. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The fluctuation of the exact full statistic is square integrable, using square integrability already established by the component variance proofs. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (20) bounds the unconditional second moment of the exact full estimator's fluctuation about its projected mean. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.ExactStatisticBridge 23 declarations This file identifies the abstract block-centering constants with the marked-density cell averages used by the quadratic and cubic statistics.
Exact bridges from histogram residuals to centered block scores
This file identifies the abstract block-centering constants with the marked-density cell averages used by the quadratic and cubic statistics. It also records that the clipped pilot and its Taylor coefficients are measurable with respect to the training block.
The mean of every flattened held-out block height is the corresponding marked-density cell average. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
At a cell midpoint, each exact histogram residual is its block-centered score plus the training shift from the true cell average to the clipped pilot. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A training-block channel covariate is unchanged by the training view. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A training-block channel mark is unchanged by the training view. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The block-zero histogram only sees the training view. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The clipped pilot only sees the training view. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A fixed pilot coordinate is measurable in the full sample. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A fixed pilot coordinate is strongly measurable with respect to the training σ-algebra. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
At the clipped pilot, the second derivative coefficient equals its explicit rational formula. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
At the clipped pilot, the third derivative coefficient equals its explicit rational formula. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every quadratic Taylor coefficient evaluated at the clipped pilot is strongly measurable with respect to the training σ-algebra. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every cubic Taylor coefficient evaluated at the clipped pilot is strongly measurable with respect to the training σ-algebra. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact quadratic residual product, after removing its training-only part, is the sum of its three nonempty centered subsets. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact cubic residual product, after removing its training-only part, is the sum of its seven nonempty centered subsets. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A single centered held-out cell score is square integrable under the flattened product experiment. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A product of centered scores from two distinct evaluation blocks is square integrable under the flattened product experiment. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Unflattening the product experiment is measurable from the block-zero sigma algebra to the paper's training sigma algebra. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Pilot coordinates pulled back to the flattened experiment are measurable with respect to block zero. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Quadratic derivative coefficients pulled back to the flattened experiment are measurable with respect to block zero. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cubic derivative coefficients pulled back to the flattened experiment are measurable with respect to block zero. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every marked-density coordinate is nonnegative and bounded by the common model envelope. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A marked-density cell average has absolute value at most the common model envelope. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The deterministic training shift in every residual is bounded by the uniform envelope used by the variance constants. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.FinalAssembly 9 declarations Final mean-square assembly for the exact cubic estimator
Final mean-square assembly for the exact cubic estimator
The pilot plug-in integral only uses the training sample. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact projected estimator mean only uses the training sample. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The squared error of the exact projected mean is integrable. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A variable minus its conditional expectation is conditionally centered. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrability follows from square integrability after conditional centering. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact estimator fluctuation has zero training-conditional mean. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The fluctuation is orthogonal to the training-measurable projected bias. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Squared error is the sum of fluctuation risk and projected squared bias. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact fluctuation and projected-bias bounds assemble to the frozen mean-square envelope. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.FlatHistogramBlocks 11 declarations Histogram scores on flattened held-out blocks
Histogram scores on flattened held-out blocks
The flat block height object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about measurable flat block height holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about flat block height proj holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about flat block height proj target holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about flat block height proj source holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about covariance flat law source holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about covariance flat law target holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about covariance flat law source target zero holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about flat block height nonneg holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about flat block height le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about flat block height mem lp holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.FourthDerivative 6 declarations Explicit differentiation of the two marked ratios completes the roadmap's fourth-order envelope on the deterministic clipping rectangle.
Fourth coordinate derivative of the observable transport integrand
Explicit differentiation of the two marked ratios completes the roadmap's fourth-order envelope on the deterministic clipping rectangle.
The cubic ratio d4 apply object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about fderiv cubic ratio d3 apply holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about iterated fderiv four cubic ratio term holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about iterated fderiv four phi holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about cubic ratio d4 basis abs le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about d phi4 abs le holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.HistogramCellRepresentation 5 declarations Histogram cell heights as iid block averages
Histogram cell heights as iid block averages
Given the supplied inputs, the stated result about midpoint mem cell holds.
Proof (Lean source)
Given the supplied inputs, the stated result about midpoint mem cell iff holds.
Proof (Lean source)
Given the supplied inputs, the stated result about source cell mark eq channel mark holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about marked histogram midpoint target holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about marked histogram midpoint source holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.IidBlockAverage 6 declarations Covariance of iid block histogram heights
Covariance of iid block histogram heights
The iid block height object is defined from the supplied inputs.
Given the supplied inputs, the stated result about covariance iid block height holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source iid block height same cell covariance le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source iid block height off cell covariance le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about target iid block height same cell covariance le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about target iid block height off cell covariance le holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.IntegratedRemainder 6 declarations Jensen and Fubini turn the clipped pilot eighth moment into the integrated remainder bound in roadmap (9), without adding regularity assumptions.
Spatial integration of the cubic Taylor remainder
Jensen and Fubini turn the clipped pilot eighth moment into the integrated remainder bound in roadmap (9), without adding regularity assumptions.
A bounded nonnegative majorant controls the square of a spatial integral by its second moment under a probability measure. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Joint measurability and a bounded majorant justify Fubini in the integrated second-moment estimate. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The histogram is jointly measurable in the sample and covariate. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Clipping preserves joint measurability of the pilot. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The true marked density, extended by zero outside its covariate domain, is measurable; continuity on that domain provides this regularity. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (9): the expected square of the spatially integrated exact cubic Taylor remainder is bounded by the clipped pilot eighth moment. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.LinearCellVariance 2 declarations Training coefficients pull out of the exact cell cross moments.
Conditional second moments of bounded linear cell scores
Training coefficients pull out of the exact cell cross moments. The signed covariance quadratic form is bounded by the single-record envelope, yielding the density-free per-coordinate bound needed in roadmap (19).
The conditional square of a weighted normalized cell sum equals its signed covariance quadratic form, keeping cancellation between cells. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each bounded training-weighted marked coordinate in a held-out block has conditional second moment at most 5 C² / n. This is the sharp per-coordinate ingredient of the linear variance estimate (19). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.LinearProjectionMean 5 declarations The spatial linear Taylor term has no projection bias: on any refinement of the pilot partition it is exactly the weighted sum of cell-average shifts.
Exact finite-cell representation of the linear projected mean
The spatial linear Taylor term has no projection bias: on any refinement of the pilot partition it is exactly the weighted sum of cell-average shifts.
A linear cell integral is exactly its cell-average shift times cell width. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The linear projected mean has an exact finite-cell formula on every refinement of the pilot partition, with no spatial approximation error. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The first coordinate derivative has the explicit rational formula on its natural domain, where both assignment densities are nonzero. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The linear coefficient evaluated at the clipped pilot is measurable with respect to training; no held-out observation enters this coefficient. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The spatial linear projected mean is training measurable, as follows from its exact finite-cell representation. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.LinearStatisticBridge 8 declarations The empirical linear correction and its pilot subtraction are represented on the pilot partition.
Exact cell representation of the held-out linear statistic
The empirical linear correction and its pilot subtraction are represented on the pilot partition. This connects the actual observation-level statistic to the centered histogram scores used in the conditional moment arguments.
An arbitrary function of the pilot integrates exactly as a midpoint sum on any refinement of the pilot partition. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A pilot coefficient at an observed covariate equals its unique cell coefficient. The support condition is supplied by the model's covariate law. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observation-level marked average is exactly a weighted histogram midpoint sum. This uses the actual block normalization, including unequal block sizes, and holds whenever its observations lie in the covariate region. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
On samples in the covariate support, the exact linear correction is the cell sum of pilot coefficients times block-one histogram residuals. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every recorded covariate lies in the covariate region almost surely under the model's actual two-sample experiment. Both marginal density identities are used, and no support hypothesis is added to the model. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact held-out linear statistic is almost surely a centered block-one cell sum plus its spatial projected mean. This is the genuine statistic bridge needed for its conditional mean and variance. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The first derivative uses the same explicit envelope as the higher Taylor coefficients. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The held-out linear correction has exactly its spatial linear Taylor term as conditional mean. Training coefficients pull out of the conditional expectation, and the centered block-one histograms have mean zero. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.LinearVariance 2 declarations The exact observation statistic is represented by its centered pilot-cell sum.
Conditional variance of the exact held-out linear correction
The exact observation statistic is represented by its centered pilot-cell sum. Bounded training derivatives and the signed iid covariance bound give roadmap (19), with the stated constant and no added assumptions.
Roadmap (19) for the actual linear correction, conditioned on the two training blocks. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (19) for the exact linear correction. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.MarkedCellCovariance 21 declarations Single-record marked cell covariance bounds
Single-record marked cell covariance bounds
The source cell mark object is defined from the supplied inputs.
Definition (Lean source)
The source cell score object is defined from the supplied inputs.
Definition (Lean source)
The target cell score object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about source cell mark mem unit interval holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about measurable source cell mark holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about measurable source cell score holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about measurable target cell score holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source cell score mem unit interval holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about target cell score mem unit interval holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source cell score le indicator holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about target cell score le indicator holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about mem lp two of mem unit interval holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about integral bounded score le measure real holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about abs covariance bounded on event holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about abs covariance le sq of cross zero holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about abs covariance bounded on disjoint events holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source event mass le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source same cell covariance le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source off cell covariance le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about target same cell covariance le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about target off cell covariance le holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.NestedCells 5 declarations Dyadic divisibility puts each evaluation cell inside a pilot cell.
Nested evaluation cells and the clipped pilot
Dyadic divisibility puts each evaluation cell inside a pilot cell. Consequently histograms, the clipped pilot, and Taylor coefficients are constant there, including the closed right endpoint of the final cell.
Increasing the exponent preserves divisibility of the exact dyadic resolutions. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Both correction resolutions refine the pilot partition. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
For an integer refinement, every fine cell is contained in a coarse cell. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A marked histogram takes the same value at any two points in one cell. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
On any partition refining the pilot partition, the pilot equals its midpoint value throughout each cell. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.PilotEighthMoment 9 declarations The bounded iid sum theorem cancels singleton index patterns and counts the survivors.
Eighth-moment closure for the exact clipped pilot
The bounded iid sum theorem cancels singleton index patterns and counts the survivors. Scaling the bin sums, transferring them to the two-sample experiment, and applying clipping and the dyadic resolution bounds gives equation (5).
Normalize the exact eighth-moment bound for a bounded iid bin sum. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The one-record covariance envelope implies the roadmap's variance factor. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact source bin height has the eighth-moment bound in equation (3). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact target bin height has the eighth-moment bound in equation (3). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Transfer the eighth bin moment to the actual source sample channel. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Transfer the eighth bin moment to the actual target sample channel. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
All seven observable histogram channels obey equation (3). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The bounded histogram makes its centered eighth power integrable for every fixed cell. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about pilot eighth moment holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.PilotMoments 12 declarations Clipped pilot moment bounds
Clipped pilot moment bounds
Given the supplied inputs, the stated result about abs clip sub le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about pilot error le histogram error holds.
Formal statement
Proof (Lean source)
The one-dimensional Hölder-ball condition controls function increments. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
All seven marked densities have the common Hölder modulus used in the pilot analysis. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Splitting an error at an intermediate value costs at most the factor 2⁷ in its eighth power. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The clipped pilot's eighth-power error splits into histogram fluctuation and deterministic bias. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every centered bounded bin mark lies in the unit ball. This controls all multiplicities in the eighth-power index-pattern expansion. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every multiplicity of at least two is controlled by the centered second moment of a bounded bin mark. Independence can then multiply these bounds over the distinct indices in a surviving eighth-power term. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Centering a bounded bin mark removes the singleton moment exactly. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
In the product experiment, any monomial with a singleton sample index has zero expectation. This is the exact cancellation used before counting the surviving eighth-power index patterns. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
For a surviving monomial, independence bounds the product of the multiplicity moments by one variance factor per distinct sample index. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The pilot eighth constant object is defined from the supplied inputs.
Definition (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.PilotProjection 12 declarations The seven marked densities have Hölder modulus 3 (1 + C_f) L.
Deterministic cell projection bias for the clipped pilot
The seven marked densities have Hölder modulus 3 (1 + C_f) L. Cell averaging
therefore introduces at most this modulus times the cell width to power 1/8.
Together with clipping contraction, this separates eighth-power pilot error
into histogram fluctuation and a deterministic projection contribution.
Two points in the same histogram cell are separated by at most its width. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging on a cell preserves a uniform bound on oscillation around a fixed value. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each marked density is continuous on the covariate interval. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The marked-density projection bias is bounded by the common Hölder modulus times cell width. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The clipped pilot's eighth-power error is controlled by its centered histogram fluctuation plus the explicit H⁸/K₀ projection-bias contribution. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The deterministic eighth-power pilot bias has precisely the constant in equation (6). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Clipping and the exact dyadic bias rate reduce the pointwise pilot error to its centered histogram fluctuation, without a stochastic bound as a premise. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
After removing the two one-residual terms, the quadratic projection error is exactly the product of the two within-cell residuals. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The cubic projection error has precisely the three two-residual terms and the three-residual term; every single-residual contribution cancels. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Within-cell marked-density residuals retain the already proved continuity. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Exact quadratic Taylor projection identity for the actual marked densities and arbitrary cell values of the pilot and Taylor coefficient. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Exact cubic Taylor projection identity for the actual marked densities. Only products with two or three within-cell residuals survive integration. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.PilotSampling 11 declarations This implements the mean and fluctuation calculation in equation (2) of the marked-cubic proof for the bounded, observable bin scores.
Exact means and second moments of the pilot bin averages
This implements the mean and fluctuation calculation in equation (2) of the marked-cubic proof for the bounded, observable bin scores. The eighth-moment index-pattern calculation remains a separate step.
A normalized block height has mean K times the one-record bin mean. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Centering at the exact bin mean turns the second moment into self-covariance. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact source bin average obeys the roadmap's V K / m bound. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact target bin average obeys the same V K / m bound. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The target bin probability is the integral of its marked density. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The target block height is unbiased for the exact Lebesgue cell average. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The target histogram in the actual two-sample experiment satisfies equation (2). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Clipping the source mark preserves its observable mean, since outcomes lie in [0,1]. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every source bin height is unbiased for its marked-density cell average. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every source histogram in the actual two-sample experiment satisfies equation (2). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
All seven actual marked histogram channels satisfy the common cellwise second-moment bound. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.PilotSecondMoment 8 declarations The exact bin variance and Hölder projection bias give equation (5)'s second-moment bound, with the constant A₂ used in the cubic projection bias.
The clipped pilot's second-moment rate
The exact bin variance and Hölder projection bias give equation (5)'s second-moment bound, with the constant A₂ used in the cubic projection bias.
Histogram heights are constant throughout each cell, including its endpoint convention. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
At a fixed point, the bounded bin statistic is measurable in the data. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A cell histogram lies between zero and its normalization K. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Fixed centered histogram squares are integrable; their deterministic bound supplies regularity. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Clipping, bin variance, and the exact Hölder cell bias control pilot risk before rate substitution. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The dyadic pilot bias has the exact second-moment constant from equation (6). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every covariate belongs to a histogram cell; the final cell includes one. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The clipped pilot satisfies the second-moment part of equation (5), with exactly A₂ from equation (6), uniformly over the seven channels and [0,1]. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.QuadVariance 3 declarations Constants for the quadratic conditional variance calculation
Constants for the quadratic conditional variance calculation
The quad variance constant object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about quadratic conditional variance with mem lp holds.
Formal statement
Proof (Lean source)
The exact quadratic correction variance bound. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.QuadraticProjectionBias 6 declarations The exact cell cancellation identity gives the deterministic quadratic bias bound.
Summed quadratic projection bias
The exact cell cancellation identity gives the deterministic quadratic bias bound. Dyadic rounding and the block-size lower bound give its squared sample-size rate, with the constant BQ in roadmap (11).
The quadratic Taylor projection error, summed over all marked coordinates and cells with the pilot frozen at each cell midpoint. For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
Exact cancellation of the single-residual terms bounds the total quadratic projection bias by half the coordinate count squared times the derivative and squared Hölder envelopes. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The inverse quadratic resolution has the explicit rate required by the quadratic projection bias, including the factor lost to dyadic rounding. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The squared exact cellwise quadratic projection bias obeys roadmap (11) with the computable constant used in the MSE envelope. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The summed cell bias is exactly the midpoint-frozen quadratic Taylor integral minus the projection polynomial that is the statistic's conditional mean. This identity keeps the exact coefficient and all seven coordinates. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The deterministic quadratic bias bound also holds after averaging over training data, without any extra regularity premise. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.RemainderMajorant 4 declarations The nonnegative fourth-order pilot-error envelope has an integrable square and the exact BR bound.
Integrable majorant for the integrated Taylor remainder
The nonnegative fourth-order pilot-error envelope has an integrable square and the exact BR bound. This permits combining bias components without assuming measurability or integrability of their Taylor representations.
The spatial integral of the fourth-order Taylor remainder envelope. For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
Clipping and the eighth pilot moment give an integrable squared remainder envelope and the exact second-moment constant BR. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact spatial Taylor remainder is dominated by its nonnegative, integrable spatial envelope. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The remainder envelope has the common n^(-2/3) rate needed in (14). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.RemainderMoments 4 declarations The finite-dimensional Jensen inequality and the clipped pilot eighth moment control the squared remainder with the constants in roadmap (9).
Pointwise second moment of the exact cubic Taylor remainder
The finite-dimensional Jensen inequality and the clipped pilot eighth moment control the squared remainder with the constants in roadmap (9). The spatial integral and the projection-bias assembly remain separate proof obligations.
Given the supplied inputs, the stated result about sum abs eighth le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about clipping rectangle coordinate abs le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about integrable pilot error eighth holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about pilot phi cubic taylor remainder second moment holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.ResolutionBounds 8 declarations These bounds implement equation (1) of the marked-cubic MSE proof, including its exact floor-based resolutions and the block-size conversion to sample size.
Dyadic resolutions and the deterministic pilot bias rate
These bounds implement equation (1) of the marked-cubic MSE proof, including its exact floor-based resolutions and the block-size conversion to sample size.
Every block is nonempty above the threshold. Under the displayed assumptions and inputs, the stated conclusion holds.
Proof (Lean source)
The exact block size never exceeds the sample size. Under the displayed assumptions and inputs, the stated conclusion holds.
Proof (Lean source)
Rounding down a base-two logarithm loses at most a factor of two. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The pilot resolution has exactly the bounds used for its moments. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The quadratic resolution has exactly the bounds used for its variance and bias. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The inverse pilot resolution supplies the deterministic eighth-power bias rate. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every nonnegative power of the pilot fluctuation scale has its explicit sample-size rate. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Both histogram fluctuation terms in the eighth-moment roadmap are bounded at rate n⁻⁴ᐟ⁵. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.SharpProjectionBias 5 declarations The surviving two-residual terms retain the absolute training shifts rather than a uniform envelope.
Pilot-sensitive cubic projection bias
The surviving two-residual terms retain the absolute training shifts rather than a uniform envelope. This is the cellwise estimate needed in roadmap (12). The integrated pilot moment supplies the L1 control in roadmap (7).
The four surviving cubic residual terms are bounded while retaining each projected pilot error as a factor. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Exact single-residual cancellation yields a cubic cell bias bound with three individual projected pilot errors, as required by roadmap (12). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A projected error divided by the cell resolution is at most the cell's L1 error; no uniform bound on the pilot error is substituted. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (7): the clipped pilot's spatial L1 error has the same squared moment rate as its pointwise error, by Jensen and Fubini. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact cubic Taylor coefficient gives a cell bias controlled by the three L1 pilot errors and the third power of the Hölder projection modulus. Summing this inequality yields the constants C1 and C2 in roadmap (12). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.SpatialProjectionBridge 5 declarations The pilot is constant on each nested cell, so the spatial quadratic Taylor term is exactly the midpoint-frozen cell sum.
Spatial Taylor terms and exact projection means
The pilot is constant on each nested cell, so the spatial quadratic Taylor term is exactly the midpoint-frozen cell sum. Its difference from the exact conditional quadratic mean has the already established BQ bound.
The histogram cells form an exact finite partition, including the endpoint one. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integration of a Taylor monomial is exactly the sum over nested cells with its pilot and coefficient frozen at the cell midpoint. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every spatial Taylor monomial with exactly one within-cell residual has zero cell integral: the pilot-derived coefficient and all projected factors are constant on that cell. This covers every quadratic and cubic single-residual term without an extra constancy premise. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact quadratic projection bias is the spatial quadratic Taylor term minus the exact conditional mean of the quadratic statistic. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (11) applies directly to the true spatial Taylor term, without a midpoint approximation or any extra assumption on the training data. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.SpatialTaylorAssembly 14 declarations These identities connect the Fréchet Taylor remainder to the coordinate sums used in the exact quadratic and cubic projection means.
Coordinate and spatial assembly of the exact Taylor polynomial
These identities connect the Fréchet Taylor remainder to the coordinate sums used in the exact quadratic and cubic projection means.
Expansion of a multilinear form on the diagonal in the estimator's basis. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reindexing a sum over a finite tuple by its first entry and its tail. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The first Fréchet Taylor term is the exact coordinate linear polynomial. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The second Fréchet Taylor term is the exact ordered coordinate sum. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The third Fréchet Taylor term is the exact ordered coordinate sum. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A function continuous in the spatial argument at each fixed pilot value is integrable on the compact covariate region: the pilot has finitely many values. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every spatial coordinate Taylor monomial is integrable, without additional regularity assumptions on the data or a pilot-dependent coefficient. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
If a function satisfies the stated Hölder condition, then it is continuous on the covariate region.
Formal statement
Proof (Lean source)
The exact spatial Taylor polynomial and remainder integrate to the transported form. All ordered coordinate sums retain their factorial factors. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The spatial linear Taylor term, the proposed conditional mean of the held-out linear statistic in roadmap (10). For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
The projected mean of the exact cubic statistic. Identification with conditional expectation still requires the held-out linear mean identity. For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
The exact projected mean has precisely the three spatial errors from roadmap (14), with a common negative sign. No bias term is omitted. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact projected mean's squared bias is the expression already bounded by combined_spatial_projection_bias_second_moment in roadmap (14). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (14) holds for the exact projected estimator mean, with the paper's explicit constant 3(BR+BQ+BC). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.SubsetAggregation 2 declarations Cell-pair aggregation for one, two, or three residual blocks
Cell-pair aggregation for one, two, or three residual blocks
The diagonal/off-diagonal cell-pair estimate uniformly for any finite number q of factored residual blocks. The cubic proof consumes q=1,2,3. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Variance of a cell sum after a q-block conditional covariance has factored into its blockwise cell-pair covariances. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.TaylorRemainder 5 declarations Exact cubic Taylor remainder for the marked transport integrand
Exact cubic Taylor remainder for the marked transport integrand
The remainder after the degree-three Taylor polynomial of a marked ratio has an exact factored rational expression. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Bounding the factored remainder uses only endpoint denominator bounds and the sum of the absolute coordinate increments. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Two distinct coordinate increments are bounded by the full coordinate sum used in the Taylor remainder. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (8), with the paper's constant: the exact third-order Taylor polynomial of either transport channel leaves a fourth-order remainder. Both endpoints lie in the clipping rectangle, so all denominators are positive. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact clipped pilot and true marked-density vector satisfy the fourth-order Taylor bound used by the MSE proof, pointwise on the covariate support. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.TotalVariance 3 declarations The heterogeneous Cauchy--Schwarz inequality retains the three distinct paper constants and does not require independence between corrections.
Aggregation of the three exact centered correction variances
The heterogeneous Cauchy--Schwarz inequality retains the three distinct paper constants and does not require independence between corrections.
Conditional second moments of a finite sum are bounded by the cardinality times the sum of the individual bounds, even for dependent summands. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (20) for the sum of the three exact conditionally centered corrections. Square integrability is derived from the component proofs. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating the combined conditional bound gives the expected variance constant in roadmap (20). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.VarianceAggregation 2 declarations This module supplies the finite-family Cauchy--Schwarz step used to assemble the nonempty residual subsets in the quadratic and cubic statistics.
Finite conditional second-moment aggregation
This module supplies the finite-family Cauchy--Schwarz step used to assemble the nonempty residual subsets in the quadratic and cubic statistics.
Adding an integrable quantity measurable with respect to the conditioning sigma algebra does not change conditional centering. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A uniform conditional second-moment bound for a finite family controls the conditional second moment of its sum with the square of the family size. No independence between different family members is required. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.VarianceRates 6 declarations The dyadic resolution bounds convert the conditional variance ladders to roadmap (17)--(19), with the paper's constants.
Sample-rate bounds for the exact correction variances
The dyadic resolution bounds convert the conditional variance ladders to roadmap (17)--(19), with the paper's constants. These estimates apply to the exact held-out sums and retain their conditional centering.
The parametric variance rate is bounded by the target MSE rate. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The quadratic ladder has rate n⁻²ᐟ³ for the actual dyadic resolution. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Both higher cubic ladder terms are at most the parametric rate. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (17), after converting the exact quadratic resolution to sample size. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (18), after converting the exact cubic resolution to sample size. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap (19) expressed at the common target MSE rate. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.CubicMse.WeightedCenteredCells 1 declarations The coefficient pull-out and integrability argument in roadmap (16), uniformly for every nonempty subset of evaluation blocks.
Bounded training coefficients in centered cell averages
The coefficient pull-out and integrability argument in roadmap (16), uniformly for every nonempty subset of evaluation blocks.
Bounded training coefficients preserve the factored centered-cell variance estimate. The input cross moments are identities, rather than variance gates. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.Estimator 29 declarations Four-block marked histogram score and affine inversion
Four-block marked histogram score and affine inversion
The block idx object is defined from the supplied inputs.
The block size object is defined from the supplied inputs.
Definition (Lean source)
The dyadic resolution object is defined from the supplied inputs.
The pilot resolution object is defined from the supplied inputs.
Definition (Lean source)
The quadratic resolution object is defined from the supplied inputs.
Definition (Lean source)
The cubic resolution object is defined from the supplied inputs.
Definition (Lean source)
The cell object is defined from the supplied inputs.
The midpoint object is defined from the supplied inputs.
Definition (Lean source)
The source channel object is defined from the supplied inputs.
The channel x object is defined from the supplied inputs.
Definition (Lean source)
The channel mark object is defined from the supplied inputs.
Definition (Lean source)
The marked histogram object is defined from the supplied inputs.
Definition (Lean source)
The clip object is defined from the supplied inputs.
The clip channel object is defined from the supplied inputs.
Definition (Lean source)
The pilot object is defined from the supplied inputs.
Definition (Lean source)
The residual object is defined from the supplied inputs.
Definition (Lean source)
The basis object is defined from the supplied inputs.
The d phi1 object is defined from the supplied inputs.
The d phi2 object is defined from the supplied inputs.
The d phi3 object is defined from the supplied inputs.
The pilot integral object is defined from the supplied inputs.
The linear term object is defined from the supplied inputs.
Definition (Lean source)
The quadratic term object is defined from the supplied inputs.
Definition (Lean source)
The cubic term object is defined from the supplied inputs.
Definition (Lean source)
The cubic estimator object is defined from the supplied inputs.
Definition (Lean source)
The mse envelope object is defined from the supplied inputs.
Definition (Lean source)
The score radius object is defined from the supplied inputs.
Definition (Lean source)
The score inversion object is defined from the supplied inputs.
Definition (Lean source)
The score interval object is defined from the supplied inputs.
Definition (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.Identification_Part1 19 declarations Conditional IV identities and transported CACE
Conditional IV identities and transported CACE
Given the supplied inputs, the stated result about potential outcome difference holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about monotone receipt difference eq complier holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about potential outcome difference eq complier holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about conditional mean congr full ae holds.
Formal statement
Proof (Lean source)
the stated result about measurable complier holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about target cace mem parameter space holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about target integral eq density integral holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source set integral eq density integral holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about assignment slice eq with density holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about assignment slice integral eq holds.
Formal statement
Proof (Lean source)
The potential arm value object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about observed arm value eq potential arm value holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source arm potential integral holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about measurable ae eq of forall set integral eq holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about target absolutely continuous source holds.
Formal statement
Proof (Lean source)
The arm mean version object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about arm mean version measurable holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about arm mean version ae eq holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.Identification_Part2 6 declarations Conditional IV identities and transported CACE
Conditional IV identities and transported CACE
Given the supplied inputs, the stated result about arm mean version conditional mean holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source xlaw eq source population map holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about conditional mean unique source holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the difference of two conditional means is the conditional mean of the difference.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about arm contrast version conditional mean holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about transported cace identification holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture 2 declarations Legal full-elbow monotone-IV mixture
Legal full-elbow monotone-IV mixture
Choose an amplitude below any positive membership ceiling while satisfying the exponential distance calibration in roadmap (29). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about legal iv mixture full elbow holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.ArmHolder 9 declarations Finite summation identifies the receipt and outcome arm means in roadmap (10); the rational outcome mean is controlled using the overlap denominator.
Exact arm means of the primitive lower experiment
Finite summation identifies the receipt and outcome arm means in roadmap (10); the rational outcome mean is controlled using the overlap denominator.
The primitive receipt arm mean is the baseline receipt probability. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact outcome arm mean agrees with roadmap (10) on the overlap domain. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the small-amplitude overlap domain the rational arm mean has Lipschitz constant two as a function of the tiled perturbation. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact rational outcome arm mean has radius L under the amplitude ceiling used for roadmap (12). Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
All four primitive arm means satisfy the Hölder clause of model membership, using the exact finite-sum formulas rather than contrasts alone. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The center's four arm means belong to the same Hölder ball. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Coordinatewise measurability of primitive masses implies measurable arm means. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
All four component arm means are measurable and lie in the unit interval. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The center's constant arm means are measurable and lie in the unit interval. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.Assembly 14 declarations Legal-mixture two-channel assembly
Legal-mixture two-channel assembly
The covariate center is probability object is defined without additional inputs.
Definition (Lean source)
The lower explicit source is probability object is defined from the supplied inputs.
Definition (Lean source)
The lower target density is probability object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about legal data law eq product holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about center data law eq product holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about lower mixture eq uniform mixture holds.
Formal statement
Proof (Lean source)
Finite mixtures inherit domination and square-integrable density deviations from their integrable pairwise density products. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about tv uniform mixture le half sqrt holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source overlap coefficient le holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about sample height exponent bound holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about legal two channel exp bound holds.
Formal statement
Proof (Lean source)
The legal product mixture has an integrable squared likelihood deviation. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about legal tv le half sqrt chi holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about legal chi exp bound holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.Assignment 9 declarations The primitive construction records consistent receipt and outcome values.
Randomized assignment and independent product sampling
The primitive construction records consistent receipt and outcome values. A normalized binary assignment kernel preserves the primitive marginal and provides the conditional event identity in roadmap (13)--(18).
The assignment overlay draws the instrument and records its consistent observables. For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
If the assignment propensity is measurable, then the induced assignment kernel is measurable.
Formal statement
Proof (Lean source)
The assigned overlay is supported on consistent receipt and outcome records. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Assignment preserves the primitive marginal for unit-interval propensities. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A probability primitive marginal gives a probability assigned overlay. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The assignment event probability is the integral of its conditional instrument mass. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Primitive binary outcomes remain bounded after randomized assignment. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The primitive-law assignment construction satisfies consistency and randomization. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Both product-sample marginals and their independence follow from normalized channels. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.CenterMembership 5 declarations The finite primitive populations give the same conditional complier margins in both populations.
Assignment and transport conditions of the mixture components and center
The finite primitive populations give the same conditional complier margins in both populations. Their assignment kernels satisfy randomization and consistency, completing the law-level clauses in roadmap (13)--(18).
Either center population is the corresponding normalized primitive population. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The component assignment realizes randomized encouragement and consistent records. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The center assignment also realizes the model's consistency and randomization clauses. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A bounded finite primitive mean gives the center's conditional mean in either population. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Both center populations have the same constant share and zero weighted outcome margins. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.ChannelLaws 12 declarations One-observation channel laws for the legal mixture
One-observation channel laws for the legal mixture
For the source-arm strength, the tilt parameter, the covariate perturbation, and an observed source record, source observation likelihood is the likelihood of that record's encoded latent cell.
Definition (Lean source)
Given the supplied inputs, the stated result about source obs likelihood eq cell holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source obs likelihood on cell holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source obs likelihood measurable holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about explicit source law apply holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about explicit source law eq with density holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source cell mass nonneg of primitive holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source obs likelihood nonneg of cell mass holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about primitive mass sum holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about actual strength bounds holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about tiled perturbation zero holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about center source law eq explicit holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.ChiSquare 2 declarations Finite sign-mixture chi-square and total-variation estimates
Finite sign-mixture chi-square and total-variation estimates
The legal uniform mixture has an absolutely continuous likelihood with an integrable squared real density deviation relative to the center experiment. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about legal mixture distance holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.ConditionalMargins 9 declarations The normalized primitive kernel disintegrates along its covariate coordinate.
Conditional integration of the primitive finite law
The normalized primitive kernel disintegrates along its covariate coordinate.
Every real function is integrable against the finite primitive kernel. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The primitive kernel integrates a function by the displayed sixteen-cell sum. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A bounded observable on the primitive atoms disintegrates over every covariate set. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Normalized primitive masses preserve the total base mass. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditioning a half-mixture on a population event selects its supported component. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The legal law's conditional population is exactly its primitive mixture component. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A measurable finite-cell mean is a conditional mean under either legal population. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The primitive complier margins give both transport conditional means. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The center's target effect vanishes by its primitive complier outcome margins. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.Likelihood 45 declarations Likelihood identities for the legal finite sign mixture
Likelihood identities for the legal finite sign mixture
The encoded cell set mass object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the encoded-cell measure is the stated density tilt of the base measure.
Formal statement
Proof (Lean source)
The source cell object is defined without additional inputs.
The source cell mass object is defined from the supplied inputs.
Definition (Lean source)
The source center mass object is defined from the supplied inputs.
Definition (Lean source)
The source direction object is defined from the supplied inputs.
Definition (Lean source)
The source likelihood object is defined from the supplied inputs.
Definition (Lean source)
The observed primitive mass object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about observed primitive mass eq holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source cell mass affine holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source center mass pos holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source center mass sum holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source direction sum holds.
Formal statement
Proof (Lean source)
The source overlap coefficient object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about source direction sq sum holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source likelihood pair sum holds.
Formal statement
Proof (Lean source)
The source cell observation object is defined from the supplied inputs.
Definition (Lean source)
The explicit source law object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about cell mem unique holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about tiled perturbation abs le abs lower height holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about tiled perturbation abs le lower height holds.
Formal statement
Proof (Lean source)
Admissibility bounds the covariate-indexed assignment probabilities. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about complier margin nonneg of bounds holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about primitive mass nonneg of bounds holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, every lower-construction latent-cell mass is nonnegative.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about lower assignment weight mem icc holds.
Formal statement
Proof (Lean source)
The lower assignment kernel object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about tiled perturbation measurable holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about lower mass measurable holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about lower primitive kernel measurable holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about lower assignment kernel measurable holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about observed primitive ennmass eq holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, summing over observations can be regrouped as the corresponding finite weighted cell sum.
Formal statement
Proof (Lean source)
The source latent object is defined without additional inputs.
The source latent cell object is defined without additional inputs.
Definition (Lean source)
The source latent weight object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about source latent weight group eq holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the source latent-cell sum expands into its explicit finite expression.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about observe assigned latent holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source cell observation measurable holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about measurable lower assignment kernel holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about assignment kernel eq lower holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about fixed source kernel apply holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source law eq explicit of nonneg holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the lower source law equals its explicit construction.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.Margins 18 declarations Complier-share, effect, and separation identities
Complier-share, effect, and separation identities
the stated result about bump sq integral holds.
Formal statement
Proof (Lean source)
the stated result about bump integral zero holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about bump odd ratio integral zero holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about bump cell integral zero holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about tiled bump cell integral zero holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about tiled bump odd ratio cell integral zero holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about tiled perturbation integrable and integral zero holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about separation integral bounds holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about primitive mass complier sum holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about primitive mass complier outcome sum holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about lower pointwise mean complier margins holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about arm mean from primitive receipt contrast holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about arm mean from primitive outcome contrast holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about legal ivcomponent arm contrasts holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about mixture center arm contrasts holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about mixture center first stage holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about mixture center transported outcome holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about legal mixture separation holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.Membership 1 declarations The roadmap (9) provides an amplitude ceiling: every smaller positive amplitude satisfies the same model conditions.
Monotone-IV component and center membership
The roadmap (9) provides an amplitude ceiling: every smaller positive amplitude satisfies the same model conditions. Keeping this quantifier explicit allows the assembly to impose the independent distance calibration (29).
Given the supplied inputs, the stated result about legal mixture membership holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.MembershipAmplitude 3 declarations Roadmap (9) chooses one positive ceiling independent of the sample size, strength, signs, and continuum index.
Uniform amplitude ceiling for mixture membership
Roadmap (9) chooses one positive ceiling independent of the sample size, strength, signs, and continuum index. The resulting height bound discharges the density envelopes before the remaining smoothness and assignment checks.
The tile-height scaling never increases a nonnegative amplitude. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A positive ceiling satisfies all five margin restrictions in roadmap (9), with the smaller admissibility ceiling already established in Lean. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The ceiling and admissibility bounds verify both density identities, the density envelopes, and propensity overlap for every component. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.MembershipSupport 9 declarations These lemmas implement the no-defiers and bounded-potential-outcome checks in steps (13)--(18) of the legal-mixture roadmap, directly on the primitive atoms.
Primitive support for the legal IV completion
These lemmas implement the no-defiers and bounded-potential-outcome checks in steps (13)--(18) of the legal-mixture roadmap, directly on the primitive atoms.
An atomwise support condition survives covariate mixing. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The primitive completion places no mass on the defier stratum. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Both potential outcomes in the binary completion lie in the unit interval. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The no-defiers property holds for the full source-target component law. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The baseline center also has no defiers. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Exclusion is built into the component's assignment potential outcomes. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Exclusion is also built into the baseline center. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The component's full-data law retains both potential-outcome bounds. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The center's full-data law retains both potential-outcome bounds. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.ObservedArm 4 declarations The finite source-cell kernel disintegrates each observed arm integral.
Observed arm identities for the lower experiment
The finite source-cell kernel disintegrates each observed arm integral. Its weighted cell sum reproduces the exact primitive arm mean in roadmap (10).
Summing the eight observed source cells reproduces the conditional arm mean. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A normalized nonnegative finite source-cell kernel gives its exact arm set integral. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every legal component has the exact observed-arm integral required by the model class. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The unperturbed center satisfies the same exact observed-arm identity. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.Overlap 11 declarations Pairwise sign overlap identities
Pairwise sign overlap identities
Given the supplied inputs, the stated result about bump sq affine interval holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about bump sq cell integral holds.
Formal statement
Proof (Lean source)
The tiled term object is defined from the supplied inputs.
Given the supplied inputs, the stated result about tiled perturbation eq sum tiled term holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about tiled term mul eq zero of ne holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about tiled term product integrable holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about tiled term pair integral holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about tiled perturbation pair integral holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about target likelihood pair integrable holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about tiled perturbation product integrable holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about target likelihood pair integral holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.ProbabilitySupport 14 declarations The normalized finite masses and the zero-integral perturbation verify the probability-law requirement in the membership roadmap (7), (13)--(18).
Probability and covariate support of the legal primitive laws
The normalized finite masses and the zero-integral perturbation verify the probability-law requirement in the membership roadmap (7), (13)--(18).
Covariate mixing preserves the unit-interval covariate support. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Two normalized primitive populations give a normalized full-data mixture. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full mixture satisfies the covariate and potential-outcome support clause. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The baseline center's full-data law is a probability measure. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The perturbed component's full-data law is a probability measure. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
All primitive component covariates and potential outcomes have the required support. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The center's covariates and potential outcomes have the required support. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing the normalized observed cells leaves the uniform covariate marginal. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The center's observed source covariate density is exactly one. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The component's observed source covariate density is exactly one. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The center satisfies every source-density bound and full-data support requirement. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The perturbed component satisfies every source-density and full-data support requirement. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The center's target density is uniform and obeys both envelopes. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The component's target density obeys the envelopes when the height respects their margins. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.SeparationIdentity 11 declarations Exact nonlinear tiled-bump integrals for the lower separation
Exact nonlinear tiled-bump integrals for the lower separation
A nonlinear function vanishing at zero acts cellwise on the disjoint tiled bump. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integration of an integrable transform reduces to the finite cell sum. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The affine substitution on a tile has Jacobian equal to the reciprocal cell count. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The rational bump powers integrate exactly tile by tile, including their sign factors. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The odd rational correction has zero integral on every tile. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The even rational term equals the paper's separation, independently of the signs. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The rational powers used in the separation calculation are integrable. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact transported outcome is minus tau times the separation; the tilted cubic correction cancels rather than contributing a bias term. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The target integral uses exactly the tilted covariate density in the construction. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The target conditional margins identify CACE with the exact transported outcome divided by the construction's constant complier share. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about legal mixture margins holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.SourceOverlap 9 declarations Source-channel overlap identities
Source-channel overlap identities
Given the supplied inputs, the stated result about explicit center source law univ holds.
Formal statement
Proof (Lean source)
The explicit center source law is probability object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about source cell mass sum holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about explicit source law univ of nonneg holds.
Formal statement
Proof (Lean source)
The explicit source law is probability of nonneg object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about lower source cell mass nonneg holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about lower source likelihood nonneg holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source likelihood pair integrable holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source likelihood pair integral holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.TargetLaws 8 declarations Target covariate and conditioning identities
Target covariate and conditioning identities
Given the supplied inputs, the stated result about primitive kernel measurable of holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about primitive kernel univ holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about map covariate primitive population holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about primitive population population event holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about cond half supported mixture holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about target density univ holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about legal target law eq density holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about center target law eq volume holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LegalMixture.TiledHolder 12 declarations The sinusoidal tile bump vanishes at every cell boundary.
Hölder control of the tiled lower-bound perturbation
The sinusoidal tile bump vanishes at every cell boundary. This makes the signed tiling globally Lipschitz despite arbitrary sign changes between cells; combining that estimate with its uniform height bound gives the required one-eighth Hölder radius.
Every point of the covariate interval belongs to one tiled cell. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
On a cell, the tiled perturbation is its unique active summand. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Membership in a tile supplies its closed endpoint bounds. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The active sinusoid is controlled by distance to either endpoint of its tile. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The signed tiled sine is globally Lipschitz on the covariate interval. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The scale K⁻¹/⁸ converts the tiled Lipschitz estimate into a uniform one-eighth Hölder modulus. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The tiled perturbation is continuous on the covariate interval. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A bounded scalar function with the target modulus belongs to the paper's one-dimensional standard Hölder ball. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Adding a constant preserves the tiled Hölder modulus; the displayed supremum condition supplies the radius bound. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Constant functions with value in the radius belong to the Hölder ball. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The perturbed target density has radius L. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The perturbed assignment propensity has radius L. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.Length 1 declarations Specialize the measurable random-set identity to the two-sample expected-length functional and the parameter interval [-1,1].
Restricted random-set length support
Specialize the measurable random-set identity to the two-sample
expected-length functional and the parameter interval [-1,1].
Expected restricted length is the integral of pointwise inclusion probabilities. The shared theorem interchanges the two integrals of the measurable indicator. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.LowerLength 8 declarations Componentwise honesty passes to the finite sign mixture, and total variation then transfers it to the center.
Coverage averaging and continuum length for the lower experiment
Componentwise honesty passes to the finite sign mixture, and total variation then transfers it to the center. Integrating inclusion probabilities gives the lower length bound without requiring connected confidence sets.
The three sampling conditions and the marginal probability laws make the data law a probability. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Expected restricted lengths are nonnegative, even before regularity is imposed. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
A probability expectation of restricted length cannot exceed the length two of the parameter space. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The definition's power-of-two normalization is the cardinality normalization of a uniform mixture. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging preserves a common lower coverage bound over a finite nonempty family. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite-size fallback parameter interval is an honest connected confidence set. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The floor chosen by the mixture implements the exact capped inverse-strength rate. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating a uniform inclusion bound over a symmetric subinterval gives its length times coverage. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.Mixture 38 declarations Finite sign-mixture full-data construction
Finite sign-mixture full-data construction
The lower cells object is defined from the supplied inputs.
Definition (Lean source)
The bump object is defined from the supplied inputs.
The lower height object is defined from the supplied inputs.
Definition (Lean source)
The sign object is defined from the supplied inputs.
Definition (Lean source)
The tiled perturbation object is defined from the supplied inputs.
The coupled perturbation object is defined from the supplied inputs.
Definition (Lean source)
The actual strength object is defined from the supplied inputs.
Definition (Lean source)
The lower admissible object is defined from the supplied inputs.
Definition (Lean source)
The standing lower-experiment domain combines positive sample size with the paper's exact amplitude admissibility condition. Height and separation are interpreted on this domain; their range properties are derived below. For the displayed assumptions and inputs, the stated object is defined.
Definition (Lean source)
The receipt base object is defined from the supplied inputs.
The receipt outcome cell object is defined from the supplied inputs.
Definition (Lean source)
The assignment weight object is defined from the supplied inputs.
Definition (Lean source)
The paper's strength domain makes the baseline receipt a probability. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each baseline receipt-outcome cell is nonnegative. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
For each encouragement, the four baseline cells have total mass one. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about assignment weight mem icc holds.
Formal statement
Proof (Lean source)
The complier margin object is defined from the supplied inputs.
The primitive mass object is defined from the supplied inputs.
Definition (Lean source)
The primitive kernel object is defined from the supplied inputs.
The primitive population object is defined from the supplied inputs.
The assigned from object is defined from the supplied inputs.
Definition (Lean source)
The arm mean from object is defined from the supplied inputs.
Definition (Lean source)
The law from mass object is defined from the supplied inputs.
Definition (Lean source)
The lower mass object is defined from the supplied inputs.
Definition (Lean source)
The lower pointwise mean object is defined from the supplied inputs.
Definition (Lean source)
The legal ivcomponent object is defined from the supplied inputs.
Definition (Lean source)
The mixture center object is defined from the supplied inputs.
Definition (Lean source)
The lower mixture object is defined from the supplied inputs.
Definition (Lean source)
The legal ivmixture object is defined from the supplied inputs.
Definition (Lean source)
The separation object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about lower admissible of small amplitude holds.
Formal statement
Proof (Lean source)
Admissibility and positive sample size imply the paper's strict height range. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The mix constant object is defined without additional inputs.
Definition (Lean source)
The witness direction object is defined from the supplied inputs.
Definition (Lean source)
The witness amplitude object is defined from the supplied inputs.
The simple primitive kernel object is defined from the supplied inputs.
Definition (Lean source)
The simple primitive population object is defined from the supplied inputs.
Definition (Lean source)
The continuous geometry witness object is defined from the supplied inputs.
Definition (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.ObservableReduction 1 declarations Combines the observable channel identities with explicit coordinate derivative bounds.
Assembly of the observable marked-density reduction
Combines the observable channel identities with explicit coordinate derivative bounds.
Given the supplied inputs, the stated result about observable marked reduction holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.Reduction 19 declarations Observable marked-density reduction
Observable marked-density reduction
The clipping rectangle object is defined from the supplied inputs.
The coordinate mark object is defined from the supplied inputs.
Definition (Lean source)
The coordinate basis object is defined from the supplied inputs.
The fourth derivative envelope object is defined from the supplied inputs.
Definition (Lean source)
Given the supplied inputs, the stated result about coordinate mark mem unit interval holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about marked density vector assignment lower bounds holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about marked density vector mem clipping rectangle holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about phi marked density vector eq transport integrand holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about transported form eq integral phi marked density vector holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source marked arm integral holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source marked arm density holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about measurable assignment mass on covariate holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source assignment density holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about source assignment mark integral holds.
Formal statement
Proof (Lean source)
Given the supplied inputs, the stated result about phi value abs le fourth derivative envelope holds.
Formal statement
Proof (Lean source)
The derivative of one arm contribution, evaluated along an arbitrary direction. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The first derivative of the transport integrand is the difference of the two arm derivatives. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Bounded coordinate directions give a uniform first derivative bound for one arm. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The first coordinate derivative uses exactly the deterministic envelope from the reduction. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.ScoreMeasurability 2 declarations Joint pilot measurability, measurable derivatives, and parameter integration make the exact score measurable.
Measurability of the exact cubic score interval
Joint pilot measurability, measurable derivatives, and parameter integration make the exact score measurable. An explicit affine witness characterizes the nonempty inversion event, including its boundary, and justifies the fallback.
Given the supplied inputs, the stated result about measurable cubic estimator holds.
Formal statement
Proof (Lean source)
The concrete affine inversion and its fallback have a measurable graph. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.UpperGeometry 6 declarations These lemmas implement the coverage event, the zero-volume fallback, the good-slope length bound (1), and the final two-regime calculation in the honest-upper roadmap.
Deterministic steps of the honest upper bound
These lemmas implement the coverage event, the zero-volume fallback, the good-slope length bound (1), and the final two-regime calculation in the honest-upper roadmap. The probabilistic moment and tail steps remain separate.
The calibrated radius is nonnegative for every sample size. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Identification turns simultaneous reduced-form error bounds into inclusion of the true parameter in the exact interval, including the finite-size rule. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Replacing an empty acceptance set by the singleton zero preserves its restricted length exactly. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the good first-stage event, the exact fallback interval obeys roadmap equation (1), with the displayed constant eight. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The two expectation bounds in the roadmap give its exact constant max 2 (8 c_r + 8 C_mse) after separating the regimes at one. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each outcome of the prescribed affine inversion is a connected subset of the parameter interval, including both fallback rules. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.Helpers.UpperProbability 7 declarations Markov's inequality supplies the two calibrated error tails and the bad-slope probability in the roadmap.
Probabilistic steps of the honest upper bound
Markov's inequality supplies the two calibrated error tails and the bad-slope probability in the roadmap. These interfaces keep square integrability explicit; they do not add assumptions to the paper theorem. The expected-length assembly uses the exact interval's good-slope bound and its deterministic length cap.
Exact cancellation of the calibrated radius and the mean-square rate. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each reduced-form estimator has noncoverage at most α/2. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Roadmap equation (2), for the exact estimated first stage. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Square integrability suffices for null measurability of the error tail. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
The union bound and identification give honest coverage for the exact interval. Square integrability is an explicit interface obligation. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Restricted length is bounded by the parameter-space length pointwise. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating the exact good-slope bound and bounding the complement gives roadmap equations (1)--(2) with the displayed constants eight. Under the displayed assumptions and inputs, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.THonestLowerFullElbow 1 declarations Monotone-IV continuum lower bound for every honest measurable set
Monotone-IV continuum lower bound for every honest measurable set
Given the supplied inputs, the stated result about honest lower full elbow holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.THonestUpperFullElbow 1 declarations The proof follows the calibrated MSE tails, identification, good-slope length bound, and minimax assembly.
Finite-sample honest affine interval and its upper length frontier
The proof follows the calibrated MSE tails, identification, good-slope length bound, and minimax assembly. Graph measurability and square integrability of the exact construction are derived by internal helper statements from the construction and model membership.
Given the supplied inputs, the stated result about honest upper full elbow holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_TransportCaceRoughnuisanceLength_Research.TSharpLengthFrontierFullElbow 1 declarations Sharp no-logarithm equal-sample length frontier
Sharp no-logarithm equal-sample length frontier
Given the supplied inputs, the stated result about sharp length frontier full elbow holds.