Formalization: Efficient Estimation of Binary Treatment Effects under Local Differential Privacy
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 (f9001b6) — statements may have moved since the audit.
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Basic 72 declarations This file fixes the four input symbols of a randomized binary trial and gives the fourteen ray staircase program for its private information surface.
Binary trial and finite staircase program
This file fixes the four input symbols of a randomized binary trial and gives the fourteen ray staircase program for its private information surface.
the private alphabet is the mathematical object specified below.
Definition (Lean source)
Coordinates of the fourteen nonconstant rays used in the finite program. The stated result follows.
Definition (Lean source)
The declared pattern carrier is the full power set, including the empty and full sets. The stated result follows.
Definition (Lean source)
the staircase pattern space is the mathematical object specified below.
Definition (Lean source)
the staircase pattern space eq univ assertion holds.
Formal statement
Proof (Lean source)
the staircase pattern space card assertion holds.
Formal statement
Proof (Lean source)
the staircase pattern space contains constants assertion holds.
Formal statement
Proof (Lean source)
the trial parameter is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The Trial Parameter is the displayed object.
Definition (Lean source)
the staircase weight is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The Staircase Weight is the displayed object.
Definition (Lean source)
the contrast is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the contrast vector is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the control prob is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the pi theta is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the input law is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the input score is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the private record is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the arm mean parameter is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the iid subjects is the mathematical object specified below. The Iid Subjects is determined by the displayed parameters.
Definition (Lean source)
the random assignment is the mathematical object specified below. The Random Assignment is determined by the displayed parameters.
the known assignment is the mathematical object specified below. The Known Assignment is determined by the displayed parameters.
the outcome consistency is the mathematical object specified below. The Outcome Consistency is determined by the displayed parameters.
Definition (Lean source)
the binary outcomes is the mathematical object specified below. The Binary Outcomes is determined by the displayed parameters.
the interior assignment is the mathematical object specified below. The Interior Assignment is determined by the displayed parameters.
Definition (Lean source)
the interior means is the mathematical object specified below. The Interior Means is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the assignment range is the mathematical object specified below.
Definition (Lean source)
the mean range is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the contrast range is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the control range is the mathematical object specified below.
Definition (Lean source)
Under the supplied quantities and conditions, the assignment range assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the mean range assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the mean Range.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the contrast range assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the contrast Range.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the control range assertion holds.
Formal statement
Proof (Lean source)
the positive sample size is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The Positive Sample Size is the displayed object.
Definition (Lean source)
The public binary-trial model is the family of IID laws of the observed treatment-outcome record. Its nth member is the n-fold product of the four-point law at (θ,p). The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. For the displayed quantities and conditions, these specify the stated inputs. The Binary Trial Model is determined by the displayed parameters.
Definition (Lean source)
A latent representation of the public binary-trial model by potential outcomes, assignment, and the observed outcome. The Latent Binary Trial Representation is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the binary event probs assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the record law eq pi theta assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
A latent representation realizes every finite prefix of the public observed-law model. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
A family belongs to the public observed-law model exactly when some latent binary-trial representation realizes all of its finite-prefix laws. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the binary Trial Model iff latent Representation.
Formal statement
Proof (Lean source)
the privacy ratio is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the privacy increment is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
The paper's likelihood-ratio parameter is evaluated only at a positive privacy budget. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The admissible Privacy Ratio is determined by the displayed parameters.
Definition (Lean source)
The paper's staircase increment is evaluated only at a positive privacy budget. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The admissible Privacy Increment is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the admissible privacy ratio gt one assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the admissible Privacy Ratio gt one.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the admissible privacy increment pos assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the admissible Privacy Increment pos.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the admissible privacy ratio covers assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the admissible privacy increment covers assertion holds.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pattern contains is the mathematical object specified below.
The fixed enumeration embeds the fourteen nonconstant masks into the full power set. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the pattern ray is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the pattern mass is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
The paper's mass factor is computed on the declared probability-parameter domains. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. For the displayed quantities and conditions, these specify the stated inputs. The admissible Pattern Mass is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the admissible pattern mass pos assertion holds. For the displayed quantities and conditions, these specify the stated inputs. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the admissible Pattern Mass pos.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pattern gradient is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the staircase matrix is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the staircase feasible is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the direction is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the projected gradient is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the pattern information is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the information matrix is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the output score is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the projected score is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the information objective is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
The optimized Fisher-information value is determined by the displayed parameters.
Definition (Lean source)
The reciprocal optimized contrast variance is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the private history is the mathematical object specified below. The Private History is determined by the displayed parameters.
the sequential kernel is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the fixed privacy is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the sequential ldp is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, this sequential channels packages the stated mathematical data. For the displayed quantities and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the pilot diverges is the mathematical object specified below.
For the supplied quantities and conditions, the pilot sublinear is the mathematical object specified below.
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.AttainmentRigidity 3 declarations Variance attainment forces equality in every certified information direction.
Directional equality and postprocessing nonmerger
Variance attainment forces equality in every certified information direction. After staircase refinement, distinct projected scores then force the active postprocessing rows to be pairwise mutually singular, giving an output cardinality lower bound for arbitrary measurable output spaces.
If a stationary channel attains the oracle variance, its Fisher information in every affine contrast direction is at least the oracle information. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the attainment forces direction lower.
Formal statement
Proof (Lean source)
Under a uniform directional upper bound, an attaining channel has a staircase refinement with equality in that direction, so the refinement's equality-rigidity conclusion is available. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the attaining staircase refinement direction eq.
Formal statement
Proof (Lean source)
A certified attaining direction with positive, pairwise distinct active scores requires at least as many output atoms as active staircase rays. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the output Cardinality ge of attainment direction.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.BalancedBinary 20 declarations This file groups the four trial cells by the signed treatment--outcome bit.
Binary submodel for the balanced trial
This file groups the four trial cells by the signed treatment--outcome bit. The grouped experiment is the one-dimensional Bernoulli submodel used in the balanced randomized-response calculation.
the half nn is the mathematical object specified below.
Definition (Lean source)
the half is the mathematical object specified below.
Definition (Lean source)
Average the two full-record rows having the same signed bit. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Under the supplied quantities and conditions, the grouped channel apply assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the grouped channel markov assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the grouped channel private assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the reference grouped channel assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the grouped density true assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the grouped density false assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the abs contrast lt one assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the abs contrast lt one.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pi theta balanced by val assertion holds.
Formal statement
Proof (Lean source)
the channel output density balanced assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the directional derivative balanced assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the grouped information eq channel quadratic assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the grouped information eq channel Quadratic.
Formal statement
Proof (Lean source)
the grouped staircase atom assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the grouped Staircase atom.
Formal statement
Proof (Lean source)
the pattern mass balanced assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the projected gradient balanced assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the grouped staircase information eq objective assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the grouped Staircase information eq objective.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the information objective balanced le sharp assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the information Objective balanced le sharp.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the jstar balanced le sharp assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the Jstar balanced le sharp.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.CenteredR5Certificate 42 declarations Explicit centered five-ray certificate
Explicit centered five-ray certificate
For the supplied quantities and conditions, the centered r5 scale is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the centered r5 denom is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the centered r5 direction is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the centered r5 mix is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the centered r5 value is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the centered r5 dual is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the centered r5 left score is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the centered r5 right score is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the centered r5 information table is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the centered r5 dual coeff is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the centered r5 weight is the mathematical object specified below.
Definition (Lean source)
Under the supplied quantities and conditions, the centered pi theta assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered pattern mass assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered pattern mass inv assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered pattern information assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered projected score assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 information table assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 dual table assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 scale sq assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 scale bounds assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 denom pos assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 mix mem ioo assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 direction neg assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 left score pos assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 right score pos assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 direction add one assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 common score assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 value eq common score sq assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 value pos assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 slack mask12 assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 slack mask5 10 assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 slack mask7 11 assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 slack mask12 zero assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 slack mask13 14 assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 weight feasible assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 weight active assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 weight stationary assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 active dual equalities assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 inactive dual slacks assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 active scores pairwise ne assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 supported stationary eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the centered R5 supported stationary eq.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered point mem r5 assertion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.CenteredR5Rigidity 2 declarations Centered five-ray profile rigidity
Centered five-ray profile rigidity
Under the supplied quantities and conditions, the centered r5 profile optimal unique assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered r5 output cardinality ge five assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.CertificateRigidity 5 declarations These lemmas isolate the finite duality step used by the certified support regions.
Consequences of a strict staircase dual certificate
These lemmas isolate the finite duality step used by the certified support regions. Equality in the certificate bound forces every inactive staircase weight to vanish.
the feasible dual ray sum general assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the feasible dual Ray sum general.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the certificate dual upper bound assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the certificate dual upper bound.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the certificate equality forces inactive zero assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the certificate equality forces inactive zero.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the strict certificate profile optimal and rigid assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the strict Certificate profile optimal and rigid.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 certificate profile optimal and rigid assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.Channels 16 declarations Radon–Nikodym densities are taken against the finite sum of the four channel rows, so no countable-generation condition is imposed on the output space.
Stationary private channels and their information
Radon–Nikodym densities are taken against the finite sum of the four channel rows, so no countable-generation condition is imposed on the output space.
the stationary ldp is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The Stationary LDP is determined by the displayed parameters.
Definition (Lean source)
the dominating measure is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
For the supplied quantities and conditions, the channel density is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the input derivative is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the channel output density is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The channel Output Density is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the channel derivative density is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the channel fisher info is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The channel Fisher Info is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the output law is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The output Law is determined by the displayed parameters.
For the supplied quantities and conditions, the output cardinality is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The output Cardinality is determined by the displayed parameters.
Definition (Lean source)
the staircase channel is the mathematical object specified below. The staircase Channel is determined by the displayed parameters.
Definition (Lean source)
the channel density staircase ae assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the channel Density staircase ae.
Formal statement
Proof (Lean source)
the dominating measure staircase singleton real assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the dominating Measure staircase singleton real.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pattern ray ldp assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pattern Ray ldp.
Formal statement
Proof (Lean source)
the staircase channel markov assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the staircase Channel markov.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the staircase channel private assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the staircase Channel private.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the staircase channel stationary ldp assertion holds. Under the stated assumptions, the staircase Channel stationary LDP.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.GeneralR3Cardinality 3 declarations General three-ray cardinality in the distinct-score neighborhood
General three-ray cardinality in the distinct-score neighborhood
Under the supplied quantities and conditions, the r3 certificate direction eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the r3 Certificate direction eq.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r3 certificate staircase attains three assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r3 certificate output cardinality ge three of distinct assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.GeneralR5Rigidity 3 declarations General five-ray certificate rigidity
General five-ray certificate rigidity
Every R5 certificate has a unique optimal staircase weight, including away from the centered explicit family. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Every channel attaining an oracle certified by R5 has at least five positive output atoms. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The primal witness carried by an R5 certificate attains the oracle and has exactly five positive staircase outputs. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.Laplace 9 declarations The custom Horvitz–Thompson score is released with independent centered Laplace noise at the published sensitivity scale.
Published custom Laplace comparator
The custom Horvitz–Thompson score is released with independent centered Laplace noise at the published sensitivity scale.
For the supplied quantities and conditions, the sensitivity is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the comparator noise law is the mathematical object specified below. The comparator Noise Law is determined by the displayed parameters.
Definition (Lean source)
The observed-record/noise pairs are jointly independent across subjects; each noise has the published Laplace marginal and is independent of its observed private record. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The Comparator Noise is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the oa release value is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The oa Release Value is determined by the displayed parameters.
Definition (Lean source)
the oa release is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The oa Release is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the tau oa is the mathematical object specified below. The tau OA is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the vhat oa is the mathematical object specified below. The Vhat OA is determined by the displayed parameters.
Definition (Lean source)
the vhat oa eq second moment sub sq assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the voa is the mathematical object specified below. The VOA is determined by the displayed parameters.
Definition (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.LaplaceMoments 5 declarations This file records the first two moments and square integrability of the positive-scale centered Laplace distribution used by the comparator release.
Moments of the centered Laplace law
This file records the first two moments and square integrability of the positive-scale centered Laplace distribution used by the comparator release.
A centered Laplace draw has mean zero at every positive scale. For the displayed inputs and conditions, the stated result follows.
Formal statement
Proof (Lean source)
The square of a centered Laplace draw is integrable at every positive scale. For the displayed inputs and conditions, the stated result follows.
Formal statement
Proof (Lean source)
The second moment of a centered Laplace draw with positive scale b is 2 * b ^ 2. For the displayed inputs and conditions, the stated result follows.
Formal statement
Proof (Lean source)
Each comparator noise coordinate is almost everywhere measurable. This is recovered from its stipulated nonzero Laplace pushforward law, so no separate measurability assumption is needed. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the aemeasurable.
Formal statement
Proof (Lean source)
Every noisy release coordinate is almost everywhere measurable under the binary-trial and comparator-noise assumptions. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the oa Release Value aemeasurable.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.LaplaceRatio 1 declarations A nonnegative estimated denominator makes the ordinary square-root ratio agree with the total fallback map.
Coupled variance-ratio continuity
A nonnegative estimated denominator makes the ordinary square-root ratio agree with the total fallback map. Consequently marginal convergence in probability passes through every coupling of the two rows.
Under the supplied quantities and conditions, the vhat star nonneg assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.OAConsistency 28 declarations IID and moment adapters for the custom Laplace release
IID and moment adapters for the custom Laplace release
For the supplied quantities and conditions, the oa trial value is the mathematical object specified below.
Definition (Lean source)
Under the supplied quantities and conditions, the oa trial value mean input law assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the oa Trial Value mean input Law.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the oa trial value sq mean input law assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the oa Trial Value sq mean input Law.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the oa trial part is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The oa Trial Part is determined by the displayed parameters.
Definition (Lean source)
the private record measurable of model assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the oa trial part ae eq record assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the oa trial part integral assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the oa trial part sq integral assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the oa trial part integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the oa trial part sq integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the comparator noise integral assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the comparator Noise integral.
Formal statement
Proof (Lean source)
the comparator noise sq integral assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the comparator Noise sq integral.
Formal statement
Proof (Lean source)
the comparator noise sq integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the comparator Noise sq integrable.
Formal statement
Proof (Lean source)
the comparator noise integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the comparator Noise integrable.
Formal statement
Proof (Lean source)
the oa trial part indep noise assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the oa release value eq trial add assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the oa release value integral assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the oa Release Value integral.
Formal statement
Proof (Lean source)
the oa release value sq integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the oa Release Value sq integrable.
Formal statement
Proof (Lean source)
the oa release value sq integral assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the oa Release Value sq integral.
Formal statement
Proof (Lean source)
the oa release value centered sq integral assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the oa Release Value centered sq integral.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the oa combined value is the mathematical object specified below.
Definition (Lean source)
Under the supplied quantities and conditions, the oa combined value measurable assertion holds.
Formal statement
Proof (Lean source)
the oa release value ae eq combined assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the oa release value i indep assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the oa combined ident distrib assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the oa Combined ident Distrib.
Formal statement
Proof (Lean source)
the oa release value ident distrib assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the oa Release Value ident Distrib.
Formal statement
Proof (Lean source)
the oa release clt assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the oa Release clt.
Formal statement
Proof (Lean source)
the oa variance consistency assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the oa Variance consistency.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.OracleEnvelope 9 declarations Staircase information envelope
Staircase information envelope
Under the supplied quantities and conditions, the information objective affine weights assertion holds.
Formal statement
Proof (Lean source)
the information objective exists maximizer assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the information Objective exists maximizer.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the upper envelope attained assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the upper Envelope attained.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the upper envelope quadratic lower bound assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the upper Envelope quadratic lower bound.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the upper envelope continuous assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the upper Envelope continuous.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the vertex envelope is the mathematical object specified below. The vertex Envelope is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the upper envelope eq vertex envelope assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the upper Envelope eq vertex Envelope.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the jstar le upper envelope assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the Jstar le upper Envelope.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the upper envelope exists minimizer assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the upper Envelope exists minimizer.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.OracleGeometry 31 declarations The contrast variance is the information-matrix quadratic solution value, with infinity when the contrast is outside the information range.
Exact finite staircase oracle
The contrast variance is the information-matrix quadratic solution value, with infinity when the contrast is outside the information range. The theorem states both the arbitrary-channel comparison and the finite saddle identity.
the contrast in range is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the contrast variance is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the feasible set is the mathematical object specified below. The feasible Set is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the pi theta pos interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pi Theta pos interior.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pattern ray one le interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pattern Ray one le interior.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pattern mass pos interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pattern Mass pos interior.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the information objective nonneg interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the information Objective nonneg interior.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the information quadratic nonneg staircase assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the information Quadratic nonneg staircase.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the information matrix pos semidef interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the information Matrix pos Semidef interior.
Formal statement
Proof (Lean source)
the contrast solution value pos assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the contrast solution value unique assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the contrast variance eq solution value assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the contrast information cauchy assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the reciprocal le contrast variance assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the contrast variance eq reciprocal of minimizer assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the first pattern information quadratic assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the information objective eq information quadratic assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the staircase feasible weight le one assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the staircase Feasible weight le one.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the staircase feasible sum le one assertion holds. Under the stated assumptions, the staircase Feasible sum le one.
Formal statement
Proof (Lean source)
the staircase feasible nonempty assertion holds.
Formal statement
Proof (Lean source)
the staircase feasible singleton design assertion holds.
Formal statement
Proof (Lean source)
the staircase feasible positive first pattern assertion holds.
Formal statement
Proof (Lean source)
the staircase feasible closed assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the staircase feasible compact assertion holds. Under the stated assumptions, the staircase Feasible compact.
Formal statement
Proof (Lean source)
the staircase feasible convex assertion holds.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the upper envelope is the mathematical object specified below. The upper Envelope is determined by the displayed parameters.
Definition (Lean source)
the information objective continuous weight assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the information objective quadratic difference assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the information objective min of stationary assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the information Objective min of stationary.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the information objective stationary of min assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the information objective exists minimizer assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the information Objective exists minimizer.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.OracleValue 5 declarations Staircase profile values
Staircase profile values
Under the supplied quantities and conditions, the information objective profile upper semicontinuous assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the information Objective profile upper Semicontinuous.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the information objective profile exists maximizer assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the information Objective profile exists maximizer.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the jstar exists optimal weight assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the Jstar exists optimal weight.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the jstar pos interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the Jstar pos interior.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the jstar eq envelope of stationary maximizer assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the Jstar eq envelope of stationary maximizer.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.Pilot 32 declarations Four-category randomized response estimates the input probabilities.
Private pilot and affine main-sample estimator
Four-category randomized response estimates the input probabilities. A measurable saddle selector chooses the main staircase channel and influence values from that pilot, with the pilot discarded from the final average.
the pilot output is the mathematical object specified below.
the pilot output family is the mathematical object specified below.
Definition (Lean source)
The measurable-space instance for pilot outputs is determined by the displayed parameters.
Definition (Lean source)
the inst measurable singleton class pilot output is the mathematical object specified below.
Definition (Lean source)
The measurable-singleton instance for pilot outputs is determined by the displayed parameters.
Definition (Lean source)
The countability instance for private pilot histories is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the inst measurable singleton class pilot history is the mathematical object specified below.
Definition (Lean source)
For the supplied quantities and conditions, the rr pilot probability is the mathematical object specified below. The rr Pilot Probability is determined by the displayed parameters.
Under the supplied quantities and conditions, the rr pilot probability ldp assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the rr Pilot Probability ldp.
Formal statement
Proof (Lean source)
the rr pilot kernel is the mathematical object specified below. The rr Pilot Kernel is determined by the displayed parameters.
the rr pilot kernel markov assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the rr pilot kernel private assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the rr Pilot Kernel private.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the clip interior is the mathematical object specified below. The clip Interior is determined by the displayed parameters.
For the supplied quantities and conditions, the pilot frequency is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the pilot theta is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The pilot Theta is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the pilot history frequency is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, the pilot history theta is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The pilot History Theta is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the clip interior interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the clip Interior interior.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot history theta interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the saddle selection is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The Saddle Selection is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the strong saddle selection is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The Strong Saddle Selection is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the exists measurable strong saddle selector assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the exists measurable strong saddle selector.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the exists measurable saddle selector assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the exists measurable saddle selector.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the phi tilde is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The phi Tilde is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the phi output is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The phi Output is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the tau star is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The tau Star is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the vhat star is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The Vhat Star is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the pilot protocol is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The pilot Protocol is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the pilot protocol private assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Protocol private.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the tau star measurable assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the exists pilot transcript assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the exists pilot transcript.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pilot estimator is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The pilot Estimator is determined by the displayed parameters.
Definition (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotAdaptiveAveraging 7 declarations Finite pilot averaging and main-row scale transfer
Finite pilot averaging and main-row scale transfer
the finite pilot average error le assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the finite Pilot average error le.
Formal statement
Proof (Lean source)
the finite pilot average tendsto of bad mass assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the adaptive main size is the mathematical object specified below.
Definition (Lean source)
Under the supplied quantities and conditions, the adaptive main size add pilot assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive main size ratio tendsto one assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive main size tendsto at top assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive row main sqrt ratio tendsto one assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotAdaptiveContinuity 6 declarations Continuity of the private-pilot oracle value and adaptive variance
Continuity of the private-pilot oracle value and adaptive variance
For the supplied quantities and conditions, the adaptive pilot polytope is the mathematical object specified below. The adaptive Pilot Polytope is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the adaptive pilot quadratics is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Pilot Quadratics is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the jstar eq adaptive quadratic value assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the Jstar eq adaptive Quadratic Value.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at jstar assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the continuous At Jstar.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at vstar assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the continuous At Vstar.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at adaptive score variance diag assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the continuous At adaptive Score Variance diag.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotAdaptiveInputs 19 declarations Finite adaptive main-release inputs
Finite adaptive main-release inputs
For the supplied quantities and conditions, the adaptive main mass is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Main Mass is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the adaptive selected score is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Selected Score is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the adaptive main mass nonneg assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Main Mass nonneg.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the staircase weighted mass sum assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the staircase Weighted Mass sum.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive main mass sum assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Main Mass sum.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive selected score mean assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Selected Score mean.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive selected score second moment diag assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Selected Score second Moment diag.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the adaptive score variance is the mathematical object specified below. The adaptive Score Variance is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the adaptive score moment is the mathematical object specified below. The adaptive Score Moment is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the adaptive score moment nonneg assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Score Moment nonneg.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive score variance eq centered sum assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Score Variance eq centered sum.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive score variance nonneg assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Score Variance nonneg.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive score variance diag assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Score Variance diag.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive selected score abs le assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Selected Score abs le.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive selected score second moment le assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Selected Score second Moment le.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive selected score abs moment le assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Selected Score abs Moment le.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive score moment le assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Score Moment le.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive score variance le assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Score Variance le.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive rare event integrand bounds assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Rare Event Integrand bounds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotAdaptiveLaw 15 declarations Exact finite-law bridges for the adaptive pilot protocol
Exact finite-law bridges for the adaptive pilot protocol
Under the supplied quantities and conditions, the fin prod split assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pilot adaptive encode is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Under the supplied quantities and conditions, the pilot adaptive encode pilot assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot adaptive encode main assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pilot adaptive prefix theta is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The pilot Adaptive Prefix Theta is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the pilot theta pilot adaptive encode assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the finite sequence transcript singleton apply assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot history frequency restrict eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot history theta restrict eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot protocol main singleton assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Protocol main singleton.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot protocol main output singleton assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Protocol main output singleton.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot protocol pilot output singleton assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Protocol pilot output singleton.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot adaptive joint singleton assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Adaptive joint singleton.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot protocol main wrong tag assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Protocol main wrong Tag.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot protocol pilot wrong tag assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Protocol pilot wrong Tag.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotAdaptiveLocalization 2 declarations Localization bounds for adaptive pilot inputs
Localization bounds for adaptive pilot inputs
Under the supplied quantities and conditions, the pilot theta interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive pilot rare event integral le assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Rare Event integral le.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotAdaptiveModelFields 19 declarations This file packages the finite pilot sample, its selected parameter, and fixed compact interior neighborhoods used by the adaptive asymptotic model.
Routine model fields for adaptive pilot asymptotics
This file packages the finite pilot sample, its selected parameter, and fixed compact interior neighborhoods used by the adaptive asymptotic model. It does not depend on the generic adaptive limit theorem.
For the supplied quantities and conditions, the adaptive pilot sample is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The Adaptive Pilot Sample is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the adaptive pilot selector is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Pilot Selector is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the adaptive pilot selector interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the measurable adaptive pilot selector assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the measurable adaptive selected score pair assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the measurable adaptive Selected Score pair.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the measurable adaptive main mass pair assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the measurable adaptive Main Mass pair.
Formal statement
Proof (Lean source)
the adaptive interior margin is the mathematical object specified below. The adaptive Interior Margin is determined by the displayed parameters.
Definition (Lean source)
the adaptive neighborhood is the mathematical object specified below.
Definition (Lean source)
the adaptive compact values is the mathematical object specified below. The adaptive Compact Values is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the adaptive interior margin pos assertion holds. Under the stated assumptions, the adaptive Interior Margin pos.
Formal statement
Proof (Lean source)
the adaptive neighborhood is open assertion holds.
Formal statement
Proof (Lean source)
the adaptive compact values is compact assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive compact values mem assertion holds. Under the stated assumptions, the adaptive Compact Values mem.
Formal statement
Proof (Lean source)
the adaptive compact values mem interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Compact Values mem interior.
Formal statement
Proof (Lean source)
the adaptive compact values interior means assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Compact Values interior Means.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the adaptive good pilot is the mathematical object specified below. The adaptive Good Pilot is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the adaptive good pilot measurable assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive good pilot selector mem assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive score moment uniform on compact assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Score Moment uniform on compact.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotAdaptiveRegularization 20 declarations Finite-row regularization for the adaptive pilot
Finite-row regularization for the adaptive pilot
For the supplied quantities and conditions, the adaptive pilot size is the mathematical object specified below.
Definition (Lean source)
Under the supplied quantities and conditions, the adaptive pilot size le assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive pilot size eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive pilot size tendsto at top assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive pilot size sublinear assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the adaptive true param is the mathematical object specified below. The adaptive True Param is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the adaptive true param interior assertion holds. Under the stated assumptions, the adaptive True Param interior.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive true param eq local alternative assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the local alternative tendsto assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the eventually local alternative interior assertion holds. Under the stated assumptions, the eventually local Alternative interior.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the eventually adaptive true param eq assertion holds. Under the stated assumptions, the eventually adaptive True Param eq.
Formal statement
Proof (Lean source)
the direction coord abs le assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the eventually local alternative dist lt uniform assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the eventually local Alternative dist lt uniform.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the eventually local alternative interior uniform assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the eventually local Alternative interior uniform.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the eventually adaptive true param eq uniform assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the eventually adaptive True Param eq uniform.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the eventually adaptive true param dist lt uniform assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the eventually adaptive True Param dist lt uniform.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the eventually adaptive true param mem open uniform assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the eventually adaptive True Param mem open uniform.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the adaptive pilot prefix mass is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Pilot Prefix Mass is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the adaptive pilot prefix mass nonneg assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Prefix Mass nonneg.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive pilot prefix mass sum assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotAdaptiveTransfer 6 declarations Finite pilot transfer lemmas for local limits and risks
Finite pilot transfer lemmas for local limits and risks
the finite pilot conditional cdf tendsto assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the finite pilot good bad average error le assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the finite Pilot good bad average error le.
Formal statement
Proof (Lean source)
the finite pilot good bad average tendsto assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the adaptive main scale tendsto one assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the adaptive main scale mul tendsto assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the adaptive sqrt scale mul tendsto assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotAttainmentSupport 23 declarations This file supplies the finite pilot-prefix integral decomposition and the outer asymptotic packaging used by the private-pilot theorem.
Assembly lemmas for private-pilot attainment
This file supplies the finite pilot-prefix integral decomposition and the outer asymptotic packaging used by the private-pilot theorem. It deliberately does not depend on the generic triangular-array limit theorem.
The observed coordinates lying in the pilot portion of a transcript. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
Under a finite product law with normalized one-coordinate weights, the weighted expectation of a coordinate sum is the number of coordinates times the one-coordinate weighted expectation. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For a fixed pilot selection and a nonempty main row, the product-law expectation of the corrected main-sample estimator is centered at the true contrast. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Main centered product sum.
Formal statement
Proof (Lean source)
Split a finite sum at a bounded initial segment. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
On an encoded pilot/main transcript, tauStar is the pilot contrast plus the average of the selected main-release scores. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the tau Star pilot Adaptive Encode.
Formal statement
Proof (Lean source)
Conditional on a proper pilot prefix, the exact joint-law atom masses center the encoded main-row estimator at the true contrast. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Adaptive encoded centered sum.
Formal statement
Proof (Lean source)
A transcript outside the correctly tagged pilot/main encoding has zero mass under the exact private-pilot law. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Adaptive singleton zero of not range.
Formal statement
Proof (Lean source)
The joint pilot/main transcript encoding is injective. For the displayed inputs and conditions, the stated result follows.
Formal statement
Proof (Lean source)
A finite sum supported on an injectively parameterized range can be reindexed by the parameters. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The centered private-pilot estimator has integral zero on every observed pilot-prefix fiber. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot prefix cell centered.
Formal statement
Proof (Lean source)
A Wald pivot with an explicit zero-variance fallback. The fallback makes the closed-interval event exactly equivalent to the unstudentized Wald event, including samples on which the variance estimate is zero. The wald Fallback Pivot is determined by the displayed parameters.
Membership of the fallback pivot in the symmetric cutoff interval is exactly the corresponding Wald inequality. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The main-sample empirical variance is nonnegative on every transcript. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The fallback-studentized private-pilot estimation error. The pilot Wald Pivot is determined by the displayed parameters.
Definition (Lean source)
At every positive sample size, the private-pilot Wald coverage event is the symmetric closed-interval event for the fallback pivot. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot wald event eq.
Formal statement
Proof (Lean source)
Convergence of the fallback-pivot interval probability transfers directly to the private-pilot Wald coverage probability. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot wald coverage of pivot Icc.
Formal statement
Proof (Lean source)
If a centered integrand has integral zero on every finite pilot-prefix fiber, multiplying it by any statistic determined by the pilot prefix remains integrable and has integral zero. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Fiberwise centering of the pilot estimator implies the full conditional unbiasedness clause against every bounded measurable pilot statistic. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot conditional unbiasedness of prefix cells.
Formal statement
Proof (Lean source)
The private-pilot estimator satisfies the headline conditional unbiasedness clause under the stated sublinear pilot condition. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot conditional unbiasedness.
Formal statement
Proof (Lean source)
A centered Gaussian law has a finite second moment in the extended-real form required by RegularProcedure. For the displayed inputs and conditions, the stated result follows.
Formal statement
Proof (Lean source)
A weak local Gaussian limit and the defining uniform squared-tail condition assemble into the regular-procedure interface. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The pilot weak limit, plug-in variance consistency, and uniform squared tails package the three asymptotic interfaces consumed together by the attainment theorem. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot limit variance regular of core.
Formal statement
Proof (Lean source)
If every positive-radius local worst-risk sequence has the same liminf, the outer radius supremum in localAsymptoticRisk equals that value. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotBridge 20 declarations This file isolates two interfaces needed by the pilot construction: reducing conditional cylinder factorization to a joint-law identity, and the pointwise existence part of the saddle selector.
Bridges for the private-pilot construction
This file isolates two interfaces needed by the pilot construction: reducing conditional cylinder factorization to a joint-law identity, and the pointwise existence part of the saddle selector.
the transcript factorizes of joint assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the exists saddle pointwise assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the exists saddle pointwise.
Formal statement
Proof (Lean source)
the fs history to private is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the measurable fs history to private assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the private to fs history is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
the measurable private to fs history assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the fs history to private left inv assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the fs history to private right inv assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the history measurable equiv is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the fs transcript to transcript is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the transcript to fs transcript is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the measurable fs transcript to transcript assertion holds.
Formal statement
Proof (Lean source)
the measurable transcript to fs transcript assertion holds.
Formal statement
Proof (Lean source)
The finite-sequence kernel family is determined by the displayed parameters.
Definition (Lean source)
The transcript law generated by a finite sequence of kernels is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the transcript prefix is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
the measurable transcript prefix assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The explicit finite transcript construction has exactly the library finite-sequence prefix law. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the finite sequence transcript factorizes assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the exists transcript factorization assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotCDFIdentity 6 declarations This file separates the finite-sample distributional step from the later triangular-row Gaussian limit.
Exact conditional CDF identity for the private pilot estimator
This file separates the finite-sample distributional step from the later
triangular-row Gaussian limit. The conditional CDF below is the literal iid
main-row product mass evaluated on the centered root-n estimator error.
A finite sum is invariant under the canonical transport along an equality of its row lengths. For the displayed inputs and conditions, the stated result follows.
Formal statement
The conditional CDF of the centered root-n error in one adaptive iid main row. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Pilot Row Scaled CDF is determined by the displayed parameters.
Definition (Lean source)
The genuine released-prefix mixture of the conditional adaptive-row CDF. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The pilot Prefix Scaled Error CDF is determined by the displayed parameters.
Definition (Lean source)
On a correctly encoded transcript, the centered scaled estimator error is the scaled average of the literal centered adaptive main-row scores. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the scaled Error pilot Adaptive Encode eq adaptive Pilot Row.
Formal statement
Proof (Lean source)
At every proper pilot split with an interior local alternative, the actual scaled-error transcript CDF is exactly the released-prefix mixture of the conditional centered iid-row CDFs. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Law scaled Error le eq of Real pilot Prefix Scaled Error CDF.
Formal statement
Proof (Lean source)
The real-valued CDF of the actual scaled estimator error is the genuine prefix-weighted conditional row CDF. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Law real scaled Error le eq pilot Prefix Scaled Error CDF.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotGaussianTransfer 7 declarations This module transfers an explicit conditional Gaussian CDF limit for every convergent sequence of genuine pilot selectors to the unconditional CDF of the actual private-pilot transcript.
Transfer of conditional pilot-row Gaussian limits
This module transfers an explicit conditional Gaussian CDF limit for every convergent sequence of genuine pilot selectors to the unconditional CDF of the actual private-pilot transcript. It contains no triangular-array CLT: that analytic input remains a premise of the main theorem.
The shrinking localization radius used to average conditional row limits. It goes to zero slowly enough that the pilot Chebyshev bound still vanishes. For the displayed inputs and conditions, the stated result follows. The pilot Gaussian Radius is determined by the displayed parameters.
Definition (Lean source)
The pilot-size component of pilotGaussianRadius tends to zero. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The localization radius tends to zero. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Convergence along every selected subsequence gives uniform control over raw released prefixes in the shrinking Gaussian-transfer neighborhood. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Prefix CDF uniform of subsequential tendsto.
Formal statement
Proof (Lean source)
The varying-radius Chebyshev envelope used in Gaussian transfer vanishes. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Gaussian Bad Envelope tendsto zero.
Formal statement
Proof (Lean source)
An explicit conditional adaptive-row Gaussian CDF limit along every subsequence and every convergent genuine selector sequence implies the exact unconditional scaled-error CDF limit of the private-pilot transcript. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot scaled Error cdf tendsto of conditional Rows.
Formal statement
Proof (Lean source)
A conditional adaptive-row Gaussian CDF limit for every local direction and threshold transfers to the corresponding family of actual transcript CDF limits. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot scaled Error cdf tendsto of all conditional Rows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotGrowth 29 declarations Uniform growth bounds for the pilot saddle score
Uniform growth bounds for the pilot saddle score
Under the supplied quantities and conditions, the pattern ray le exp assertion holds. Under the stated assumptions, the pattern Ray le exp.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pattern mass one le assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pattern Mass one le.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pattern mass le exp assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pattern Mass le exp.
Formal statement
Proof (Lean source)
the pilot reference weight is the mathematical object specified below. The pilot Reference Weight is determined by the displayed parameters.
Definition (Lean source)
the pilot reference weight feasible assertion holds.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pilot lower a is the mathematical object specified below. The pilot Lower A is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the pilot lower b is the mathematical object specified below. The pilot Lower B is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the pilot lower a pos assertion holds. Under the stated assumptions, the pilot Lower A pos.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot lower b pos assertion holds. Under the stated assumptions, the pilot Lower B pos.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the seventh pattern information quadratic assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot reference objective lower assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Reference Objective lower.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pilot j lower is the mathematical object specified below. The pilot JLower is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the pilot j lower pos assertion holds. Under the stated assumptions, the pilot JLower pos.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot j lower le quadratic assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot JLower le quadratic.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the staircase weight le one assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the staircase Weight le one.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pilot objective zero upper is the mathematical object specified below. The pilot Objective Zero Upper is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the information objective zero le upper assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the information Objective zero le upper.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the strong selector j bounds assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the strong Selector J bounds.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pilot t upper is the mathematical object specified below. The pilot TUpper is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the strong selector t bound assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the strong Selector t bound.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pilot score growth upper is the mathematical object specified below. The pilot Score Growth Upper is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the strong selector score growth bound assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the strong Selector score Growth bound.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pilot gradient upper is the mathematical object specified below. The pilot Gradient Upper is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the pilot gradient upper nonneg assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the projected gradient abs le assertion holds.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pilot phi upper is the mathematical object specified below. The pilot Phi Upper is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the strong selector phi tilde bound assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the strong Selector phi Tilde bound.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot phi upper nonneg assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Phi Upper nonneg.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the strong selector phi output bound assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the strong Selector phi Output bound.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotLocalRiskAttainment 10 declarations Exact local-risk attainment for the private-pilot estimator
Exact local-risk attainment for the private-pilot estimator
The parameter-free Chebyshev envelope appearing in the bad-prefix bound. For the displayed inputs and conditions, the stated result follows. The pilot Bad Mass Envelope is determined by the displayed parameters.
Definition (Lean source)
For every fixed positive localization radius, pilot divergence makes the uniform Chebyshev envelope vanish. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Bad Mass Envelope tendsto zero.
Formal statement
Proof (Lean source)
The clipping regularizer is eventually smaller than every fixed positive margin when the pilot size diverges. For the displayed inputs and conditions, the stated result follows.
Formal statement
Proof (Lean source)
For every bounded local direction, the genuine prefix-averaged selected variance converges uniformly to the oracle variance. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the eventually uniform pilot Prefix Variance Average.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot prefix variance average bounds assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Prefix Variance Average bounds.
Formal statement
Proof (Lean source)
The finite main-row correction preserves the uniform prefix-risk limit. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the eventually uniform scaled Prefix Variance Average.
Formal statement
Proof (Lean source)
Uniform real-risk control sandwiches the local worst risk between two finite ENNReal.ofReal bounds. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the eventually local Worst Risk sandwich.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot local worst risk tendsto assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot local Worst Risk tendsto.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot liminf local worst risk eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot liminf local Worst Risk eq.
Formal statement
Proof (Lean source)
The private-pilot estimator attains the exact local asymptotic risk. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot local Asymptotic Risk eq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotLocalRiskConvergence 10 declarations Uniform finite-prefix control for private-pilot local risk
Uniform finite-prefix control for private-pilot local risk
The literal probability mass of a released pilot prefix. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The pilot Prefix Weight is determined by the displayed parameters.
Definition (Lean source)
Prefix mass on which the clipped pilot selector leaves a coordinatewise r-neighborhood of the row parameter. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The pilot Prefix Bad Mass is determined by the displayed parameters.
Definition (Lean source)
The selected-score variance averaged over the genuine pilot-prefix law. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The pilot Prefix Variance Average is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the pilot prefix weight nonneg assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Prefix Weight nonneg.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot prefix weight sum assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The real bad-prefix mass is exactly the corresponding event probability under the full transcript law. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Law pilot Theta bad eq of Real prefix Bad Mass.
Formal statement
Proof (Lean source)
Uniform Chebyshev control of the bad prefix mass. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Prefix Bad Mass le.
Formal statement
Proof (Lean source)
A deterministic good/bad decomposition for the prefix-averaged variance. It uses the exact prefix weights and leaves only the genuine bad-prefix mass. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Prefix Variance Average error le.
Formal statement
Proof (Lean source)
Continuity at the diagonal gives one common neighborhood controlling both the local row parameter and the selected pilot parameter. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Score Variance uniform near diag.
Formal statement
Proof (Lean source)
Compact notation for the exact local-risk identity on the local index set. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Estimator local Risk eq scaled prefix Variance Average.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotLocalRiskIdentity 2 declarations Exact transcript-law identity for private-pilot local risk
Exact transcript-law identity for private-pilot local risk
At every proper finite pilot split for which the local alternative is interior, the transcript-law local risk is exactly the prefix average of the conditional selected-score variances, including the finite main-size factor. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Estimator local Risk eq prefix Variance.
Formal statement
Proof (Lean source)
The exact risk identity applies to every direction in the finite-sample local index set; its membership condition supplies precisely the interiority needed by the transcript-law factorization. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Estimator local Risk eq prefix Variance of mem local Index Set.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotLocalRiskSupport 5 declarations Exact conditional local risk of the adaptive main row
Exact conditional local risk of the adaptive main row
The squared sum of a centered finite iid row has expectation equal to the row length times the one-coordinate second moment. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Conditional on a convergent sequence of interior pilot selectors, the exact squared main-row estimation error is the adaptive score variance divided by the main-row size. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row conditional mean Square.
Formal statement
Proof (Lean source)
The exact conditional mean-square error after root-n scaling. The finite-sample discrepancy from the selected-score variance is precisely the main-row fraction n / (n - m n). For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row conditional root N mean Square.
Formal statement
Proof (Lean source)
Along every convergent sequence of interior pilot selectors, the exact conditional root-n risk value converges to the oracle variance. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row root N risk Value tendsto.
Formal statement
Proof (Lean source)
Averaging the exact conditional risk over every finite pilot prefix leaves only the prefix average of the selected-score variances. This is the exact finite-law risk decomposition, before any pilot-localization limit is used. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Prefix root N mean Square.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotLocalization 7 declarations Quantitative localization of the randomized-response pilot
Quantitative localization of the randomized-response pilot
The affine inverse applied to one released-category frequency. For the displayed inputs and conditions, the stated result follows. The pilot Inverse Frequency is determined by the displayed parameters.
Under the supplied quantities and conditions, the pilot inverse frequency sub private mass assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Inverse Frequency sub private Mass.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot inverse frequency error abs assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Inverse Frequency error abs.
Formal statement
Proof (Lean source)
Clipping does not change a raw inverse which lies in its clipping interval. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the clip Interior eq of abs sub lt.
Formal statement
Proof (Lean source)
A sufficiently accurate pair of calibrated pilot frequencies puts the clipped pilot estimate in the fixed coordinatewise r-neighborhood of the truth. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Theta localized of frequency.
Formal statement
Proof (Lean source)
Uniform Chebyshev concentration of one released pilot-cell frequency. The bound is parameter free apart from the exact centering probability. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Frequency deviation le.
Formal statement
Proof (Lean source)
The two-coordinate clipped pilot leaves an r-neighborhood of its true parameter with probability at most the sum of two parameter-uniform Chebyshev bounds. This form applies row by row to local parameter sequences. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Theta deviation le.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotMoments 14 declarations Algebraic moment identities for the pilot score
Algebraic moment identities for the pilot score
The randomized-response pilot output has the affine categorical probability used by the inverse-frequency estimator. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Inverting the exact randomized-response pilot probability recovers the corresponding private-input cell probability. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the rr Pilot inverse marginal probability.
Formal statement
Proof (Lean source)
Clipping is inactive once its margin is inside both distances to the boundary. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
At a minimizing contrast direction, the information matrix sends that direction to its quadratic value times the contrast vector. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The saddle direction satisfies the exact score normal equation. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pattern mass affine difference assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pattern gradient eq ray sub assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the staircase weighted gradient sum eq zero assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the staircase weighted Gradient sum eq zero.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the staircase weighted projected gradient sum eq zero assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the staircase weighted Projected Gradient sum eq zero.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the information matrix mul vec direction apply assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Exact one-step affine correction identity. If η selects a feasible saddle (α,t,J), then averaging its influence score under the true parameter θ corrects contrast η exactly to contrast θ. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the affine Correction mean identity.
Formal statement
Proof (Lean source)
The selected affine correction has the exact mean shift under every interior parameter. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the phi Tilde mean identity.
Formal statement
Proof (Lean source)
At its construction parameter, a saddle affine correction has second moment equal to reciprocal saddle information. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the affine Correction second Moment identity.
Formal statement
Proof (Lean source)
The selected influence value has exact conditional second moment Vstar at the selection parameter. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the phi Tilde second Moment identity.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotPrefix 29 declarations Finite-prefix laws for the randomized-response pilot
Finite-prefix laws for the randomized-response pilot
the fin prod ite lt assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the fin prod ite lt.
Formal statement
Proof (Lean source)
the fin sum ite lt assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the fin sum ite lt.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the rr pilot kernel singleton assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pi theta sum eq one assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the input path probability sum eq one assertion holds.
Formal statement
Proof (Lean source)
the transcript law is probability assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Law is Probability.
Formal statement
Proof (Lean source)
Marginalizing independent private inputs turns the deterministic-path pilot prefix product into the product of calibrated RR marginals. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the input Path prefix rr sum.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the rr pilot marginal sum eq one assertion holds.
Formal statement
Proof (Lean source)
The one-coordinate randomized-response marginal after integrating out the private four-cell input. For the displayed inputs and conditions, the stated result follows. The rr Pilot Marginal is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the rr pilot marginal singleton assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the rr pilot marginal is probability assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the rr Pilot Marginal is Probability.
Formal statement
Proof (Lean source)
For a deterministic private-input path, every initial segment lying wholly inside the pilot has the product randomized-response atom probability. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Prefix component singleton.
Formal statement
Proof (Lean source)
After marginalizing the IID private-input path, every all-pilot prefix atom has the product of the calibrated RR marginal probabilities. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Prefix marginal singleton.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pilot prefix embed is the mathematical object specified below.
Definition (Lean source)
the pilot prefix embed injective assertion holds.
Formal statement
Proof (Lean source)
The marginalized pilot prefix is concentrated on four-category releases; the masses of those atoms sum to one. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Prefix range measure.
Formal statement
Proof (Lean source)
The finite pilot prefix has exactly the IID product law of the calibrated four-category randomized-response marginal, embedded into pilot outputs. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Prefix law eq map pi.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pilot prefix frequency is the mathematical object specified below.
For the supplied quantities and conditions, the pilot prefix output frequency is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
Under the supplied quantities and conditions, the pilot frequency eq prefix frequency assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Each empirical pilot-cell frequency is measurable.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot prefix frequency embed assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot frequency map eq pi assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Frequency map eq pi.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the pilot cell indicator is the mathematical object specified below.
Definition (Lean source)
Each pilot-cell indicator is measurable.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the integrable pilot cell indicator assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the integrable pilot Cell Indicator.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the integral pilot cell indicator assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the integral pilot Cell Indicator.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot prefix frequency map pi eq sample mean assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Prefix Frequency map pi eq sample Mean.
Formal statement
Proof (Lean source)
Each released pilot-cell frequency obeys the categorical weak law under the actual finite transcript experiment. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Frequency tendsto In Probability.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotRates 2 declarations The integer square-root pilot size diverges, remains asymptotically negligible, and lies strictly between zero and the full sample size once n ≥ 2.
Square-root pilot sample size
The integer square-root pilot size diverges, remains asymptotically negligible,
and lies strictly between zero and the full sample size once n ≥ 2.
The integer square-root pilot sample size tends to infinity. The stated result follows.
Formal statement
Proof (Lean source)
The integer square-root pilot is sublinear and is a nonempty proper split for every sample size at least two. The stated result follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotRowGaussianLimit 1 declarations This module instantiates the finite bounded iid triangular-row central limit theorem with the genuine adaptive main-release mass and centered score.
Gaussian limit for the conditional adaptive pilot row
This module instantiates the finite bounded iid triangular-row central limit theorem with the genuine adaptive main-release mass and centered score. It also transfers the generic row-length normalization to the paper's root-total-sample normalization.
Along every strict sample-size subsequence and every convergent sequence of interior pilot selectors, the actual centered conditional main-row CDF converges to the oracle Gaussian CDF under root-total-sample scaling. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotRowInputs 17 declarations This module packages the exact finite alphabet mass and centered score used by the adaptive main sample.
Finite triangular-row inputs for private-pilot attainment
This module packages the exact finite alphabet mass and centered score used by the adaptive main sample. It stays independent of the generic triangular-array substrate, so a later adapter can instantiate that substrate without rebuilding the paper-specific mass, centering, boundedness, variance, and finite-product algebra.
The one-coordinate mass in the adaptive main row along a local alternative and a chosen sequence of pilot selectors. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Pilot Row Mass is determined by the displayed parameters.
Definition (Lean source)
The selected main-release score centered by its exact one-coordinate mean. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Pilot Row Score is determined by the displayed parameters.
Definition (Lean source)
The limiting row variance as a nonnegative real. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Pilot Limit Variance is determined by the displayed parameters.
Definition (Lean source)
The adaptive main row has nonnegative one-coordinate masses. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row Mass nonneg.
Formal statement
Proof (Lean source)
The adaptive main row masses sum to one. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row Mass sum.
Formal statement
Proof (Lean source)
The adaptive main-row score is exactly centered under its row mass. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row Score centered.
Formal statement
Proof (Lean source)
The exact mean correction is no larger than the common selected-score bound. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row Mean abs le.
Formal statement
Proof (Lean source)
Every centered adaptive row score is bounded by twice the common selected-score bound. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row Score abs le.
Formal statement
Proof (Lean source)
The one-coordinate second moment of the centered row score is exactly the adaptive score variance. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row second Moment eq.
Formal statement
Proof (Lean source)
The regularized local parameter converges to the base parameter. For the displayed inputs and conditions, the stated result follows. Under the stated assumptions, the adaptive True Param tendsto.
Formal statement
Proof (Lean source)
If the selected pilot parameters converge to the base point, the centered adaptive row variances converge to the oracle variance. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row variance tendsto.
Formal statement
Proof (Lean source)
The limiting adaptive row variance is strictly positive. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Limit Variance pos.
Formal statement
Proof (Lean source)
The literal iid product mass of an adaptive main row. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Pilot Row Product Mass is determined by the displayed parameters.
Definition (Lean source)
Every conditional main-row product atom has nonnegative mass. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row Product Mass nonneg.
Formal statement
Proof (Lean source)
The conditional iid main-row product masses sum to one. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row Product Mass sum.
Formal statement
Proof (Lean source)
Summing the centered row score subtracts exactly the row length times the paper estimator's mean correction. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row Score sum eq.
Formal statement
Proof (Lean source)
For a nonempty main row, its corrected sample average minus the true contrast is the average centered row score. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row estimator Error eq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotRowUniformization 1 declarations This module turns convergence along every selected bad subsequence of finite pilot prefixes into eventual uniform control over all prefixes whose selected parameter lies in a shrinking neighborhood of the base point.
Sequential uniformization over shrinking pilot neighborhoods
This module turns convergence along every selected bad subsequence of finite pilot prefixes into eventual uniform control over all prefixes whose selected parameter lies in a shrinking neighborhood of the base point.
If every subsequence of finite pilot prefixes whose selected parameters converge to the base point has the same scalar limit, then the scalar errors are eventually uniform over all pilot prefixes selected inside any shrinking radius. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Selector uniform of subsequential tendsto.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotRowVariance 12 declarations This module identifies the paper's main-sample variance estimator with the literal empirical variance of the centered finite row.
Empirical variance identities for adaptive pilot rows
This module identifies the paper's main-sample variance estimator with the literal empirical variance of the centered finite row. It also records the encoded-transcript support factorization and the sample-size scaling used for root-n errors.
The empirical mean of the centered adaptive row score. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Pilot Row Empirical Mean is determined by the displayed parameters.
Definition (Lean source)
The empirical second moment of the centered adaptive row score. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Pilot Row Empirical Second is determined by the displayed parameters.
Definition (Lean source)
The empirical variance of the centered adaptive row score. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Pilot Row Empirical Variance is determined by the displayed parameters.
Definition (Lean source)
A finite nonempty sample's second-moment-minus-mean-square formula equals its average squared deviation from the empirical mean. For the displayed inputs and conditions, the stated result follows.
Formal statement
Proof (Lean source)
The adaptive row empirical variance is its average squared deviation from the empirical row mean. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row Empirical Variance eq average sq deviation.
Formal statement
Proof (Lean source)
On an encoded transcript, summing any transformed main-release score over the full transcript is the corresponding sum over the main row. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Adaptive Encode main score sum.
Formal statement
Proof (Lean source)
On a properly encoded transcript, VhatStar is exactly the empirical variance of the selected main-release scores. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the Vhat Star pilot Adaptive Encode.
Formal statement
Proof (Lean source)
Centering every selected score by the same population correction does not change its empirical variance. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row Empirical Variance eq selected.
Formal statement
Proof (Lean source)
The empirical variance of the population-centered scores in an encoded main row. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The adaptive Encoded Row Empirical Variance is determined by the displayed parameters.
Definition (Lean source)
Under a proper nonempty pilot split, VhatStar on an encoded transcript is exactly the empirical variance of the population-centered main-row score. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the Vhat Star pilot Adaptive Encode eq row Variance.
Formal statement
Proof (Lean source)
Root-n squared main-estimation error is the row-normalized squared sum multiplied by the exact sample-size ratio n / adaptiveMainSize m n. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the adaptive Pilot Row root N error sq.
Formal statement
Proof (Lean source)
The exact transcript atom is its pilot-prefix mass times the conditional iid main-row product mass. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Adaptive joint singleton eq prefix mul main Product.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotSelectorBridge 2 declarations Measurable finite-quadratic selector adapter
Measurable finite-quadratic selector adapter
Under the supplied quantities and conditions, the exists measurable saddle selector bridge strong assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the exists measurable saddle selector bridge strong.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the exists measurable saddle selector bridge assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the exists measurable saddle selector bridge.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotStudentizationSupport 3 declarations This file derives the Slutsky approximation required by the varying-law Wald adapter from the genuine CDF and plug-in variance consistency premises.
Row-varying studentization for the private pilot
This file derives the Slutsky approximation required by the varying-law Wald adapter from the genuine CDF and plug-in variance consistency premises.
A row-varying statistic whose CDF converges to the standard normal is tight. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the varying Law tight of standard Normal cdf.
Formal statement
Proof (Lean source)
Plug-in variance consistency and the Gaussian CDF limit imply that the fallback-studentized pilot pivot is asymptotically indistinguishable from the oracle-standardized scaled error. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Wald Pivot approx standardized Scaled Error.
Formal statement
Proof (Lean source)
The actual standardized-error CDF limit and consistent VhatStar imply the private-pilot Wald coverage limit, with the zero-variance fallback handled inside the proved Slutsky approximation. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot wald coverage of standardized cdf and Vhat Star consistent.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotUniformTails 1 declarations Uniform squared tails for the private-pilot estimator — finite-product fourth moments.
Uniform squared tails for the private-pilot estimator — finite-product fourth moments.
The private-pilot scaled error has uniformly vanishing squared tails over bounded local directions. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot scaled Error uniform squared tails.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotVarianceConsistency 5 declarations The arguments here use only finite-product second-moment bounds.
Consistency of the pilot plug-in variance
The arguments here use only finite-product second-moment bounds. In particular, they are independent of the triangular-array central limit theorem.
A finite-row Chebyshev bound for empirical variance around its own one-coordinate second moment. For the displayed inputs and conditions, the stated result follows. Under the stated assumptions, the event Probability empirical Variance sub one Second le.
Formal statement
Proof (Lean source)
Conditional main-row probability that the encoded empirical variance misses the oracle variance. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The pilot Conditional Variance Bad Mass is determined by the displayed parameters.
Definition (Lean source)
Prefix mixture of the conditional bad-variance probabilities. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The pilot Variance Bad Mass is determined by the displayed parameters.
Definition (Lean source)
The finite-product Chebyshev bound, specialized to one genuine adaptive main row and centered at its population variance. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Conditional Variance Bad Mass le.
Formal statement
Proof (Lean source)
Averaging the uniform finite-row bound over the genuine pilot prefixes gives vanishing bad variance mass. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Variance Bad Mass tendsto zero.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotVhatConsistency 5 declarations Transcript-law wrapper for pilot variance consistency
Transcript-law wrapper for pilot variance consistency
Empirical variance is invariant under transport along an equality of finite row lengths. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Average squared deviations are invariant under transport along an equality of finite row lengths. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
On an encoded row, VhatStar equals the adaptive empirical variance after the canonical main-size reindexing. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the Vhat Star pilot Adaptive Encode eq adaptive Empirical Variance.
Formal statement
Proof (Lean source)
The actual bad-variance transcript event is exactly the real prefix mixture proved consistent in PilotVarianceConsistency. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Law Vhat Star bad eq of Real pilot Variance Bad Mass.
Formal statement
Proof (Lean source)
Under the pilot growth and interiority conditions, the probability under the actual transcript law that VhatStar differs from Vstar by more than any positive tolerance tends to zero. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot Vhat Star consistent.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotWaldLimitSupport 3 declarations The standard studentization API uses one fixed sample space.
Varying-law support for pilot Wald limits
The standard studentization API uses one fixed sample space. Pilot transcripts change with the sample size, so this file supplies the corresponding CDF-level converging-together and interval-probability adapters.
CDF-level converging together for row-varying probability spaces. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the varying Law cdf converging together.
Formal statement
Proof (Lean source)
A negligible row-varying perturbation of a statistic with continuous-limit CDF has the expected probability limit on every continuity interval. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the varying Law Icc tendsto of cdf and approx.
Formal statement
Proof (Lean source)
Exact pilot Wald coverage once the standardized oracle CDF and the row-varying Slutsky approximation to the fallback pivot have been proved. The fallback is retained verbatim, so samples with zero estimated variance are handled by pilot_wald_event_eq. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot wald coverage of standardized cdf and approx.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PilotWeakLimitSupport 2 declarations This file supplies the measure-theoretic bridge from convergence of real CDFs to weak convergence.
CDF support for the pilot weak limit
This file supplies the measure-theoretic bridge from convergence of real CDFs to weak convergence. The paper-specific theorem below deliberately leaves the CDF convergence of the actual centered estimator as an explicit hypothesis.
Pointwise convergence of the CDFs of real probability measures implies weak convergence. This all-points form is convenient for triangular-array adapters. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the probability Measure tendsto of cdf tendsto.
Formal statement
Proof (Lean source)
CDF convergence of the actual centered, root-scaled estimator laws implies the bounded-continuous-test formulation of the local weak limit. The transcript spaces may vary with n; the hypothesis is stated directly using their induced laws. No pilot CLT or CDF convergence is hidden in this adapter. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the weak Local Limit of scaled Error cdf tendsto.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.PostprocessCardinality 3 declarations Positive active staircase rays whose postprocessing laws are pairwise mutually singular require distinct positive-mass output atoms.
Output cardinality under a singular postprocessing refinement
Positive active staircase rays whose postprocessing laws are pairwise mutually singular require distinct positive-mass output atoms. The argument works for arbitrary measurable structures on a finite output type and returns the definitional infinite bound for nonfinite output types.
the postprocess row ac input assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the input zero ac output law assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the active card le output cardinality of pairwise singular assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the active card le output Cardinality of pairwise singular.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.Procedures 18 declarations A transcript experiment carries its history-dependent channels and the induced finite transcript laws.
Sequential experiments and local procedures
A transcript experiment carries its history-dependent channels and the induced finite transcript laws. The laws are pinned by the conditional cylinder factorization, which is valid on arbitrary measurable output spaces.
For the supplied quantities and conditions, the output family is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The Output Family is the displayed object.
Definition (Lean source)
For the supplied quantities and conditions, the transcript is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The Transcript is determined by the displayed parameters.
Definition (Lean source)
the history prefix is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the transcript factorizes is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
For the supplied quantities and conditions, this procedure sequence packages the stated mathematical data. The Procedure Sequence is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the input path probability is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The input Path Probability is determined by the displayed parameters.
Definition (Lean source)
the transcript law is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The transcript Law is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the local alternative is the mathematical object specified below. The local Alternative is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the local index set is the mathematical object specified below. The local Index Set is determined by the displayed parameters.
Definition (Lean source)
the scaled error is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The scaled Error is determined by the displayed parameters.
Definition (Lean source)
the local risk is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The local Risk is determined by the displayed parameters.
Definition (Lean source)
the local worst risk is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The local Worst Risk is determined by the displayed parameters.
Definition (Lean source)
the local asymptotic risk is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The local Asymptotic Risk is determined by the displayed parameters.
Definition (Lean source)
the weak local limit is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The Weak Local Limit is determined by the displayed parameters.
Definition (Lean source)
the regular procedure is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The Regular Procedure is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the exists selected direction assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the exists selected Direction.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the selected direction is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The selected Direction is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the vt handle is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The vt Handle is determined by the displayed parameters.
Definition (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.QuadraticConvexity 2 declarations The profile is a nonnegative weighted sum of squared affine scores.
Convexity of the staircase information profile
The profile is a nonnegative weighted sum of squared affine scores.
Under the supplied quantities and conditions, the information objective convex time assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the information Objective convex time.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the information objective convex on time assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the information Objective convex On time.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.R3Continuity 19 declarations This file supplies the canonical stationarity direction, continuity of the rational information data on the interior, and an explicit right inverse for the three active dual-ray equations.
Continuous certificate data for the three-output region
This file supplies the canonical stationarity direction, continuity of the rational information data on the interior, and an explicit right inverse for the three active dual-ray equations. It also gives the local form of the promoted anchored linear solver needed when coefficients are only continuous at the certificate point.
The scalar score direction used in the three-output region is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the r3 stationarity affine assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r3 stationarity r3 direction eq zero assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the region parameter is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The Region Parameter is the displayed object.
Definition (Lean source)
For the supplied quantities and conditions, the region theta is the mathematical object specified below.
Definition (Lean source)
Under the supplied quantities and conditions, the continuous pattern ray region assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous pattern mass region assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at projected gradient region assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at pattern information region assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at projected score region assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at pattern information slope region assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at r3 stationarity region assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at r3 direction region assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the r3 mask is the mathematical object specified below.
The dual constraint matrix for the three-output region is determined by the displayed parameters.
Definition (Lean source)
A right inverse for the three-output dual matrix is determined by the displayed parameters.
Under the supplied quantities and conditions, the r3 dual matrix mul right inverse assertion holds. Under the stated assumptions, the r3 Dual Matrix mul right Inverse.
Formal statement
Proof (Lean source)
the continuous r3 dual matrix assertion holds.
Formal statement
Proof (Lean source)
the exists eventually anchored solution of right inverse assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the exists eventually anchored Solution of right Inverse.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.R3Rigidity 3 declarations The strict certificate confines every optimal staircase design to the three active masks.
Rigidity of the three-ray certificate
The strict certificate confines every optimal staircase design to the three
active masks. At privacy level log 3, normalization then fixes all three
weights to 1/5.
Under the supplied quantities and conditions, the r3 certificate profile optimal and rigid assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the r3 feasible eq canonical assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the r3 feasible eq canonical.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r3 certificate unique optimum log3 assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.R5Continuity 48 declarations The four active rows used to determine the dual certificate have an explicit right inverse throughout the positive-privacy parameter region.
Continuous active-dual solver for the five-output region
The four active rows used to determine the dual certificate have an explicit right inverse throughout the positive-privacy parameter region. The fifth active equality is supplied separately by the two constituent-objective identity in the R5 continuation argument.
For the supplied quantities and conditions, the r5 dual mask is the mathematical object specified below.
The dual constraint matrix for the five-output region is determined by the displayed parameters.
Definition (Lean source)
A right inverse for the five-output dual matrix is determined by the displayed parameters.
Under the supplied quantities and conditions, the r5 dual matrix mul right inverse assertion holds. Under the stated assumptions, the r5 Dual Matrix mul right Inverse.
Formal statement
Proof (Lean source)
the continuous r5 dual matrix assertion holds.
Formal statement
Proof (Lean source)
The normalized objective contributed by the two binary active rays. The r5 Binary Objective is determined by the displayed parameters.
Definition (Lean source)
The normalized objective contributed by the three ternary active rays. The r5 Ternary Objective is determined by the displayed parameters.
Definition (Lean source)
The binary component coefficient in the five-output continuation argument is determined by the displayed parameters.
Definition (Lean source)
The ternary component coefficient in the five-output continuation argument is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the r5 binary objective eq quadratic assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 ternary objective eq quadratic assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 coeffs pos of interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the r5 Coeffs pos of interior.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at r5 binary coeff assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at r5 ternary coeff assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The scaling factor in the five-output continuation argument is determined by the displayed parameters.
Definition (Lean source)
The selected directional branch for the five-output region is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the r5 scale sq assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 direction branch objectives eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the r5 Direction Branch objectives eq.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the exists r5 direction branch eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at r5 scale assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at r5 direction branch assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The mixture coordinate induced by a staircase weight is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the r5 supported feasible parameterization assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the r5 supported feasible parameterization.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 mixture coordinate mem ioo assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the r5 Mixture Coordinate mem Ioo.
Formal statement
Proof (Lean source)
The derivative of the binary continuation component is determined by the displayed parameters.
Definition (Lean source)
The derivative of the ternary continuation component is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the r5 binary derivative eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 ternary derivative eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 stationarity eq mixture assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the r5 stationarity eq mixture.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 ternary derivative ne zero of objectives eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the mixture stationarity solve assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The continued mixture coordinate for the five-output region is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the r5 continued mixture eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the r5 Continued Mixture eq.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at r5 binary derivative comp assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at r5 ternary derivative comp assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the continuous at r5 continued mixture assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The staircase weight reconstructed from a mixture coordinate is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the r5 weight from coordinate feasible assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 weight from coordinate eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the r5 Weight From Coordinate eq.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 weight from coordinate active assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 weight from coordinate pos assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 weight from coordinate stationarity assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 continued weight stationary assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The target vector in the five-output dual system is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the continuous at r5 dual target assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the exists local r5 dual assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the exists local r5 Dual.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the r5 fifth dual eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The five active dual equalities force the two normalized constituent objectives to agree. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.R5Rigidity 3 declarations Linear rigidity of the five-ray feasible family
Linear rigidity of the five-ray feasible family
the r5 active is the mathematical object specified below.
The four normalization equations leave exactly the expected one-dimensional family on the five active rays. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the r5 supported feasible coordinates.
Formal statement
Proof (Lean source)
A single binary-ray coordinate determines a feasible weight supported on the five-ray family. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the r5 supported feasible eq of five eq.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.Refinement 17 declarations The refinement splits each output density into fourteen extreme rays.
Measurable staircase refinement
The refinement splits each output density into fourteen extreme rays. Equality in one information direction constrains rays mixed by a common output law.
Under the supplied quantities and conditions, the channel fisher info staircase eq information matrix assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the channel Fisher Info staircase eq information Matrix.
Formal statement
Proof (Lean source)
the information quadratic is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Under the supplied quantities and conditions, the information quadratic eq pattern sum assertion holds.
Formal statement
Proof (Lean source)
Every row of a finite-input channel is bounded by its dominating measure.
Formal statement
Proof (Lean source)
the channel row absolutely continuous dominating assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the channel density measurable assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the channel density nonneg assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the channel density le one ae assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Directional information as a single row-sum Radon--Nikodym integral. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the information Quadratic eq channel Integral.
Formal statement
Proof (Lean source)
the ldp row le assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the integral channel density assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the integral channel density eq one assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the privacy increment pos assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the complementary pattern ray assertion holds.
Formal statement
Proof (Lean source)
the staircase refinement interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the staircase refinement interior.
Formal statement
Proof (Lean source)
the channel fisher info pos semidef assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the channel Fisher Info pos Semidef.
Formal statement
Proof (Lean source)
the staircase refinement assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.RegionOpenness 6 declarations This file provides the positivity facts and affine stationarity coefficient used to construct local certificates for the three-mask support regime.
Continuity substrate for the three-output region
This file provides the positivity facts and affine stationarity coefficient used to construct local certificates for the three-mask support regime.
Every staircase-pattern mass is positive at interior trial parameters. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pattern Mass pos of interior.
Formal statement
Proof (Lean source)
The canonical weights on masks 0, 5, and 7. The stated result follows. The r3 Weight is determined by the displayed parameters.
Definition (Lean source)
The stationarity equation evaluated at the canonical three-mask weights. For the displayed inputs and conditions, the stated result follows. The r3 Stationarity is determined by the displayed parameters.
Definition (Lean source)
The linear coefficient of the canonical three-mask stationarity equation. For the displayed inputs and conditions, the stated result follows. The r3 Stationarity Coeff is determined by the displayed parameters.
Definition (Lean source)
The unit finite difference of a pattern's information slope is its positive quadratic coefficient. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The canonical three-mask stationarity equation has positive linear coefficient at interior trial parameters and positive privacy budget. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the r3 Stationarity Coeff pos.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.Regions 6 declarations The two support regimes are instances of one finite primal and strict dual certificate predicate.
Certified staircase support regions
The two support regimes are instances of one finite primal and strict dual certificate predicate. The pattern numbers follow the four-bit enumeration.
For the supplied quantities and conditions, the pattern information slope is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The pattern Information Slope is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the dual ray is the mathematical object specified below. The dual Ray is determined by the displayed parameters.
Definition (Lean source)
the active support is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The active Support is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the certified region is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the r3 is the mathematical object specified below.
Definition (Lean source)
the r5 is the mathematical object specified below.
Definition (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialAdjacentScore 16 declarations Actual adjacent-prefix score characterization
Actual adjacent-prefix score characterization
Canonical splitting coordinates, with the last coordinate indexed by the literal successor index rather than by an opaque proof term. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
The inverse of canonicalInitLast. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the measurable canonical init last assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the measurable canonical snoc assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the stated assumptions, canonically rejoining a history with its last observation recovers the original history.
Formal statement
Proof (Lean source)
Under the stated assumptions, splitting a canonically extended history recovers its original history and last observation.
Formal statement
Proof (Lean source)
the integrable transcript prefix mixture real derivative assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the conditional transcript prefix directional score integrable general assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the conditional Transcript Prefix Directional Score integrable general.
Formal statement
Proof (Lean source)
the set integral conditional transcript prefix directional score assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the set Integral conditional Transcript Prefix Directional Score.
Formal statement
Proof (Lean source)
the transcript successor law map canonical init last assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Successor Law map canonical Init Last.
Formal statement
Proof (Lean source)
The actual successor-prefix score, written in canonical split coordinates. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The actual Successor Score In Coordinates is determined by the displayed parameters.
Definition (Lean source)
the measurable actual successor score in coordinates assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the actual successor score in coordinates integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the actual Successor Score In Coordinates integrable.
Formal statement
Proof (Lean source)
the has deriv at transcript prefix event mass assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the has Deriv At transcript Prefix Event Mass.
Formal statement
Proof (Lean source)
The actual adjacent prefix score is the inherited prefix score plus the current channel score, almost everywhere under the actual successor law. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the actual Successor Score In Coordinates ae eq candidate.
Formal statement
Proof (Lean source)
Consequently, the adjacent score increment is exactly the current joint-channel directional score almost everywhere. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the actual Successor Score Increment ae eq channel Directional Score.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialBayesMeasurability 4 declarations Measurability of scalar-direction local risks
Measurability of scalar-direction local risks
Squared scaled error is jointly measurable in a scalar local direction and an arbitrary released transcript. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For every procedure, the local risk along a scalar direction is measurable without any countability assumption on the output spaces. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The scalar local-risk measurability hypothesis used by compact-prior Bayes ordering is therefore automatic. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The compact-prior Bayes ordering theorem has no remaining measurability premise for a paper procedure. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialBayesOrdering 6 declarations Compact-prior Bayes risk versus local worst risk
Compact-prior Bayes risk versus local worst risk
Scalar multiplication of a trial-parameter direction. For the displayed inputs and conditions, the stated result follows.
Definition (Lean source)
Euclidean norm scales by the absolute scalar along a trial direction. For the displayed inputs and conditions, the stated result follows.
Formal statement
Proof (Lean source)
The scalar directions indexed by [-R,R] fit in the radius obtained by multiplying R by the Euclidean norm of the base direction. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
An integrable nonnegative real density normalized in the Bochner integral is also normalized after embedding into ENNReal. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
A normalized nonnegative weight preserves a uniform ENNReal upper bound under integration. The measurability conclusion records the exact hypothesis needed by later product and iterated-integral rewrites. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
If a compact family of scalar directions fits inside radius H, then at all sufficiently large sample sizes its normalized Bayes average risk is at most the local worst risk at that radius. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialDomination 8 declarations For a fixed procedure and sample size, summing the deterministic-input transcript laws gives one finite reference measure.
Common domination of sequential transcript experiments
For a fixed procedure and sample size, summing the deterministic-input transcript laws gives one finite reference measure. Every parameterized transcript mixture is absolutely continuous with respect to this measure and therefore has a Radon--Nikodym density on arbitrary measurable output spaces.
The sum of all deterministic-input transcript laws is a common reference measure for the fixed procedure and sample size. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
Every deterministic-input transcript law is dominated by the common reference measure. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Every parameterized transcript law is dominated by the same reference measure, without any countability assumption on the output sigma-fields. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The reference measure has total mass equal to the number of deterministic input paths. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the transcript reference measure is finite is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the transcript law is finite is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The transcript Law is Finite is determined by the displayed parameters.
Definition (Lean source)
The Radon--Nikodym density of a transcript law against its common finite reference measure. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The transcript Density is determined by the displayed parameters.
Definition (Lean source)
Integrating the transcript density against the common reference measure recovers the parameterized transcript law. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialDoob 11 declarations This file equips a full released transcript with its coordinate-prefix filtration and instantiates the generic finite-horizon Doob information decomposition for the paper's global finite-mixture score.
Doob decomposition of the sequential transcript score
This file equips a full released transcript with its coordinate-prefix filtration and instantiates the generic finite-horizon Doob information decomposition for the paper's global finite-mixture score. Identifying the conditional expectations with the explicit prefix scores is kept separate until the score-projection substrate is available.
The prefix filtration on a length-n transcript is generated at time k by the coordinates whose indices are strictly below k. The stated result follows.
Definition (Lean source)
the transcript prefix filtration zero assertion holds.
Formal statement
Proof (Lean source)
the transcript prefix filtration terminal assertion holds.
Formal statement
Proof (Lean source)
The coordinate-prefix filtration agrees with the sigma-algebra pulled back by the explicit prefix map. This is the bridge needed to apply measurable-statistic score projection to the Doob increments. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
At the terminal time, conditioning the global transcript score on the prefix filtration returns the score itself. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the cond Exp global Score terminal.
Formal statement
Proof (Lean source)
At time zero, conditioning the centered global transcript score on the prefix filtration is zero. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the cond Exp global Score initial.
Formal statement
Proof (Lean source)
The paper's global transcript Fisher information is the sum of the squared Doob prefix increments. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the global Score fisher eq doob sum.
Formal statement
Proof (Lean source)
Every prefix increment of the global transcript score is square-integrable. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the global Score doob Increment mem Lp two.
Formal statement
Proof (Lean source)
Every prefix increment of the global transcript score has conditional mean zero given the preceding prefix sigma-algebra. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the cond Exp global Score doob Increment zero.
Formal statement
Proof (Lean source)
The finite sum of the prefix increments recovers the centered global transcript score almost everywhere. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the global Score eq sum doob Increment.
Formal statement
Proof (Lean source)
Distinct prefix increments of the global transcript score are orthogonal. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the global Score doob Increment orthogonal.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialFisherInformation 13 declarations Square integrability and one-step Fisher information
Square integrability and one-step Fisher information
the transcript prefix derivative eq complete data score mixture assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the abs conditional transcript prefix directional score le assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the abs conditional Transcript Prefix Directional Score le.
Formal statement
Proof (Lean source)
the conditional transcript prefix directional score mem lp two assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the conditional Transcript Prefix Directional Score mem Lp two.
Formal statement
Proof (Lean source)
the conditional transcript prefix directional score sq integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the conditional Transcript Prefix Directional Score sq integrable.
Formal statement
Proof (Lean source)
the actual successor score in coordinates sq integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the actual Successor Score In Coordinates sq integrable.
Formal statement
Proof (Lean source)
the lifted prefix directional score sq integrable successor law assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the lifted Prefix Directional Score sq integrable successor Law.
Formal statement
Proof (Lean source)
the channel directional score sq integrable successor law assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the channel Directional Score sq integrable successor Law.
Formal statement
Proof (Lean source)
the integral channel directional score sq successor law assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the integral channel Directional Score sq successor Law.
Formal statement
Proof (Lean source)
the successor channel fisher le upper envelope assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the successor channel Fisher le upper Envelope.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the sum input directional derivative eq zero assertion holds.
Formal statement
Proof (Lean source)
The current channel score has zero integral on every event determined by the predecessor history. This is the exact first-marginal centering input for the remaining cross-term argument. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the set Integral channel Directional Score fst preimage eq zero.
Formal statement
Proof (Lean source)
The score increment is conditionally centered given the predecessor history. This formulation is the one needed to kill the Fisher cross term. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the cond Exp channel Directional Score fst eq zero.
Formal statement
Proof (Lean source)
The lifted predecessor score is orthogonal to the current channel-score increment under the actual successor law. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the integral lifted Prefix mul channel Directional Score eq zero.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialFisherRecursion 13 declarations Finite sequential Fisher recursion
Finite sequential Fisher recursion
the integral lifted prefix score sq eq prefix score sq assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the integral lifted Prefix Score sq eq prefix Score sq.
Formal statement
Proof (Lean source)
the integral actual successor score sq eq prefix successor score sq assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the integral actual Successor Score sq eq prefix Successor Score sq.
Formal statement
Proof (Lean source)
the measurable channel directional score recursion assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the prefix score energy succ assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the prefix Score Energy succ.
Formal statement
Proof (Lean source)
the integral transcript prefix mixture real derivative eq zero assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the prefix score energy zero assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the prefix Score Energy zero.
Formal statement
Proof (Lean source)
the prefix score energy le mul upper envelope assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the prefix Score Energy le mul upper Envelope.
Formal statement
Proof (Lean source)
the terminal prefix score energy eq transcript score energy assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the transcript directional fisher le mul upper envelope assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Directional Fisher le mul upper Envelope.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the input directional derivative scaled direction assertion holds.
Formal statement
Proof (Lean source)
the input path directional derivative scaled direction assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the conditional transcript directional score scaled direction assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the transcript scaled directional fisher le assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Scaled Directional Fisher le.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialGlobalScore 17 declarations Global finite-mixture transcript scores
Global finite-mixture transcript scores
A finite bound for the complete-data path scores. For the displayed inputs and conditions, the stated result follows. The input Path Score Bound is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the input path score bound nonneg assertion holds.
Formal statement
Proof (Lean source)
the abs input path directional score le bound assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the measurable transcript component real density assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the measurable transcript mixture real density assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the measurable transcript mixture real derivative assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the measurable conditional transcript directional score assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the transcript mixture real density nonneg assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Mixture Real Density nonneg.
Formal statement
Proof (Lean source)
The observed transcript score is a finite weighted average of the complete-data path scores and is therefore uniformly bounded. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the abs conditional Transcript Directional Score le.
Formal statement
Proof (Lean source)
the conditional transcript directional score mem lp two assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the conditional Transcript Directional Score mem Lp two.
Formal statement
Proof (Lean source)
the transcript reference ac transcript law of interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Reference ac transcript Law of interior.
Formal statement
Proof (Lean source)
the transcript mixture real density pos ae assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Mixture Real Density pos ae.
Formal statement
Proof (Lean source)
the sum input path directional derivative eq zero assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the integral transcript mixture real derivative eq zero assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the conditional transcript directional score integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the conditional Transcript Directional Score integrable.
Formal statement
Proof (Lean source)
The global observed transcript score is centered under the transcript law. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the integral conditional Transcript Directional Score eq zero.
Formal statement
Proof (Lean source)
the conditional transcript directional score sq integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the conditional Transcript Directional Score sq integrable.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialHistoryTransport 3 declarations Canonical successor history index
Canonical successor history index
The successor index is the canonical Fin n value with numeral part k. Rewriting by this equality before forming a dependent History also aligns its measurable-space instance; the remaining bound proofs are propositionally irrelevant. For the displayed inputs and conditions, the stated result follows.
Definition (Lean source)
Under the supplied quantities and conditions, the next index eq canonical next index assertion holds.
Formal statement
Proof (Lean source)
Under the stated assumptions, the canonical next index has natural-number value equal to the current history length.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialInformationEnvelope 6 declarations This file identifies the least-favorable contrast direction and proves local continuity of its stationary staircase information envelope.
Local sequential information envelope
This file identifies the least-favorable contrast direction and proves local continuity of its stationary staircase information envelope. The resulting sequential criterion is uniform over arbitrary scalar sequences staying in a fixed compact interval.
The selected least-favorable direction has unit contrast. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the contrast selected Direction.
Formal statement
Proof (Lean source)
At the base parameter, the selected direction attains the stationary staircase envelope value Jstar. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the upper Envelope selected Direction.
Formal statement
Proof (Lean source)
Every history-conditioned sequential channel has directional Fisher information at most the stationary envelope in the selected direction. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the sequential Joint Channel fisher selected Direction le upper Envelope.
Formal statement
Proof (Lean source)
At fixed direction, the staircase upper envelope is continuous on the interior trial-parameter space. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the continuous upper Envelope interior.
Formal statement
Proof (Lean source)
Any interior parameter sequence converging to the base point has its selected-direction envelope converge to Jstar at that point. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the tendsto upper Envelope selected Direction of tendsto.
Formal statement
Proof (Lean source)
Uniform sequential form: along any scalar sequence contained in a fixed compact interval, the inverse-root-sample local envelope in the selected direction converges to the base Jstar. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the tendsto upper Envelope compact Scaled selected Direction.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialJointChannel 6 declarations Joint prefix and next-release channels
Joint prefix and next-release channels
The original next-release channel, with a finite input row and a released finite-sequence history. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
Adjoin a common random released prefix to each of the four current-input rows. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The sequential Joint Channel is determined by the displayed parameters.
Definition (Lean source)
the sequential joint channel is markov assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the sequential joint channel stationary ldp assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Mixing the four joint rows gives the prefix measure composed with the observed next-release kernel. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the output Law sequential Joint Channel.
Formal statement
Proof (Lean source)
The joint channel's directional Fisher information is bounded by the finite staircase envelope. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the sequential Joint Channel fisher le upper Envelope.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialLocalRiskOrder 9 declarations Order and limit calculus for the sequential local minimax lower bound
Order and limit calculus for the sequential local minimax lower bound
Every admissible local alternative's risk is bounded by the corresponding local worst risk. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Every fixed direction whose Euclidean norm is at most the radius is eventually admissible at an interior base parameter. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Consequently, the risk at any fixed bounded direction is eventually below the local worst-risk sequence. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
A lower bound on the liminf at one positive radius is already a lower bound on the outer-radius local asymptotic risk. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
An eventually valid finite-sample lower envelope transfers through the liminf and the outer radius supremum. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
A real finite-sample Bayes envelope converging to v gives the exact ENNReal.ofReal v local asymptotic lower bound. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The result identifies the relation called tendsto nat div const add nat mul: given the declared inputs and assumptions, the stated mathematical conclusion holds. Under the stated assumptions, the tendsto nat div const add nat mul.
Formal statement
Proof (Lean source)
The preceding real van Trees envelope also converges after embedding into nonnegative extended reals. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
A finite-n van Trees lower bound with a convergent per-sample information envelope yields the exact local asymptotic reciprocal-information bound. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialLowerBound 6 declarations Universal sequential local asymptotic lower bound
Universal sequential local asymptotic lower bound
the likelihood score vt density eq transcript score assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the likelihood Score vt Density eq transcript Score.
Formal statement
Proof (Lean source)
the fisher information vt density eq transcript score energy assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the fisher Information vt Density eq transcript Score Energy.
Formal statement
Proof (Lean source)
the fisher information scaled selected le upper envelope assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the fisher Information scaled Selected le upper Envelope.
Formal statement
Proof (Lean source)
the integrable vt likelihood fisher section assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the scaled selected fisher integrable and control assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the scaled Selected fisher integrable and control.
Formal statement
Proof (Lean source)
Every sequentially private procedure has local asymptotic risk at least the stationary minimax reciprocal information. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the sequential local Asymptotic Risk lower bound.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialMinimaxAssembly 5 declarations This file packages the elementary order-theoretic and pilot-rate steps used to assemble the sequential local asymptotic minimax theorem.
Structural assembly for sequential minimaxity
This file packages the elementary order-theoretic and pilot-rate steps used to assemble the sequential local asymptotic minimax theorem. In particular, the infimum argument only needs a universal risk lower bound and one regular procedure attaining that bound.
The risks achieved by regular sequential procedures over arbitrary measurable output families. For the displayed inputs and conditions, the stated result follows. The regular Procedure Risk Set is determined by the displayed parameters.
Definition (Lean source)
The integer square-root pilot simultaneously diverges and is sublinear. The stated result follows.
Formal statement
Proof (Lean source)
A universal lower bound for procedure risk is a lower bound for the risks of regular procedures. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The risk of any displayed regular procedure belongs to the regular risk set. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
If every procedure has risk at least the target and one regular procedure attains it, then the infimum over regular risks equals the target. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialObservedKernel 7 declarations Observed kernels for finite IID latent inputs
Observed kernels for finite IID latent inputs
Average one private release row over the fresh IID four-cell input. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The observed Stage Measure is determined by the displayed parameters.
Definition (Lean source)
the measurable observed stage measure assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The observed next-output kernel. The unit coordinate matches the generic finite-horizon score API; the history is the released history only. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The observed Stage Kernel is determined by the displayed parameters.
Definition (Lean source)
the observed stage kernel apply assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the observed stage kernel is markov assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the observed Stage Kernel is Markov.
Formal statement
Proof (Lean source)
Parameterize the observed release kernels along a local affine path. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The observed Kernel Family is determined by the displayed parameters.
Definition (Lean source)
the observed kernel family is markov assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialObservedLaw 1 declarations This file marginalizes the finite IID four-cell input path and identifies the resulting transcript law with the law generated by the observed kernels.
Exact law of the observed sequential experiment
This file marginalizes the finite IID four-cell input path and identifies the resulting transcript law with the law generated by the observed kernels.
Marginalizing the IID four-cell input path in the paper transcript law gives exactly the promoted finite-sequence law of the observed kernels. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialPastScoreIntegral 7 declarations This file rewrites the explicit prefix-mixture derivative from SequentialSuccessorDerivative as an integral of the prefix directional score against the actual prefix law.
The predecessor score in a successor event derivative
This file rewrites the explicit prefix-mixture derivative from
SequentialSuccessorDerivative as an integral of the prefix directional score
against the actual prefix law. It uses only finite-mixture domination and does
not invoke score projection.
The explicit prefix derivative remains integrable after multiplication by a measurable successor-row event section. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
A prefix law is its common reference measure weighted by its Radon--Nikodym derivative. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Multiplying the guarded prefix score by the prefix density recovers the explicit real derivative density everywhere. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the conditional Transcript Prefix Directional Score mul density.
Formal statement
Proof (Lean source)
The predecessor-row derivative is the integral of the actual prefix score times the bounded row-event section under the actual prefix law. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the predecessor Row Event Derivative eq integral past Score.
Formal statement
Proof (Lean source)
The past-score integrand used above is integrable under the actual prefix law. This is the integrability input needed by a subsequent projection or conditional-expectation uniqueness argument. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the integrable conditional Transcript Prefix Directional Score mul successor Row Kernel Section.
Formal statement
Proof (Lean source)
Summing the row identities with the base four-cell probabilities gives the complete predecessor contribution in the successor product rule. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the predecessor Successor Event Derivative eq sum integral past Score.
Formal statement
Proof (Lean source)
Paper-side successor characterization before score projection: the mapped successor law is the joint-channel output law, and every predecessor row derivative is represented by the integrable prefix-score kernel integral. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Successor Law past Score characterization.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialPrefixDensity 13 declarations This file constructs explicit common references, densities, and directional derivative densities after projecting a full transcript to a finite prefix.
Dominated finite-mixture scores on transcript prefixes
This file constructs explicit common references, densities, and directional derivative densities after projecting a full transcript to a finite prefix. The identities are paper-side inputs for score projection and do not use a conditional expectation theorem.
the transcript prefix reference measure is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the transcript prefix law is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The transcript Prefix Law is determined by the displayed parameters.
Definition (Lean source)
the transcript prefix component real density is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the transcript prefix mixture real density is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The transcript Prefix Mixture Real Density is determined by the displayed parameters.
Definition (Lean source)
the transcript prefix mixture real derivative is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The transcript Prefix Mixture Real Derivative is determined by the displayed parameters.
Definition (Lean source)
the conditional transcript prefix directional score is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The conditional Transcript Prefix Directional Score is determined by the displayed parameters.
Definition (Lean source)
the transcript prefix reference measure eq sum assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the transcript prefix law eq sum assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the transcript prefix law ac reference assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the transcript prefix density to real ae eq mixture of interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Prefix Density to Real ae eq mixture of interior.
Formal statement
Proof (Lean source)
the measurable transcript prefix mixture real density assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the measurable transcript prefix mixture real derivative assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the transcript prefix derivative pushforward assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialPriorInformationEnvelope 8 declarations This file upgrades the local stationary-envelope limit to uniform convergence over the compact scalar prior and integrates that envelope against the exact normalized quartic prior used by the sequential van Trees argumen
Compact-prior sequential information envelope
This file upgrades the local stationary-envelope limit to uniform convergence over the compact scalar prior and integrates that envelope against the exact normalized quartic prior used by the sequential van Trees argument.
The inverse-root-sample parameter path agrees with the local alternative indexed by the corresponding scalar multiple of the direction. For the displayed inputs and conditions, the stated result follows.
Formal statement
Proof (Lean source)
A compact scalar family of inverse-root-sample paths is eventually contained in the interior parameter space. For the displayed inputs and conditions, the stated result follows. Under the stated assumptions, the eventually parameter Path compact Scaled interior.
Formal statement
Proof (Lean source)
The selected stationary information envelope converges uniformly over a fixed compact scalar family of inverse-root-sample local paths. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the tendsto Uniformly On upper Envelope compact Scaled selected Direction.
Formal statement
Proof (Lean source)
The prior-averaged per-sample stationary information envelope. The sequential Prior Information Envelope is determined by the displayed parameters.
Definition (Lean source)
Once the compact path lies in the interior, its selected envelope is continuous on the scalar interval and hence measurable for the prior measure. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the aestrongly Measurable prior Weighted upper Envelope.
Formal statement
Proof (Lean source)
For all sufficiently large sample sizes, the prior-weighted stationary information envelope is integrable under the compact parameter measure. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the eventually integrable prior Weighted upper Envelope.
Formal statement
Proof (Lean source)
A pointwise compact-prior Fisher bound by n times the stationary envelope integrates to n times the per-sample prior information envelope. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the integral prior Weighted le nat mul sequential Prior Information Envelope.
Formal statement
Proof (Lean source)
The normalized compact-prior average of the selected per-sample envelope converges to the least-favorable stationary information Jstar. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the tendsto sequential Prior Information Envelope.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialPriorRadiusLimit 3 declarations This file separates the two limits in a local van Trees argument.
Sequential removal of the van Trees prior-radius penalty
This file separates the two limits in a local van Trees argument. At a fixed
prior radius R, the prior Fisher-information term 40 / R ^ 2 remains after
the sample-size limit. Only after transferring that fixed-radius bound to the
local asymptotic risk may one send R to infinity.
At fixed positive prior radius, convergence of the experiment information gives convergence of the full reciprocal denominator, including the prior information term. For the displayed inputs and conditions, the stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
A finite-sample lower bound with a fixed prior radius first yields the corresponding penalized reciprocal-information local asymptotic bound. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Correct two-step assembly for a family of finite-sample van Trees bounds. Under the stated assumptions, the inv information le local Asymptotic Risk of prior Radius family.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialScore 19 declarations This file differentiates the finite latent-input mixture against the common transcript reference measure.
Directional scores for finite sequential transcript mixtures
This file differentiates the finite latent-input mixture against the common transcript reference measure. It identifies the complete-data input-path score and the induced conditional transcript score pointwise.
For the supplied quantities and conditions, the parameter path is the mathematical object specified below. The parameter Path is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the input directional derivative is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
Under the supplied quantities and conditions, the pi theta by val score assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pi theta pos of interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pi Theta pos of interior.
Formal statement
Proof (Lean source)
the input path probability pos of interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the input Path Probability pos of interior.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the has deriv at pi theta parameter path assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the input path directional derivative is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The input Path Directional Derivative is determined by the displayed parameters.
Definition (Lean source)
the has deriv at input path probability parameter path assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The real-valued density of one transcript component is determined by the displayed parameters.
Definition (Lean source)
The real-valued density of the transcript mixture is determined by the displayed parameters.
Definition (Lean source)
The directional derivative of the real-valued transcript-mixture density is determined by the displayed parameters.
Definition (Lean source)
On a parameter range where the four-cell path probabilities are nonnegative, the explicit finite-mixture density is the Radon--Nikodym density of the transcript law. This is the paper-side interface between the finite latent-input expansion and score calculus on an arbitrary transcript measurable space. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the transcript density to real ae eq mixture of interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Density to Real ae eq mixture of interior.
Formal statement
Proof (Lean source)
the has deriv at transcript mixture real density parameter path assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The complete-data directional score of one latent input path. The input Path Directional Score is determined by the displayed parameters.
Definition (Lean source)
the input path derivative eq probability mul score assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The conditional transcript score: the derivative of the finite complete-data mixture density divided by that mixture density. The conditional Transcript Directional Score is determined by the displayed parameters.
Definition (Lean source)
the transcript derivative eq density mul conditional score assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the transcript derivative eq complete data score mixture assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialScoreProjectionInputs 5 declarations Paper inputs for measurable-statistic score projection
Paper inputs for measurable-statistic score projection
A full transcript mixture derivative vanishes wherever its positive-weight finite-mixture density vanishes. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The raw quotient defining the full transcript score agrees with the guarded zero convention used by score projection. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Prefix finite-mixture densities are nonnegative under interior parameters. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
A prefix mixture derivative vanishes wherever its positive-weight finite-mixture density vanishes. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The raw quotient defining a prefix score agrees with the guarded zero convention used by score projection. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialSuccessor 6 declarations Successor-prefix and finite joint-channel identities
Successor-prefix and finite joint-channel identities
the transcript prefix law eq observed prefix law assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Prefix Law eq observed Prefix Law.
Formal statement
Proof (Lean source)
the transcript successor law eq joint channel assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Successor Law eq joint Channel.
Formal statement
Proof (Lean source)
the sequential joint event derivative is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The sequential Joint Event Derivative is determined by the displayed parameters.
Definition (Lean source)
the has deriv at sequential joint real mixture assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the sequential joint real mixture eq output law to real assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the sequential Joint real Mixture eq output Law to Real.
Formal statement
Proof (Lean source)
the has deriv at sequential joint output law assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the has Deriv At sequential Joint output Law.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialSuccessorDerivative 12 declarations This file records the exact product rule for the successor-prefix law.
Derivative decomposition for a sequential successor event
This file records the exact product rule for the successor-prefix law. It keeps the derivative caused by the varying predecessor prefix law separate from the derivative of the current four-row mixture.
The mass of a successor event in one fixed current-input row while the predecessor prefix law varies along the parameter path. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The varying Predecessor Row Event Mass is determined by the displayed parameters.
Definition (Lean source)
The derivative contribution from the varying predecessor law, after mixing the four current-input rows at the base parameter. For the displayed inputs and conditions, the stated result follows. The predecessor Successor Event Derivative is determined by the displayed parameters.
Definition (Lean source)
The real mass of a successor-prefix event after splitting the successor history into its predecessor and final output coordinates. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The successor Prefix Event Mass is determined by the displayed parameters.
Definition (Lean source)
Integrating a fixed measurable function against the varying prefix law differentiates by integrating it against the explicit finite-mixture prefix derivative density. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the has Deriv At integral transcript Prefix Law.
Formal statement
Proof (Lean source)
The real event section of one fixed current-input row as a function of the released predecessor history. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
A fixed-row successor event section is measurable on the predecessor history space, with no regularity assumption on the output space. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The row section is integrable under every deterministic-input predecessor prefix component. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the sequential joint channel apply to real eq integral assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The predecessor contribution for one current-input row is the prefix derivative density integrated against that row's bounded event section. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The predecessor Row Event Derivative is determined by the displayed parameters.
Definition (Lean source)
The derivative of a fixed current-input row is exactly the predecessor prefix derivative contribution; the current row itself is held fixed here. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the has Deriv At varying Predecessor Row Event Mass.
Formal statement
Proof (Lean source)
The successor-event derivative is the sum of the varying-predecessor contribution and the current joint-channel directional derivative. The row derivative premise concerns only variation of the predecessor prefix law; the current four-cell weights are differentiated explicitly here. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the has Deriv At successor Prefix Event Mass of predecessor rows.
Formal statement
Proof (Lean source)
The exact successor-event derivative obtained by differentiating both the varying predecessor prefix law and the current observation-dependent row. The first summand is the finite-mixture pushforward of the prefix score; the second is the directional derivative of the current joint channel with its predecessor law fixed at the base parameter. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the has Deriv At successor Prefix Event Mass.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialSuccessorScore 13 declarations This file identifies the directional score of the four-row joint channel which generates a released prefix together with its next output.
Directional scores for successor joint channels
This file identifies the directional score of the four-row joint channel which generates a released prefix together with its next output. The score is expressed against the finite row-sum dominating measure, so the result does not require countable generation of the output spaces.
the channel directional derivative density is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
the channel directional score is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The channel Directional Score is determined by the displayed parameters.
Definition (Lean source)
the channel directional derivative density eq input sum assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the channel output density nonneg of interior assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the channel Output Density nonneg of interior.
Formal statement
Proof (Lean source)
the channel directional derivative density eq zero of output density eq zero assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the channel Directional Derivative Density eq zero of output Density eq zero.
Formal statement
Proof (Lean source)
the channel directional score mul output density assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the channel Directional Score mul output Density.
Formal statement
Proof (Lean source)
the integrable channel density dominating assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the set integral channel directional derivative density assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the set integral sequential joint channel directional score assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the set Integral sequential Joint channel Directional Score.
Formal statement
Proof (Lean source)
the channel directional score sq mul output density assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the channel Directional Score sq mul output Density.
Formal statement
Proof (Lean source)
the integral sequential joint channel directional score sq assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the integral sequential Joint channel Directional Score sq.
Formal statement
Proof (Lean source)
the transcript prefix law is probability assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Prefix Law is Probability.
Formal statement
Proof (Lean source)
Under the successor coordinates (init,last), the exact joint-channel score identities apply to the pushed-forward prefix law. The derivative here holds the predecessor prefix law fixed; differentiation of the whole successor law additionally contains the predecessor score. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Successor Law joint Score characterization.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialSuccessorScoreCharacterization 15 declarations Event characterization of the successor score candidate
Event characterization of the successor score candidate
the output law ac dominating measure assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the output law density to real ae eq channel output density assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the output Law Density to Real ae eq channel Output Density.
Formal statement
Proof (Lean source)
the channel directional derivative density integrable dominating assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the channel directional score integrable output law assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the channel Directional Score integrable output Law.
Formal statement
Proof (Lean source)
the set integral channel directional score output law assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the set Integral channel Directional Score output Law.
Formal statement
Proof (Lean source)
The prefix score lifted to successor coordinates. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The lifted Prefix Directional Score is determined by the displayed parameters.
Definition (Lean source)
the measurable lifted prefix directional score assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the conditional transcript prefix directional score integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the conditional Transcript Prefix Directional Score integrable.
Formal statement
Proof (Lean source)
Exact event characterization before the final projection step. The past part is in its verified row-disintegrated form, while the current channel score is integrated against the actual joint-channel output law. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the successor Event Derivative eq past Rows add current Score Integral.
Formal statement
Proof (Lean source)
the lifted prefix directional score integrable successor law assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the lifted Prefix Directional Score integrable successor Law.
Formal statement
Proof (Lean source)
the set integral lifted prefix directional score successor law assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the set Integral lifted Prefix Directional Score successor Law.
Formal statement
Proof (Lean source)
The full successor score candidate: the inherited prefix score plus the directional score of the current privatization channel. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. The successor Directional Score Candidate is determined by the displayed parameters.
Definition (Lean source)
the successor directional score candidate integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the successor Directional Score Candidate integrable.
Formal statement
Proof (Lean source)
Canonical successor-coordinate packaging of the entire event derivative coefficient as one score integral. The first term is the derivative carried by the predecessor law and the second is the current-channel derivative. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the set Integral successor Directional Score Candidate successor Law.
Formal statement
Proof (Lean source)
The actual predecessor-plus-current successor derivative equals the single integral of the full candidate score. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the successor Event Derivative eq set Integral successor Directional Score Candidate.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialVanTrees 14 declarations This file packages the finite-mixture transcript density along a scalar parameter path into the globally nonnegative likelihood fields required by the observation-dependent van Trees inequality.
Arbitrary-output van Trees likelihood fields
This file packages the finite-mixture transcript density along a scalar parameter path into the globally nonnegative likelihood fields required by the observation-dependent van Trees inequality. No countability or stagewise Radon--Nikodym selector is used.
the transcript law eq with density mixture assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the transcript Law eq with Density mixture.
Formal statement
Proof (Lean source)
the integral transcript mixture real density eq one assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the integral transcript Mixture Real Density eq one.
Formal statement
Proof (Lean source)
the vt density is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The vt Density is determined by the displayed parameters.
Definition (Lean source)
the vt density deriv is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The vt Density Deriv is determined by the displayed parameters.
Definition (Lean source)
the vt density nonneg assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the vt density has deriv at assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The interval-extended likelihood has its declared derivative jointly almost everywhere under parameter measure times the arbitrary-output reference measure. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the vt density integral eq one assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the vt density integral has deriv at assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the integrable transcript mixture real derivative assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the vt density integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the vt density deriv integrable assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the transcript density path cont diff assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the vt density absolutely continuous assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialVanTreesAssembly 2 declarations This file assembles the paper's already verified likelihood, prior, target, and product-integral adapters into a finite-sample Bayes inequality.
Finite-sample sequential van Trees assembly
This file assembles the paper's already verified likelihood, prior, target, and product-integral adapters into a finite-sample Bayes inequality. Transcript Fisher integrability and its numerical upper bound remain explicit premises; they are the score-projection and Doob-information obligations.
Prior-score, likelihood-score, and cross-term integrability imply integrability of the guarded joint-score square. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For a compact scalar path, finite weighted transcript Fisher information and an explicit bound on its prior average give the finite-sample Bayes risk lower bound. The Fisher premises are precisely the part supplied later by score projection and the sequential Doob bound. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialVanTreesIntegrals 10 declarations Product integral identities for the sequential van Trees adapter
Product integral identities for the sequential van Trees adapter
Integrable normalized likelihood sections lift an integrable nonnegative prior density to an integrable joint density. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Joint-density integrability gives integrability of the affine target sensitivity field. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Prior-score integrability and normalized integrable likelihood sections imply integrability of the lifted prior-score square on product space. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
A normalized likelihood lifts the prior score square from parameter space to parameter--observation product space without changing its integral. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The product integral of the weighted likelihood-score square is the prior average of conditional Fisher information. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Conditional centering of the likelihood score makes the prior--likelihood score cross term integrate to zero. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For the affine contrast target, normalized prior and likelihood make the integrated sensitivity equal the directional contrast. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the usual zero-density derivative conditions, the derivative-balance field is exactly error-score minus sensitivity. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Prior and likelihood weighted square integrability implies integrability of their weighted score cross term. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Once the error-score and sensitivity fields are integrable, their exact balance identity supplies derivative-balance integrability. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialVanTreesRegularity 19 declarations Remaining measurable fields for the sequential van Trees adapter
Remaining measurable fields for the sequential van Trees adapter
The centered quartic prior used on the scalar local interval [-R,R]. The sequential VTPrior is determined by the displayed parameters.
Definition (Lean source)
The declared derivative of the centered local prior. The sequential VTPrior Deriv is determined by the displayed parameters.
Definition (Lean source)
All paper-independent smooth-prior fields needed by van Trees on [-R,R]. For the displayed inputs and conditions, this structure records the stated data. The Sequential VTPrior Facts is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the sequential vt prior facts assertion holds.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the vt target is the mathematical object specified below. The vt Target is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the vt target deriv is the mathematical object specified below.
Definition (Lean source)
Under the supplied quantities and conditions, the vt target eq parameter path assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the has deriv at vt target assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the vt target absolutely continuous assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the measurable vt density joint assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the continuous transcript mixture real derivative path assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the measurable vt density deriv joint assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
A weighted cross term is integrable whenever both weighted square terms are integrable. This is the Cauchy–Schwarz step used for the van Trees error-score field. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
A nonnegative measurable risk is either integrable or has infinite Lebesgue integral. This supplies the harmless infinite-risk branch before applying the finite-risk van Trees argument. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The product-measurability fields required by the observation-dependent van Trees theorem. For the displayed quantities and conditions, the stated result follows.
Definition (Lean source)
Joint measurability of the primitive density, derivative, target, and estimator functions supplies every product-measurability side condition in van Trees. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The sequential mixture likelihood, affine contrast target, and smooth prior satisfy all van Trees product-measurability conditions for every measurable transcript estimator. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Finite weighted squared error and finite joint-score information imply integrability of the signed error-score field. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The centered smooth prior vanishes at both endpoints of the wider local parameter interval. For the displayed inputs and conditions, the stated result follows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SequentialVanTreesRiskBridge 10 declarations This file converts the native-real product-space Bayes error in the finite van Trees inequality into the weighted ENNReal local risk used by the sequential minimax statement.
Sequential van Trees risk and scaling bridge
This file converts the native-real product-space Bayes error in the finite
van Trees inequality into the weighted ENNReal local risk used by the
sequential minimax statement.
Scaling a parameter direction by inverse root sample size makes its scalar path exactly the corresponding local alternative. For the displayed inputs and conditions, the stated result follows.
Formal statement
Proof (Lean source)
Along the sample-scaled van Trees path, the squared scaled error is sample size times the unscaled target error. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Contrast is linear along scalar multiples of a trial direction. For the displayed inputs and conditions, the stated result follows.
Formal statement
Proof (Lean source)
For positive sample size, sample scaling cancels after multiplying the squared contrast sensitivity by the sample size. For the displayed inputs and conditions, the stated result follows.
Formal statement
Proof (Lean source)
On the compact scalar interval, the local risk is the reference-measure integral weighted by the interval-extended transcript density. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The scaled nonnegative product-space error integral equals the weighted compact-prior local risk, without any finiteness assumption. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Compact-prior averaging is bounded by local worst risk whenever the scalar directions fit in the chosen radius and remain interior. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
In the finite-error branch, multiplying the native-real Bayes error by the sample size gives exactly the compact-prior weighted local risk. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
The finite van Trees bound, after sample scaling and compact-prior ordering, yields a finite-sample lower bound on local worst risk. Transcript Fisher control remains explicit. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the of Real van Trees Envelope le local Worst Risk of fisher control.
Formal statement
Proof (Lean source)
The finite-sample local-worst-risk lower bound holds for every estimator: the finite-error branch uses van Trees, while a nonintegrable weighted squared error forces the compact-prior Bayes risk and local worst risk to be infinite. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.SparseSaddle 1 declarations The finite linear-program support theorem is applied at an attained minimizer of the upper envelope.
Sparse stationary staircase saddles
The finite linear-program support theorem is applied at an attained minimizer of the upper envelope. It preserves the four normalization moments, the stationarity moment, and the information value, leaving at most five active staircase rays.
Under the supplied quantities and conditions, the exists sparse staircase saddle assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the exists sparse staircase saddle.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.TranscriptUniqueness 3 declarations This file shows that the conditional cylinder factorization determines every finite transcript law uniquely.
Uniqueness of finite transcript factorization
This file shows that the conditional cylinder factorization determines every finite transcript law uniquely.
The cylinder factorization determines the joint law of each private history and its next output. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Every prefix marginal of a factorizing transcript law is the recursively constructed finite-sequence prefix law. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
A factorizing deterministic transcript law equals the canonical finite sequence construction. The stated result follows. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.Helpers.TreatmentSwap 47 declarations Treatment-arm swap symmetry for centered staircase designs
Treatment-arm swap symmetry for centered staircase designs
Transpose the two-by-two treatment/outcome membership table of a staircase ray. For the displayed inputs and conditions, the stated result follows.
the swapped support is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
Exchange the two treatment arms in the four-point input alphabet. The stated result follows.
the swap treatment weight is the mathematical object specified below. The swap Treatment Weight is determined by the displayed parameters.
Definition (Lean source)
the swap treatment pattern involutive assertion holds.
Formal statement
Proof (Lean source)
the swap treatment input involutive assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the swap treatment input val assertion holds.
Formal statement
Proof (Lean source)
the swap treatment pattern equiv is the mathematical object specified below.
Definition (Lean source)
the swap treatment input equiv is the mathematical object specified below.
Definition (Lean source)
Under the supplied quantities and conditions, the pattern ray swap treatment assertion holds.
Formal statement
Proof (Lean source)
the swap treatment weight involutive assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the staircase matrix swap treatment assertion holds.
Formal statement
Proof (Lean source)
the staircase feasible swap treatment assertion holds.
Formal statement
Proof (Lean source)
the staircase support swap treatment assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered pi theta swap treatment assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered pattern mass swap treatment assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pattern gradient swap treatment assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the projected gradient swap treatment assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered pattern information swap treatment assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered information objective swap treatment assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered profile set swap treatment assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered jstar swap treatment assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered vstar swap treatment assertion holds.
Formal statement
Proof (Lean source)
the swap treatment channel is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
Under the supplied quantities and conditions, the swap treatment channel apply assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the stationary ldp swap treatment assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the dominating measure swap treatment assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the channel density swap treatment assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered channel output density swap treatment assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered channel output density swap treatment inv two assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the input derivative swap treatment assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the channel derivative density swap treatment assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the swap treatment parameter is the mathematical object specified below.
the swap treatment matrix is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
Under the supplied quantities and conditions, the channel derivative density swap treatment zero assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the channel derivative density swap treatment one assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the channel fisher info swap treatment assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered output law swap treatment assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the centered output cardinality swap treatment assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
For the supplied quantities and conditions, the reflect treatment parameter is the mathematical object specified below.
Definition (Lean source)
the reflect treatment parameter involutive assertion holds.
Formal statement
Proof (Lean source)
the swap treatment matrix mul vec assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the neg contrast vector swap assertion holds.
Formal statement
Proof (Lean source)
the contrast in range swap treatment assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the contrast pairing reflect assertion holds.
Formal statement
Proof (Lean source)
the contrast solution values swap treatment assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the contrast variance swap treatment assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.TBalancedReduction 20 declarations When assignment is balanced and the arm means sum to one, randomized response to the signed treatment–outcome bit attains the information oracle.
Balanced randomized-response reduction
When assignment is balanced and the arm means sum to one, randomized response to the signed treatment–outcome bit attains the information oracle.
the signed bit is the mathematical object specified below.
the balanced rr is the mathematical object specified below. The balanced RR is determined by the displayed parameters.
Under the supplied quantities and conditions, the balanced rr atom assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the grouped balanced rr atom assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the randomized response atom assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pi theta balanced by val assertion holds.
Formal statement
Proof (Lean source)
the signed bit probability one assertion holds.
Formal statement
Proof (Lean source)
the signed bit probability zero assertion holds.
Formal statement
Proof (Lean source)
the balanced rr output probability one assertion holds.
Formal statement
Proof (Lean source)
the balanced rr output probability zero assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the balanced rr stationary assertion holds. Under the stated assumptions, the balanced RR stationary.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the grouped balanced rr information eq randomized response assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the grouped balanced RR information eq randomized Response.
Formal statement
Proof (Lean source)
the grouped balanced rr information eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the grouped balanced RR information eq.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the balanced rr directional derivative assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the balanced rr quadratic eq assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the balanced RR quadratic eq.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the sharp information pos assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the sharp information pos.
Formal statement
Proof (Lean source)
the balanced rr variance eq sharp assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the balanced RR variance eq sharp.
Formal statement
Proof (Lean source)
the vstar balanced eq sharp reciprocal assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the Vstar balanced eq sharp reciprocal.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the contraction inv eq coth assertion holds. Under the stated assumptions, the contraction inv eq coth.
Formal statement
Proof (Lean source)
the balanced reduction assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the balanced reduction.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.TFiniteOracle 2 declarations Exact finite staircase oracle
Exact finite staircase oracle
Under the supplied quantities and conditions, the finite oracle minimax assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the finite Oracle minimax.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the finite oracle assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.TFiveOutputRegion 6 declarations The centered family has a unique five-ray optimum; distinct projected scores prevent any attaining stationary channel from merging those rays.
Five-output certificate region
The centered family has a unique five-ray optimum; distinct projected scores prevent any attaining stationary channel from merging those rays.
the r5 nonempty centered assertion holds.
Formal statement
Proof (Lean source)
the centered five output region assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the reflected point mem r5 assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the reflected five output region assertion holds.
Formal statement
Proof (Lean source)
the is open r5 continuous certificate assertion holds.
Proof (Lean source)
Under the supplied quantities and conditions, the five output region assertion holds. The five output region.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.TFiveOutputUpperBound 6 declarations An optimal finite staircase design has at most five positive pattern weights, and therefore at most five active released symbols.
Five-output upper bound
An optimal finite staircase design has at most five positive pattern weights, and therefore at most five active released symbols.
the staircase support is the mathematical object specified below. The staircase Support is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the staircase output zero of weight zero assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the output cardinality staircase le support card assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the staircase output pos of weight pos assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the staircase output pos of weight pos.
Formal statement
Proof (Lean source)
the output cardinality staircase eq support card assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the output Cardinality staircase eq support card.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the five output upper bound assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the five output upper bound.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.TLaplaceComparison 5 declarations The custom known-assignment sample mean has the displayed asymptotic variance.
Comparison with the published custom Laplace release
The custom known-assignment sample mean has the displayed asymptotic variance. Its Wald half-length constant exceeds the private-pilot oracle's at the balanced binary-trial point.
For the supplied quantities and conditions, the asymptotic wald half length is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs.
Definition (Lean source)
Under the supplied quantities and conditions, the vstar nonneg assertion holds. For the displayed quantities and conditions, these specify the stated inputs. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the Vstar nonneg.
Formal statement
Proof (Lean source)
the voa balanced value assertion holds.
Formal statement
Proof (Lean source)
the balanced coth sq lt 34 assertion holds.
Proof (Lean source)
the laplace comparison assertion holds. For the displayed quantities and conditions, these specify the stated inputs. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the laplace comparison.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.TPilotAttainment 7 declarations The complete pilot procedure is private, conditionally unbiased, regular and asymptotically Gaussian.
Attainment by the private-pilot estimator
The complete pilot procedure is private, conditionally unbiased, regular and asymptotically Gaussian. Its main-sample variance gives Wald coverage at every interior parameter, including channel-support boundaries.
For the supplied quantities and conditions, the standard normal cdf is the mathematical object specified below.
Definition (Lean source)
the wald critical value is the mathematical object specified below. The wald Critical Value is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the standard normal cdf eq std normal cdf assertion holds.
Formal statement
Proof (Lean source)
the wald critical value eq probit assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the wald critical value pos assertion holds. Under the stated assumptions, the wald Critical Value pos.
Formal statement
Proof (Lean source)
the gaussian measure wald critical value icc assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the gaussian Measure wald Critical Value Icc.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the pilot attainment assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the pilot attainment.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.TSequentialMinimax 2 declarations The lower bound covers every history-dependent private procedure on arbitrary measurable output spaces, whether regular or not.
Sequential local asymptotic minimax equality
The lower bound covers every history-dependent private procedure on arbitrary measurable output spaces, whether regular or not. A single private-pilot sequence is regular and attains the bound, giving the infimum equality.
For the supplied quantities and conditions, the regular risk set is the mathematical object specified below. The regular Risk Set is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the sequential minimax assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the sequential minimax.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.TSupportTransition 13 declarations Disjoint neighborhoods of the balanced and low-mean points have unique optimal staircase supports of sizes five and three, respectively.
Transition between optimal support sizes
Disjoint neighborhoods of the balanced and low-mean points have unique optimal staircase supports of sizes five and three, respectively.
For the supplied quantities and conditions, the unique optimal support is the mathematical object specified below. For the displayed quantities and conditions, these specify the stated inputs. The unique Optimal Support is determined by the displayed parameters.
Definition (Lean source)
For the supplied quantities and conditions, the optimal cardinality is the mathematical object specified below. The optimal Cardinality is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the pi theta by val transition assertion holds.
Formal statement
Proof (Lean source)
the low mean information matrix value assertion holds.
Formal statement
Proof (Lean source)
the low mean information matrix direction assertion holds.
Formal statement
Proof (Lean source)
the low mean projected scores distinct assertion holds.
Formal statement
Proof (Lean source)
the low mean output cardinality of attainment assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the support region slices assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the optimal cardinality of mem r5 assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the unique optimal support of mem r5 assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the unique optimal support of mem r3 assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the optimal cardinality of mem r3 of distinct assertion holds. For the displayed quantities and conditions, these specify the stated inputs.
Formal statement
Proof (Lean source)
the support transition assertion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpAteEfficiencySurface_Research.TThreeOutputRegion 27 declarations At the low-mean point, the exact primal and dual values certify a unique three-ray optimum and its open neighborhood.
Three-output rational certificate
At the low-mean point, the exact primal and dual values certify a unique three-ray optimum and its open neighborhood.
Under the supplied quantities and conditions, the three mask weights feasible assertion holds. Under the stated assumptions, the three Mask Weights feasible.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the three mask weights unique assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the three Mask Weights unique.
Formal statement
Proof (Lean source)
the three mask weights support assertion holds.
Formal statement
Proof (Lean source)
the three mask weights continuous assertion holds.
Formal statement
Proof (Lean source)
the low mean candidate feasible assertion holds.
Formal statement
Proof (Lean source)
the low mean candidate information value assertion holds.
Formal statement
Proof (Lean source)
the low mean candidate stationary assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the low mean candidate global min assertion holds.
Formal statement
Proof (Lean source)
The fixed dual certificate for the low-mean three-output region is the displayed object.
Definition (Lean source)
Under the supplied quantities and conditions, the low mean dual value assertion holds. The low Mean Dual value.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the low mean dual slack assertion holds.
Formal statement
Proof (Lean source)
the low mean point mem r3 assertion holds.
Proof (Lean source)
the feasible dual ray sum assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the feasible dual Ray sum.
Formal statement
Proof (Lean source)
the low mean dual upper bound assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the low Mean dual upper bound.
Formal statement
Proof (Lean source)
the low mean information nonneg assertion holds. For the displayed quantities and conditions, these specify the stated inputs. Under the stated assumptions, the low Mean information nonneg.
Formal statement
Proof (Lean source)
the low mean candidate inf value assertion holds.
Formal statement
Proof (Lean source)
the low mean jstar value assertion holds.
Proof (Lean source)
The target vector in the three-output dual system is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the r3 mask mem assertion holds.
Under the supplied quantities and conditions, the exists local r3 dual of mem assertion holds.
Formal statement
Proof (Lean source)
the low mean r3 direction eq assertion holds.
Formal statement
Proof (Lean source)
Under the supplied quantities and conditions, the low mean r3 projected scores distinct assertion holds.
Formal statement
Proof (Lean source)
The projected score coordinate in the three-output region is determined by the displayed parameters.
Definition (Lean source)
Under the supplied quantities and conditions, the r3 projected score at eq assertion holds.
Formal statement
Proof (Lean source)
the exists low mean r3 distinct score neighborhood assertion holds.
Formal statement
Proof (Lean source)
the is open r3 continuous certificate assertion holds.
Proof (Lean source)
the three output region assertion holds.