Estimation.NPIV.Primal.EmpiricalProcessEvent
The high-probability empirical-process events (Gram-matrix control, residual concentration) underlying the sieve NPIV rate.
Regime 2 core · 0 supporting This file bundles the localized empirical-process hypotheses required for the primal NPIV rate theorem.
Localized Empirical-Process Regimes
This file bundles the localized empirical-process hypotheses required for the
primal NPIV rate theorem. LocalizedRegimeBundle packages one abstract
localized loss class with its sample map, critical-radius certificate, and
radius-uniform boundedness/integrability assumptions. LocalizedRegimes
assembles the four concrete bundles used downstream, for H · F, m ∘ F,
F, and H, together with the law bridge, realizability, closedness, diameter,
pair-gap interpretation, and peeling-slack fields needed by the class-specific
deviation events and the empirical-process discharge.
structure LocalizedRegimeBundle reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
A localized regime bundle packages a countable index set and a measurable family of loss functions on a nonempty covariate space, together with a localization norm, nonnegative on every class member and a measurable sample embedding into that covariate space. It further records a localized empirical-process regime whose critical radius is at most the target localization scale δ_n, is strictly positive, and is a fixed point of the process's expected-supremum function at that scale. Finally, uniformly over every radius at least δ_n, it requires that the empirical Rademacher process on the star-hull is almost-surely bounded and that the corresponding empirical Rademacher complexity is integrable.
Definition (Lean source)
parameters
fields
ι :
Type
𝒳 :
nonempty_ι :
Nonempty ι
countable_ι :
Countable ι
Loss-class family.
F :
ι → 𝒳 → ℝ
Norm/seminorm used for star-hull localization.
norm :
(𝒳 → ℝ) → ℝ
Nonnegativity of the localization norm on the indexed class. The
paper's localized concentration inputs use genuine radii/norms; Lean
keeps the class norm abstract, so this implicit mathematical fact is
carried explicitly.
norm_nonneg :
∀ i, 0 ≤ norm (F i)
Sample-side embedding `Ω → 𝒳`.
X :
Ω → 𝒳
X_meas :
F_meas :
∀ i, Measurable (F i)
regime :
LocalizedRegime Ω ι 𝒳 F norm μ X
crit_le :
criticalRadius (regime.ψ n) ≤ δ_n
crit_pos :
0 < criticalRadius (regime.ψ n)
crit_fp :
regime.ψ n (criticalRadius (regime.ψ n)) ≤ (criticalRadius (regime.ψ n)) ^ 2
**Radius-uniform boundedness** of the empirical Rademacher process
on the zero-out star-hull. Quantified over all radii `r ≥ δ_n`,
so that `localized_omega_event_for_H` may apply at the bilinear
radius `‖h₁ − h₂‖ + δ_n`.
rad_bdd :
∀ r : ℝ,
δ_n
≤ r → ∀ Ssamp : Fin n → 𝒳, ∀ σ : Signs n, BddAbove (Set.range fun p : starHullParam ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r p (Ssamp k)|)
**Radius-uniform integrability** of the empirical Rademacher
complexity on the zero-out star-hull, quantified over all radii
`r ≥ δ_n` for the same reason as `rad_bdd`.
rad_int :
∀ r : ℝ
if
δ_n ≤ r
then
Integrable (fun ω : Fin n → Ω => empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω)) (Measure.pi (fun _ => μ))
structure LocalizedRegimes reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
This structure bundles four localized regime witnesses, one for each function class entering the empirical-process and centred-regulariser arguments — the product, moment, critic, and candidate classes, with the deterministic hypotheses that the observation variable has the stated law, that the population Tikhonov solution is realizable in the statistical candidate class, that the moment, candidate, and critic maps are almost-surely uniformly bounded, and that every candidate admits a critic whose L² lift realizes the projected residual. It also records that the empirical sup-min objective is bounded above by, and attained at, the population sup objective; diameter caps on the candidate class and the critic class; and nonnegative proportionality constants together with a matching radius lower bound for the moment-class pair differences and for the product-class cross terms. For the candidate class it further supplies an interpretation triple: an index into the H-bundle whose norm controls the pairwise loss gap, and whose composed evaluation equals the difference of squared candidate losses. For the product class it supplies both a single-candidate interpretation triple bounded by the localization scale and a pair-difference interpretation triple scaling with the candidate gap. For the moment class it likewise supplies a single-critic interpretation triple and a pair-difference interpretation triple.
Definition (Lean source)
parameters
S :
OperatorSystem Ω μ
TC :
P_W :
Measure S.𝒲
sample :
IIDSample Ω S.𝒲 μ P_W
β lambda :
ℝ
sc :
SourceCondition S β
tb :
TikhonovBiasBound S β lambda sc
n :
ℕ
δ_n :
ℝ
fields
Regime for the product class `star(H · F)` over `(S.𝒲, P_W)`.
bundle_HF :
LocalizedRegimeBundle S.𝒲 P_W n δ_n
Regime for the moment class `star(m ∘ F)` over `(S.𝒲, P_W)`.
bundle_mF :
LocalizedRegimeBundle S.𝒲 P_W n δ_n
Regime for the critic class `star(F)` over `(S.𝒲, P_W)`.
bundle_F :
LocalizedRegimeBundle S.𝒲 P_W n δ_n
Regime for the candidate class `star(H)` (centred regulariser),
over `(S.𝒲, P_W)`.
bundle_H :
LocalizedRegimeBundle S.𝒲 P_W n δ_n
**Law bridge.** The observation random variable `S.W` has law
`P_W` under `μ`. This is *not* implied by the existing fields of
`OperatorSystem` or `IIDSample` (the latter only constrains
`μ.map (sample.Z 0) = P_W`). Without this hypothesis the helpers
below cannot equate `∫ ω' f(S.W ω') ∂μ` with the population mean
`μ_{P_W}[f]` produced by `localized_uniform_deviation`.
law_W :
μ.map S.W = P_W
**Realizability**: the population Tikhonov solution lies in the
statistical class. Needed to apply `is_estimator.opt` against
`tb.h_lambda_star_fun`.
realizability :
tb.h_lambda_star_fun ∈ TC.H
**Boundedness**: a.s. uniform bound on `m(W; f), h(X), f(Z)` over
`h ∈ TC.H, f ∈ TC.F`. Needed for the centred-regulariser
Cauchy–Schwarz step (controls `‖h*‖ + ‖ĥ‖`) and the McDiarmid
step inside `localized_uniform_deviation`.
bounded :
∃ B : ℝ,
0 ≤ B ∧
(∀ᵐ ω ∂μ, (∀ f ∈ TC.F, |S.m (S.W ω) f| ≤ B) ∧ (∀ h ∈ TC.H, |h (S.xOf (S.W ω))| ≤ B) ∧ (∀ f ∈ TC.F, |f (S.zOf (S.W ω))| ≤ B))
**Closedness (Hilbert form)**: for every `h ∈ TC.H` there is a
critic `f ∈ TC.F` whose `L²` lift coincides with the projected
residual `T(h₀ − h)` *as elements of* `Lp ℝ 2 μ`.
This is the standard NPIV closedness assumption (Dikkala–Lewis–
Mackey–Syrgkanis; Chen–Pouzo): the projected residual is realized
by an element of the critic class. Needed to convert the empirical
sup-min comparison into operator-side `weakNorm` expressions in
step (iii) below — a weak (test-against-`Qbar` inner-product) form
does not suffice unless `{q_L2 g | g ∈ Qbar}` is total in
`Qbar_L2`, which is not currently part of the `OperatorSystem`
interface.
closedness :
∀ h,
∀ hh : h ∈ TC.H,
∃ f,
∃ hf : f ∈ TC.F, S.T (S.hL2 S.h₀_mem - S.hL2 (TC.H_subset hh)) = S.qL2 (TC.F_subset hf)
**Critic max order.** The paper states the critic objective with
`max_{f ∈ F}`. Since Lean encodes it as `supObjective`, we expose
the corresponding maximum-order facts explicitly: every feasible
inner objective is below the max, and the max is attained.
inner_le_supObjective :
∀ (split' : OneShotSplit sample) (horizon : ℕ) (ω : Ω),
∀ h,
h ∈ TC.H → ∀ f, f ∈ TC.F → innerObjective S sample split' lambda h f horizon ω
≤ supObjective S TC sample split' lambda h horizon ω
supObjective_attained :
∀ (split' : OneShotSplit sample) (horizon : ℕ) (ω : Ω),
∀ h,
h ∈ TC.H → ∃ f, ∃ _hf : f ∈ TC.F, supObjective S TC sample split' lambda h horizon ω
≤ innerObjective S sample split' lambda h f horizon ω
**`TC.H` strong-norm diameter cap.** Upper bound on the
strongNorm-gap `‖h₁ − h₂‖_{strong}` for every pair `(h₁, h₂) ∈ TC.H × TC.H`.
This caps the radius scale over which the peeled H-side localized
deviation operates — `localized_omega_event_for_H` peels dyadically
across `[δ_n, H_diameter]` to produce a *single* high-probability
event simultaneously valid for all pairs, with the bilinear
scaling `4 · (‖h₁ − h₂‖ + δ_n) · critRad` plus an extra peeling
`√(log(H_diameter/δ_n + 1)/n)` log-factor.
H_diameter :
ℝ
H_diameter_lb :
δ_n ≤ H_diameter
H_diameter_bound :
∀ h₁ h₂ (hh₁ : h₁ ∈ TC.H) (hh₂ : h₂ ∈ TC.H),
S.strongNorm (S.hL2 (TC.H_subset hh₁) - S.hL2 (TC.H_subset hh₂)) ≤ H_diameter
**Interpretation: centred-regulariser class.** For each pair
`(h₁, h₂) ∈ TC.H × TC.H` there is a `bundle_H`-index whose
composed evaluation equals the *difference* of squared candidate
losses, `h₁(S.xOf w)² − h₂(S.xOf w)²`. The
`bundle_H.norm`-radius of this index is bounded by the **gap norm**
`‖h₁ − h₂‖_{L²(P_X)}`, so the localized deviation rate scales with
`‖h₁ − h₂‖ · δ_n + δ_n²` — matching proof-sketch line 345.
This is the star-hull-localized form needed for the centred
regulariser bound (the uniform-radius form `‖h‖_X · δ_n + δ_n²` per
single `h ∈ TC.H` does not suffice, since the bilinear gap
`(h*-ĥ)(h*+ĥ)` is what controls `D_n`).
interp_H_idx :
∀ h₁ h₂
if
h₁ ∈ TC.H
and
h₂ ∈ TC.H
then
bundle_H.ι
interp_H_norm :
∀ h₁ h₂ (hh₁ : h₁ ∈ TC.H) (hh₂ : h₂ ∈ TC.H),
bundle_H.norm (bundle_H.F (interp_H_idx h₁ h₂ hh₁ hh₂))
≤ S.strongNorm (S.hL2 (TC.H_subset hh₁) - S.hL2 (TC.H_subset hh₂))
interp_H_eval :
∀ h₁ h₂ (hh₁ : h₁ ∈ TC.H) (hh₂ : h₂ ∈ TC.H),
∀ w : S.𝒲,
bundle_H.F (interp_H_idx h₁ h₂ hh₁ hh₂) (bundle_H.X w)
= (h₁ (S.xOf w)) ^ 2 - (h₂ (S.xOf w)) ^ 2
**Interpretation: product class `star(H · F)` (single-index form).**
Each pair `(h, f) ∈ TC.H × TC.F` has a `bundle_HF`-index of radius
`≤ δ_n` whose composed evaluation equals `h(S.xOf ·) · f(S.zOf ·)`.
Used in the `h*_λ`-side realizability step where the comparison
point is fixed and only the critic varies.
interp_HF_idx :
∀ h, h ∈ TC.H → ∀ f, f ∈ TC.F → bundle_HF.ι
interp_HF_norm :
∀ h (hh : h ∈ TC.H),
∀ f (hf : f ∈ TC.F), bundle_HF.norm (bundle_HF.F (interp_HF_idx h hh f hf)) ≤ δ_n
interp_HF_eval :
∀ h (hh : h ∈ TC.H),
∀ f (hf : f ∈ TC.F),
∀ w : S.𝒲,
bundle_HF.F (interp_HF_idx h hh f hf) (bundle_HF.X w) = h (S.xOf w) * f (S.zOf w)
**Foster constant for HF cross-terms.** An upper bound on the
bundle radius for the cross-class integrand `(h₁ - h₂)(X) · f(Z)`,
bilinear in the strong-norm gap `‖h₁ - h₂‖_{strong}` and the
critic-side scale `δ_n`. Concretely `HF_pair_const ≤ B` (the
boundedness constant from `bounded`) by Cauchy–Schwarz with the
sup-norm bound on `f`.
HF_pair_const :
ℝ
HF_pair_const_nonneg :
0 ≤ HF_pair_const
**Interpretation: pair-gap form for `star(H · F)` (Foster pair-gap).**
For each triple `(h₁, h₂, f) ∈ TC.H × TC.H × TC.F`, an index whose
`bundle_HF.norm`-radius scales bilinearly with
`HF_pair_const · ‖h₁ - h₂‖_{strong} · δ_n` and whose composed
evaluation equals the *difference* `(h₁ - h₂)(X) · f(Z)`.
This is the Foster pair-gap form (Foster–Syrgkanis Lemma 11; TRAE
paper, Bennett–Kallus–Mao–Newey–Syrgkanis–Uehara 2023): the
localized deviation on the cross class scales with the *actual*
L²-norm of the loss-difference at the comparison point, not with
a fixed star-hull radius. Required to obtain the cross term
`δ_n · weak_gap` on the EP RHS (where
`weak_gap = ‖T(ĥ - h*_λ)‖`); the single-index form alone yields
only the weaker `(R_b + δ_n) · rate` envelope.
**Note (consistency with existing helpers).** The deviation
helper for HF that consumes this pair-form interpretation is
`localized_omega_event_for_HF_pair`, which instantiates the
localized concentration at the *worst-case* radius
`HF_pair_const · H_diameter · δ_n + δ_n` (mirroring the design of
`localized_omega_event_for_H`, which uses `H_diameter + δ_n`),
not at the per-pair radius — strict Foster pair-gap requires
peeling infrastructure analogous to the H-side. The pair-gap
norm field below provides the *interpretation* the EP proof
consumes; tightening the deviation rate from worst-case to
per-pair is a separate (peeling) upgrade.
interp_HF_idx_pair :
∀ h₁ h₂, h₁ ∈ TC.H → h₂ ∈ TC.H → ∀ f, f ∈ TC.F → bundle_HF.ι
interp_HF_norm_pair :
∀ h₁ h₂ (hh₁ : h₁ ∈ TC.H) (hh₂ : h₂ ∈ TC.H),
∀ f (hf : f ∈ TC.F),
bundle_HF.norm (bundle_HF.F (interp_HF_idx_pair h₁ h₂ hh₁ hh₂ f hf))
≤ HF_pair_const * S.strongNorm (S.hL2 (TC.H_subset hh₁) - S.hL2 (TC.H_subset hh₂)) * δ_n
interp_HF_eval_pair :
∀ h₁ h₂ (hh₁ : h₁ ∈ TC.H) (hh₂ : h₂ ∈ TC.H),
∀ f (hf : f ∈ TC.F),
∀ w : S.𝒲,
bundle_HF.F (interp_HF_idx_pair h₁ h₂ hh₁ hh₂ f hf) (bundle_HF.X w)
= (h₁ (S.xOf w) - h₂ (S.xOf w)) * f (S.zOf w)
**L²-norm constant for the moment class** `m(W; f)`: an explicit
bound `‖m(W;f)‖_{L²(P_W)} ≤ mF_L2_const · ‖f‖_{L²(P_Z)}` for every
`f ∈ TC.F`, i.e. `√C_m` from the mean-square continuity hypothesis
`PrimalRateHypotheses.msc`. Carried at the bundle layer because
the EP loss-difference L²-norm calculation (Foster Lemma 11
input) needs it, but the import cycle with `Rate.lean` would
otherwise force replication. Bundle norm `interp_mF_norm` is
kept at `≤ δ_n` (separate from the L²-radius).
mF_L2_const :
ℝ
mF_L2_const_nonneg :
0 ≤ mF_L2_const
**`TC.F` diameter cap.** Upper bound on critic L² gaps. This is a
formal consequence of the paper's a.s. uniform boundedness
assumption, exposed here as the radius cap needed by dyadic
peeling for the `m∘F` and `F²` pair-difference classes.
F_diameter :
ℝ
F_diameter_lb :
δ_n ≤ F_diameter
F_diameter_bound :
∀ f₁ f₂ (hf₁ : f₁ ∈ TC.F) (hf₂ : f₂ ∈ TC.F),
S.strongNorm (S.qL2 (TC.F_subset hf₁) - S.qL2 (TC.F_subset hf₂)) ≤ F_diameter
Radius lower bound for the `m∘F` pair class at this localization
scale. In concrete applications this is discharged by increasing
the critical-radius floor constant.
mF_pair_radius_lb :
δ_n ≤ mF_L2_const * F_diameter
**Interpretation: moment class `star(m ∘ F)`.** Each `f ∈ TC.F` has
a `bundle_mF`-index of bundle-radius `≤ δ_n` whose composed
evaluation equals `S.m · f`.
interp_mF_idx :
∀ f
if
f ∈ TC.F
then
bundle_mF.ι
interp_mF_norm :
∀ f (hf : f ∈ TC.F), bundle_mF.norm (bundle_mF.F (interp_mF_idx f hf)) ≤ δ_n
interp_mF_eval :
∀ f (hf : f ∈ TC.F),
∀ w : S.𝒲, bundle_mF.F (interp_mF_idx f hf) (bundle_mF.X w) = S.m w f
Algebra 1 core · 0 supporting Collects deterministic algebra for the NPIV empirical-process master event. ★ young_cross_envelope
Collects deterministic algebra for the NPIV empirical-process master event. The lemmas turn localized deviation inequalities and regularizer bounds into the additive envelopes used by the primal rate proof.
lemma young_cross_envelope reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Young / AM-GM cross-term envelope. For nonnegative reals R, δ, w, and κ, the mixed sum δ · (R + w + δ) + R · κ is bounded above by the quadratic envelope R² + δ · w + (3/2) · δ² + (1/2) · κ².
Formal statement
hypotheses
R δ w κ :
ℝ
_hR :
0 ≤ R
_hδ :
0 ≤ δ
_hw :
0 ≤ w
_hκ :
0 ≤ κ
conclusion
δ * (R + w + δ) + R * κ ≤ R ^ 2 + δ * w + (3 / 2) * δ ^ 2 + (1 / 2) * κ ^ 2
Proof (Lean source)
lemma young_cross_envelope (R δ w κ : ℝ)
(_hR : 0 ≤ R) (_hδ : 0 ≤ δ) (_hw : 0 ≤ w) (_hκ : 0 ≤ κ) :
δ * (R + w + δ) + R * κ
≤ R ^ 2 + δ * w + (3 / 2) * δ ^ 2 + (1 / 2) * κ ^ 2 := by
nlinarith [sq_nonneg (R - δ), sq_nonneg (R - κ)]
EPMasterEvent 1 core · 3 supporting States the explicit-rate empirical-process master event for the NPIV primal estimator. ★ ep_master_event_from_localized
States the explicit-rate empirical-process master event for the NPIV primal estimator. The module packages the localized deviation and centered-regularizer bounds in the form consumed by the rate proof.
theorem ep_master_event_from_localized reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Master localized empirical-process event for the primal NPIV analysis. Given, for every sample size n, a localized-regime bundle for the weak-norm, regularizer, and cross function classes at that fold-A sample size, and a confidence level ζ strictly between 0 and 1, there is a single event of probability at least 1 − ζ on which, simultaneously for every n with 1 ≤ split.n₁ n, the population weak-objective excess plus the empirical regularizer excess is bounded by the empirical sup-objective excess plus a localized envelope built from the regimes' critical radii and a √(log(1/ζ)/n) term.
Formal statement
hypotheses
S :
split :
OneShotSplit sample
lambda β :
ℝ
delta :
ℕ → ℝ
h_hat :
ℕ → Ω → S.𝒳 → ℝ
is_estimator :
IsTRAEPrimalEstimator S TC sample split lambda h_hat
sc :
SourceCondition S β
tb :
TikhonovBiasBound S β lambda sc
regimes :
∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n)
ζ :
ℝ
hζ_pos :
0 < ζ
hζ_lt :
ζ < 1
conclusion
∃ Aζ_master : Set Ω
if
then
((S.weakNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n ω)) - S.hL2 S.h₀_mem)) ^ 2 + lambda * (((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (h_hat n ω (S.xOf (sample.Z (k : ℕ) ω))) ^ 2))
- ((S.weakNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2 + lambda * (((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (tb.h_lambda_star_fun (S.xOf (sample.Z (k : ℕ) ω))) ^ 2))
≤ supObjective S TC sample split lambda (h_hat n ω) n ω
- supObjective S TC sample split lambda tb.h_lambda_star_fun n ω
+ (16 * delta n * criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n)) + 16 * delta n * criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n)) + 8 * delta n * criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n)) + (4 * (regimes n).bundle_HF.regime.b + 4 * (regimes n).bundle_mF.regime.b + 2 * (regimes n).bundle_F.regime.b) * sqrt (2 * log (4 * (2 : ℝ) ^ (n + 1) / ζ) / (split.n₁ n)))
Proof (Lean source)
theorem ep_master_event_from_localized
{S : OperatorSystem Ω μ} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
{split : OneShotSplit sample}
{lambda β : ℝ} {delta : ℕ → ℝ}
{h_hat : ℕ → Ω → S.𝒳 → ℝ}
(is_estimator : IsTRAEPrimalEstimator S TC sample split lambda h_hat)
(sc : SourceCondition S β)
(tb : TikhonovBiasBound S β lambda sc)
[IsProbabilityMeasure μ]
(regimes : ∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n))
{ζ : ℝ} (hζ_pos : 0 < ζ) (hζ_lt : ζ < 1) :
∃ Aζ_master : Set Ω,
MeasurableSet Aζ_master ∧ μ Aζ_master ≥ 1 - ofReal ζ ∧
∀ ω ∈ Aζ_master, ∀ n : ℕ, 1 ≤ split.n₁ n →
((S.weakNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n ω))
- S.hL2 S.h₀_mem)) ^ 2
+ lambda *
(((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(h_hat n ω (S.xOf (sample.Z (k : ℕ) ω))) ^ 2))
- ((S.weakNorm
(S.hL2 tb.h_lambda_star_mem
- S.hL2 S.h₀_mem)) ^ 2
+ lambda *
(((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(tb.h_lambda_star_fun (S.xOf (sample.Z (k : ℕ) ω))) ^ 2))
≤ supObjective S TC sample split lambda (h_hat n ω) n ω
- supObjective S TC sample split lambda tb.h_lambda_star_fun n ω
+ (16 * delta n *
criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n))
+ 16 * delta n *
criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n))
+ 8 * delta n *
criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n))
+ (4 * (regimes n).bundle_HF.regime.b
+ 4 * (regimes n).bundle_mF.regime.b
+ 2 * (regimes n).bundle_F.regime.b) *
sqrt
(2 * log (4 * (2 : ℝ) ^ (n + 1) / ζ)
/ (split.n₁ n))) := by
classical
let ε : ℕ → ℝ := fun n => ζ * ((1 / 2 : ℝ) ^ (n + 1))
let η : ℕ → ℝ := fun n => ε n / 4
have hε_pos : ∀ n, 0 < ε n := by
intro n
exact mul_pos hζ_pos (pow_pos (by norm_num) _)
have hε_le_one : ∀ n, ε n ≤ 1 := by
intro n
have hζ_le : ζ ≤ 1 := le_of_lt hζ_lt
have hpow_le_one : ((1 / 2 : ℝ) ^ (n + 1)) ≤ 1 := by
exact pow_le_one₀ (by norm_num) (by norm_num)
have hpow_nonneg : 0 ≤ ((1 / 2 : ℝ) ^ (n + 1)) := by positivity
nlinarith
have hη_pos : ∀ n, 0 < η n := by
intro n
dsimp [η]
positivity
have hη_le_one : ∀ n, η n ≤ 1 := by
intro n
dsimp [η]
nlinarith [hε_le_one n]
let EHF : ℕ → Set Ω := fun n =>
if hn : 0 < split.n₁ n then
(localized_omega_event_for_HF (regimes n) hn (hη_pos n) (hη_le_one n)).choose
else Set.univ
let EmF : ℕ → Set Ω := fun n =>
if hn : 0 < split.n₁ n then
(localized_omega_event_for_mF (regimes n) hn (hη_pos n) (hη_le_one n)).choose
else Set.univ
let EF : ℕ → Set Ω := fun n =>
if hn : 0 < split.n₁ n then
(localized_omega_event_for_F (regimes n) hn (hη_pos n) (hη_le_one n)).choose
else Set.univ
let En : ℕ → Set Ω := fun n => EHF n ∩ EmF n ∩ EF n
have hEHF_meas : ∀ n, MeasurableSet (EHF n) := by
intro n
by_cases hn : 0 < split.n₁ n
· simpa [EHF, hn] using
(localized_omega_event_for_HF (regimes n) hn
(hη_pos n) (hη_le_one n)).choose_spec.1
· simp [EHF, hn]
have hEmF_meas : ∀ n, MeasurableSet (EmF n) := by
intro n
by_cases hn : 0 < split.n₁ n
· simpa [EmF, hn] using
(localized_omega_event_for_mF (regimes n) hn
(hη_pos n) (hη_le_one n)).choose_spec.1
· simp [EmF, hn]
have hEF_meas : ∀ n, MeasurableSet (EF n) := by
intro n
by_cases hn : 0 < split.n₁ n
· simpa [EF, hn] using
(localized_omega_event_for_F (regimes n) hn
(hη_pos n) (hη_le_one n)).choose_spec.1
· simp [EF, hn]
have hEHF_mass : ∀ n, μ (EHF n) ≥ 1 - ofReal (η n) := by
intro n
by_cases hn : 0 < split.n₁ n
· simpa [EHF, hn] using
(localized_omega_event_for_HF (regimes n) hn
(hη_pos n) (hη_le_one n)).choose_spec.2.1
· simp [EHF, hn]
have hEmF_mass : ∀ n, μ (EmF n) ≥ 1 - ofReal (η n) := by
intro n
by_cases hn : 0 < split.n₁ n
· simpa [EmF, hn] using
(localized_omega_event_for_mF (regimes n) hn
(hη_pos n) (hη_le_one n)).choose_spec.2.1
· simp [EmF, hn]
have hEF_mass : ∀ n, μ (EF n) ≥ 1 - ofReal (η n) := by
intro n
by_cases hn : 0 < split.n₁ n
· simpa [EF, hn] using
(localized_omega_event_for_F (regimes n) hn
(hη_pos n) (hη_le_one n)).choose_spec.2.1
· simp [EF, hn]
have hEn_meas : ∀ n, MeasurableSet (En n) := by
intro n
exact ((hEHF_meas n).inter (hEmF_meas n)).inter (hEF_meas n)
have hEn_mass : ∀ n, μ (En n) ≥ 1 - ofReal (ε n) := by
intro n
have h12 :
μ (EHF n ∩ EmF n)
≥ 1 - (ofReal (η n) + ofReal (η n)) :=
measure_inter_ge_one_sub_add_of_ge (hEHF_meas n) (hEmF_meas n)
(hEHF_mass n) (hEmF_mass n)
have h123 :
μ ((EHF n ∩ EmF n) ∩ EF n)
≥ 1 -
((ofReal (η n) + ofReal (η n))
+ ofReal (η n)) :=
measure_inter_ge_one_sub_add_of_ge
((hEHF_meas n).inter (hEmF_meas n)) (hEF_meas n)
h12 (hEF_mass n)
have hη_nonneg : 0 ≤ η n := le_of_lt (hη_pos n)
have htriple_eq :
(ofReal (η n) + ofReal (η n))
+ ofReal (η n)
= ofReal (η n + η n + η n) := by
rw [← ENNReal.ofReal_add hη_nonneg hη_nonneg]
rw [← ENNReal.ofReal_add (add_nonneg hη_nonneg hη_nonneg) hη_nonneg]
have htriple_le :
(ofReal (η n) + ofReal (η n))
+ ofReal (η n)
≤ ofReal (ε n) := by
rw [htriple_eq]
apply ENNReal.ofReal_le_ofReal
dsimp [η]
nlinarith [hε_pos n]
simpa [En, Set.inter_assoc] using
(tsub_le_tsub_left htriple_le 1).trans h123
have htsum_ε : (∑' n, ofReal (ε n)) ≤ ofReal ζ := by
have hterm :
(fun n => ofReal (ε n))
=
fun n => ofReal ζ * (2⁻¹ : ENNReal) ^ (n + 1) := by
funext n
rw [show ε n = ζ * (1 / 2 : ℝ) ^ (n + 1) by rfl]
rw [ENNReal.ofReal_mul (le_of_lt hζ_pos)]
simp [one_div, ENNReal.inv_pow]
rw [hterm, ENNReal.tsum_mul_left, ENNReal.tsum_geometric_add_one]
have hgeom : (2⁻¹ : ENNReal) * (1 - 2⁻¹)⁻¹ = 1 := by
rw [ENNReal.one_sub_inv_two, inv_inv]
exact ENNReal.inv_mul_cancel (Ne.symm (NeZero.ne' (2 : ENNReal)))
(by norm_num : (2 : ENNReal) ≠ ⊤)
rw [hgeom, mul_one]
let Aζ_master : Set Ω := ⋂ n, En n
refine ⟨Aζ_master, MeasurableSet.iInter hEn_meas, ?_, ?_⟩
· exact (tsub_le_tsub_left htsum_ε 1).trans
(measure_iInter_nat_ge_one_sub_tsum_of_ge hEn_meas hEn_mass)
· intro ω hω n _hn
have hn_pos : 0 < split.n₁ n := lt_of_lt_of_le zero_lt_one _hn
have hωn : ω ∈ En n := Set.mem_iInter.mp hω n
have hωHF : ω ∈ EHF n := hωn.1.1
have hωmF : ω ∈ EmF n := hωn.1.2
have hωF : ω ∈ EF n := hωn.2
have hωHF_event :
ω ∈ (localized_omega_event_for_HF (regimes n) hn_pos
(hη_pos n) (hη_le_one n)).choose := by
simpa [EHF, hn_pos] using hωHF
have hωmF_event :
ω ∈ (localized_omega_event_for_mF (regimes n) hn_pos
(hη_pos n) (hη_le_one n)).choose := by
simpa [EmF, hn_pos] using hωmF
have hωF_event :
ω ∈ (localized_omega_event_for_F (regimes n) hn_pos
(hη_pos n) (hη_le_one n)).choose := by
simpa [EF, hn_pos] using hωF
obtain ⟨f_h, hf_h, hcl_h⟩ :=
(regimes n).closedness (h_hat n ω) (is_estimator.mem_H n ω)
obtain ⟨f_star, hf_star, hstar_sup_le_inner⟩ :=
(regimes n).supObjective_attained split n ω
tb.h_lambda_star_fun (regimes n).realizability
have hinner_le_sup :
innerObjective S sample split lambda (h_hat n ω) f_h n ω
≤ supObjective S TC sample split lambda (h_hat n ω) n ω :=
(regimes n).inner_le_supObjective split n ω
(h_hat n ω) (is_estimator.mem_H n ω) f_h hf_h
have hlog : 1 / η n = 4 * (2 : ℝ) ^ (n + 1) / ζ := by
dsimp [η, ε]
simp only [one_div]
rw [inv_pow]
field_simp [ne_of_gt hζ_pos,
pow_ne_zero (n + 1) (show (2 : ℝ) ≠ 0 by norm_num)]
have hHF_h :=
(localized_omega_event_for_HF (regimes n) hn_pos
(hη_pos n) (hη_le_one n)).choose_spec.2.2
ω hωHF_event (h_hat n ω) (is_estimator.mem_H n ω) f_h hf_h
have hmF_h :=
(localized_omega_event_for_mF (regimes n) hn_pos
(hη_pos n) (hη_le_one n)).choose_spec.2.2
ω hωmF_event f_h hf_h
have hF_h :=
(localized_omega_event_for_F (regimes n) hn_pos
(hη_pos n) (hη_le_one n)).choose_spec.2.2
ω hωF_event f_h hf_h
have hHF_star :=
(localized_omega_event_for_HF (regimes n) hn_pos
(hη_pos n) (hη_le_one n)).choose_spec.2.2
ω hωHF_event tb.h_lambda_star_fun (regimes n).realizability
f_star hf_star
have hmF_star :=
(localized_omega_event_for_mF (regimes n) hn_pos
(hη_pos n) (hη_le_one n)).choose_spec.2.2
ω hωmF_event f_star hf_star
have hF_star :=
(localized_omega_event_for_F (regimes n) hn_pos
(hη_pos n) (hη_le_one n)).choose_spec.2.2
ω hωF_event f_star hf_star
rw [hlog] at hHF_h hmF_h hF_h hHF_star hmF_star hF_star
let rHF : ℝ :=
4 * delta n * criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n))
+ (regimes n).bundle_HF.regime.b *
sqrt (2 * log (4 * (2 : ℝ) ^ (n + 1) / ζ)
/ (split.n₁ n))
let rmF : ℝ :=
4 * delta n * criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n))
-- … truncated; follow the source link for the rest …
3 supporting declarations (lemmas, instances)
-
population_closedness_critic_gap_eqlemma — Population curvature at the closedness critic. For a fixed candidate h, the closedness witness f_closed is the population maximizer of the quadratic adversarial criterion, and the drop at any critic f is exactly the squared L² critic gap.hypothesesS :h :S.𝒳 → ℝhh :h ∈ TC.Hf_closed :S.𝒵 → ℝhf_closed :f_closed ∈ TC.Ff :S.𝒵 → ℝhf :f ∈ TC.Fhcl :S.T (S.hL2 S.h₀_mem - S.hL2 (TC.H_subset hh)) = S.qL2 (TC.F_subset hf_closed)conclusion(2 * (∫ ω, S.m (S.W ω) f_closed ∂μ) - 2 * (∫ ω, h (S.xOf (S.W ω)) * f_closed (S.zOf (S.W ω)) ∂μ) - ∫ ω, (f_closed (S.zOf (S.W ω))) ^ 2 ∂μ)- (2 * (∫ ω, S.m (S.W ω) f ∂μ) - 2 * (∫ ω, h (S.xOf (S.W ω)) * f (S.zOf (S.W ω)) ∂μ) - ∫ ω, (f (S.zOf (S.W ω))) ^ 2 ∂μ)= ‖S.qL2 (TC.F_subset hf_closed) - S.qL2 (TC.F_subset hf)‖ ^ 2Proof (Lean source)
lemma population_closedness_critic_gap_eq {S : OperatorSystem Ω μ} {TC : TRAEClasses S} [IsProbabilityMeasure μ] {h : S.𝒳 → ℝ} (hh : h ∈ TC.H) {f_closed : S.𝒵 → ℝ} (hf_closed : f_closed ∈ TC.F) {f : S.𝒵 → ℝ} (hf : f ∈ TC.F) (hcl : S.T (S.hL2 S.h₀_mem - S.hL2 (TC.H_subset hh)) = S.qL2 (TC.F_subset hf_closed)) : (2 * (∫ ω, S.m (S.W ω) f_closed ∂μ) - 2 * (∫ ω, h (S.xOf (S.W ω)) * f_closed (S.zOf (S.W ω)) ∂μ) - ∫ ω, (f_closed (S.zOf (S.W ω))) ^ 2 ∂μ) - (2 * (∫ ω, S.m (S.W ω) f ∂μ) - 2 * (∫ ω, h (S.xOf (S.W ω)) * f (S.zOf (S.W ω)) ∂μ) - ∫ ω, (f (S.zOf (S.W ω))) ^ 2 ∂μ) = ‖S.qL2 (TC.F_subset hf_closed) - S.qL2 (TC.F_subset hf)‖ ^ 2 := by let qc := S.qL2 (TC.F_subset hf_closed) let q := S.qL2 (TC.F_subset hf) have hclosed := population_inner_eq_closedness_inner (S := S) (TC := TC) (hh := hh) (hf_closed := hf_closed) (hf := hf_closed) hcl have hf_eq := population_inner_eq_closedness_inner (S := S) (TC := TC) (hh := hh) (hf_closed := hf_closed) (hf := hf) hcl have hqc_self : inner ℝ qc qc = ‖qc‖ ^ 2 := real_inner_self_eq_norm_sq qc have hq_self : inner ℝ q q = ‖q‖ ^ 2 := real_inner_self_eq_norm_sq q have hnorm : ‖qc - q‖ ^ 2 = ‖qc‖ ^ 2 + ‖q‖ ^ 2 - 2 * inner ℝ qc q := by rw [norm_sub_sq_real] ring rw [hclosed, hf_eq, hnorm] dsimp [qc, q] at hqc_self hq_self nlinarith [hqc_self, hq_self] -
empirical_critic_argmax_localizedlemma — Deterministic argmax-localization bridge. If f_emp empirically beats the closedness witness for the same candidate h, and the population-vs-empirical loss difference is controlled by R, then the empirical critic is within squared L² distance R of the closedness witness.hypothesesS :split :OneShotSplit samplelambda :ℝh :S.𝒳 → ℝhh :h ∈ TC.Hf_closed :S.𝒵 → ℝhf_closed :f_closed ∈ TC.Ff_emp :S.𝒵 → ℝhf_emp :f_emp ∈ TC.Fn :ℕω :ΩR :ℝhcl :S.T (S.hL2 S.h₀_mem - S.hL2 (TC.H_subset hh)) = S.qL2 (TC.F_subset hf_closed)hopt :innerObjective S sample split lambda h f_closed n ω≤ innerObjective S sample split lambda h f_emp n ωhdev :(2 * (∫ ω', S.m (S.W ω') f_closed ∂μ) - 2 * (∫ ω', h (S.xOf (S.W ω')) * f_closed (S.zOf (S.W ω')) ∂μ) - ∫ ω', (f_closed (S.zOf (S.W ω'))) ^ 2 ∂μ)- (2 * (∫ ω', S.m (S.W ω') f_emp ∂μ) - 2 * (∫ ω', h (S.xOf (S.W ω')) * f_emp (S.zOf (S.W ω')) ∂μ) - ∫ ω', (f_emp (S.zOf (S.W ω'))) ^ 2 ∂μ)≤ innerObjective S sample split lambda h f_closed n ω- innerObjective S sample split lambda h f_emp n ω+ Rconclusion‖S.qL2 (TC.F_subset hf_closed) - S.qL2 (TC.F_subset hf_emp)‖ ^ 2 ≤ RProof (Lean source)
lemma empirical_critic_argmax_localized {S : OperatorSystem Ω μ} {TC : TRAEClasses S} {P_W : Measure S.𝒲} {sample : IIDSample Ω S.𝒲 μ P_W} {split : OneShotSplit sample} [IsProbabilityMeasure μ] {lambda : ℝ} {h : S.𝒳 → ℝ} (hh : h ∈ TC.H) {f_closed : S.𝒵 → ℝ} (hf_closed : f_closed ∈ TC.F) {f_emp : S.𝒵 → ℝ} (hf_emp : f_emp ∈ TC.F) {n : ℕ} {ω : Ω} {R : ℝ} (hcl : S.T (S.hL2 S.h₀_mem - S.hL2 (TC.H_subset hh)) = S.qL2 (TC.F_subset hf_closed)) (hopt : innerObjective S sample split lambda h f_closed n ω ≤ innerObjective S sample split lambda h f_emp n ω) (hdev : (2 * (∫ ω', S.m (S.W ω') f_closed ∂μ) - 2 * (∫ ω', h (S.xOf (S.W ω')) * f_closed (S.zOf (S.W ω')) ∂μ) - ∫ ω', (f_closed (S.zOf (S.W ω'))) ^ 2 ∂μ) - (2 * (∫ ω', S.m (S.W ω') f_emp ∂μ) - 2 * (∫ ω', h (S.xOf (S.W ω')) * f_emp (S.zOf (S.W ω')) ∂μ) - ∫ ω', (f_emp (S.zOf (S.W ω'))) ^ 2 ∂μ) ≤ innerObjective S sample split lambda h f_closed n ω - innerObjective S sample split lambda h f_emp n ω + R) : ‖S.qL2 (TC.F_subset hf_closed) - S.qL2 (TC.F_subset hf_emp)‖ ^ 2 ≤ R := by have hgap := population_closedness_critic_gap_eq (S := S) (TC := TC) (hh := hh) (hf_closed := hf_closed) (hf := hf_emp) hcl rw [← hgap] linarith [hdev, hopt] -
empirical_critic_argmax_localized_from_componentslemma — Componentwise version of empirical_critic_argmax_localized.hypothesesS :split :OneShotSplit samplelambda :ℝh :S.𝒳 → ℝhh :h ∈ TC.Hf_closed :S.𝒵 → ℝhf_closed :f_closed ∈ TC.Ff_emp :S.𝒵 → ℝhf_emp :f_emp ∈ TC.Fn :ℕω :ΩRm_closed RHF_closed RF_closed Rm_emp RHF_emp RF_emp :ℝhcl :S.T (S.hL2 S.h₀_mem - S.hL2 (TC.H_subset hh)) = S.qL2 (TC.F_subset hf_closed)hopt :innerObjective S sample split lambda h f_closed n ω≤ innerObjective S sample split lambda h f_emp n ωhmF_closed :|((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), S.m (sample.Z (k : ℕ) ω) f_closed- ∫ ω', S.m (S.W ω') f_closed ∂μ|≤ Rm_closedhHF_closed :|((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), h (S.xOf (sample.Z (k : ℕ) ω)) * f_closed (S.zOf (sample.Z (k : ℕ) ω))- ∫ ω', h (S.xOf (S.W ω')) * f_closed (S.zOf (S.W ω')) ∂μ|≤ RHF_closedhF_closed :|((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (f_closed (S.zOf (sample.Z (k : ℕ) ω))) ^ 2- ∫ ω', (f_closed (S.zOf (S.W ω'))) ^ 2 ∂μ|≤ RF_closedhmF_emp :|((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), S.m (sample.Z (k : ℕ) ω) f_emp- ∫ ω', S.m (S.W ω') f_emp ∂μ|≤ Rm_emphHF_emp :|((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), h (S.xOf (sample.Z (k : ℕ) ω)) * f_emp (S.zOf (sample.Z (k : ℕ) ω))- ∫ ω', h (S.xOf (S.W ω')) * f_emp (S.zOf (S.W ω')) ∂μ|≤ RHF_emphF_emp :|((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (f_emp (S.zOf (sample.Z (k : ℕ) ω))) ^ 2- ∫ ω', (f_emp (S.zOf (S.W ω'))) ^ 2 ∂μ|≤ RF_empconclusion‖S.qL2 (TC.F_subset hf_closed) - S.qL2 (TC.F_subset hf_emp)‖ ^ 2≤ (2 * Rm_closed + 2 * RHF_closed + RF_closed) + (2 * Rm_emp + 2 * RHF_emp + RF_emp)Proof (Lean source)
lemma empirical_critic_argmax_localized_from_components {S : OperatorSystem Ω μ} {TC : TRAEClasses S} {P_W : Measure S.𝒲} {sample : IIDSample Ω S.𝒲 μ P_W} {split : OneShotSplit sample} [IsProbabilityMeasure μ] {lambda : ℝ} {h : S.𝒳 → ℝ} (hh : h ∈ TC.H) {f_closed : S.𝒵 → ℝ} (hf_closed : f_closed ∈ TC.F) {f_emp : S.𝒵 → ℝ} (hf_emp : f_emp ∈ TC.F) {n : ℕ} {ω : Ω} {Rm_closed RHF_closed RF_closed Rm_emp RHF_emp RF_emp : ℝ} (hcl : S.T (S.hL2 S.h₀_mem - S.hL2 (TC.H_subset hh)) = S.qL2 (TC.F_subset hf_closed)) (hopt : innerObjective S sample split lambda h f_closed n ω ≤ innerObjective S sample split lambda h f_emp n ω) (hmF_closed : |((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), S.m (sample.Z (k : ℕ) ω) f_closed - ∫ ω', S.m (S.W ω') f_closed ∂μ| ≤ Rm_closed) (hHF_closed : |((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), h (S.xOf (sample.Z (k : ℕ) ω)) * f_closed (S.zOf (sample.Z (k : ℕ) ω)) - ∫ ω', h (S.xOf (S.W ω')) * f_closed (S.zOf (S.W ω')) ∂μ| ≤ RHF_closed) (hF_closed : |((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (f_closed (S.zOf (sample.Z (k : ℕ) ω))) ^ 2 - ∫ ω', (f_closed (S.zOf (S.W ω'))) ^ 2 ∂μ| ≤ RF_closed) (hmF_emp : |((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), S.m (sample.Z (k : ℕ) ω) f_emp - ∫ ω', S.m (S.W ω') f_emp ∂μ| ≤ Rm_emp) (hHF_emp : |((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), h (S.xOf (sample.Z (k : ℕ) ω)) * f_emp (S.zOf (sample.Z (k : ℕ) ω)) - ∫ ω', h (S.xOf (S.W ω')) * f_emp (S.zOf (S.W ω')) ∂μ| ≤ RHF_emp) (hF_emp : |((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (f_emp (S.zOf (sample.Z (k : ℕ) ω))) ^ 2 - ∫ ω', (f_emp (S.zOf (S.W ω'))) ^ 2 ∂μ| ≤ RF_emp) : ‖S.qL2 (TC.F_subset hf_closed) - S.qL2 (TC.F_subset hf_emp)‖ ^ 2 ≤ (2 * Rm_closed + 2 * RHF_closed + RF_closed) + (2 * Rm_emp + 2 * RHF_emp + RF_emp) := by let D_closed : ℝ := 2 * Rm_closed + 2 * RHF_closed + RF_closed let D_emp : ℝ := 2 * Rm_emp + 2 * RHF_emp + RF_emp have hclosed_upper : 2 * (∫ ω', S.m (S.W ω') f_closed ∂μ) - 2 * (∫ ω', h (S.xOf (S.W ω')) * f_closed (S.zOf (S.W ω')) ∂μ) - ∫ ω', (f_closed (S.zOf (S.W ω'))) ^ 2 ∂μ + lambda * (((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (h (S.xOf (sample.Z (k : ℕ) ω))) ^ 2) ≤ innerObjective S sample split lambda h f_closed n ω + D_closed := by simpa [D_closed] using population_regularized_le_innerObjective_add_deviation split lambda h f_closed n ω hmF_closed hHF_closed hF_closed have hemp_upper : innerObjective S sample split lambda h f_emp n ω ≤ 2 * (∫ ω', S.m (S.W ω') f_emp ∂μ) - 2 * (∫ ω', h (S.xOf (S.W ω')) * f_emp (S.zOf (S.W ω')) ∂μ) - ∫ ω', (f_emp (S.zOf (S.W ω'))) ^ 2 ∂μ + lambda * (((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (h (S.xOf (sample.Z (k : ℕ) ω))) ^ 2) + D_emp := by simpa [D_emp] using innerObjective_le_population_regularized_add_deviation split lambda h f_emp n ω hmF_emp hHF_emp hF_emp apply empirical_critic_argmax_localized (S := S) (TC := TC) (sample := sample) (split := split) (lambda := lambda) (hh := hh) (hf_closed := hf_closed) (hf_emp := hf_emp) (n := n) (ω := ω) (R := D_closed + D_emp) hcl hopt linarith [hclosed_upper, hemp_upper]
EPPerN 2 core · 1 supporting This file states the per-sample-size empirical-process control used by the primal NPIV rate theorem. ★ ep_per_n_inequality_from_deviations★ ep_inequality_from_localized
Per-Sample Empirical-Process Bound
This file states the per-sample-size empirical-process control used by the primal NPIV rate theorem. It packages the master localized event into the form consumed by the estimator analysis at a fixed sample size.
lemma ep_per_n_inequality_from_deviations reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
EP per-n inequality from an objective-level localized modulus (Helper B). Pure analytic per-n step, with no probability statement. Given a sample size n with 1 ≤ split.n₁ n, a localized-regime bundle at that fold-A sample size, a confidence level ζ strictly between 0 and 1, and the pointwise objective-level inequality, at sample point ω, bounding the population weak-objective-plus-regularizer excess by the empirical sup-objective excess plus the localized envelope, the weak-norm estimation excess is bounded by the empirical regularizer gap plus the same localized envelope, the empirical sup-objective excess having been eliminated using the optimality of ĥ_n (is_estimator.opt) against tb.h_lambda_star_fun. This statement is intentionally not vacuous: the hypothesis still contains the empirical sup-objective excess, which the proof cancels rather than assumes away.
Formal statement
hypotheses
S :
split :
OneShotSplit sample
lambda β :
ℝ
delta :
ℕ → ℝ
h_hat :
ℕ → Ω → S.𝒳 → ℝ
is_estimator :
IsTRAEPrimalEstimator S TC sample split lambda h_hat
sc :
SourceCondition S β
tb :
TikhonovBiasBound S β lambda sc
regimes :
∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n)
ζ :
ℝ
_hζ_pos :
0 < ζ
_hζ_lt :
ζ < 1
n :
ℕ
_hn :
1 ≤ split.n₁ n
ω :
Ω
objective_gap :
((S.weakNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n ω)) - S.hL2 S.h₀_mem)) ^ 2 + lambda * (((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (h_hat n ω (S.xOf (sample.Z (k : ℕ) ω))) ^ 2))
- ((S.weakNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2 + lambda * (((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (tb.h_lambda_star_fun (S.xOf (sample.Z (k : ℕ) ω))) ^ 2))
≤ supObjective S TC sample split lambda (h_hat n ω) n ω
- supObjective S TC sample split lambda tb.h_lambda_star_fun n ω
+ (16 * delta n * criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n)) + 16 * delta n * criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n)) + 8 * delta n * criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n)) + (4 * (regimes n).bundle_HF.regime.b + 4 * (regimes n).bundle_mF.regime.b + 2 * (regimes n).bundle_F.regime.b) * sqrt (2 * log (4 * (2 : ℝ) ^ (n + 1) / ζ) / (split.n₁ n)))
conclusion
(S.weakNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n ω)) - S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2
≤ lambda * (((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (tb.h_lambda_star_fun (S.xOf (sample.Z (k : ℕ) ω))) ^ 2 - ((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (h_hat n ω (S.xOf (sample.Z (k : ℕ) ω))) ^ 2)
+ (16 * delta n * criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n)) + 16 * delta n * criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n)) + 8 * delta n * criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n)) + (4 * (regimes n).bundle_HF.regime.b + 4 * (regimes n).bundle_mF.regime.b + 2 * (regimes n).bundle_F.regime.b) * sqrt (2 * log (4 * (2 : ℝ) ^ (n + 1) / ζ) / (split.n₁ n)))
Proof (Lean source)
lemma ep_per_n_inequality_from_deviations
{S : OperatorSystem Ω μ} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
{split : OneShotSplit sample}
{lambda β : ℝ} {delta : ℕ → ℝ}
{h_hat : ℕ → Ω → S.𝒳 → ℝ}
(is_estimator : IsTRAEPrimalEstimator S TC sample split lambda h_hat)
(sc : SourceCondition S β)
(tb : TikhonovBiasBound S β lambda sc)
[IsProbabilityMeasure μ]
(regimes : ∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n))
{ζ : ℝ} (_hζ_pos : 0 < ζ) (_hζ_lt : ζ < 1)
(n : ℕ) (_hn : 1 ≤ split.n₁ n) (ω : Ω)
(objective_gap :
((S.weakNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n ω))
- S.hL2 S.h₀_mem)) ^ 2
+ lambda *
(((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(h_hat n ω (S.xOf (sample.Z (k : ℕ) ω))) ^ 2))
- ((S.weakNorm
(S.hL2 tb.h_lambda_star_mem
- S.hL2 S.h₀_mem)) ^ 2
+ lambda *
(((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(tb.h_lambda_star_fun (S.xOf (sample.Z (k : ℕ) ω))) ^ 2))
≤ supObjective S TC sample split lambda (h_hat n ω) n ω
- supObjective S TC sample split lambda tb.h_lambda_star_fun n ω
+ (16 * delta n *
criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n))
+ 16 * delta n *
criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n))
+ 8 * delta n *
criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n))
+ (4 * (regimes n).bundle_HF.regime.b
+ 4 * (regimes n).bundle_mF.regime.b
+ 2 * (regimes n).bundle_F.regime.b) *
sqrt
(2 * log (4 * (2 : ℝ) ^ (n + 1) / ζ)
/ (split.n₁ n)))) :
(S.weakNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n ω))
- S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm
(S.hL2 tb.h_lambda_star_mem
- S.hL2 S.h₀_mem)) ^ 2
≤ lambda *
(((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(tb.h_lambda_star_fun (S.xOf (sample.Z (k : ℕ) ω))) ^ 2
- ((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(h_hat n ω (S.xOf (sample.Z (k : ℕ) ω))) ^ 2)
+ (16 * delta n *
criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n))
+ 16 * delta n *
criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n))
+ 8 * delta n *
criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n))
+ (4 * (regimes n).bundle_HF.regime.b
+ 4 * (regimes n).bundle_mF.regime.b
+ 2 * (regimes n).bundle_F.regime.b) *
sqrt
(2 * log (4 * (2 : ℝ) ^ (n + 1) / ζ)
/ (split.n₁ n))) := by
have hopt :
supObjective S TC sample split lambda (h_hat n ω) n ω
≤ supObjective S TC sample split lambda tb.h_lambda_star_fun n ω :=
is_estimator.opt n ω tb.h_lambda_star_fun (regimes n).realizability
linarith [objective_gap, hopt]
theorem ep_inequality_from_localized reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Localized empirical-process inequality for the primal NPIV estimator. Given, for every n, a localized-regime bundle for the weak-norm, regularizer, and cross function classes at that fold-A sample size, and a confidence level ζ strictly between 0 and 1, there is an event of probability at least 1 − ζ on which, simultaneously for every n with 1 ≤ split.n₁ n, the weak-norm estimation excess ‖T(ĥ_n − h_0)‖² − ‖T(h*_λ − h_0)‖² is bounded by the empirical regularizer gap λ · (‖h*‖²_{A(n)} − ‖ĥ‖²_{A(n)}) plus a localized envelope built from the per-n critical radii scaled by δ_n and a √(log(1/ζ)/n) deviation term, where ‖h‖²_{A(n)} := (split.n₁ n)⁻¹ ∑_{k < split.n₁ n} h(X_k)² is the fold-A empirical second moment.
Formal statement
hypotheses
S :
split :
OneShotSplit sample
lambda β :
ℝ
delta :
ℕ → ℝ
h_hat :
ℕ → Ω → S.𝒳 → ℝ
IsTRAEPrimalEstimator S TC sample split lambda h_hat
sc :
SourceCondition S β
tb :
TikhonovBiasBound S β lambda sc
regimes :
∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n)
ζ :
ℝ
hζ_pos :
0 < ζ
hζ_lt :
ζ < 1
conclusion
∃ Aζ_ep : Set Ω
if
then
(S.weakNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n ω)) - S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2
≤ lambda * (((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (tb.h_lambda_star_fun (S.xOf (sample.Z (k : ℕ) ω))) ^ 2 - ((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (h_hat n ω (S.xOf (sample.Z (k : ℕ) ω))) ^ 2)
+ (16 * delta n * criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n)) + 16 * delta n * criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n)) + 8 * delta n * criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n)) + (4 * (regimes n).bundle_HF.regime.b + 4 * (regimes n).bundle_mF.regime.b + 2 * (regimes n).bundle_F.regime.b) * sqrt (2 * log (4 * (2 : ℝ) ^ (n + 1) / ζ) / (split.n₁ n)))
Proof (Lean source)
theorem ep_inequality_from_localized
{S : OperatorSystem Ω μ} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
{split : OneShotSplit sample}
{lambda β : ℝ} {delta : ℕ → ℝ}
{h_hat : ℕ → Ω → S.𝒳 → ℝ}
{is_estimator : IsTRAEPrimalEstimator S TC sample split lambda h_hat}
(sc : SourceCondition S β)
(tb : TikhonovBiasBound S β lambda sc)
[IsProbabilityMeasure μ]
(regimes : ∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n))
{ζ : ℝ} (hζ_pos : 0 < ζ) (hζ_lt : ζ < 1) :
∃ Aζ_ep : Set Ω,
MeasurableSet Aζ_ep ∧ μ Aζ_ep ≥ 1 - ofReal ζ ∧
∀ ω ∈ Aζ_ep, ∀ n : ℕ, 1 ≤ split.n₁ n →
(S.weakNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n ω))
- S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm
(S.hL2 tb.h_lambda_star_mem
- S.hL2 S.h₀_mem)) ^ 2
≤ lambda *
(((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(tb.h_lambda_star_fun (S.xOf (sample.Z (k : ℕ) ω))) ^ 2
- ((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(h_hat n ω (S.xOf (sample.Z (k : ℕ) ω))) ^ 2)
+ (16 * delta n *
criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n))
+ 16 * delta n *
criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n))
+ 8 * delta n *
criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n))
+ (4 * (regimes n).bundle_HF.regime.b
+ 4 * (regimes n).bundle_mF.regime.b
+ 2 * (regimes n).bundle_F.regime.b) *
sqrt
(2 * log (4 * (2 : ℝ) ^ (n + 1) / ζ)
/ (split.n₁ n))) := by
-- The master event provides the objective-level explicit modulus; the
-- per-`n` lemma removes the remaining empirical sup-objective excess
-- using `is_estimator.opt`.
obtain ⟨Aζ_master, hAζ_meas, hAζ_mass, hAζ_payload⟩ :=
ep_master_event_from_localized (h_hat := h_hat) is_estimator sc tb regimes
hζ_pos hζ_lt
refine ⟨Aζ_master, hAζ_meas, hAζ_mass, ?_⟩
intro ω hω n hn
exact ep_per_n_inequality_from_deviations is_estimator sc tb regimes
hζ_pos hζ_lt n hn ω (hAζ_payload ω hω n hn)
1 supporting declaration (lemmas, instances)
-
ep_pop_inner_at_closedness_witnesslemma — EP closedness-witness population identity (Helper B1).hypothesesS :h :S.𝒳 → ℝhh :h ∈ TC.Hf :S.𝒵 → ℝhf :f ∈ TC.Fhcl :S.T (S.hL2 S.h₀_mem - S.hL2 (TC.H_subset hh)) = S.qL2 (TC.F_subset hf)conclusion2 * (∫ ω, S.m (S.W ω) f ∂μ)- 2 * (∫ ω, h (S.xOf (S.W ω)) * f (S.zOf (S.W ω)) ∂μ)- ∫ ω, (f (S.zOf (S.W ω))) ^ 2 ∂μ= (S.weakNorm (S.hL2 (TC.H_subset hh) - S.hL2 S.h₀_mem)) ^ 2Proof (Lean source)
lemma ep_pop_inner_at_closedness_witness {S : OperatorSystem Ω μ} {TC : TRAEClasses S} [IsProbabilityMeasure μ] {h : S.𝒳 → ℝ} (hh : h ∈ TC.H) {f : S.𝒵 → ℝ} (hf : f ∈ TC.F) (hcl : S.T (S.hL2 S.h₀_mem - S.hL2 (TC.H_subset hh)) = S.qL2 (TC.F_subset hf)) : 2 * (∫ ω, S.m (S.W ω) f ∂μ) - 2 * (∫ ω, h (S.xOf (S.W ω)) * f (S.zOf (S.W ω)) ∂μ) - ∫ ω, (f (S.zOf (S.W ω))) ^ 2 ∂μ = (S.weakNorm (S.hL2 (TC.H_subset hh) - S.hL2 S.h₀_mem)) ^ 2 := by haveI := S.isFiniteMeasure haveI := S.Qbar_L2_hasProj -- Step 1: ⟨T(hL2 h₀ - hL2 hh), qL2 hf⟩ = ∫ (h₀ - h)·f via T_inner_eq_integral. have h_inner_int : inner ℝ (S.T (S.hL2 S.h₀_mem - S.hL2 (TC.H_subset hh))) (S.qL2 (TC.F_subset hf)) = ∫ ω, (S.h₀ (S.xOf (S.W ω)) - h (S.xOf (S.W ω))) * f (S.zOf (S.W ω)) ∂μ := S.T_inner_eq_integral S.h₀_mem (TC.H_subset hh) (TC.F_subset hf) -- Step 2: primal_moment: ∫ m(W;f) = ∫ h₀(X)·f(Z). have h_moment : ∫ ω, S.m (S.W ω) f ∂μ = ∫ ω, S.h₀ (S.xOf (S.W ω)) * f (S.zOf (S.W ω)) ∂μ := S.primal_moment f (TC.F_subset hf) -- Step 3: ∫ (h₀ - h)·f = ∫ h₀·f - ∫ h·f via integral_sub. have hh₀f_int : Integrable (fun ω => S.h₀ (S.xOf (S.W ω)) * f (S.zOf (S.W ω))) μ := by have := S.integrable_qh S.h₀ S.h₀_mem f (TC.F_subset hf) simpa [mul_comm] using this have hhf_int : Integrable (fun ω => h (S.xOf (S.W ω)) * f (S.zOf (S.W ω))) μ := by have := S.integrable_qh h (TC.H_subset hh) f (TC.F_subset hf) simpa [mul_comm] using this have h_int_diff : ∫ ω, (S.h₀ (S.xOf (S.W ω)) - h (S.xOf (S.W ω))) * f (S.zOf (S.W ω)) ∂μ = (∫ ω, S.h₀ (S.xOf (S.W ω)) * f (S.zOf (S.W ω)) ∂μ) - ∫ ω, h (S.xOf (S.W ω)) * f (S.zOf (S.W ω)) ∂μ := by have : (fun ω => (S.h₀ (S.xOf (S.W ω)) - h (S.xOf (S.W ω))) * f (S.zOf (S.W ω))) = fun ω => S.h₀ (S.xOf (S.W ω)) * f (S.zOf (S.W ω)) - h (S.xOf (S.W ω)) * f (S.zOf (S.W ω)) := by funext ω; ring rw [this] exact integral_sub hh₀f_int hhf_int -- Combine 1+2+3: have h_diff_eq_inner : (∫ ω, S.m (S.W ω) f ∂μ) - ∫ ω, h (S.xOf (S.W ω)) * f (S.zOf (S.W ω)) ∂μ = inner ℝ (S.T (S.hL2 S.h₀_mem - S.hL2 (TC.H_subset hh))) (S.qL2 (TC.F_subset hf)) := by rw [h_moment, h_inner_int, h_int_diff] -- Step 4: ⟨qL2 hf, qL2 hf⟩ = ∫ f². have h_qL2_self : inner ℝ (S.qL2 (TC.F_subset hf)) (S.qL2 (TC.F_subset hf)) = ∫ ω, (f (S.zOf (S.W ω))) ^ 2 ∂μ := by rw [MeasureTheory.L2.inner_def] refine integral_congr_ae ?_ filter_upwards [(S.toQbarL2 f (TC.F_subset hf)).coeFn_toLp] with ω hω simp [OperatorSystem.qL2, hω, pow_two] -- Step 5: substitute hcl in the inner-product side, then close with norm. have h_diff_eq_int_fsq : (∫ ω, S.m (S.W ω) f ∂μ) - ∫ ω, h (S.xOf (S.W ω)) * f (S.zOf (S.W ω)) ∂μ = ∫ ω, (f (S.zOf (S.W ω))) ^ 2 ∂μ := by rw [h_diff_eq_inner, hcl, h_qL2_self] -- Step 6: weakNorm of the negated argument. have h_T_neg : S.T (S.hL2 (TC.H_subset hh) - S.hL2 S.h₀_mem) = - S.qL2 (TC.F_subset hf) := by rw [S.T_sub] have hcl' : S.T (S.hL2 S.h₀_mem) - S.T (S.hL2 (TC.H_subset hh)) = S.qL2 (TC.F_subset hf) := by rw [← S.T_sub]; exact hcl rw [← hcl'] abel have h_weak_eq_intf : (S.weakNorm (S.hL2 (TC.H_subset hh) - S.hL2 S.h₀_mem)) ^ 2 = ∫ ω, (f (S.zOf (S.W ω))) ^ 2 ∂μ := by rw [OperatorSystem.weakNorm, h_T_neg, norm_neg] have : ‖S.qL2 (TC.F_subset hf)‖ ^ 2 = inner ℝ (S.qL2 (TC.F_subset hf)) (S.qL2 (TC.F_subset hf)) := by rw [real_inner_self_eq_norm_sq] rw [this, h_qL2_self] -- Final algebraic close: -- 2·∫m - 2·∫h·f - ∫f² = 2·(∫m - ∫h·f) - ∫f² -- = 2·∫f² - ∫f² = ∫f² = (weakNorm)². rw [h_weak_eq_intf] linarith [h_diff_eq_int_fsq]
EventAssembly 4 core · 1 supporting Assembles the localized empirical-process and centered-regularizer events into the final NPIV primal-rate event. ★ empirical_process_event_from_localized★ empirical_process_event_of_absorption
Assembles the localized empirical-process and centered-regularizer events into the final NPIV primal-rate event. The module exposes the event-level implication used by the headline primal estimator theorem.
theorem empirical_process_event_from_localized reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Discharge of empirical_process_event from localized_uniform_deviation — explicit-rate form. Given a localized-regime bundle for the weak-norm, regularizer, and cross function classes at each fold-A sample size and a nonnegative Tikhonov regularization weight lambda, for every confidence level ζ strictly between 0 and 1 there is an event of probability at least 1 − ζ on which, simultaneously for every n with 1 ≤ split.n₁ n, the weak-norm estimation excess plus lambda times the strong-norm estimation excess is bounded by the sum of the explicit per-n empirical-process rate and the explicit per-n centred-regularizer rate — each an additive combination of critical radii and a √(log/n) deviation term.
Formal statement
hypotheses
S :
split :
OneShotSplit sample
lambda β :
ℝ
delta :
ℕ → ℝ
h_hat :
ℕ → Ω → S.𝒳 → ℝ
IsTRAEPrimalEstimator S TC sample split lambda h_hat
sc :
SourceCondition S β
tb :
TikhonovBiasBound S β lambda sc
regimes :
∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n)
lambda_nonneg :
0 ≤ lambda
conclusion
∀ ζ : ℝ,
0 < ζ → ζ < 1 → ∃ Aζ : Set Ω, MeasurableSet Aζ ∧ μ Aζ
≥ 1 - ofReal ζ ∧
∀ ω ∈ Aζ,
∀ n : ℕ,
1
≤ split.n₁ n → (S.weakNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n ω)) - S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2
+ lambda * ((S.strongNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n ω)))) ^ 2 - (S.strongNorm (S.hL2 tb.h_lambda_star_mem)) ^ 2)
≤ (16 * delta n * criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n)) + 16 * delta n * criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n)) + 8 * delta n * criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n)) + (4 * (regimes n).bundle_HF.regime.b + 4 * (regimes n).bundle_mF.regime.b + 2 * (regimes n).bundle_F.regime.b) * sqrt (2 * log (8 * (2 : ℝ) ^ (n + 1) / ζ) / (split.n₁ n)))
+ lambda * (4 * ((regimes n).H_diameter + delta n) * criticalRadius ((regimes n).bundle_H.regime.ψ (split.n₁ n)) + (regimes n).bundle_H.regime.b * sqrt (2 * log ((2 : ℝ) ^ (n + 2) / ζ) / (split.n₁ n)))
Proof (Lean source)
theorem empirical_process_event_from_localized
{S : OperatorSystem Ω μ} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
{split : OneShotSplit sample}
{lambda β : ℝ} {delta : ℕ → ℝ}
{h_hat : ℕ → Ω → S.𝒳 → ℝ}
{is_estimator : IsTRAEPrimalEstimator S TC sample split lambda h_hat}
(sc : SourceCondition S β)
(tb : TikhonovBiasBound S β lambda sc)
[IsProbabilityMeasure μ]
(regimes : ∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n))
(lambda_nonneg : 0 ≤ lambda) :
∀ ζ : ℝ, 0 < ζ → ζ < 1 →
∃ Aζ : Set Ω,
MeasurableSet Aζ ∧ μ Aζ ≥ 1 - ofReal ζ ∧
∀ ω ∈ Aζ, ∀ n : ℕ, 1 ≤ split.n₁ n →
(S.weakNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n ω))
- S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm
(S.hL2 tb.h_lambda_star_mem
- S.hL2 S.h₀_mem)) ^ 2
+ lambda *
((S.strongNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n ω)))) ^ 2
- (S.strongNorm
(S.hL2 tb.h_lambda_star_mem)) ^ 2)
≤
-- D-side raw explicit rate (EP step, before absorption).
(16 * delta n *
criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n))
+ 16 * delta n *
criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n))
+ 8 * delta n *
criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n))
+ (4 * (regimes n).bundle_HF.regime.b
+ 4 * (regimes n).bundle_mF.regime.b
+ 2 * (regimes n).bundle_F.regime.b) *
sqrt
(2 * log (8 * (2 : ℝ) ^ (n + 1) / ζ)
/ (split.n₁ n)))
-- C-side rate (centred regulariser).
+ lambda *
(4 * ((regimes n).H_diameter + delta n) *
criticalRadius ((regimes n).bundle_H.regime.ψ (split.n₁ n))
+ (regimes n).bundle_H.regime.b *
sqrt
(2 * log ((2 : ℝ) ^ (n + 2) / ζ)
/ (split.n₁ n))) := by
-- Proof: combine `ep_inequality_from_localized` (D) and
-- `centred_regulariser_bound_from_localized` (C) at confidence `ζ/2`
-- each. Splitting `ζ → ζ/2` per side doubles the inner argument of
-- the log: D-side `log(4·2^(n+1)/(ζ/2)) = log(8·2^(n+1)/ζ)`, C-side
-- `log(2^(n+1)/(ζ/2)) = log(2^(n+2)/ζ)`. Intersection of the two
-- events has mass `≥ 1 - ζ/2 - ζ/2 = 1 - ζ`.
intro ζ hζ_pos hζ_lt
have hζ_half_pos : 0 < ζ / 2 := by linarith
have hζ_half_lt : ζ / 2 < 1 := by linarith
obtain ⟨Aζ_ep, hAζ_ep_meas, hAζ_ep_mass, hAζ_ep_bound⟩ :=
ep_inequality_from_localized (h_hat := h_hat) (is_estimator := is_estimator)
sc tb regimes hζ_half_pos hζ_half_lt
obtain ⟨Aζ_reg, hAζ_reg_meas, hAζ_reg_mass, hAζ_reg_bound⟩ :=
centred_regulariser_bound_from_localized (h_hat := h_hat)
(is_estimator := is_estimator) sc tb regimes lambda_nonneg hζ_half_pos
hζ_half_lt
refine ⟨Aζ_ep ∩ Aζ_reg, hAζ_ep_meas.inter hAζ_reg_meas, ?_, ?_⟩
· have hhalf_nonneg : 0 ≤ ζ / 2 := by linarith
have hmass :=
measure_inter_ge_one_sub_add_of_ge hAζ_ep_meas hAζ_reg_meas
hAζ_ep_mass hAζ_reg_mass
simpa [← ENNReal.ofReal_add hhalf_nonneg hhalf_nonneg, add_halves] using hmass
· intro ω hω n hn
rcases hω with ⟨hω_ep, hω_reg⟩
have hlog_ep : 4 * (2 : ℝ) ^ (n + 1) / (ζ / 2) =
8 * (2 : ℝ) ^ (n + 1) / ζ := by
field_simp [ne_of_gt hζ_pos]
ring
have hlog_reg : (2 : ℝ) ^ (n + 1) / (ζ / 2) =
(2 : ℝ) ^ (n + 2) / ζ := by
field_simp [ne_of_gt hζ_pos]
rw [pow_succ]
ring
have hD := hAζ_ep_bound ω hω_ep n hn
rw [hlog_ep] at hD
have hC_abs := hAζ_reg_bound ω hω_reg n hn
rw [hlog_reg] at hC_abs
have hC_upper := (le_abs_self _).trans hC_abs
nlinarith [hD, hC_upper]
def explicitRate reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Per-n explicit rate appearing on the RHS of empirical_process_event_from_localized, packaged as a function of (ω, n, ζ) for use as the LHS of the absorption hypothesis below.
Definition (Lean source)
noncomputable def explicitRate
{S : OperatorSystem Ω μ} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
{split : OneShotSplit sample}
{lambda β : ℝ} {delta : ℕ → ℝ}
{h_hat : ℕ → Ω → S.𝒳 → ℝ}
{sc : SourceCondition S β}
{tb : TikhonovBiasBound S β lambda sc}
(regimes : ∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n))
(_is_estimator : IsTRAEPrimalEstimator S TC sample split lambda h_hat)
(_ω : Ω) (n : ℕ) (ζ : ℝ) : ℝ :=
(16 * delta n *
criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n))
+ 16 * delta n *
criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n))
+ 8 * delta n *
criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n))
+ (4 * (regimes n).bundle_HF.regime.b
+ 4 * (regimes n).bundle_mF.regime.b
+ 2 * (regimes n).bundle_F.regime.b) *
sqrt
(2 * log (8 * (2 : ℝ) ^ (n + 1) / ζ) / (split.n₁ n)))
+ lambda *
(4 * ((regimes n).H_diameter + delta n) *
criticalRadius ((regimes n).bundle_H.regime.ψ (split.n₁ n))
+ (regimes n).bundle_H.regime.b *
sqrt
(2 * log ((2 : ℝ) ^ (n + 2) / ζ)
/ (split.n₁ n)))
def populationShape reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Population shape appearing on the RHS of TRAERatePrimalAbstractHyps.empirical_process_event (Rate.lean, line 167):
Definition (Lean source)
noncomputable def populationShape
{S : OperatorSystem Ω μ} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
{split : OneShotSplit sample}
{lambda β : ℝ} {delta : ℕ → ℝ}
{h_hat : ℕ → Ω → S.𝒳 → ℝ}
{sc : SourceCondition S β}
{tb : TikhonovBiasBound S β lambda sc}
(is_estimator : IsTRAEPrimalEstimator S TC sample split lambda h_hat)
(ω : Ω) (n : ℕ) : ℝ :=
(S.weakNorm
(S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2
+ delta n *
S.weakNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n ω))
- S.hL2 tb.h_lambda_star_mem)
+ (delta n) ^ 2
+ lambda * delta n *
S.strongNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n ω))
- S.hL2 tb.h_lambda_star_mem)
+ lambda * (delta n) ^ 2
theorem empirical_process_event_of_absorption reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Empirical-process event in the Rate.lean shape, conditional on absorption. Given a localized-regime bundle for the weak-norm, regularizer, and cross classes at each fold-A sample size, a nonnegative regularization weight lambda, an absorption hypothesis providing, for every confidence level ζ in (0, 1), a nonnegative constant K_ep bounding the explicit per-n empirical-process rate by K_ep times the population shape R² + δ_n·y + δ_n² + λ·δ_n·x + λ·δ_n², for every ω and every n with 1 ≤ split.n₁ n, and a small-n slack hypothesis extending the same K_ep-domination, for every set Aζ and every nonnegative K_ep, to every n with split.n₁ n = 0 and every ω ∈ Aζ, then for every confidence level ζ in (0, 1) there is an event of probability at least 1 − ζ and a nonnegative constant K_ep such that, for every ω in the event and every n, the weak-norm estimation excess plus lambda times the strong-norm estimation excess is bounded by K_ep times the population shape.
Formal statement
hypotheses
S :
split :
OneShotSplit sample
lambda β :
ℝ
delta :
ℕ → ℝ
h_hat :
ℕ → Ω → S.𝒳 → ℝ
IsTRAEPrimalEstimator S TC sample split lambda h_hat
sc :
SourceCondition S β
tb :
TikhonovBiasBound S β lambda sc
regimes :
∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n)
lambda_nonneg :
0 ≤ lambda
**Absorption hypothesis.** A uniform-in-`n` constant `K_ep ≥ 0`
(depending on `ζ`) such that the explicit per-`n` rate is bounded
by `K_ep` times the population shape, on every `(ω, n)` with
`1 ≤ split.n₁ n`.
absorption :
∀ ζ : ℝ,
0 < ζ → ζ < 1 → ∃ K_ep : ℝ, 0
≤ K_ep ∧
∀ ω : Ω,
∀ n : ℕ,
1
≤ split.n₁ n → explicitRate regimes is_estimator ω n ζ ≤ K_ep * populationShape (lambda := lambda) (delta := delta) (tb := tb) is_estimator ω n
**Small-`n` slack.** The `Rate.lean` field quantifies over all
`n : ℕ` (including `n` for which `split.n₁ n = 0`). We absorb
the small-`n` cases into the same `K_ep` via this hypothesis,
which the caller typically discharges using `split.grow` and a
finite-set bound.
small_n_slack :
∀ ζ : ℝ,
0 < ζ → ζ < 1 → ∀ Aζ : Set Ω, ∀ K_ep : ℝ, 0
≤ K_ep → ∀ ω ∈ Aζ, ∀ n : ℕ, ¬ 1 ≤ split.n₁ n → (S.weakNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n ω)) - S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2
+ lambda * ((S.strongNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n ω)))) ^ 2 - (S.strongNorm (S.hL2 tb.h_lambda_star_mem)) ^ 2)
≤ K_ep * populationShape (lambda := lambda) (delta := delta) (tb := tb) is_estimator ω n
conclusion
∀ ζ : ℝ
if
0 < ζ
and
ζ < 1
then
∃ Aζ : Set Ω,
∃ K_ep : ℝ,
MeasurableSet Aζ ∧
μ Aζ ≥ 1 - ofReal ζ ∧
0 ≤ K_ep ∧
∀ ω ∈ Aζ,
∀ n : ℕ,
(S.weakNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n ω)) - S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2
+ lambda * ((S.strongNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n ω)))) ^ 2 - (S.strongNorm (S.hL2 tb.h_lambda_star_mem)) ^ 2)
≤ K_ep * populationShape (lambda := lambda) (delta := delta) (tb := tb) is_estimator ω n
Proof (Lean source)
theorem empirical_process_event_of_absorption
{S : OperatorSystem Ω μ} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
{split : OneShotSplit sample}
{lambda β : ℝ} {delta : ℕ → ℝ}
{h_hat : ℕ → Ω → S.𝒳 → ℝ}
{is_estimator : IsTRAEPrimalEstimator S TC sample split lambda h_hat}
(sc : SourceCondition S β)
(tb : TikhonovBiasBound S β lambda sc)
[IsProbabilityMeasure μ]
(regimes : ∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n))
(lambda_nonneg : 0 ≤ lambda)
/- **Absorption hypothesis.** A uniform-in-`n` constant `K_ep ≥ 0`
(depending on `ζ`) such that the explicit per-`n` rate is bounded
by `K_ep` times the population shape, on every `(ω, n)` with
`1 ≤ split.n₁ n`. -/
(absorption :
∀ ζ : ℝ, 0 < ζ → ζ < 1 →
∃ K_ep : ℝ, 0 ≤ K_ep ∧
∀ ω : Ω, ∀ n : ℕ, 1 ≤ split.n₁ n →
explicitRate regimes is_estimator ω n ζ
≤ K_ep * populationShape (lambda := lambda) (delta := delta)
(tb := tb) is_estimator ω n)
/- **Small-`n` slack.** The `Rate.lean` field quantifies over all
`n : ℕ` (including `n` for which `split.n₁ n = 0`). We absorb
the small-`n` cases into the same `K_ep` via this hypothesis,
which the caller typically discharges using `split.grow` and a
finite-set bound. -/
(small_n_slack :
∀ ζ : ℝ, 0 < ζ → ζ < 1 → ∀ Aζ : Set Ω, ∀ K_ep : ℝ, 0 ≤ K_ep →
∀ ω ∈ Aζ, ∀ n : ℕ, ¬ 1 ≤ split.n₁ n →
(S.weakNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n ω))
- S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm
(S.hL2 tb.h_lambda_star_mem
- S.hL2 S.h₀_mem)) ^ 2
+ lambda *
((S.strongNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n ω)))) ^ 2
- (S.strongNorm
(S.hL2 tb.h_lambda_star_mem)) ^ 2)
≤ K_ep *
populationShape (lambda := lambda) (delta := delta)
(tb := tb) is_estimator ω n) :
∀ ζ : ℝ, 0 < ζ → ζ < 1 →
∃ Aζ : Set Ω, ∃ K_ep : ℝ,
MeasurableSet Aζ ∧ μ Aζ ≥ 1 - ofReal ζ ∧ 0 ≤ K_ep ∧
∀ ω ∈ Aζ, ∀ n : ℕ,
(S.weakNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n ω))
- S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm
(S.hL2 tb.h_lambda_star_mem
- S.hL2 S.h₀_mem)) ^ 2
+ lambda *
((S.strongNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n ω)))) ^ 2
- (S.strongNorm
(S.hL2 tb.h_lambda_star_mem)) ^ 2)
≤ K_ep *
populationShape (lambda := lambda) (delta := delta)
(tb := tb) is_estimator ω n := by
-- Proof: combine `empirical_process_event_from_localized` with the
-- `absorption` and `small_n_slack` hypotheses. The Aζ event and
-- K_ep are taken from those hypotheses; the per-`ω, n` inequality
-- splits on `1 ≤ split.n₁ n`.
intro ζ hζ_pos hζ_lt
obtain ⟨Aζ, hAζ_meas, hAζ_mass, hAζ_bound⟩ :=
empirical_process_event_from_localized
(is_estimator := is_estimator) sc tb regimes lambda_nonneg ζ hζ_pos hζ_lt
obtain ⟨K_ep, hK_nonneg, hK_bound⟩ := absorption ζ hζ_pos hζ_lt
refine ⟨Aζ, K_ep, hAζ_meas, hAζ_mass, hK_nonneg, ?_⟩
intro ω hω n
rcases em (1 ≤ split.n₁ n) with hn | hn
· have hlocalized := hAζ_bound ω hω n hn
have habsorbed :
explicitRate regimes is_estimator ω n ζ
≤ K_ep *
populationShape (lambda := lambda) (delta := delta)
(tb := tb) is_estimator ω n :=
hK_bound ω n hn
exact hlocalized.trans (by simpa [explicitRate] using habsorbed)
· exact small_n_slack ζ hζ_pos hζ_lt Aζ K_ep hK_nonneg ω hω n hn
1 supporting declaration (lemmas, instances)
-
measure_inter_ge_one_sub_add_of_gelemma — The intersection of two high-probability events has probability at least one minus the sum of their two failure probabilities.hypothesesconclusionμ (A ∩ B) ≥ 1 - (a + b)Proof (Lean source)
lemma measure_inter_ge_one_sub_add_of_ge [IsProbabilityMeasure μ] {A B : Set Ω} {a b : ENNReal} (hA_meas : MeasurableSet A) (hB_meas : MeasurableSet B) (hA : μ A ≥ 1 - a) (hB : μ B ≥ 1 - b) : μ (A ∩ B) ≥ 1 - (a + b) := by have hA_compl : μ Aᶜ ≤ a := by have hone_le : (1 : ENNReal) ≤ a + μ A := tsub_le_iff_left.mp hA rw [measure_compl hA_meas (measure_ne_top _ _), measure_univ] exact tsub_le_iff_right.mpr (by simpa [add_comm] using hone_le) have hB_compl : μ Bᶜ ≤ b := by have hone_le : (1 : ENNReal) ≤ b + μ B := tsub_le_iff_left.mp hB rw [measure_compl hB_meas (measure_ne_top _ _), measure_univ] exact tsub_le_iff_right.mpr (by simpa [add_comm] using hone_le) have hbad_le : μ (A ∩ B)ᶜ ≤ a + b := by rw [Set.compl_inter] exact (measure_union_le Aᶜ Bᶜ).trans (add_le_add hA_compl hB_compl) have hAB_meas : MeasurableSet (A ∩ B) := hA_meas.inter hB_meas rw [measure_compl hAB_meas (measure_ne_top _ _), measure_univ] at hbad_le have hone_le : (1 : ENNReal) ≤ (a + b) + μ (A ∩ B) := tsub_le_iff_right.mp hbad_le exact tsub_le_iff_left.mpr hone_le
LocalizedEventF 1 core · 2 supporting This file constructs high-probability sample-space events that control the empirical fluctuation of squared critic functions in the primal NPIV analysis. ★ localized_omega_event_for_F_pair_peeled
Localized Deviation for the Critic Class F
This file constructs high-probability sample-space events that control the
empirical fluctuation of squared critic functions in the primal NPIV analysis.
Here F is the critic/test-function class TC.F; the event is pulled back from
the product sample law to the underlying probability space used by the
estimator.
lemma localized_omega_event_for_F_pair_peeled reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Peeled pair-form localized deviation event for the squared critic class star(F). Given a positive sample size n and a confidence level δ in (0, 1], there is a single event of probability at least 1 − δ, valid simultaneously for every pair f₁, f₂ in the critic class TC.F, on which the gap between the empirical and population second-moment differences of f₁ and f₂ is bounded by 8 · F_L2_const · ‖f₁ − f₂‖_strong · δ_n + 5 · δ_n², where the strong norm is taken in the critic's L² embedding and F_L2_const comes from the supplied localized-regime witness.
Formal statement
hypotheses
S :
β lambda :
n :
ℕ
δ_n :
ℝ
regime :
LocalizedRegimes S TC sample sc tb n δ_n
hn :
0 < n
δ :
ℝ
hδ_pos :
0 < δ
hδ_le :
δ ≤ 1
conclusion
∃ E : Set Ω,
MeasurableSet E ∧
μ E ≥ 1 - ofReal δ ∧
∀ ω ∈ E,
∀ f₁,
∀ hf₁ : f₁ ∈ TC.F,
∀ f₂,
∀ hf₂ : f₂ ∈ TC.F,
|(n : ℝ)⁻¹ * ∑ k : Fin n, ((f₁ (S.zOf (sample.Z k ω))) ^ 2 - (f₂ (S.zOf (sample.Z k ω))) ^ 2)
- ∫ ω', ((f₁ (S.zOf (S.W ω'))) ^ 2 - (f₂ (S.zOf (S.W ω'))) ^ 2) ∂μ|
≤ 8 * regime.F_L2_const * S.strongNorm (S.qL2 (TC.F_subset hf₁) - S.qL2 (TC.F_subset hf₂)) * δ_n
+ 5 * δ_n ^ 2
Proof (Lean source)
lemma localized_omega_event_for_F_pair_peeled
{S : OperatorSystem Ω μ} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
[IsProbabilityMeasure μ]
{β lambda : ℝ}
{sc : SourceCondition S β}
{tb : TikhonovBiasBound S β lambda sc}
{n : ℕ} {δ_n : ℝ}
(regime : LocalizedRegimes S TC sample sc tb n δ_n)
(hn : 0 < n)
{δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) :
∃ E : Set Ω,
MeasurableSet E ∧ μ E ≥ 1 - ofReal δ ∧
∀ ω ∈ E, ∀ f₁, ∀ hf₁ : f₁ ∈ TC.F, ∀ f₂, ∀ hf₂ : f₂ ∈ TC.F,
|(n : ℝ)⁻¹ * ∑ k : Fin n,
((f₁ (S.zOf (sample.Z k ω))) ^ 2
- (f₂ (S.zOf (sample.Z k ω))) ^ 2)
- ∫ ω',
((f₁ (S.zOf (S.W ω'))) ^ 2
- (f₂ (S.zOf (S.W ω'))) ^ 2) ∂μ|
≤ 8 * regime.F_L2_const *
S.strongNorm
(S.qL2 (TC.F_subset hf₁) - S.qL2 (TC.F_subset hf₂)) *
δ_n
+ 5 * δ_n ^ 2 := by
classical
let B := regime.bundle_F
let Rmax : ℝ := max δ_n (regime.F_L2_const * regime.F_diameter)
have hδn_pos : 0 < δ_n := lt_of_lt_of_le B.crit_pos B.crit_le
have hδn_nonneg : 0 ≤ δ_n := le_of_lt hδn_pos
have hRmax_lb : δ_n ≤ Rmax := by
exact le_max_left _ _
have hslack : ∀ K : ℕ,
Rmax ≤ δ_n * (2 : ℝ) ^ K →
B.regime.b * sqrt
(2 * log (2 * ((K : ℝ) + 1) / δ) / n)
≤ δ_n ^ 2 := by
intro K hK
have htop : regime.F_L2_const * regime.F_diameter
≤ δ_n * (2 : ℝ) ^ K := by
exact (le_max_right _ _).trans hK
simpa [B] using regime.peeling_slack_F K δ hδ_pos hδ_le hn htop
obtain ⟨E, hE_meas, hE_prob, hE_bound⟩ :=
localized_omega_event_sharp_for_bundle
(S := S) (P_W := P_W) (sample := sample) (B := B)
regime.law_W hn hδ_pos hδ_le hδn_pos hRmax_lb hslack
refine ⟨E, hE_meas, hE_prob, ?_⟩
intro ω hω f₁ hf₁ f₂ hf₂
let i : B.ι := regime.interp_F_idx_pair f₁ f₂ hf₁ hf₂
let gap : ℝ :=
S.strongNorm (S.qL2 (TC.F_subset hf₁) - S.qL2 (TC.F_subset hf₂))
have hgap_top : gap ≤ regime.F_diameter := by
simpa [gap] using regime.F_diameter_bound f₁ f₂ hf₁ hf₂
have hi_gap : B.norm (B.F i) ≤ regime.F_L2_const * gap := by
simpa [B, i, gap] using regime.interp_F_norm_pair f₁ f₂ hf₁ hf₂
have hi_diam : B.norm (B.F i) ≤ Rmax := by
have htop : regime.F_L2_const * gap
≤ regime.F_L2_const * regime.F_diameter :=
mul_le_mul_of_nonneg_left hgap_top regime.F_L2_const_nonneg
exact hi_gap.trans (htop.trans (le_max_right _ _))
have hdev := hE_bound ω hω i hi_diam
have heval_sample :
(Finset.univ.sum fun k : Fin n => B.F i (B.X (sample.Z k ω))) =
∑ k : Fin n,
((f₁ (S.zOf (sample.Z k ω))) ^ 2
- (f₂ (S.zOf (sample.Z k ω))) ^ 2) := by
apply Finset.sum_congr rfl
intro k _
simpa [B, i] using regime.interp_F_eval_pair f₁ f₂ hf₁ hf₂ (sample.Z k ω)
have heval_pop :
(fun ω' => B.F i (B.X (S.W ω'))) =
fun ω' =>
(f₁ (S.zOf (S.W ω'))) ^ 2 - (f₂ (S.zOf (S.W ω'))) ^ 2 := by
funext ω'
simpa [B, i] using regime.interp_F_eval_pair f₁ f₂ hf₁ hf₂ (S.W ω')
have hdev_concrete :
|(n : ℝ)⁻¹ * ∑ k : Fin n,
((f₁ (S.zOf (sample.Z k ω))) ^ 2
- (f₂ (S.zOf (sample.Z k ω))) ^ 2)
- ∫ ω',
((f₁ (S.zOf (S.W ω'))) ^ 2
- (f₂ (S.zOf (S.W ω'))) ^ 2) ∂μ|
≤ 8 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2 := by
simpa [B, i, heval_sample, heval_pop] using hdev
have hrate :
8 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2
≤ 8 * regime.F_L2_const * gap * δ_n + 5 * δ_n ^ 2 := by
have hlead := mul_le_mul_of_nonneg_left hi_gap
(by nlinarith [hδn_nonneg] : 0 ≤ 8 * δ_n)
nlinarith
simpa [gap, mul_assoc, mul_comm, mul_left_comm] using hdev_concrete.trans hrate
2 supporting declarations (lemmas, instances)
-
localized_omega_event_for_Flemma — Ω-side localized deviation event for the critic class star(F) — controls |(1/n) Σ f(Z_i)² − E[f(Z)²]| uniformly over f ∈ TC.F.hypothesesS :β lambda :n :ℕδ_n :ℝregime :LocalizedRegimes S TC sample sc tb n δ_nhn :0 < nδ :ℝhδ_pos :0 < δhδ_le :δ ≤ 1conclusion∃ E : Set Ω,MeasurableSet E ∧μ E ≥ 1 - ofReal δ ∧∀ ω ∈ E,∀ f ∈ TC.F,|(n : ℝ)⁻¹ * ∑ k : Fin n, (f (S.zOf (sample.Z k ω))) ^ 2- ∫ ω', (f (S.zOf (S.W ω'))) ^ 2 ∂μ|≤ 4 * δ_n * criticalRadius (regime.bundle_F.regime.ψ n)Proof (Lean source)
lemma localized_omega_event_for_F {S : OperatorSystem Ω μ} {TC : TRAEClasses S} {P_W : Measure S.𝒲} {sample : IIDSample Ω S.𝒲 μ P_W} [IsProbabilityMeasure μ] {β lambda : ℝ} {sc : SourceCondition S β} {tb : TikhonovBiasBound S β lambda sc} {n : ℕ} {δ_n : ℝ} (regime : LocalizedRegimes S TC sample sc tb n δ_n) (hn : 0 < n) {δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) : ∃ E : Set Ω, MeasurableSet E ∧ μ E ≥ 1 - ofReal δ ∧ ∀ ω ∈ E, ∀ f ∈ TC.F, |(n : ℝ)⁻¹ * ∑ k : Fin n, (f (S.zOf (sample.Z k ω))) ^ 2 - ∫ ω', (f (S.zOf (S.W ω'))) ^ 2 ∂μ| ≤ 4 * δ_n * criticalRadius (regime.bundle_F.regime.ψ n) + regime.bundle_F.regime.b * sqrt (2 * log (1 / δ) / n) := by classical let B := regime.bundle_F haveI : IsProbabilityMeasure P_W := by rw [← regime.law_W] exact Measure.isProbabilityMeasure_map S.meas_W.aemeasurable obtain ⟨E₀, hE₀_meas, hE₀_prob, hE₀_bound⟩ := localized_uniform_deviation B.F B.norm P_W B.X B.X_meas B.F_meas B.regime hδ_pos hδ_le n hn B.crit_le B.crit_pos B.crit_fp (B.rad_bdd δ_n le_rfl) (B.rad_int δ_n le_rfl) let Ψ : Ω → (Fin n → S.𝒲) := fun ω k => sample.Z k ω let E : Set Ω := Ψ ⁻¹' E₀ have hpull := event_pullback_along_iidSample sample n hE₀_meas hE₀_prob refine ⟨E, ?_, ?_, ?_⟩ · simpa [E, Ψ] using hpull.1 · simpa [E, Ψ] using hpull.2 · intro ω hω f hf let i : B.ι := regime.interp_F_idx f hf have hω₀ : Ψ ω ∈ E₀ := by simpa [E, Ψ] using hω have hi_norm : B.norm (B.F i) ≤ δ_n := by simpa [B, i] using regime.interp_F_norm f hf have hdev := hE₀_bound (Ψ ω) hω₀ i hi_norm have hpop : ∫ w, B.F i (B.X w) ∂P_W = ∫ ω', B.F i (B.X (S.W ω')) ∂μ := by exact integral_comp_law_W regime.law_W ((B.F_meas i).comp B.X_meas) have heval_sample : (Finset.univ.sum fun k : Fin n => B.F i (B.X (sample.Z k ω))) = ∑ k : Fin n, (f (S.zOf (sample.Z k ω))) ^ 2 := by apply Finset.sum_congr rfl intro k _ simpa [B, i] using regime.interp_F_eval f hf (sample.Z k ω) have heval_pop : (fun ω' => B.F i (B.X (S.W ω'))) = fun ω' => (f (S.zOf (S.W ω'))) ^ 2 := by funext ω' simpa [B, i] using regime.interp_F_eval f hf (S.W ω') simpa [Ψ, hpop, heval_sample, heval_pop] using hdev -
localized_omega_event_for_F_pairlemma — Ω-side fixed-diameter pair-form localized deviation event for the squared critic class star(F). This is the non-peeled building block for the Foster pair-gap bridge.hypothesesS :β lambda :n :ℕδ_n :ℝregime :LocalizedRegimes S TC sample sc tb n δ_nhn :0 < nδ :ℝhδ_pos :0 < δhδ_le :δ ≤ 1conclusion∃ E : Set Ω,MeasurableSet E ∧μ E ≥ 1 - ofReal δ ∧∀ ω ∈ E,∀ f₁,∀ _hf₁ : f₁ ∈ TC.F,∀ f₂,∀ _hf₂ : f₂ ∈ TC.F,|(n : ℝ)⁻¹ * ∑ k : Fin n, ((f₁ (S.zOf (sample.Z k ω))) ^ 2 - (f₂ (S.zOf (sample.Z k ω))) ^ 2)- ∫ ω', ((f₁ (S.zOf (S.W ω'))) ^ 2 - (f₂ (S.zOf (S.W ω'))) ^ 2) ∂μ|≤ 4 * (regime.F_L2_const * regime.F_diameter) * criticalRadius (regime.bundle_F.regime.ψ n)Proof (Lean source)
lemma localized_omega_event_for_F_pair {S : OperatorSystem Ω μ} {TC : TRAEClasses S} {P_W : Measure S.𝒲} {sample : IIDSample Ω S.𝒲 μ P_W} [IsProbabilityMeasure μ] {β lambda : ℝ} {sc : SourceCondition S β} {tb : TikhonovBiasBound S β lambda sc} {n : ℕ} {δ_n : ℝ} (regime : LocalizedRegimes S TC sample sc tb n δ_n) (hn : 0 < n) {δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) : ∃ E : Set Ω, MeasurableSet E ∧ μ E ≥ 1 - ofReal δ ∧ ∀ ω ∈ E, ∀ f₁, ∀ _hf₁ : f₁ ∈ TC.F, ∀ f₂, ∀ _hf₂ : f₂ ∈ TC.F, |(n : ℝ)⁻¹ * ∑ k : Fin n, ((f₁ (S.zOf (sample.Z k ω))) ^ 2 - (f₂ (S.zOf (sample.Z k ω))) ^ 2) - ∫ ω', ((f₁ (S.zOf (S.W ω'))) ^ 2 - (f₂ (S.zOf (S.W ω'))) ^ 2) ∂μ| ≤ 4 * (regime.F_L2_const * regime.F_diameter) * criticalRadius (regime.bundle_F.regime.ψ n) + regime.bundle_F.regime.b * sqrt (2 * log (1 / δ) / n) := by classical let B := regime.bundle_F let r : ℝ := regime.F_L2_const * regime.F_diameter haveI : IsProbabilityMeasure P_W := by rw [← regime.law_W] exact Measure.isProbabilityMeasure_map S.meas_W.aemeasurable have hr_delta : δ_n ≤ r := by simpa [r] using regime.F_pair_radius_lb have hr_lb : criticalRadius (B.regime.ψ n) ≤ r := B.crit_le.trans hr_delta obtain ⟨E₀, hE₀_meas, hE₀_prob, hE₀_bound⟩ := localized_uniform_deviation B.F B.norm P_W B.X B.X_meas B.F_meas B.regime hδ_pos hδ_le n hn hr_lb B.crit_pos B.crit_fp (B.rad_bdd r hr_delta) (B.rad_int r hr_delta) let Ψ : Ω → (Fin n → S.𝒲) := fun ω k => sample.Z k ω let E : Set Ω := Ψ ⁻¹' E₀ have hpull := event_pullback_along_iidSample sample n hE₀_meas hE₀_prob refine ⟨E, ?_, ?_, ?_⟩ · simpa [E, Ψ] using hpull.1 · simpa [E, Ψ] using hpull.2 · intro ω hω f₁ hf₁ f₂ hf₂ let i : B.ι := regime.interp_F_idx_pair f₁ f₂ hf₁ hf₂ have hω₀ : Ψ ω ∈ E₀ := by simpa [E, Ψ] using hω have hpair : S.strongNorm (S.qL2 (TC.F_subset hf₁) - S.qL2 (TC.F_subset hf₂)) ≤ regime.F_diameter := regime.F_diameter_bound f₁ f₂ hf₁ hf₂ have hi_norm : B.norm (B.F i) ≤ r := by exact (regime.interp_F_norm_pair f₁ f₂ hf₁ hf₂).trans (mul_le_mul_of_nonneg_left hpair regime.F_L2_const_nonneg) have hdev := hE₀_bound (Ψ ω) hω₀ i hi_norm have hpop : ∫ w, B.F i (B.X w) ∂P_W = ∫ ω', B.F i (B.X (S.W ω')) ∂μ := by exact integral_comp_law_W regime.law_W ((B.F_meas i).comp B.X_meas) have heval_sample : (Finset.univ.sum fun k : Fin n => B.F i (B.X (sample.Z k ω))) = ∑ k : Fin n, ((f₁ (S.zOf (sample.Z k ω))) ^ 2 - (f₂ (S.zOf (sample.Z k ω))) ^ 2) := by apply Finset.sum_congr rfl intro k _ simpa [B, i] using regime.interp_F_eval_pair f₁ f₂ hf₁ hf₂ (sample.Z k ω) have heval_pop : (fun ω' => B.F i (B.X (S.W ω'))) = fun ω' => (f₁ (S.zOf (S.W ω'))) ^ 2 - (f₂ (S.zOf (S.W ω'))) ^ 2 := by funext ω' simpa [B, i] using regime.interp_F_eval_pair f₁ f₂ hf₁ hf₂ (S.W ω') simpa [Ψ, r, hpop, heval_sample, heval_pop] using hdev
LocalizedEventH 1 core · 0 supporting This file constructs high-probability events controlling empirical fluctuations over pairs of candidate primal functions in the NPIV primal rate argument. ★ localized_omega_event_for_H
Localized Deviation for the Primal Class H
This file constructs high-probability events controlling empirical fluctuations
over pairs of candidate primal functions in the NPIV primal rate argument. Here
H is the primal hypothesis class TC.H. The event is one component of the
localized empirical-process control needed for the Tikhonov-regularized
adversarial estimator.
lemma localized_omega_event_for_H reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Fixed-diameter localized deviation event for the candidate class star(H). Given a positive sample size n and a confidence level δ in (0, 1], there is a single event of probability at least 1 − δ, valid simultaneously for every pair h₁, h₂ in the primal hypothesis class TC.H, on which the gap between the fold's empirical second-moment difference (1/n) Σ_k h₁(X_k)² − (1/n) Σ_k h₂(X_k)² and its population counterpart E[h₁(X)²] − E[h₂(X)²] is bounded by 4 · (H_diameter + δ_n) · criticalRadius(ψ n) plus a √(2·log(1/δ)/n) deviation term, where H_diameter and the critical-radius regime come from the supplied localized-regime witness.
Formal statement
hypotheses
S :
β lambda :
n :
ℕ
δ_n :
ℝ
regime :
LocalizedRegimes S TC sample sc tb n δ_n
hn :
0 < n
δ :
ℝ
hδ_pos :
0 < δ
hδ_le :
δ ≤ 1
conclusion
∃ E : Set Ω,
MeasurableSet E ∧
μ E ≥ 1 - ofReal δ ∧
∀ ω ∈ E,
∀ h₁,
∀ _hh₁ : h₁ ∈ TC.H,
∀ h₂,
∀ _hh₂ : h₂ ∈ TC.H,
|((n : ℝ)⁻¹ * ∑ k : Fin n, (h₁ (S.xOf (sample.Z k ω))) ^ 2 - (n : ℝ)⁻¹ * ∑ k : Fin n, (h₂ (S.xOf (sample.Z k ω))) ^ 2)
- (∫ ω', (h₁ (S.xOf (S.W ω'))) ^ 2 ∂μ - ∫ ω', (h₂ (S.xOf (S.W ω'))) ^ 2 ∂μ)|
≤ 4 * (regime.H_diameter + δ_n) * criticalRadius (regime.bundle_H.regime.ψ n)
Proof (Lean source)
lemma localized_omega_event_for_H
{S : OperatorSystem Ω μ} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
[IsProbabilityMeasure μ]
{β lambda : ℝ}
{sc : SourceCondition S β}
{tb : TikhonovBiasBound S β lambda sc}
{n : ℕ} {δ_n : ℝ}
(regime : LocalizedRegimes S TC sample sc tb n δ_n)
(hn : 0 < n)
{δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) :
∃ E : Set Ω,
MeasurableSet E ∧ μ E ≥ 1 - ofReal δ ∧
∀ ω ∈ E, ∀ h₁, ∀ _hh₁ : h₁ ∈ TC.H, ∀ h₂, ∀ _hh₂ : h₂ ∈ TC.H,
|((n : ℝ)⁻¹ * ∑ k : Fin n, (h₁ (S.xOf (sample.Z k ω))) ^ 2
- (n : ℝ)⁻¹ * ∑ k : Fin n, (h₂ (S.xOf (sample.Z k ω))) ^ 2)
- (∫ ω', (h₁ (S.xOf (S.W ω'))) ^ 2 ∂μ
- ∫ ω', (h₂ (S.xOf (S.W ω'))) ^ 2 ∂μ)|
≤ 4 * (regime.H_diameter + δ_n) *
criticalRadius (regime.bundle_H.regime.ψ n)
+ regime.bundle_H.regime.b *
sqrt (2 * log (1 / δ) / n) := by
classical
let B := regime.bundle_H
let r : ℝ := regime.H_diameter + δ_n
haveI : IsProbabilityMeasure P_W := by
rw [← regime.law_W]
exact Measure.isProbabilityMeasure_map S.meas_W.aemeasurable
have hδn_pos : 0 < δ_n := lt_of_lt_of_le B.crit_pos B.crit_le
have hδn_nonneg : 0 ≤ δ_n := le_of_lt hδn_pos
have hdiam_nonneg : 0 ≤ regime.H_diameter :=
hδn_nonneg.trans regime.H_diameter_lb
have hr_lb : criticalRadius (B.regime.ψ n) ≤ r := by
dsimp [r]
linarith [B.crit_le, hdiam_nonneg]
have hr_delta : δ_n ≤ r := by
dsimp [r]
linarith [hdiam_nonneg]
obtain ⟨E₀, hE₀_meas, hE₀_prob, hE₀_bound⟩ :=
localized_uniform_deviation B.F B.norm P_W B.X B.X_meas B.F_meas B.regime
hδ_pos hδ_le n hn hr_lb B.crit_pos B.crit_fp
(B.rad_bdd r hr_delta) (B.rad_int r hr_delta)
let Ψ : Ω → (Fin n → S.𝒲) := fun ω k => sample.Z k ω
let E : Set Ω := Ψ ⁻¹' E₀
have hpull :=
event_pullback_along_iidSample sample n hE₀_meas hE₀_prob
refine ⟨E, ?_, ?_, ?_⟩
· simpa [E, Ψ] using hpull.1
· simpa [E, Ψ] using hpull.2
· intro ω hω h₁ hh₁ h₂ hh₂
let i : B.ι := regime.interp_H_idx h₁ h₂ hh₁ hh₂
have hω₀ : Ψ ω ∈ E₀ := by
simpa [E, Ψ] using hω
have hgap_le :
S.strongNorm (S.hL2 (TC.H_subset hh₁) - S.hL2 (TC.H_subset hh₂))
≤ regime.H_diameter :=
regime.H_diameter_bound h₁ h₂ hh₁ hh₂
have hi_norm : B.norm (B.F i) ≤ r := by
have hi_gap := regime.interp_H_norm h₁ h₂ hh₁ hh₂
dsimp [r]
linarith
have hdev := hE₀_bound (Ψ ω) hω₀ i hi_norm
have hpop :
∫ w, B.F i (B.X w) ∂P_W =
∫ ω', B.F i (B.X (S.W ω')) ∂μ := by
exact integral_comp_law_W regime.law_W ((B.F_meas i).comp B.X_meas)
have heval_sample :
(Finset.univ.sum fun k : Fin n => B.F i (B.X (sample.Z k ω))) =
∑ k : Fin n,
((h₁ (S.xOf (sample.Z k ω))) ^ 2
- (h₂ (S.xOf (sample.Z k ω))) ^ 2) := by
apply Finset.sum_congr rfl
intro k _
simpa [B, i] using regime.interp_H_eval h₁ h₂ hh₁ hh₂ (sample.Z k ω)
have heval_pop :
(fun ω' => B.F i (B.X (S.W ω'))) =
fun ω' =>
(h₁ (S.xOf (S.W ω'))) ^ 2 - (h₂ (S.xOf (S.W ω'))) ^ 2 := by
funext ω'
simpa [B, i] using regime.interp_H_eval h₁ h₂ hh₁ hh₂ (S.W ω')
have hsample_split :
(n : ℝ)⁻¹ *
(∑ k : Fin n,
((h₁ (S.xOf (sample.Z k ω))) ^ 2
- (h₂ (S.xOf (sample.Z k ω))) ^ 2))
=
(n : ℝ)⁻¹ * ∑ k : Fin n, (h₁ (S.xOf (sample.Z k ω))) ^ 2
- (n : ℝ)⁻¹ * ∑ k : Fin n, (h₂ (S.xOf (sample.Z k ω))) ^ 2 := by
rw [Finset.sum_sub_distrib, mul_sub]
have hsample_split' :
(n : ℝ)⁻¹ *
((∑ k : Fin n, (h₁ (S.xOf (sample.Z k ω))) ^ 2)
- ∑ k : Fin n, (h₂ (S.xOf (sample.Z k ω))) ^ 2)
=
(n : ℝ)⁻¹ * ∑ k : Fin n, (h₁ (S.xOf (sample.Z k ω))) ^ 2
- (n : ℝ)⁻¹ * ∑ k : Fin n, (h₂ (S.xOf (sample.Z k ω))) ^ 2 := by
ring
have hsq₁_int :
Integrable (fun ω' => (h₁ (S.xOf (S.W ω'))) ^ 2) μ := by
exact (S.toHbarL2 h₁ (TC.H_subset hh₁)).integrable_sq
have hsq₂_int :
Integrable (fun ω' => (h₂ (S.xOf (S.W ω'))) ^ 2) μ := by
exact (S.toHbarL2 h₂ (TC.H_subset hh₂)).integrable_sq
have hpop_split :
(∫ ω',
(h₁ (S.xOf (S.W ω'))) ^ 2 - (h₂ (S.xOf (S.W ω'))) ^ 2 ∂μ)
=
(∫ ω', (h₁ (S.xOf (S.W ω'))) ^ 2 ∂μ)
- ∫ ω', (h₂ (S.xOf (S.W ω'))) ^ 2 ∂μ := by
exact integral_sub hsq₁_int hsq₂_int
simpa [Ψ, r, hpop, heval_sample, heval_pop, hsample_split,
hsample_split', hpop_split]
using hdev
LocalizedEventHF 1 core · 2 supporting This file constructs the high-probability event controlling empirical fluctuations of products of candidate primal functions and critic functions in the primal NPIV analysis. ★ localized_omega_event_for_HF_pair_peeled
Localized Deviation for Products from H and F
This file constructs the high-probability event controlling empirical
fluctuations of products of candidate primal functions and critic functions in
the primal NPIV analysis. Here HF denotes the product class formed from
h ∈ TC.H and f ∈ TC.F; the result supplies the product-class component of
the localized empirical-process event used in the rate proof.
lemma localized_omega_event_for_HF_pair_peeled reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Peeled pair-form localized deviation event for the cross class star(H · F). Given a positive sample size n and a confidence level δ in (0, 1], there is a single event of probability at least 1 − δ, valid simultaneously for every pair h₁, h₂ in the primal class TC.H and every critic f in TC.F, on which the gap between the empirical and population means of (h₁ − h₂) · f is bounded by 8 · HF_pair_const · δ_n² · ‖h₁ − h₂‖_strong + 5 · δ_n², where the strong norm is taken in the primal L² embedding and HF_pair_const comes from the supplied localized-regime witness.
Formal statement
hypotheses
S :
β lambda :
n :
ℕ
δ_n :
ℝ
regime :
LocalizedRegimes S TC sample sc tb n δ_n
hn :
0 < n
δ :
ℝ
hδ_pos :
0 < δ
hδ_le :
δ ≤ 1
conclusion
∃ E : Set Ω,
MeasurableSet E ∧
μ E ≥ 1 - ofReal δ ∧
∀ ω ∈ E,
∀ h₁,
∀ hh₁ : h₁ ∈ TC.H,
∀ h₂,
∀ hh₂ : h₂ ∈ TC.H,
∀ f,
∀ _hf : f ∈ TC.F,
|(n : ℝ)⁻¹ * ∑ k : Fin n, (h₁ (S.xOf (sample.Z k ω)) - h₂ (S.xOf (sample.Z k ω))) * f (S.zOf (sample.Z k ω))
- ∫ ω', (h₁ (S.xOf (S.W ω')) - h₂ (S.xOf (S.W ω'))) * f (S.zOf (S.W ω')) ∂μ|
≤ 8 * regime.HF_pair_const * δ_n ^ 2 * S.strongNorm (S.hL2 (TC.H_subset hh₁) - S.hL2 (TC.H_subset hh₂))
+ 5 * δ_n ^ 2
Proof (Lean source)
lemma localized_omega_event_for_HF_pair_peeled
{S : OperatorSystem Ω μ} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
[IsProbabilityMeasure μ]
{β lambda : ℝ}
{sc : SourceCondition S β}
{tb : TikhonovBiasBound S β lambda sc}
{n : ℕ} {δ_n : ℝ}
(regime : LocalizedRegimes S TC sample sc tb n δ_n)
(hn : 0 < n)
{δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) :
∃ E : Set Ω,
MeasurableSet E ∧ μ E ≥ 1 - ofReal δ ∧
∀ ω ∈ E, ∀ h₁, ∀ hh₁ : h₁ ∈ TC.H, ∀ h₂, ∀ hh₂ : h₂ ∈ TC.H,
∀ f, ∀ _hf : f ∈ TC.F,
|(n : ℝ)⁻¹ * ∑ k : Fin n,
(h₁ (S.xOf (sample.Z k ω)) - h₂ (S.xOf (sample.Z k ω)))
* f (S.zOf (sample.Z k ω))
- ∫ ω',
(h₁ (S.xOf (S.W ω')) - h₂ (S.xOf (S.W ω')))
* f (S.zOf (S.W ω')) ∂μ|
≤ 8 * regime.HF_pair_const * δ_n ^ 2 *
S.strongNorm (S.hL2 (TC.H_subset hh₁) - S.hL2 (TC.H_subset hh₂))
+ 5 * δ_n ^ 2 := by
classical
let B := regime.bundle_HF
let Rmax : ℝ := max δ_n (regime.HF_pair_const * regime.H_diameter * δ_n)
have hδn_pos : 0 < δ_n := lt_of_lt_of_le B.crit_pos B.crit_le
have hδn_nonneg : 0 ≤ δ_n := le_of_lt hδn_pos
have hRmax_lb : δ_n ≤ Rmax := by
exact le_max_left _ _
have hslack : ∀ K : ℕ,
Rmax ≤ δ_n * (2 : ℝ) ^ K →
B.regime.b * sqrt
(2 * log (2 * ((K : ℝ) + 1) / δ) / n)
≤ δ_n ^ 2 := by
intro K hK
have htop : regime.HF_pair_const * regime.H_diameter * δ_n
≤ δ_n * (2 : ℝ) ^ K := by
exact (le_max_right _ _).trans hK
simpa [B] using regime.peeling_slack_HF K δ hδ_pos hδ_le hn htop
obtain ⟨E, hE_meas, hE_prob, hE_bound⟩ :=
localized_omega_event_sharp_for_bundle
(S := S) (P_W := P_W) (sample := sample) (B := B)
regime.law_W hn hδ_pos hδ_le hδn_pos hRmax_lb hslack
refine ⟨E, hE_meas, hE_prob, ?_⟩
intro ω hω h₁ hh₁ h₂ hh₂ f hf
let i : B.ι := regime.interp_HF_idx_pair h₁ h₂ hh₁ hh₂ f hf
let gap : ℝ :=
S.strongNorm (S.hL2 (TC.H_subset hh₁) - S.hL2 (TC.H_subset hh₂))
have hgap_diam : gap ≤ regime.H_diameter := by
simpa [gap] using regime.H_diameter_bound h₁ h₂ hh₁ hh₂
have hi_gap : B.norm (B.F i) ≤ regime.HF_pair_const * gap * δ_n := by
simpa [B, i, gap] using regime.interp_HF_norm_pair h₁ h₂ hh₁ hh₂ f hf
have hi_diam : B.norm (B.F i) ≤ Rmax := by
have hpair_mult : regime.HF_pair_const * gap * δ_n
≤ regime.HF_pair_const * regime.H_diameter * δ_n := by
have hmul : regime.HF_pair_const * gap
≤ regime.HF_pair_const * regime.H_diameter :=
mul_le_mul_of_nonneg_left hgap_diam regime.HF_pair_const_nonneg
exact mul_le_mul_of_nonneg_right hmul hδn_nonneg
exact hi_gap.trans (hpair_mult.trans (le_max_right _ _))
have hdev := hE_bound ω hω i hi_diam
have heval_sample :
(Finset.univ.sum fun k : Fin n => B.F i (B.X (sample.Z k ω))) =
∑ k : Fin n,
(h₁ (S.xOf (sample.Z k ω)) - h₂ (S.xOf (sample.Z k ω)))
* f (S.zOf (sample.Z k ω)) := by
apply Finset.sum_congr rfl
intro k _
simpa [B, i] using
regime.interp_HF_eval_pair h₁ h₂ hh₁ hh₂ f hf (sample.Z k ω)
have heval_pop :
(fun ω' => B.F i (B.X (S.W ω'))) =
fun ω' =>
(h₁ (S.xOf (S.W ω')) - h₂ (S.xOf (S.W ω')))
* f (S.zOf (S.W ω')) := by
funext ω'
simpa [B, i] using
regime.interp_HF_eval_pair h₁ h₂ hh₁ hh₂ f hf (S.W ω')
have hdev_concrete :
|(n : ℝ)⁻¹ * ∑ k : Fin n,
(h₁ (S.xOf (sample.Z k ω)) - h₂ (S.xOf (sample.Z k ω)))
* f (S.zOf (sample.Z k ω))
- ∫ ω',
(h₁ (S.xOf (S.W ω')) - h₂ (S.xOf (S.W ω')))
* f (S.zOf (S.W ω')) ∂μ|
≤ 8 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2 := by
simpa [B, i, heval_sample, heval_pop] using hdev
have hrate :
8 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2
≤ 8 * regime.HF_pair_const * δ_n ^ 2 * gap + 5 * δ_n ^ 2 := by
have hlead := mul_le_mul_of_nonneg_left hi_gap
(by nlinarith [hδn_nonneg] : 0 ≤ 8 * δ_n)
nlinarith
simpa [gap] using hdev_concrete.trans hrate
2 supporting declarations (lemmas, instances)
-
localized_omega_event_for_HFlemma — Ω-side localized deviation event for the product class star(H · F) — controls |(1/n) Σ h(X_i) f(Z_i) − E[h(X) f(Z)]| uniformly over h ∈ TC.H, f ∈ TC.F.hypothesesS :β lambda :n :ℕδ_n :ℝregime :LocalizedRegimes S TC sample sc tb n δ_nhn :0 < nδ :ℝhδ_pos :0 < δhδ_le :δ ≤ 1conclusion∃ E : Set Ω,MeasurableSet E ∧μ E ≥ 1 - ofReal δ ∧∀ ω ∈ E,∀ h ∈ TC.H,∀ f ∈ TC.F,|(n : ℝ)⁻¹ * ∑ k : Fin n, h (S.xOf (sample.Z k ω)) * f (S.zOf (sample.Z k ω))- ∫ ω', h (S.xOf (S.W ω')) * f (S.zOf (S.W ω')) ∂μ|≤ 4 * δ_n * criticalRadius (regime.bundle_HF.regime.ψ n)Proof (Lean source)
lemma localized_omega_event_for_HF {S : OperatorSystem Ω μ} {TC : TRAEClasses S} {P_W : Measure S.𝒲} {sample : IIDSample Ω S.𝒲 μ P_W} [IsProbabilityMeasure μ] {β lambda : ℝ} {sc : SourceCondition S β} {tb : TikhonovBiasBound S β lambda sc} {n : ℕ} {δ_n : ℝ} (regime : LocalizedRegimes S TC sample sc tb n δ_n) (hn : 0 < n) {δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) : ∃ E : Set Ω, MeasurableSet E ∧ μ E ≥ 1 - ofReal δ ∧ ∀ ω ∈ E, ∀ h ∈ TC.H, ∀ f ∈ TC.F, |(n : ℝ)⁻¹ * ∑ k : Fin n, h (S.xOf (sample.Z k ω)) * f (S.zOf (sample.Z k ω)) - ∫ ω', h (S.xOf (S.W ω')) * f (S.zOf (S.W ω')) ∂μ| ≤ 4 * δ_n * criticalRadius (regime.bundle_HF.regime.ψ n) + regime.bundle_HF.regime.b * sqrt (2 * log (1 / δ) / n) := by classical let B := regime.bundle_HF haveI : IsProbabilityMeasure P_W := by rw [← regime.law_W] exact Measure.isProbabilityMeasure_map S.meas_W.aemeasurable obtain ⟨E₀, hE₀_meas, hE₀_prob, hE₀_bound⟩ := localized_uniform_deviation B.F B.norm P_W B.X B.X_meas B.F_meas B.regime hδ_pos hδ_le n hn B.crit_le B.crit_pos B.crit_fp (B.rad_bdd δ_n le_rfl) (B.rad_int δ_n le_rfl) let Ψ : Ω → (Fin n → S.𝒲) := fun ω k => sample.Z k ω let E : Set Ω := Ψ ⁻¹' E₀ have hpull := event_pullback_along_iidSample sample n hE₀_meas hE₀_prob refine ⟨E, ?_, ?_, ?_⟩ · simpa [E, Ψ] using hpull.1 · simpa [E, Ψ] using hpull.2 · intro ω hω h hh f hf let i : B.ι := regime.interp_HF_idx h hh f hf have hω₀ : Ψ ω ∈ E₀ := by simpa [E, Ψ] using hω have hi_norm : B.norm (B.F i) ≤ δ_n := by simpa [B, i] using regime.interp_HF_norm h hh f hf have hdev := hE₀_bound (Ψ ω) hω₀ i hi_norm have hpop : ∫ w, B.F i (B.X w) ∂P_W = ∫ ω', B.F i (B.X (S.W ω')) ∂μ := by exact integral_comp_law_W regime.law_W ((B.F_meas i).comp B.X_meas) have heval_sample : (Finset.univ.sum fun k : Fin n => B.F i (B.X (sample.Z k ω))) = ∑ k : Fin n, h (S.xOf (sample.Z k ω)) * f (S.zOf (sample.Z k ω)) := by apply Finset.sum_congr rfl intro k _ simpa [B, i] using regime.interp_HF_eval h hh f hf (sample.Z k ω) have heval_pop : (fun ω' => B.F i (B.X (S.W ω'))) = fun ω' => h (S.xOf (S.W ω')) * f (S.zOf (S.W ω')) := by funext ω' simpa [B, i] using regime.interp_HF_eval h hh f hf (S.W ω') simpa [Ψ, hpop, heval_sample, heval_pop] using hdev -
localized_omega_event_for_HF_pairlemma — Ω-side fixed-diameter pair-form localized deviation event for the cross class star(H · F) — produces a *single* μ-event simultaneously valid for every triple (h₁, h₂, f) ∈ TC.H × TC.H × TC.F.hypothesesS :β lambda :n :ℕδ_n :ℝregime :LocalizedRegimes S TC sample sc tb n δ_nhn :0 < nδ :ℝhδ_pos :0 < δhδ_le :δ ≤ 1conclusion∃ E : Set Ω,MeasurableSet E ∧μ E ≥ 1 - ofReal δ ∧∀ ω ∈ E,∀ h₁,∀ _hh₁ : h₁ ∈ TC.H,∀ h₂,∀ _hh₂ : h₂ ∈ TC.H,∀ f,∀ _hf : f ∈ TC.F,|(n : ℝ)⁻¹ * ∑ k : Fin n, (h₁ (S.xOf (sample.Z k ω)) - h₂ (S.xOf (sample.Z k ω))) * f (S.zOf (sample.Z k ω))- ∫ ω', (h₁ (S.xOf (S.W ω')) - h₂ (S.xOf (S.W ω'))) * f (S.zOf (S.W ω')) ∂μ|≤ 4 * (regime.HF_pair_const * regime.H_diameter * δ_n + δ_n) * criticalRadius (regime.bundle_HF.regime.ψ n)Proof (Lean source)
lemma localized_omega_event_for_HF_pair {S : OperatorSystem Ω μ} {TC : TRAEClasses S} {P_W : Measure S.𝒲} {sample : IIDSample Ω S.𝒲 μ P_W} [IsProbabilityMeasure μ] {β lambda : ℝ} {sc : SourceCondition S β} {tb : TikhonovBiasBound S β lambda sc} {n : ℕ} {δ_n : ℝ} (regime : LocalizedRegimes S TC sample sc tb n δ_n) (hn : 0 < n) {δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) : ∃ E : Set Ω, MeasurableSet E ∧ μ E ≥ 1 - ofReal δ ∧ ∀ ω ∈ E, ∀ h₁, ∀ _hh₁ : h₁ ∈ TC.H, ∀ h₂, ∀ _hh₂ : h₂ ∈ TC.H, ∀ f, ∀ _hf : f ∈ TC.F, |(n : ℝ)⁻¹ * ∑ k : Fin n, (h₁ (S.xOf (sample.Z k ω)) - h₂ (S.xOf (sample.Z k ω))) * f (S.zOf (sample.Z k ω)) - ∫ ω', (h₁ (S.xOf (S.W ω')) - h₂ (S.xOf (S.W ω'))) * f (S.zOf (S.W ω')) ∂μ| ≤ 4 * (regime.HF_pair_const * regime.H_diameter * δ_n + δ_n) * criticalRadius (regime.bundle_HF.regime.ψ n) + regime.bundle_HF.regime.b * sqrt (2 * log (1 / δ) / n) := by classical let B := regime.bundle_HF let r : ℝ := regime.HF_pair_const * regime.H_diameter * δ_n + δ_n haveI : IsProbabilityMeasure P_W := by rw [← regime.law_W] exact Measure.isProbabilityMeasure_map S.meas_W.aemeasurable have hδn_pos : 0 < δ_n := lt_of_lt_of_le B.crit_pos B.crit_le have hδn_nonneg : 0 ≤ δ_n := le_of_lt hδn_pos have hdiam_nonneg : 0 ≤ regime.H_diameter := hδn_nonneg.trans regime.H_diameter_lb have hpair_nonneg : 0 ≤ regime.HF_pair_const := regime.HF_pair_const_nonneg have hr_delta : δ_n ≤ r := by dsimp [r] have hpair_term_nonneg : 0 ≤ regime.HF_pair_const * regime.H_diameter * δ_n := by positivity linarith have hr_lb : criticalRadius (B.regime.ψ n) ≤ r := by dsimp [r] nlinarith [B.crit_le, hr_delta] obtain ⟨E₀, hE₀_meas, hE₀_prob, hE₀_bound⟩ := localized_uniform_deviation B.F B.norm P_W B.X B.X_meas B.F_meas B.regime hδ_pos hδ_le n hn hr_lb B.crit_pos B.crit_fp (B.rad_bdd r hr_delta) (B.rad_int r hr_delta) let Ψ : Ω → (Fin n → S.𝒲) := fun ω k => sample.Z k ω let E : Set Ω := Ψ ⁻¹' E₀ have hpull := event_pullback_along_iidSample sample n hE₀_meas hE₀_prob refine ⟨E, ?_, ?_, ?_⟩ · simpa [E, Ψ] using hpull.1 · simpa [E, Ψ] using hpull.2 · intro ω hω h₁ hh₁ h₂ hh₂ f hf let i : B.ι := regime.interp_HF_idx_pair h₁ h₂ hh₁ hh₂ f hf have hω₀ : Ψ ω ∈ E₀ := by simpa [E, Ψ] using hω have hpair : S.strongNorm (S.hL2 (TC.H_subset hh₁) - S.hL2 (TC.H_subset hh₂)) ≤ regime.H_diameter := regime.H_diameter_bound h₁ h₂ hh₁ hh₂ have hi_norm : B.norm (B.F i) ≤ r := by have hi_gap := regime.interp_HF_norm_pair h₁ h₂ hh₁ hh₂ f hf have hpair_mult : regime.HF_pair_const * S.strongNorm (S.hL2 (TC.H_subset hh₁) - S.hL2 (TC.H_subset hh₂)) * δ_n ≤ regime.HF_pair_const * regime.H_diameter * δ_n := by have hmul : regime.HF_pair_const * S.strongNorm (S.hL2 (TC.H_subset hh₁) - S.hL2 (TC.H_subset hh₂)) ≤ regime.HF_pair_const * regime.H_diameter := mul_le_mul_of_nonneg_left hpair hpair_nonneg simpa [mul_assoc, mul_comm, mul_left_comm] using (mul_le_mul_of_nonneg_left hmul hδn_nonneg) have hpair_nonneg' : 0 ≤ regime.HF_pair_const * regime.H_diameter * δ_n := by positivity dsimp [r] have hpair_bound : B.norm (B.F i) ≤ regime.HF_pair_const * regime.H_diameter * δ_n := le_trans hi_gap hpair_mult linarith [hpair_nonneg'] have hdev := hE₀_bound (Ψ ω) hω₀ i hi_norm have hpop : ∫ w, B.F i (B.X w) ∂P_W = ∫ ω', B.F i (B.X (S.W ω')) ∂μ := by exact integral_comp_law_W regime.law_W ((B.F_meas i).comp B.X_meas) have heval_sample : (Finset.univ.sum fun k : Fin n => B.F i (B.X (sample.Z k ω))) = ∑ k : Fin n, (h₁ (S.xOf (sample.Z k ω)) - h₂ (S.xOf (sample.Z k ω))) * f (S.zOf (sample.Z k ω)) := by apply Finset.sum_congr rfl intro k _ simpa [B, i] using regime.interp_HF_eval_pair h₁ h₂ hh₁ hh₂ f hf (sample.Z k ω) have heval_pop : (fun ω' => B.F i (B.X (S.W ω'))) = fun ω' => (h₁ (S.xOf (S.W ω')) - h₂ (S.xOf (S.W ω'))) * f (S.zOf (S.W ω')) := by funext ω' simpa [B, i] using regime.interp_HF_eval_pair h₁ h₂ hh₁ hh₂ f hf (S.W ω') simpa [Ψ, r, hpop, heval_sample, heval_pop] using hdev
LocalizedEventMF 1 core · 2 supporting This file constructs the high-probability event controlling empirical fluctuations of the moment map multiplied by critic functions in the primal NPIV analysis. ★ localized_omega_event_for_mF_pair_peeled
Localized Deviation for Moment-Critic Products mF
This file constructs the high-probability event controlling empirical
fluctuations of the moment map multiplied by critic functions in the primal
NPIV analysis. Here mF denotes the class W ↦ m(W; f) indexed by
f ∈ TC.F; it supplies the moment-class component of the localized
empirical-process event used downstream.
lemma localized_omega_event_for_mF_pair_peeled reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Peeled pair-form localized deviation event for the moment class star(m ∘ F). Given a positive sample size n and a confidence level δ in (0, 1], there is a single event of probability at least 1 − δ, valid simultaneously for every pair f₁, f₂ in the critic class TC.F, on which the gap between the empirical and population means of m(·; f₁) − m(·; f₂) is bounded by 8 · mF_L2_const · δ_n · ‖f₁ − f₂‖_strong + 5 · δ_n², where the strong norm is taken in the critic's L² embedding and mF_L2_const comes from the supplied localized-regime witness.
Formal statement
hypotheses
S :
β lambda :
n :
ℕ
δ_n :
ℝ
regime :
LocalizedRegimes S TC sample sc tb n δ_n
hn :
0 < n
δ :
ℝ
hδ_pos :
0 < δ
hδ_le :
δ ≤ 1
conclusion
∃ E : Set Ω,
MeasurableSet E ∧
μ E ≥ 1 - ofReal δ ∧
∀ ω ∈ E,
∀ f₁,
∀ _hf₁ : f₁ ∈ TC.F,
∀ f₂,
∀ _hf₂ : f₂ ∈ TC.F,
|(n : ℝ)⁻¹ * ∑ k : Fin n, (S.m (sample.Z k ω) f₁ - S.m (sample.Z k ω) f₂)
- ∫ ω', (S.m (S.W ω') f₁ - S.m (S.W ω') f₂) ∂μ|
≤ 8 * regime.mF_L2_const * δ_n * S.strongNorm (S.qL2 (TC.F_subset _hf₁) - S.qL2 (TC.F_subset _hf₂))
+ 5 * δ_n ^ 2
Proof (Lean source)
lemma localized_omega_event_for_mF_pair_peeled
{S : OperatorSystem Ω μ} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
[IsProbabilityMeasure μ]
{β lambda : ℝ}
{sc : SourceCondition S β}
{tb : TikhonovBiasBound S β lambda sc}
{n : ℕ} {δ_n : ℝ}
(regime : LocalizedRegimes S TC sample sc tb n δ_n)
(hn : 0 < n)
{δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) :
∃ E : Set Ω,
MeasurableSet E ∧ μ E ≥ 1 - ofReal δ ∧
∀ ω ∈ E, ∀ f₁, ∀ _hf₁ : f₁ ∈ TC.F, ∀ f₂, ∀ _hf₂ : f₂ ∈ TC.F,
|(n : ℝ)⁻¹ * ∑ k : Fin n,
(S.m (sample.Z k ω) f₁ - S.m (sample.Z k ω) f₂)
- ∫ ω', (S.m (S.W ω') f₁ - S.m (S.W ω') f₂) ∂μ|
≤ 8 * regime.mF_L2_const * δ_n *
S.strongNorm (S.qL2 (TC.F_subset _hf₁) - S.qL2 (TC.F_subset _hf₂))
+ 5 * δ_n ^ 2 := by
classical
let B := regime.bundle_mF
let Rmax : ℝ := max δ_n (regime.mF_L2_const * regime.F_diameter)
have hδn_pos : 0 < δ_n := lt_of_lt_of_le B.crit_pos B.crit_le
have hδn_nonneg : 0 ≤ δ_n := le_of_lt hδn_pos
have hRmax_lb : δ_n ≤ Rmax := by
exact le_max_left _ _
have hslack : ∀ K : ℕ,
Rmax ≤ δ_n * (2 : ℝ) ^ K →
B.regime.b * sqrt
(2 * log (2 * ((K : ℝ) + 1) / δ) / n)
≤ δ_n ^ 2 := by
intro K hK
have htop : regime.mF_L2_const * regime.F_diameter
≤ δ_n * (2 : ℝ) ^ K := by
exact (le_max_right _ _).trans hK
simpa [B] using regime.peeling_slack_mF K δ hδ_pos hδ_le hn htop
obtain ⟨E, hE_meas, hE_prob, hE_bound⟩ :=
localized_omega_event_sharp_for_bundle
(S := S) (P_W := P_W) (sample := sample) (B := B)
regime.law_W hn hδ_pos hδ_le hδn_pos hRmax_lb hslack
refine ⟨E, hE_meas, hE_prob, ?_⟩
intro ω hω f₁ hf₁ f₂ hf₂
let i : B.ι := regime.interp_mF_idx_pair f₁ f₂ hf₁ hf₂
let gap : ℝ :=
S.strongNorm (S.qL2 (TC.F_subset hf₁) - S.qL2 (TC.F_subset hf₂))
have hgap_top : gap ≤ regime.F_diameter := by
simpa [gap] using regime.F_diameter_bound f₁ f₂ hf₁ hf₂
have hi_gap : B.norm (B.F i) ≤ regime.mF_L2_const * gap := by
simpa [B, i, gap] using regime.interp_mF_norm_pair f₁ f₂ hf₁ hf₂
have hi_diam : B.norm (B.F i) ≤ Rmax := by
have htop : regime.mF_L2_const * gap
≤ regime.mF_L2_const * regime.F_diameter :=
mul_le_mul_of_nonneg_left hgap_top regime.mF_L2_const_nonneg
exact hi_gap.trans (htop.trans (le_max_right _ _))
have hdev := hE_bound ω hω i hi_diam
have heval_sample :
(Finset.univ.sum fun k : Fin n => B.F i (B.X (sample.Z k ω))) =
∑ k : Fin n, (S.m (sample.Z k ω) f₁ - S.m (sample.Z k ω) f₂) := by
apply Finset.sum_congr rfl
intro k _
simpa [B, i] using regime.interp_mF_eval_pair f₁ f₂ hf₁ hf₂ (sample.Z k ω)
have heval_pop :
(fun ω' => B.F i (B.X (S.W ω'))) =
fun ω' => S.m (S.W ω') f₁ - S.m (S.W ω') f₂ := by
funext ω'
simpa [B, i] using regime.interp_mF_eval_pair f₁ f₂ hf₁ hf₂ (S.W ω')
have hdev_concrete :
|(n : ℝ)⁻¹ * ∑ k : Fin n,
(S.m (sample.Z k ω) f₁ - S.m (sample.Z k ω) f₂)
- ∫ ω', (S.m (S.W ω') f₁ - S.m (S.W ω') f₂) ∂μ|
≤ 8 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2 := by
simpa [B, i, heval_sample, heval_pop] using hdev
have hrate :
8 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2
≤ 8 * regime.mF_L2_const * δ_n * gap + 5 * δ_n ^ 2 := by
have hlead := mul_le_mul_of_nonneg_left hi_gap
(by nlinarith [hδn_nonneg] : 0 ≤ 8 * δ_n)
nlinarith
simpa [gap] using hdev_concrete.trans hrate
2 supporting declarations (lemmas, instances)
-
localized_omega_event_for_mFlemma — Ω-side localized deviation event for the moment class star(m ∘ F) — controls |(1/n) Σ m(W_i; f) − E[m(W; f)]| uniformly over f ∈ TC.F.hypothesesS :β lambda :n :ℕδ_n :ℝregime :LocalizedRegimes S TC sample sc tb n δ_nhn :0 < nδ :ℝhδ_pos :0 < δhδ_le :δ ≤ 1conclusion∃ E : Set Ω,MeasurableSet E ∧μ E ≥ 1 - ofReal δ ∧∀ ω ∈ E,∀ f ∈ TC.F,|(n : ℝ)⁻¹ * ∑ k : Fin n, S.m (sample.Z k ω) f - ∫ ω', S.m (S.W ω') f ∂μ|≤ 4 * δ_n * criticalRadius (regime.bundle_mF.regime.ψ n)Proof (Lean source)
lemma localized_omega_event_for_mF {S : OperatorSystem Ω μ} {TC : TRAEClasses S} {P_W : Measure S.𝒲} {sample : IIDSample Ω S.𝒲 μ P_W} [IsProbabilityMeasure μ] {β lambda : ℝ} {sc : SourceCondition S β} {tb : TikhonovBiasBound S β lambda sc} {n : ℕ} {δ_n : ℝ} (regime : LocalizedRegimes S TC sample sc tb n δ_n) (hn : 0 < n) {δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) : ∃ E : Set Ω, MeasurableSet E ∧ μ E ≥ 1 - ofReal δ ∧ ∀ ω ∈ E, ∀ f ∈ TC.F, |(n : ℝ)⁻¹ * ∑ k : Fin n, S.m (sample.Z k ω) f - ∫ ω', S.m (S.W ω') f ∂μ| ≤ 4 * δ_n * criticalRadius (regime.bundle_mF.regime.ψ n) + regime.bundle_mF.regime.b * sqrt (2 * log (1 / δ) / n) := by classical let B := regime.bundle_mF haveI : IsProbabilityMeasure P_W := by rw [← regime.law_W] exact Measure.isProbabilityMeasure_map S.meas_W.aemeasurable obtain ⟨E₀, hE₀_meas, hE₀_prob, hE₀_bound⟩ := localized_uniform_deviation B.F B.norm P_W B.X B.X_meas B.F_meas B.regime hδ_pos hδ_le n hn B.crit_le B.crit_pos B.crit_fp (B.rad_bdd δ_n le_rfl) (B.rad_int δ_n le_rfl) let Ψ : Ω → (Fin n → S.𝒲) := fun ω k => sample.Z k ω let E : Set Ω := Ψ ⁻¹' E₀ have hpull := event_pullback_along_iidSample sample n hE₀_meas hE₀_prob refine ⟨E, ?_, ?_, ?_⟩ · simpa [E, Ψ] using hpull.1 · simpa [E, Ψ] using hpull.2 · intro ω hω f hf let i : B.ι := regime.interp_mF_idx f hf have hω₀ : Ψ ω ∈ E₀ := by simpa [E, Ψ] using hω have hi_norm : B.norm (B.F i) ≤ δ_n := by simpa [B, i] using regime.interp_mF_norm f hf have hdev := hE₀_bound (Ψ ω) hω₀ i hi_norm have hpop : ∫ w, B.F i (B.X w) ∂P_W = ∫ ω', B.F i (B.X (S.W ω')) ∂μ := by exact integral_comp_law_W regime.law_W ((B.F_meas i).comp B.X_meas) have heval_sample : (Finset.univ.sum fun k : Fin n => B.F i (B.X (sample.Z k ω))) = ∑ k : Fin n, S.m (sample.Z k ω) f := by apply Finset.sum_congr rfl intro k _ simpa [B, i] using regime.interp_mF_eval f hf (sample.Z k ω) have heval_pop : (fun ω' => B.F i (B.X (S.W ω'))) = fun ω' => S.m (S.W ω') f := by funext ω' simpa [B, i] using regime.interp_mF_eval f hf (S.W ω') simpa [Ψ, hpop, heval_sample, heval_pop] using hdev -
localized_omega_event_for_mF_pairlemma — Ω-side fixed-diameter pair-form localized deviation event for the moment class star(m ∘ F). This is the non-peeled building block for the Foster pair-gap bridge; the peeled variant can reuse the same interpretation at dyadic radii below mF_L2_const * F_diameter.hypothesesS :β lambda :n :ℕδ_n :ℝregime :LocalizedRegimes S TC sample sc tb n δ_nhn :0 < nδ :ℝhδ_pos :0 < δhδ_le :δ ≤ 1conclusion∃ E : Set Ω,MeasurableSet E ∧μ E ≥ 1 - ofReal δ ∧∀ ω ∈ E,∀ f₁,∀ _hf₁ : f₁ ∈ TC.F,∀ f₂,∀ _hf₂ : f₂ ∈ TC.F,|(n : ℝ)⁻¹ * ∑ k : Fin n, (S.m (sample.Z k ω) f₁ - S.m (sample.Z k ω) f₂)- ∫ ω', (S.m (S.W ω') f₁ - S.m (S.W ω') f₂) ∂μ|≤ 4 * (regime.mF_L2_const * regime.F_diameter) * criticalRadius (regime.bundle_mF.regime.ψ n)Proof (Lean source)
lemma localized_omega_event_for_mF_pair {S : OperatorSystem Ω μ} {TC : TRAEClasses S} {P_W : Measure S.𝒲} {sample : IIDSample Ω S.𝒲 μ P_W} [IsProbabilityMeasure μ] {β lambda : ℝ} {sc : SourceCondition S β} {tb : TikhonovBiasBound S β lambda sc} {n : ℕ} {δ_n : ℝ} (regime : LocalizedRegimes S TC sample sc tb n δ_n) (hn : 0 < n) {δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) : ∃ E : Set Ω, MeasurableSet E ∧ μ E ≥ 1 - ofReal δ ∧ ∀ ω ∈ E, ∀ f₁, ∀ _hf₁ : f₁ ∈ TC.F, ∀ f₂, ∀ _hf₂ : f₂ ∈ TC.F, |(n : ℝ)⁻¹ * ∑ k : Fin n, (S.m (sample.Z k ω) f₁ - S.m (sample.Z k ω) f₂) - ∫ ω', (S.m (S.W ω') f₁ - S.m (S.W ω') f₂) ∂μ| ≤ 4 * (regime.mF_L2_const * regime.F_diameter) * criticalRadius (regime.bundle_mF.regime.ψ n) + regime.bundle_mF.regime.b * sqrt (2 * log (1 / δ) / n) := by classical let B := regime.bundle_mF let r : ℝ := regime.mF_L2_const * regime.F_diameter haveI : IsProbabilityMeasure P_W := by rw [← regime.law_W] exact Measure.isProbabilityMeasure_map S.meas_W.aemeasurable have hδn_pos : 0 < δ_n := lt_of_lt_of_le B.crit_pos B.crit_le have hr_delta : δ_n ≤ r := by simpa [r] using regime.mF_pair_radius_lb have hr_lb : criticalRadius (B.regime.ψ n) ≤ r := by exact B.crit_le.trans hr_delta obtain ⟨E₀, hE₀_meas, hE₀_prob, hE₀_bound⟩ := localized_uniform_deviation B.F B.norm P_W B.X B.X_meas B.F_meas B.regime hδ_pos hδ_le n hn hr_lb B.crit_pos B.crit_fp (B.rad_bdd r hr_delta) (B.rad_int r hr_delta) let Ψ : Ω → (Fin n → S.𝒲) := fun ω k => sample.Z k ω let E : Set Ω := Ψ ⁻¹' E₀ have hpull := event_pullback_along_iidSample sample n hE₀_meas hE₀_prob refine ⟨E, ?_, ?_, ?_⟩ · simpa [E, Ψ] using hpull.1 · simpa [E, Ψ] using hpull.2 · intro ω hω f₁ hf₁ f₂ hf₂ let i : B.ι := regime.interp_mF_idx_pair f₁ f₂ hf₁ hf₂ have hω₀ : Ψ ω ∈ E₀ := by simpa [E, Ψ] using hω have hpair : S.strongNorm (S.qL2 (TC.F_subset hf₁) - S.qL2 (TC.F_subset hf₂)) ≤ regime.F_diameter := regime.F_diameter_bound f₁ f₂ hf₁ hf₂ have hi_norm : B.norm (B.F i) ≤ r := by exact (regime.interp_mF_norm_pair f₁ f₂ hf₁ hf₂).trans (mul_le_mul_of_nonneg_left hpair regime.mF_L2_const_nonneg) have hdev := hE₀_bound (Ψ ω) hω₀ i hi_norm have hpop : ∫ w, B.F i (B.X w) ∂P_W = ∫ ω', B.F i (B.X (S.W ω')) ∂μ := by exact integral_comp_law_W regime.law_W ((B.F_meas i).comp B.X_meas) have heval_sample : (Finset.univ.sum fun k : Fin n => B.F i (B.X (sample.Z k ω))) = ∑ k : Fin n, (S.m (sample.Z k ω) f₁ - S.m (sample.Z k ω) f₂) := by apply Finset.sum_congr rfl intro k _ simpa [B, i] using regime.interp_mF_eval_pair f₁ f₂ hf₁ hf₂ (sample.Z k ω) have heval_pop : (fun ω' => B.F i (B.X (S.W ω'))) = fun ω' => S.m (S.W ω') f₁ - S.m (S.W ω') f₂ := by funext ω' simpa [B, i] using regime.interp_mF_eval_pair f₁ f₂ hf₁ hf₂ (S.W ω') simpa [Ψ, r, hpop, heval_sample, heval_pop] using hdev
LocalizedEventsBase 1 core · 1 supporting This file supplies the shared Ω-side infrastructure for turning product-space localized deviation inequalities into events on the ambient sample space. ★ localized_omega_event_sharp_for_bundle
Base Localized Events for Primal NPIV
This file supplies the shared Ω-side infrastructure for turning product-space
localized deviation inequalities into events on the ambient sample space. The
law bridge integral_comp_law_W rewrites population means under the observation
law as integrals over S.W, and localized_omega_event_sharp_for_bundle
pulls the sharp localized event for an abstract LocalizedRegimeBundle back
along an IID sample. The class-specific event files for H, F, H · F, and
m ∘ F instantiate this wrapper through their LocalizedRegimes
interpretation fields.
lemma localized_omega_event_sharp_for_bundle reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Ω-side Foster–Syrgkanis sharp localized event for a single NPIV LocalizedRegimeBundle. Consider an IID sample drawn from a probability space, where the pushforward of the ambient measure under the observed-variable map equals the stated observation law and the sample size n is positive. Fix a confidence parameter ζ with , a localized rate with , and a radius Rmax with δ_n ≤ Rmax. If for every dyadic level K with Rmax ≤ δ_n · 2 ^ K, the corresponding complexity term stays below δ_n ^ 2, then there is an event of probability at least 1 - ζ on which, for every index in the regime bundle whose function norm is at most Rmax, the empirical average of that function over the first n sample draws deviates from its population mean by at most 8 * δ_n * norm + 5 * δ_n ^ 2.
Formal statement
hypotheses
S :
OperatorSystem Ω μ
n :
ℕ
δ_n Rmax :
ℝ
B :
LocalizedRegimeBundle S.𝒲 P_W n δ_n
h_law_W :
μ.map S.W = P_W
hn :
0 < n
ζ :
ℝ
hζ_pos :
0 < ζ
hζ_le :
ζ ≤ 1
hδn_pos :
0 < δ_n
hRmax_lb :
δ_n ≤ Rmax
conclusion
∃ E : Set Ω
if
MeasurableSet E ∧ μ E ≥ 1 - ofReal ζ ∧ ∀ ω ∈ E, ∀ i : B.ι, B.norm (B.F i) ≤ Rmax
then
|(n : ℝ)⁻¹ * ∑ k : Fin n, B.F i (B.X (sample.Z k ω)) - ∫ ω', B.F i (B.X (S.W ω')) ∂μ|
≤ 8 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2
Proof (Lean source)
lemma localized_omega_event_sharp_for_bundle
{S : OperatorSystem Ω μ} {P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
[IsProbabilityMeasure μ]
{n : ℕ} {δ_n Rmax : ℝ}
(B : LocalizedRegimeBundle S.𝒲 P_W n δ_n)
(h_law_W : μ.map S.W = P_W)
(hn : 0 < n)
{ζ : ℝ} (hζ_pos : 0 < ζ) (hζ_le : ζ ≤ 1)
(hδn_pos : 0 < δ_n)
(hRmax_lb : δ_n ≤ Rmax)
(hslack : ∀ K : ℕ,
Rmax ≤ δ_n * (2 : ℝ) ^ K →
B.regime.b * sqrt
(2 * log (2 * ((K : ℝ) + 1) / ζ) / n)
≤ δ_n ^ 2) :
∃ E : Set Ω,
MeasurableSet E ∧ μ E ≥ 1 - ofReal ζ ∧
∀ ω ∈ E, ∀ i : B.ι,
B.norm (B.F i) ≤ Rmax →
|(n : ℝ)⁻¹ * ∑ k : Fin n, B.F i (B.X (sample.Z k ω))
- ∫ ω', B.F i (B.X (S.W ω')) ∂μ|
≤ 8 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2 := by
classical
haveI : IsProbabilityMeasure P_W := by
rw [← h_law_W]
exact Measure.isProbabilityMeasure_map S.meas_W.aemeasurable
obtain ⟨E₀, hE₀_meas, hE₀_prob, hE₀_bound⟩ :=
localized_uniform_deviation_sharp B.F B.norm P_W B.X B.X_meas B.F_meas
B.regime hζ_pos hζ_le n hn (ρ := δ_n) (Rmax := Rmax)
B.crit_le hδn_pos B.crit_pos B.crit_fp
B.rad_bdd B.rad_int hslack
let Ψ : Ω → (Fin n → S.𝒲) := fun ω k => sample.Z k ω
let E : Set Ω := Ψ ⁻¹' E₀
have hpull :=
event_pullback_along_iidSample sample n hE₀_meas hE₀_prob
refine ⟨E, ?_, ?_, ?_⟩
· simpa [E, Ψ] using hpull.1
· simpa [E, Ψ] using hpull.2
· intro ω hω i hi_diam
have hω₀ : Ψ ω ∈ E₀ := by
simpa [E, Ψ] using hω
have hdev := hE₀_bound (Ψ ω) hω₀ i (B.norm_nonneg i) hi_diam
have hpop :
∫ w, B.F i (B.X w) ∂P_W =
∫ ω', B.F i (B.X (S.W ω')) ∂μ := by
exact integral_comp_law_W h_law_W ((B.F_meas i).comp B.X_meas)
simpa [Ψ, hpop] using hdev
1 supporting declaration (lemmas, instances)
-
integral_comp_law_Wlemma — Integrating a measurable function under the law of the observed variable is the same as integrating its pullback over the ambient sample space.hypothesesconclusion∫ w, g w ∂P_W = ∫ ω, g (S.W ω) ∂μProof (Lean source)
lemma integral_comp_law_W {S : OperatorSystem Ω μ} {P_W : Measure S.𝒲} (hlaw : μ.map S.W = P_W) {g : S.𝒲 → ℝ} (hg : Measurable g) : ∫ w, g w ∂P_W = ∫ ω, g (S.W ω) ∂μ := by rw [← hlaw] exact MeasureTheory.integral_map S.meas_W.aemeasurable hg.aestronglyMeasurable
Regulariser 1 core · 1 supporting This file derives the localized empirical-process event needed to compare the empirical regularized objective at the estimator with the objective at a population Tikhonov candidate. ★ centred_regulariser_bound_from_localized
Regularizer Event for the Primal NPIV Rate
This file derives the localized empirical-process event needed to compare the empirical regularized objective at the estimator with the objective at a population Tikhonov candidate. The bounds connect the localized deviation events to the regularization terms in the primal NPIV rate proof, producing an all-sample-size centred empirical regularizer bound from the localized event for the squared candidate-difference class.
theorem centred_regulariser_bound_from_localized reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
The centred empirical regularizer gap is bounded uniformly over all sample sizes by the localized rate from the squared candidate-difference event. For every sample size n, suppose a localized-regimes witness at the corresponding fold size and localization rate delta n is available, the regularization weight satisfies lambda ≥ 0, and the confidence level satisfies 0 < ζ < 1. Then there is an event of probability at least 1 - ζ on which, for every split size with at least one fold-A observation, the empirical-vs- population regularizer discrepancy between the estimator and the population Tikhonov candidate is controlled by an explicit bound built from the fold's diameter, critical radius, and localization rate.
Formal statement
hypotheses
S :
split :
OneShotSplit sample
lambda β :
ℝ
delta :
ℕ → ℝ
h_hat :
ℕ → Ω → S.𝒳 → ℝ
IsTRAEPrimalEstimator S TC sample split lambda h_hat
sc :
SourceCondition S β
tb :
TikhonovBiasBound S β lambda sc
regimes :
∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n)
lambda_nonneg :
0 ≤ lambda
ζ :
ℝ
hζ_pos :
0 < ζ
hζ_lt :
ζ < 1
conclusion
∃ Aζ_reg : Set Ω
if
then
|lambda * ((((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (tb.h_lambda_star_fun (S.xOf (sample.Z (k : ℕ) ω))) ^ 2 - ((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (h_hat n ω (S.xOf (sample.Z (k : ℕ) ω))) ^ 2) - ((S.strongNorm (S.hL2 tb.h_lambda_star_mem)) ^ 2 - (S.strongNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n ω)))) ^ 2))|
≤ lambda * (4 * ((regimes n).H_diameter + delta n) * criticalRadius ((regimes n).bundle_H.regime.ψ (split.n₁ n)) + (regimes n).bundle_H.regime.b * sqrt (2 * log ((2 : ℝ) ^ (n + 1) / ζ) / (split.n₁ n)))
Proof (Lean source)
theorem centred_regulariser_bound_from_localized
{S : OperatorSystem Ω μ} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
{split : OneShotSplit sample}
{lambda β : ℝ} {delta : ℕ → ℝ}
{h_hat : ℕ → Ω → S.𝒳 → ℝ}
{is_estimator : IsTRAEPrimalEstimator S TC sample split lambda h_hat}
(sc : SourceCondition S β)
(tb : TikhonovBiasBound S β lambda sc)
[IsProbabilityMeasure μ]
(regimes : ∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n))
(lambda_nonneg : 0 ≤ lambda)
{ζ : ℝ} (hζ_pos : 0 < ζ) (hζ_lt : ζ < 1) :
∃ Aζ_reg : Set Ω,
MeasurableSet Aζ_reg ∧ μ Aζ_reg ≥ 1 - ofReal ζ ∧
∀ ω ∈ Aζ_reg, ∀ n : ℕ, 1 ≤ split.n₁ n →
|lambda *
((((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(tb.h_lambda_star_fun (S.xOf (sample.Z (k : ℕ) ω))) ^ 2
- ((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(h_hat n ω (S.xOf (sample.Z (k : ℕ) ω))) ^ 2)
- ((S.strongNorm (S.hL2 tb.h_lambda_star_mem)) ^ 2
- (S.strongNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n ω)))) ^ 2))|
≤ lambda *
(4 * ((regimes n).H_diameter + delta n) *
criticalRadius ((regimes n).bundle_H.regime.ψ (split.n₁ n))
+ (regimes n).bundle_H.regime.b *
sqrt
(2 * log ((2 : ℝ) ^ (n + 1) / ζ)
/ (split.n₁ n))) := by
classical
let ε : ℕ → ℝ := fun n => ζ * ((1 / 2 : ℝ) ^ (n + 1))
have hε_pos : ∀ n, 0 < ε n := by
intro n
exact mul_pos hζ_pos (pow_pos (by norm_num) _)
have hε_le_one : ∀ n, ε n ≤ 1 := by
intro n
have hζ_le : ζ ≤ 1 := le_of_lt hζ_lt
have hpow_le_one : ((1 / 2 : ℝ) ^ (n + 1)) ≤ 1 := by
exact pow_le_one₀ (by norm_num) (by norm_num)
have hpow_nonneg : 0 ≤ ((1 / 2 : ℝ) ^ (n + 1)) := by positivity
nlinarith
let En : ℕ → Set Ω := fun n =>
if hn : 0 < split.n₁ n then
(localized_omega_event_for_H
(regime := regimes n) hn (hε_pos n) (hε_le_one n)).choose
else Set.univ
have hEn_meas : ∀ n, MeasurableSet (En n) := by
intro n
dsimp [En]
split
· rename_i hn
exact (localized_omega_event_for_H
(regime := regimes n) hn (hε_pos n) (hε_le_one n)).choose_spec.1
· exact MeasurableSet.univ
have hEn_mass : ∀ n, μ (En n) ≥ 1 - ofReal (ε n) := by
intro n
dsimp [En]
split
· rename_i hn
exact (localized_omega_event_for_H
(regime := regimes n) hn (hε_pos n) (hε_le_one n)).choose_spec.2.1
· rw [measure_univ]
exact tsub_le_self
have htsum_ε : (∑' n, ofReal (ε n)) ≤ ofReal ζ := by
have hterm :
(fun n => ofReal (ε n))
=
fun n => ofReal ζ * (2⁻¹ : ENNReal) ^ (n + 1) := by
funext n
rw [show ε n = ζ * (1 / 2 : ℝ) ^ (n + 1) by rfl]
rw [ENNReal.ofReal_mul (le_of_lt hζ_pos)]
simp [one_div, ENNReal.inv_pow]
rw [hterm, ENNReal.tsum_mul_left, ENNReal.tsum_geometric_add_one]
have hgeom : (2⁻¹ : ENNReal) * (1 - 2⁻¹)⁻¹ = 1 := by
rw [ENNReal.one_sub_inv_two, inv_inv]
exact ENNReal.inv_mul_cancel (Ne.symm (NeZero.ne' (2 : ENNReal)))
(by norm_num : (2 : ENNReal) ≠ ⊤)
rw [hgeom, mul_one]
let Aζ_reg : Set Ω := ⋂ n, En n
refine ⟨Aζ_reg, MeasurableSet.iInter hEn_meas, ?_, ?_⟩
· exact (tsub_le_tsub_left htsum_ε 1).trans
(measure_iInter_nat_ge_one_sub_tsum_of_ge hEn_meas hEn_mass)
· intro ω hω n hn
have hn_pos : 0 < split.n₁ n := lt_of_lt_of_le zero_lt_one hn
have hωn : ω ∈ En n := Set.mem_iInter.mp hω n
have hωn_event :
ω ∈ (localized_omega_event_for_H
(regime := regimes n) hn_pos (hε_pos n) (hε_le_one n)).choose := by
simpa [En, hn_pos] using hωn
have hdev :=
(localized_omega_event_for_H
(regime := regimes n) hn_pos (hε_pos n) (hε_le_one n)).choose_spec.2.2
ω hωn_event
tb.h_lambda_star_fun (regimes n).realizability
(h_hat n ω) (is_estimator.mem_H n ω)
have hstar_sq :
(S.strongNorm (S.hL2 tb.h_lambda_star_mem)) ^ 2 =
∫ ω', (tb.h_lambda_star_fun (S.xOf (S.W ω'))) ^ 2 ∂μ :=
S.strongNorm_sq_hL2_eq_integral tb.h_lambda_star_mem
have hhat_sq :
(S.strongNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n ω)))) ^ 2 =
∫ ω', (h_hat n ω (S.xOf (S.W ω'))) ^ 2 ∂μ :=
S.strongNorm_sq_hL2_eq_integral (TC.H_subset (is_estimator.mem_H n ω))
have hlog :
1 / ε n = (2 : ℝ) ^ (n + 1) / ζ := by
dsimp [ε]
simp only [one_div]
rw [inv_pow]
field_simp [ne_of_gt hζ_pos,
pow_ne_zero (n + 1) (show (2 : ℝ) ≠ 0 by norm_num)]
rw [hlog] at hdev
have hmul := mul_le_mul_of_nonneg_left hdev lambda_nonneg
simpa [abs_mul, abs_of_nonneg lambda_nonneg, hstar_sq, hhat_sq, mul_assoc]
using hmul
1 supporting declaration (lemmas, instances)
-
measure_iInter_nat_ge_one_sub_tsum_of_gelemma — If each event in a countable family has probability at least one minus its assigned error, then their intersection has probability at least one minus the sum of those errors.hypothesesconclusionμ (⋂ n, E n) ≥ 1 - ∑' n, a nProof (Lean source)
lemma measure_iInter_nat_ge_one_sub_tsum_of_ge [IsProbabilityMeasure μ] {E : ℕ → Set Ω} {a : ℕ → ENNReal} (hE_meas : ∀ n, MeasurableSet (E n)) (hE : ∀ n, μ (E n) ≥ 1 - a n) : μ (⋂ n, E n) ≥ 1 - ∑' n, a n := by have hE_compl : ∀ n, μ (E n)ᶜ ≤ a n := by intro n have hone_le : (1 : ENNReal) ≤ a n + μ (E n) := tsub_le_iff_left.mp (hE n) rw [measure_compl (hE_meas n) (measure_ne_top _ _), measure_univ] exact tsub_le_iff_right.mpr (by simpa [add_comm] using hone_le) have hbad_subset : (⋂ n, E n)ᶜ ⊆ ⋃ n, (E n)ᶜ := by simp have hbad_le : μ (⋂ n, E n)ᶜ ≤ ∑' n, a n := by calc μ (⋂ n, E n)ᶜ ≤ μ (⋃ n, (E n)ᶜ) := measure_mono hbad_subset _ ≤ ∑' n, μ (E n)ᶜ := measure_iUnion_le fun n => (E n)ᶜ _ ≤ ∑' n, a n := ENNReal.tsum_le_tsum hE_compl have hA_meas : MeasurableSet (⋂ n, E n) := MeasurableSet.iInter hE_meas rw [measure_compl hA_meas (measure_ne_top _ _), measure_univ] at hbad_le have hone_le : (1 : ENNReal) ≤ (∑' n, a n) + μ (⋂ n, E n) := tsub_le_iff_right.mp hbad_le exact tsub_le_iff_left.mpr hone_le