Estimation.NPIV.Primal
The sieve primal NPIV analysis: projected residuals, variance and bias terms, and the rate theorem for the structural function.
Estimator 9 core · 0 supporting This file defines the public estimator-level interface for the primal NPIV rate proof.
TRAE Primal Estimator Interface
This file defines the public estimator-level interface for the primal NPIV rate
proof. It exposes scoped measurable-space instances for the spaces stored in an
inverse-problem system, the TRAEClasses bundle of candidate and critic classes,
the empirical objective pieces innerIntegrand, innerObjective, and
supObjective, and the predicate IsTRAEPrimalEstimator recording membership,
empirical sup-min optimality, and joint measurability of the estimator.
For an inverse-problem system, the observation space is equipped with the measurable space specified by that system.
Definition (Lean source)
For an inverse-problem system, the covariate space is equipped with the measurable space specified by that system.
Definition (Lean source)
For an inverse-problem system, the instrument space is equipped with the measurable space specified by that system.
Definition (Lean source)
This structure packages a nonempty statistical candidate class for the primal nuisance that sits inside the ambient candidate set, together with a nonempty statistical critic class that sits inside the ambient critic set, for the primal Tikhonov-regularized adversarial optimization (def:est-trae-population-criterion, line 139).
Definition (Lean source)
The empirical integrand for an NPIV operator system, regularization level, candidate, and critic at an observation is 2(m(w;f) - h(x)f(z)) - f(z)² + λh(x)², with the system's covariate and instrument.
Definition (Lean source)
The fold-A inner objective averages the empirical integrand for an NPIV operator system, sample and split, regularization level, candidate, and critic over the nuisance fold selected by the sample-size index and realization.
Definition (Lean source)
The TRAE primal sup-min objective takes the supremum of the fold-A inner objective over the critic class, for an NPIV operator system, sample and split, regularization level and candidate, and the chosen sample-size index and realization.
Definition (Lean source)
An estimator, indexed by sample size and randomness, is a TRAE primal estimator relative to a nuisance fold when, at every sample size and realization, it belongs to the statistical candidate class, attains an empirical sup-min objective on that fold no worse than at any other candidate in the class, and is jointly measurable in the randomness and the covariate argument.
Definition (Lean source)
Membership of the empirical optimizer in the statistical class H.
Empirical sup-min optimality on fold A(n).
Joint measurability of (ω, x) ↦ h_hat n ω x.
For an NPIV operator system, candidate and critic classes, an independent sample, a one-shot split, a regularization sequence, and an estimator sequence, the estimator is a sample-size-dependent TRAE estimator when its candidate belongs to the statistical class, minimizes the empirical objective formed with lambda n at each index, and is jointly measurable.
Definition (Lean source)
Membership of the empirical optimizer in the statistical class H.
Empirical sup-min optimality at index n, using lambda n.
Joint measurability of (omega, x) ↦ h_hat n omega x.
RateSequence 2 core · 1 supporting This module gives the fixed-sample, fixed-confidence rate for a TRAE estimator using lambda n. ★ trae_primal_rate★ primal_strongNorm_tendstoInProb_of_rates
Primal NPIV rate with a regularization sequence
This module gives the fixed-sample, fixed-confidence rate for a TRAE estimator
using lambda n. Its constants come from a uniform Tikhonov certificate and
therefore do not depend on the selected regularization level.
Given a source condition, a uniform source-condition bias certificate, a sample-size-dependent TRAE estimator, a positive regularization sequence bounded above by two, the localized regime at index n, a positive fold size, a fixed confidence level between zero and one, and the fixed-confidence critical-radius floor, the corresponding fixed-level peeling floor, and the sample-size index, there is an event of probability at least 1 - zeta on which the squared strong error is bounded by the displayed level-independent constant times delta n ^ 2 / lambda_n n + norm(w0) * (lambda_n n) ^ min beta 1.
Formal statement
Proof (Lean source)
For a primal TRAE estimator sequence, a positive source exponent with source condition and uniform bias certificate, positive regularization levels below two, localized regimes, fixed-confidence critical-radius floors, and fixed-level peeling floors, suppose the failure probabilities vanish while remaining strictly between zero and one, the localization radii vanish, the regularization levels vanish, and the variance term delta n² / lambda_n n vanishes. Then the primal strong-norm error converges to zero in probability.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
lambda_balance_identitytheorem — For a positive smoothness exponent, a positive critical radius, and the power-balancing regularization level, the sum of delta^2/lambda and lambda^(min beta 1) equals twice their common power of delta.hypothesesbeta delta lambda :ℝhbeta :0 < betahdelta :0 < deltahlambda :lambda = delta ^ (2 / (min beta 1 + 1))Proof (Lean source)
theorem lambda_balance_identity {beta delta lambda : ℝ} (hbeta : 0 < beta) (hdelta : 0 < delta) (hlambda : lambda = delta ^ (2 / (min beta 1 + 1))) : delta ^ 2 / lambda + lambda ^ (min beta 1) = 2 * delta ^ (2 * min beta 1 / (min beta 1 + 1)) := by subst lambda let a := min beta 1 have ha : 0 < a := lt_min hbeta (by norm_num) have hden : a + 1 ≠ 0 := by linarith have hdelta_nonneg : 0 ≤ delta := hdelta.le have hfirst : delta ^ 2 / delta ^ (2 / (a + 1)) = delta ^ (2 * a / (a + 1)) := by rw [← Real.rpow_natCast] rw [← Real.rpow_sub hdelta] congr 1 field_simp [hden] ring have hsecond : (delta ^ (2 / (a + 1))) ^ a = delta ^ (2 * a / (a + 1)) := by rw [← Real.rpow_mul hdelta_nonneg] congr 1 ring rw [show min beta 1 = a by rfl, hfirst, hsecond] ring