Estimation.NPIV.Primal.EmpiricalProcessEvent
The high-probability empirical-process events (Gram-matrix control, residual concentration) underlying the sieve NPIV rate.
Regime 4 core · 0 supporting This file bundles the localized empirical-process hypotheses required for the primal NPIV rate theorem. ★ peelingFloor_quarter_of_unit_scale
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,
and pair-gap interpretation fields needed by the class-specific deviation
events. PeelingFloor separately records the finite-depth inequalities at one
chosen confidence level.
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 and is strictly positive. 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)
**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 has 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
Ω :
Type u_1
S :
OperatorSystem Ω μ
TC :
P_W :
Measure S.𝒲
sample :
IIDSample Ω S.𝒲 μ P_W
β lambda :
ℝ
sc :
SourceCondition S β
tb :
TikhonovBiasBoundAt 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 Bousquet
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.
Carried at the bundle layer because
the EP loss-difference L²-norm calculation (Foster Lemma 11
input) needs it, but the import cycle with the rate modules 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.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
structure PeelingFloor reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
At a fixed confidence allocation eta, a localized NPIV regime satisfies the peeling floor when the variance-sensitive slack is absorbed at some finite dyadic depth for the product, moment, squared-critic, and squared-candidate pair classes.
Definition (Lean source)
parameters
assumes
HF :
∃ K : ℕ,
max δ_n (regime.HF_pair_const * regime.H_diameter * δ_n) ≤ δ_n * (2 : ℝ) ^ K ∧
+ 8 * regime.bundle_HF.regime.b * log (2 * ((K : ℝ) + 1) / eta) / (n * δ_n)
≤ δ_n
Fixed-level peeling floor for product-class pair deviations.
mF :
∃ K : ℕ,
max δ_n (regime.mF_L2_const * regime.F_diameter) ≤ δ_n * (2 : ℝ) ^ K ∧
+ 8 * regime.bundle_mF.regime.b * log (2 * ((K : ℝ) + 1) / eta) / (n * δ_n)
≤ δ_n
Fixed-level peeling floor for moment-class pair deviations.
theorem peelingFloor_quarter_of_unit_scale reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
For a localized regime at unit radius with at least thirty-two observations, zero envelope constants for all four classes, and unit upper bounds on the four peeled radii, the quarter-confidence peeling floor is inhabited.
Formal statement
hypotheses
TC :
β lambda :
n :
ℕ
regime :
LocalizedRegimes S TC sample sc tb n 1
hn :
32 ≤ n
hb_HF :
regime.bundle_HF.regime.b = 0
hb_mF :
regime.bundle_mF.regime.b = 0
hb_F :
regime.bundle_F.regime.b = 0
hb_H :
regime.bundle_H.regime.b = 0
hR_HF :
regime.HF_pair_const * regime.H_diameter ≤ 1
hR_mF :
regime.mF_L2_const * regime.F_diameter ≤ 1
hR_F :
regime.F_L2_const * regime.F_diameter ≤ 1
hR_H :
regime.H_diameter ≤ 1
conclusion
PeelingFloor regime (1 / 4)
Proof (Lean source)
theorem peelingFloor_quarter_of_unit_scale
{S : OperatorSystem Ω μ} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Ω S.𝒲 μ P_W}
{β lambda : ℝ}
{sc : SourceCondition S β}
{tb : TikhonovBiasBoundAt S β lambda sc}
{n : ℕ}
(regime : LocalizedRegimes S TC sample sc tb n 1)
(hn : 32 ≤ n)
(hb_HF : regime.bundle_HF.regime.b = 0)
(hb_mF : regime.bundle_mF.regime.b = 0)
(hb_F : regime.bundle_F.regime.b = 0)
(hb_H : regime.bundle_H.regime.b = 0)
(hR_HF : regime.HF_pair_const * regime.H_diameter ≤ 1)
(hR_mF : regime.mF_L2_const * regime.F_diameter ≤ 1)
(hR_F : regime.F_L2_const * regime.F_diameter ≤ 1)
(hR_H : regime.H_diameter ≤ 1) :
PeelingFloor regime (1 / 4) := by
refine ⟨?_, ?_, ?_, ?_⟩
· refine ⟨0, ?_, ?_⟩
· norm_num [max_le_iff, hR_HF]
· simpa [hb_HF] using quarter_unit_peeling_slack hn
· refine ⟨0, ?_, ?_⟩
· norm_num [max_le_iff, hR_mF]
· simpa [hb_mF] using quarter_unit_peeling_slack hn
· refine ⟨0, ?_, ?_⟩
· norm_num [max_le_iff, hR_F]
· simpa [hb_F] using quarter_unit_peeling_slack hn
· refine ⟨0, ?_, ?_⟩
· norm_num [max_le_iff, hR_H]
· simpa [hb_H] using quarter_unit_peeling_slack hn
LocalizedEventsBase 2 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.
def npivBousquetSlack reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Given an envelope bound, localization radius, critical radius, log-confidence budget, and sample size, the NPIV fixed-radius Bousquet slack is the variance-sensitive square-root term plus its linear correction.
Definition (Lean source)
parameters
b r crit x n :
ℝ
def
npivBousquetSlack b r crit x n :
ℝ
given by
2 * sqrt ((r ^ 2 + 8 * b * r * crit) * x / n) + 8 * b * x / n
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. If there is a dyadic level K with Rmax ≤ δ_n · 2 ^ K whose 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 10 * δ_n * norm + 5 * δ_n ^ 2.
Formal statement
hypotheses
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
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)
(hslack : ∃ K : ℕ,
Rmax ≤ δ_n * (2 : ℝ) ^ K ∧
2 * sqrt
((1 + 8 * B.regime.b) * log (2 * ((K : ℝ) + 1) / ζ) / n)
+ 8 * B.regime.b * log (2 * ((K : ℝ) + 1) / ζ) / (n * δ_n)
≤ δ_n) :
∃ 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 ω')) ∂μ|
≤ 10 * δ_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_peeled B.F B.norm P_W B.X B.X_meas B.F_meas
B.norm_nonneg B.regime hζ_pos hζ_le n hn (ρ := δ_n) (Rmax := Rmax)
B.crit_le hδn_pos B.crit_pos
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
Algebra 1 core · 2 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. The mixed sum δ · (R + w + δ) + R · κ is bounded above by the quadratic envelope R² + δ · w + (3/2) · δ² + (1/2) · κ².
Formal statement
hypotheses
R δ w κ :
ℝ
conclusion
δ * (R + w + δ) + R * κ ≤ R ^ 2 + δ * w + (3 / 2) * δ ^ 2 + (1 / 2) * κ ^ 2
Proof (Lean source)
lemma young_cross_envelope (R δ w κ : ℝ) :
δ * (R + w + δ) + R * κ
≤ R ^ 2 + δ * w + (3 / 2) * δ ^ 2 + (1 / 2) * κ ^ 2 := by
nlinarith [sq_nonneg (R - δ), sq_nonneg (R - κ)]
2 supporting declarations (lemmas, instances)
-
measure_iInter_nat_ge_one_sub_tsum_of_gelemma — If every measurable 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 the 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 -
measure_inter_ge_one_sub_add_of_gelemma — If two measurable events have failure probabilities bounded by a and b, then their intersection has failure probability at most a + b.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
EPMasterEvent_Part1 1 core · 5 supporting This first implementation part relates closedness witnesses to population weak norms and compares population regularized objectives with fold-A empirical objectives. ★ empirical_critic_argmax_localized
Deterministic comparisons for the empirical-process master event
This first implementation part relates closedness witnesses to population weak norms and compares population regularized objectives with fold-A empirical objectives. These deterministic inequalities feed the localized event assembly in the second part.
lemma empirical_critic_argmax_localized reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
For a probability space, an instrumental-variables operator system, its primal function classes, an observed-data law, an independent sample, and a sample split, a regularization level and candidate structural function, membership of that candidate in the structural class, a population closedness critic, membership of that critic in the critic class, an empirical critic, membership of the empirical critic in the critic class, a sample size, population state, and nonnegative localization allowance, the closedness identity, empirical optimality of the empirical critic, and a bound on the population-to- empirical objective discrepancy, the empirical critic lies within squared population distance equal to the localization allowance of the closedness critic.
Formal statement
hypotheses
TC :
split :
OneShotSplit sample
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
conclusion
‖S.qL2 (TC.F_subset hf_closed) - S.qL2 (TC.F_subset hf_emp)‖ ^ 2 ≤ R
Proof (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]
5 supporting declarations (lemmas, instances)
-
population_inner_eq_weakNorm_sqlemma — For a candidate in the primal class and a critic in the critic class, if the critic represents the image of the primal error under the inverse-problem operator, then the population adversarial value equals the squared weak norm of that error.hypothesesTC :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 population_inner_eq_weakNorm_sq {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 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) 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) 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 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] have h_qL2_self : inner ℝ (S.qL2 (TC.F_subset hf)) (S.qL2 (TC.F_subset hf)) = ∫ ω, (f (S.zOf (S.W ω))) ^ 2 ∂μ := by change inner ℝ ((S.qL2 (TC.F_subset hf) : S.InstrumentL2) : Lp ℝ 2 μ) ((S.qL2 (TC.F_subset hf) : S.InstrumentL2) : Lp ℝ 2 μ) = _ 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] 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] 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] rw [h_weak_eq_intf] linarith [h_diff_eq_int_fsq] -
population_inner_le_weaklemma — Population adversarial inner objectives are bounded by the weak residual norm squared. This is the deterministic inequality 2⟨a,q⟩ - ‖q‖² ≤ ‖a‖², written in the NPIV integral notation.hypothesesTC :h :S.𝒳 → ℝhh :h ∈ TC.Hf :S.𝒵 → ℝhf :f ∈ TC.Fconclusion2 * (∫ ω, 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 population_inner_le_weak {S : OperatorSystem Ω μ} {TC : TRAEClasses S} [IsProbabilityMeasure μ] {h : S.𝒳 → ℝ} (hh : h ∈ TC.H) {f : S.𝒵 → ℝ} (hf : f ∈ TC.F) : 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 let a := S.T (S.hL2 S.h₀_mem - S.hL2 (TC.H_subset hh)) let q := S.qL2 (TC.F_subset hf) have h_inner_int : inner ℝ a q = ∫ ω, (S.h₀ (S.xOf (S.W ω)) - h (S.xOf (S.W ω))) * f (S.zOf (S.W ω)) ∂μ := by simpa [a, q] using S.T_inner_eq_integral S.h₀_mem (TC.H_subset hh) (TC.F_subset hf) 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) 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 have h_diff_eq_inner : (∫ ω, S.m (S.W ω) f ∂μ) - ∫ ω, h (S.xOf (S.W ω)) * f (S.zOf (S.W ω)) ∂μ = inner ℝ a q := by rw [h_moment, h_inner_int, h_int_diff] have h_qL2_self : inner ℝ q q = ∫ ω, (f (S.zOf (S.W ω))) ^ 2 ∂μ := by change inner ℝ (q : Lp ℝ 2 μ) (q : Lp ℝ 2 μ) = _ rw [MeasureTheory.L2.inner_def] refine integral_congr_ae ?_ filter_upwards [(S.toQbarL2 f (TC.F_subset hf)).coeFn_toLp] with ω hω simp [q, OperatorSystem.qL2, hω, pow_two] have hweak : (S.weakNorm (S.hL2 (TC.H_subset hh) - S.hL2 S.h₀_mem)) ^ 2 = ‖a‖ ^ 2 := by rw [OperatorSystem.weakNorm, S.T_sub] have hneg : S.T (S.hL2 (TC.H_subset hh)) - S.T (S.hL2 S.h₀_mem) = -a := by dsimp [a] rw [S.T_sub] abel rw [hneg, norm_neg] have hhilbert : 2 * inner ℝ a q - inner ℝ q q ≤ ‖a‖ ^ 2 := by have hsq : 0 ≤ ‖a - q‖ ^ 2 := sq_nonneg ‖a - q‖ rw [norm_sub_sq_real] at hsq have hqnorm : inner ℝ q q = ‖q‖ ^ 2 := real_inner_self_eq_norm_sq q nlinarith rw [hweak] nlinarith [h_diff_eq_inner, h_qL2_self, hhilbert] -
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.hypothesesTC :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 change _ = ‖qc - q‖ ^ 2 rw [hclosed, hf_eq, norm_sub_sq_real] 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 nlinarith [hqc_self, hq_self] -
population_regularized_le_innerObjective_add_deviationlemma — Given a nonparametric instrumental-variables system, sample split, regularization level, candidate functions, sample size, observation, and three deviation bounds, if the empirical moment deviation is bounded, the empirical cross-product deviation is bounded, and the empirical squared-instrument deviation is bounded, then the population regularized objective is at most the empirical inner objective plus the stated combined deviation.hypothesessplit :OneShotSplit samplelambda :ℝh :S.𝒳 → ℝf :S.𝒵 → ℝn :ℕω :ΩRm RHF RF :ℝhmF :|((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), S.m (sample.Z (k : ℕ) ω) f- ∫ ω', S.m (S.W ω') f ∂μ|≤ RmhHF :|((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), h (S.xOf (sample.Z (k : ℕ) ω)) * f (S.zOf (sample.Z (k : ℕ) ω))- ∫ ω', h (S.xOf (S.W ω')) * f (S.zOf (S.W ω')) ∂μ|≤ RHFhF :|((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (f (S.zOf (sample.Z (k : ℕ) ω))) ^ 2- ∫ ω', (f (S.zOf (S.W ω'))) ^ 2 ∂μ|≤ RFconclusion2 * (∫ ω', S.m (S.W ω') f ∂μ)- 2 * (∫ ω', h (S.xOf (S.W ω')) * f (S.zOf (S.W ω')) ∂μ)- ∫ ω', (f (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 n ω + (2 * Rm + 2 * RHF + RF)Proof (Lean source)
lemma population_regularized_le_innerObjective_add_deviation {S : OperatorSystem Ω μ} {P_W : Measure S.𝒲} {sample : IIDSample Ω S.𝒲 μ P_W} (split : OneShotSplit sample) (lambda : ℝ) (h : S.𝒳 → ℝ) (f : S.𝒵 → ℝ) (n : ℕ) (ω : Ω) {Rm RHF RF : ℝ} (hmF : |((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), S.m (sample.Z (k : ℕ) ω) f - ∫ ω', S.m (S.W ω') f ∂μ| ≤ Rm) (hHF : |((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), h (S.xOf (sample.Z (k : ℕ) ω)) * f (S.zOf (sample.Z (k : ℕ) ω)) - ∫ ω', h (S.xOf (S.W ω')) * f (S.zOf (S.W ω')) ∂μ| ≤ RHF) (hF : |((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (f (S.zOf (sample.Z (k : ℕ) ω))) ^ 2 - ∫ ω', (f (S.zOf (S.W ω'))) ^ 2 ∂μ| ≤ RF) : 2 * (∫ ω', S.m (S.W ω') f ∂μ) - 2 * (∫ ω', h (S.xOf (S.W ω')) * f (S.zOf (S.W ω')) ∂μ) - ∫ ω', (f (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 n ω + (2 * Rm + 2 * RHF + RF) := by let mEmp : ℝ := ((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), S.m (sample.Z (k : ℕ) ω) f let mPop : ℝ := ∫ ω', S.m (S.W ω') f ∂μ let hfEmp : ℝ := ((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), h (S.xOf (sample.Z (k : ℕ) ω)) * f (S.zOf (sample.Z (k : ℕ) ω)) let hfPop : ℝ := ∫ ω', h (S.xOf (S.W ω')) * f (S.zOf (S.W ω')) ∂μ let fEmp : ℝ := ((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (f (S.zOf (sample.Z (k : ℕ) ω))) ^ 2 let fPop : ℝ := ∫ ω', (f (S.zOf (S.W ω'))) ^ 2 ∂μ let hReg : ℝ := lambda * (((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (h (S.xOf (sample.Z (k : ℕ) ω))) ^ 2) have hm_abs : -Rm ≤ mEmp - mPop ∧ mEmp - mPop ≤ Rm := by simpa [mEmp, mPop] using abs_le.mp hmF have hHF_abs : -RHF ≤ hfEmp - hfPop ∧ hfEmp - hfPop ≤ RHF := by simpa [hfEmp, hfPop] using abs_le.mp hHF have hF_abs : -RF ≤ fEmp - fPop ∧ fEmp - fPop ≤ RF := by simpa [fEmp, fPop] using abs_le.mp hF have hinner : innerObjective S sample split lambda h f n ω = 2 * mEmp - 2 * hfEmp - fEmp + hReg := by rw [innerObjective_eq_fin_sum] have hsum : (∑ k : Fin (split.n₁ n), innerIntegrand S lambda h f (sample.Z (k : ℕ) ω)) = 2 * (∑ k : Fin (split.n₁ n), S.m (sample.Z (k : ℕ) ω) f) - 2 * (∑ k : Fin (split.n₁ n), h (S.xOf (sample.Z (k : ℕ) ω)) * f (S.zOf (sample.Z (k : ℕ) ω))) - (∑ k : Fin (split.n₁ n), (f (S.zOf (sample.Z (k : ℕ) ω))) ^ 2) + lambda * (∑ k : Fin (split.n₁ n), (h (S.xOf (sample.Z (k : ℕ) ω))) ^ 2) := by simp only [innerIntegrand, Finset.sum_add_distrib, Finset.sum_sub_distrib] abel_nf simp_rw [← Finset.mul_sum] rw [Finset.sum_add_distrib] rw [← Finset.smul_sum] abel_nf ring_nf rw [hsum] simp only [mEmp, hfEmp, fEmp, hReg] ring_nf rw [hinner] dsimp [mPop, hfPop, fPop, hReg] nlinarith [hm_abs.1, hm_abs.2, hHF_abs.1, hHF_abs.2, hF_abs.1, hF_abs.2] -
innerObjective_le_population_regularized_add_deviationlemma — Given a nonparametric instrumental-variables system, sample split, regularization level, candidate functions, sample size, observation, and three deviation bounds, if the empirical moment deviation is bounded, the empirical cross-product deviation is bounded, and the empirical squared-instrument deviation is bounded, then the empirical inner objective is at most the population regularized objective plus the stated combined deviation.hypothesessplit :OneShotSplit samplelambda :ℝh :S.𝒳 → ℝf :S.𝒵 → ℝn :ℕω :ΩRm RHF RF :ℝhmF :|((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), S.m (sample.Z (k : ℕ) ω) f- ∫ ω', S.m (S.W ω') f ∂μ|≤ RmhHF :|((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), h (S.xOf (sample.Z (k : ℕ) ω)) * f (S.zOf (sample.Z (k : ℕ) ω))- ∫ ω', h (S.xOf (S.W ω')) * f (S.zOf (S.W ω')) ∂μ|≤ RHFhF :|((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (f (S.zOf (sample.Z (k : ℕ) ω))) ^ 2- ∫ ω', (f (S.zOf (S.W ω'))) ^ 2 ∂μ|≤ RFconclusioninnerObjective S sample split lambda h f n ω≤ 2 * (∫ ω', S.m (S.W ω') f ∂μ)- 2 * (∫ ω', h (S.xOf (S.W ω')) * f (S.zOf (S.W ω')) ∂μ)- ∫ ω', (f (S.zOf (S.W ω'))) ^ 2 ∂μ+ lambda * (((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (h (S.xOf (sample.Z (k : ℕ) ω))) ^ 2)+ (2 * Rm + 2 * RHF + RF)Proof (Lean source)
lemma innerObjective_le_population_regularized_add_deviation {S : OperatorSystem Ω μ} {P_W : Measure S.𝒲} {sample : IIDSample Ω S.𝒲 μ P_W} (split : OneShotSplit sample) (lambda : ℝ) (h : S.𝒳 → ℝ) (f : S.𝒵 → ℝ) (n : ℕ) (ω : Ω) {Rm RHF RF : ℝ} (hmF : |((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), S.m (sample.Z (k : ℕ) ω) f - ∫ ω', S.m (S.W ω') f ∂μ| ≤ Rm) (hHF : |((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), h (S.xOf (sample.Z (k : ℕ) ω)) * f (S.zOf (sample.Z (k : ℕ) ω)) - ∫ ω', h (S.xOf (S.W ω')) * f (S.zOf (S.W ω')) ∂μ| ≤ RHF) (hF : |((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (f (S.zOf (sample.Z (k : ℕ) ω))) ^ 2 - ∫ ω', (f (S.zOf (S.W ω'))) ^ 2 ∂μ| ≤ RF) : innerObjective S sample split lambda h f n ω ≤ 2 * (∫ ω', S.m (S.W ω') f ∂μ) - 2 * (∫ ω', h (S.xOf (S.W ω')) * f (S.zOf (S.W ω')) ∂μ) - ∫ ω', (f (S.zOf (S.W ω'))) ^ 2 ∂μ + lambda * (((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (h (S.xOf (sample.Z (k : ℕ) ω))) ^ 2) + (2 * Rm + 2 * RHF + RF) := by let mEmp : ℝ := ((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), S.m (sample.Z (k : ℕ) ω) f let mPop : ℝ := ∫ ω', S.m (S.W ω') f ∂μ let hfEmp : ℝ := ((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), h (S.xOf (sample.Z (k : ℕ) ω)) * f (S.zOf (sample.Z (k : ℕ) ω)) let hfPop : ℝ := ∫ ω', h (S.xOf (S.W ω')) * f (S.zOf (S.W ω')) ∂μ let fEmp : ℝ := ((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (f (S.zOf (sample.Z (k : ℕ) ω))) ^ 2 let fPop : ℝ := ∫ ω', (f (S.zOf (S.W ω'))) ^ 2 ∂μ let hReg : ℝ := lambda * (((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n), (h (S.xOf (sample.Z (k : ℕ) ω))) ^ 2) have hm_abs : -Rm ≤ mEmp - mPop ∧ mEmp - mPop ≤ Rm := by simpa [mEmp, mPop] using abs_le.mp hmF have hHF_abs : -RHF ≤ hfEmp - hfPop ∧ hfEmp - hfPop ≤ RHF := by simpa [hfEmp, hfPop] using abs_le.mp hHF have hF_abs : -RF ≤ fEmp - fPop ∧ fEmp - fPop ≤ RF := by simpa [fEmp, fPop] using abs_le.mp hF have hinner : innerObjective S sample split lambda h f n ω = 2 * mEmp - 2 * hfEmp - fEmp + hReg := by rw [innerObjective_eq_fin_sum] have hsum : (∑ k : Fin (split.n₁ n), innerIntegrand S lambda h f (sample.Z (k : ℕ) ω)) = 2 * (∑ k : Fin (split.n₁ n), S.m (sample.Z (k : ℕ) ω) f) - 2 * (∑ k : Fin (split.n₁ n), h (S.xOf (sample.Z (k : ℕ) ω)) * f (S.zOf (sample.Z (k : ℕ) ω))) - (∑ k : Fin (split.n₁ n), (f (S.zOf (sample.Z (k : ℕ) ω))) ^ 2) + lambda * (∑ k : Fin (split.n₁ n), (h (S.xOf (sample.Z (k : ℕ) ω))) ^ 2) := by simp only [innerIntegrand, Finset.sum_add_distrib, Finset.sum_sub_distrib] abel_nf simp_rw [← Finset.mul_sum] rw [Finset.sum_add_distrib] rw [← Finset.smul_sum] abel_nf ring_nf rw [hsum] simp only [mEmp, hfEmp, fEmp, hReg] ring_nf rw [hinner] dsimp [mPop, hfPop, fPop, hReg] nlinarith [hm_abs.1, hm_abs.2, hHF_abs.1, hHF_abs.2, hF_abs.1, hF_abs.2]
EPMasterEvent_Part2 1 core · 1 supporting This second implementation part turns componentwise H·F, m·F, and F² deviation bounds into the critic comparison and intersects their events over sample sizes. ★ ep_master_event_from_localized
Localized assembly of the empirical-process master event
This second implementation part turns componentwise H·F, m·F, and F²
deviation bounds into the critic comparison and intersects their events over
sample sizes. The resulting master event supplies the explicit objective gap
used by EPPerN.
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
TC :
split :
OneShotSplit sample
lambda β :
ℝ
delta :
ℕ → ℝ
h_hat :
ℕ → Ω → S.𝒳 → ℝ
is_estimator :
IsTRAEPrimalEstimator S TC sample split lambda h_hat
sc :
SourceCondition S β
tb :
TikhonovBiasBoundAt 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 Ω,
MeasurableSet Aζ_master
μ Aζ_master ≥ 1 - ofReal ζ
conclusion 1
ω ∈ 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 * npivBousquetSlack (regimes n).bundle_HF.regime.b (delta n) (criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n))) (log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n) + 4 * npivBousquetSlack (regimes n).bundle_mF.regime.b (delta n) (criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n))) (log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n) + 2 * npivBousquetSlack (regimes n).bundle_F.regime.b (delta n) (criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n))) (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 : TikhonovBiasBoundAt 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 * npivBousquetSlack (regimes n).bundle_HF.regime.b (delta n)
(criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n)))
(log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n)
+ 4 * npivBousquetSlack (regimes n).bundle_mF.regime.b (delta n)
(criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n)))
(log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n)
+ 2 * npivBousquetSlack (regimes n).bundle_F.regime.b (delta n)
(criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n)))
(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))
-- … truncated; follow the source link for the rest …
1 supporting declaration (lemmas, instances)
-
empirical_critic_argmax_localized_from_componentslemma — Componentwise version of empirical_critic_argmax_localized.hypothesesTC :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 · 0 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). This pure analytic step uses a localized-regime bundle at the fold-A sample size 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
TC :
split :
OneShotSplit sample
lambda β :
ℝ
delta :
ℕ → ℝ
h_hat :
ℕ → Ω → S.𝒳 → ℝ
is_estimator :
IsTRAEPrimalEstimator S TC sample split lambda h_hat
sc :
SourceCondition S β
tb :
TikhonovBiasBoundAt S β lambda sc
regimes :
∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta 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 * npivBousquetSlack (regimes n).bundle_HF.regime.b (delta n) (criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n))) (log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n) + 4 * npivBousquetSlack (regimes n).bundle_mF.regime.b (delta n) (criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n))) (log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n) + 2 * npivBousquetSlack (regimes n).bundle_F.regime.b (delta n) (criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n))) (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 * npivBousquetSlack (regimes n).bundle_HF.regime.b (delta n) (criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n))) (log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n) + 4 * npivBousquetSlack (regimes n).bundle_mF.regime.b (delta n) (criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n))) (log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n) + 2 * npivBousquetSlack (regimes n).bundle_F.regime.b (delta n) (criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n))) (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 : TikhonovBiasBoundAt S β lambda sc)
[IsProbabilityMeasure μ]
(regimes : ∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta 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 * npivBousquetSlack (regimes n).bundle_HF.regime.b (delta n)
(criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n)))
(log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n)
+ 4 * npivBousquetSlack (regimes n).bundle_mF.regime.b (delta n)
(criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n)))
(log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n)
+ 2 * npivBousquetSlack (regimes n).bundle_F.regime.b (delta n)
(criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n)))
(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 * npivBousquetSlack (regimes n).bundle_HF.regime.b (delta n)
(criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n)))
(log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n)
+ 4 * npivBousquetSlack (regimes n).bundle_mF.regime.b (delta n)
(criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n)))
(log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n)
+ 2 * npivBousquetSlack (regimes n).bundle_F.regime.b (delta n)
(criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n)))
(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
TC :
split :
OneShotSplit sample
lambda β :
ℝ
delta :
ℕ → ℝ
h_hat :
ℕ → Ω → S.𝒳 → ℝ
IsTRAEPrimalEstimator S TC sample split lambda h_hat
sc :
SourceCondition S β
tb :
TikhonovBiasBoundAt 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 Ω,
MeasurableSet Aζ_ep
μ Aζ_ep ≥ 1 - ofReal ζ
conclusion 1
ω ∈ 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 * npivBousquetSlack (regimes n).bundle_HF.regime.b (delta n) (criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n))) (log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n) + 4 * npivBousquetSlack (regimes n).bundle_mF.regime.b (delta n) (criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n))) (log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n) + 2 * npivBousquetSlack (regimes n).bundle_F.regime.b (delta n) (criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n))) (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 : TikhonovBiasBoundAt 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 * npivBousquetSlack (regimes n).bundle_HF.regime.b (delta n)
(criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n)))
(log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n)
+ 4 * npivBousquetSlack (regimes n).bundle_mF.regime.b (delta n)
(criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n)))
(log (4 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n)
+ 2 * npivBousquetSlack (regimes n).bundle_F.regime.b (delta n)
(criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n)))
(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
n ω (hAζ_payload ω hω n hn)
EventAssembly 1 core · 0 supporting Assembles the localized empirical-process and centered-regularizer events for the earlier simultaneous-in-sample-size NPIV route. ★ empirical_process_event_from_localized
Assembles the localized empirical-process and centered-regularizer events for
the earlier simultaneous-in-sample-size NPIV route. The current fixed-sample
rate uses per_sample_empirical_process_event instead.
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
TC :
split :
OneShotSplit sample
lambda β :
ℝ
delta :
ℕ → ℝ
h_hat :
ℕ → Ω → S.𝒳 → ℝ
IsTRAEPrimalEstimator S TC sample split lambda h_hat
sc :
SourceCondition S β
tb :
TikhonovBiasBoundAt S β lambda sc
regimes :
∀ n, LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n)
lambda_nonneg :
0 ≤ lambda
ζ :
ℝ
0 < ζ
ζ < 1
conclusion
conclusion 1
ω ∈ 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 * npivBousquetSlack (regimes n).bundle_HF.regime.b (delta n) (criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n))) (log (8 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n) + 4 * npivBousquetSlack (regimes n).bundle_mF.regime.b (delta n) (criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n))) (log (8 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n) + 2 * npivBousquetSlack (regimes n).bundle_F.regime.b (delta n) (criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n))) (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)) + npivBousquetSlack (regimes n).bundle_H.regime.b ((regimes n).H_diameter + delta n) (criticalRadius ((regimes n).bundle_H.regime.ψ (split.n₁ n))) (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 : TikhonovBiasBoundAt 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 * npivBousquetSlack (regimes n).bundle_HF.regime.b (delta n)
(criticalRadius ((regimes n).bundle_HF.regime.ψ (split.n₁ n)))
(log (8 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n)
+ 4 * npivBousquetSlack (regimes n).bundle_mF.regime.b (delta n)
(criticalRadius ((regimes n).bundle_mF.regime.ψ (split.n₁ n)))
(log (8 * (2 : ℝ) ^ (n + 1) / ζ)) (split.n₁ n)
+ 2 * npivBousquetSlack (regimes n).bundle_F.regime.b (delta n)
(criticalRadius ((regimes n).bundle_F.regime.ψ (split.n₁ n)))
(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))
+ npivBousquetSlack (regimes n).bundle_H.regime.b
((regimes n).H_diameter + delta n)
(criticalRadius ((regimes n).bundle_H.regime.ψ (split.n₁ n)))
(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
simp only [npivBousquetSlack] at hD ⊢
nlinarith [hD, hC_upper]
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], a fixed-level peeling floor, 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
TC :
β lambda :
n :
ℕ
δ_n :
ℝ
regime :
LocalizedRegimes S TC sample sc tb n δ_n
hn :
0 < n
δ :
ℝ
hδ_pos :
0 < δ
hδ_le :
δ ≤ 1
floor :
PeelingFloor regime δ
conclusion
conclusion 1
ω ∈ 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) ∂μ|
≤ 10 * regime.F_L2_const * ‖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 : TikhonovBiasBoundAt S β lambda sc}
{n : ℕ} {δ_n : ℝ}
(regime : LocalizedRegimes S TC sample sc tb n δ_n)
(hn : 0 < n)
{δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1)
(floor : PeelingFloor regime δ) :
∃ 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) ∂μ|
≤ 10 * regime.F_L2_const *
‖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 hslack : ∃ K : ℕ,
Rmax ≤ δ_n * (2 : ℝ) ^ K ∧
2 * sqrt
((1 + 8 * B.regime.b) * log (2 * ((K : ℝ) + 1) / δ) / n)
+ 8 * B.regime.b * log (2 * ((K : ℝ) + 1) / δ) / (n * δ_n)
≤ δ_n := by
simpa [B, Rmax] using floor.F
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 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.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) ∂μ|
≤ 10 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2 := by
simpa [B, i, heval_sample, heval_pop] using hdev
have hrate :
10 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2
≤ 10 * 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 ≤ 10 * δ_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.hypothesesTC :β lambda :n :ℕδ_n :ℝregime :LocalizedRegimes S TC sample sc tb n δ_nhn :0 < nδ :ℝhδ_pos :0 < δhδ_le :δ ≤ 1conclusionconclusion 1ω ∈ 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)+ 2 * sqrt ((δ_n ^ 2 + 8 * regime.bundle_F.regime.b * δ_n * criticalRadius (regime.bundle_F.regime.ψ n)) * log (1 / δ) / n)+ 8 * regime.bundle_F.regime.b * log (1 / δ) / nProof (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 : TikhonovBiasBoundAt 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) + 2 * sqrt ((δ_n ^ 2 + 8 * regime.bundle_F.regime.b * δ_n * criticalRadius (regime.bundle_F.regime.ψ n)) * log (1 / δ) / n) + 8 * regime.bundle_F.regime.b * 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.norm_nonneg B.regime hδ_pos hδ_le n hn B.crit_le B.crit_pos (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.hypothesesTC :β lambda :n :ℕδ_n :ℝregime :LocalizedRegimes S TC sample sc tb n δ_nhn :0 < nδ :ℝhδ_pos :0 < δhδ_le :δ ≤ 1conclusionconclusion 1ω ∈ E :f₁ :_hf₁ :f₁ ∈ TC.Ff₂ :_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)+ 2 * sqrt (((regime.F_L2_const * regime.F_diameter) ^ 2 + 8 * regime.bundle_F.regime.b * (regime.F_L2_const * regime.F_diameter) * criticalRadius (regime.bundle_F.regime.ψ n)) * log (1 / δ) / n)+ 8 * regime.bundle_F.regime.b * log (1 / δ) / nProof (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 : TikhonovBiasBoundAt 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) + 2 * sqrt (((regime.F_L2_const * regime.F_diameter) ^ 2 + 8 * regime.bundle_F.regime.b * (regime.F_L2_const * regime.F_diameter) * criticalRadius (regime.bundle_F.regime.ψ n)) * log (1 / δ) / n) + 8 * regime.bundle_F.regime.b * 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.norm_nonneg B.regime hδ_pos hδ_le n hn hr_lb B.crit_pos (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.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 · 1 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
TC :
β lambda :
n :
ℕ
δ_n :
ℝ
regime :
LocalizedRegimes S TC sample sc tb n δ_n
hn :
0 < n
δ :
ℝ
hδ_pos :
0 < δ
hδ_le :
δ ≤ 1
conclusion
conclusion 1
ω ∈ 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)
+ 2 * sqrt (((regime.H_diameter + δ_n) ^ 2 + 8 * regime.bundle_H.regime.b * (regime.H_diameter + δ_n) * criticalRadius (regime.bundle_H.regime.ψ n)) * log (1 / δ) / n)
+ 8 * regime.bundle_H.regime.b * log (1 / δ) / 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 : TikhonovBiasBoundAt 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)
+ 2 * sqrt
(((regime.H_diameter + δ_n) ^ 2 +
8 * regime.bundle_H.regime.b * (regime.H_diameter + δ_n) *
criticalRadius (regime.bundle_H.regime.ψ n)) *
log (1 / δ) / n)
+ 8 * regime.bundle_H.regime.b * 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.norm_nonneg B.regime
hδ_pos hδ_le n hn hr_lb B.crit_pos
(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
1 supporting declaration (lemmas, instances)
-
localized_omega_event_for_H_pair_peeledlemma — Given a positive sample size, a confidence level in (0,1], a localized NPIV regime, and its fixed-level peeling floor, there is one event of probability at least 1 - delta on which every squared-candidate empirical-process difference is bounded by 10 * delta_n * strongNorm(h₁-h₂) + 5 * delta_n².hypothesesTC :β lambda :n :ℕδ_n :ℝregime :LocalizedRegimes S TC sample sc tb n δ_nhn :0 < nδ :ℝhdelta_pos :0 < δhdelta_le :δ ≤ 1floor :PeelingFloor regime δProof (Lean source)
lemma localized_omega_event_for_H_pair_peeled {S : OperatorSystem Ω μ} {TC : TRAEClasses S} {P_W : Measure S.𝒲} {sample : IIDSample Ω S.𝒲 μ P_W} [IsProbabilityMeasure μ] {β lambda : ℝ} {sc : SourceCondition S β} {tb : TikhonovBiasBoundAt S β lambda sc} {n : ℕ} {δ_n : ℝ} (regime : LocalizedRegimes S TC sample sc tb n δ_n) (hn : 0 < n) {δ : ℝ} (hdelta_pos : 0 < δ) (hdelta_le : δ ≤ 1) (floor : PeelingFloor regime δ) : ∃ 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 ∂μ)| ≤ 10 * δ_n * S.strongNorm (S.hL2 (TC.H_subset hh₁) - S.hL2 (TC.H_subset hh₂)) + 5 * δ_n ^ 2 := by classical let B := regime.bundle_H let Rmax : ℝ := max δ_n regime.H_diameter have hdelta_n_pos : 0 < δ_n := lt_of_lt_of_le B.crit_pos B.crit_le have hslack : ∃ K : ℕ, Rmax ≤ δ_n * (2 : ℝ) ^ K ∧ 2 * sqrt ((1 + 8 * B.regime.b) * log (2 * ((K : ℝ) + 1) / δ) / n) + 8 * B.regime.b * log (2 * ((K : ℝ) + 1) / δ) / (n * δ_n) ≤ δ_n := by simpa [B, Rmax] using floor.H obtain ⟨E, hE_meas, hE_mass, hE⟩ := localized_omega_event_sharp_for_bundle (S := S) (P_W := P_W) (sample := sample) (B := B) regime.law_W hn hdelta_pos hdelta_le hdelta_n_pos hslack refine ⟨E, hE_meas, hE_mass, ?_⟩ intro ω hω h₁ hh₁ h₂ hh₂ let i : B.ι := regime.interp_H_idx h₁ h₂ hh₁ hh₂ let gap : ℝ := S.strongNorm (S.hL2 (TC.H_subset hh₁) - S.hL2 (TC.H_subset hh₂)) have hi_gap : B.norm (B.F i) ≤ gap := by simpa [B, i, gap] using regime.interp_H_norm h₁ h₂ hh₁ hh₂ have hi_Rmax : B.norm (B.F i) ≤ Rmax := by exact hi_gap.trans <| (regime.H_diameter_bound h₁ h₂ hh₁ hh₂).trans (le_max_right _ _) have hdev := hE ω hω i hi_Rmax have hdev' : |(n : ℝ)⁻¹ * ∑ k : Fin n, B.F i (B.X (sample.Z k ω)) - ∫ ω', B.F i (B.X (S.W ω')) ∂μ| ≤ 10 * δ_n * gap + 5 * δ_n ^ 2 := by have hcoeff : 0 ≤ 10 * δ_n := mul_nonneg (by norm_num) hdelta_n_pos.le have hmul := mul_le_mul_of_nonneg_left hi_gap hcoeff nlinarith have heval_sample : (∑ 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 hsq₁_int : Integrable (fun ω' => (h₁ (S.xOf (S.W ω'))) ^ 2) μ := (S.toHbarL2 h₁ (TC.H_subset hh₁)).integrable_sq have hsq₂_int : Integrable (fun ω' => (h₂ (S.xOf (S.W ω'))) ^ 2) μ := (S.toHbarL2 h₂ (TC.H_subset hh₂)).integrable_sq rw [heval_sample, heval_pop, integral_sub hsq₁_int hsq₂_int, Finset.sum_sub_distrib, mul_sub] at hdev' simpa [gap] 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], a fixed-level peeling floor, 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
TC :
β lambda :
n :
ℕ
δ_n :
ℝ
regime :
LocalizedRegimes S TC sample sc tb n δ_n
hn :
0 < n
δ :
ℝ
hδ_pos :
0 < δ
hδ_le :
δ ≤ 1
floor :
PeelingFloor regime δ
conclusion
conclusion 1
ω ∈ 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 ω')) ∂μ|
≤ 10 * 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 : TikhonovBiasBoundAt S β lambda sc}
{n : ℕ} {δ_n : ℝ}
(regime : LocalizedRegimes S TC sample sc tb n δ_n)
(hn : 0 < n)
{δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1)
(floor : PeelingFloor regime δ) :
∃ 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 ω')) ∂μ|
≤ 10 * 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 hslack : ∃ K : ℕ,
Rmax ≤ δ_n * (2 : ℝ) ^ K ∧
2 * sqrt
((1 + 8 * B.regime.b) * log (2 * ((K : ℝ) + 1) / δ) / n)
+ 8 * B.regime.b * log (2 * ((K : ℝ) + 1) / δ) / (n * δ_n)
≤ δ_n := by
simpa [B, Rmax] using floor.HF
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 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 ω')) ∂μ|
≤ 10 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2 := by
simpa [B, i, heval_sample, heval_pop] using hdev
have hrate :
10 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2
≤ 10 * 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 ≤ 10 * δ_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.hypothesesTC :β lambda :n :ℕδ_n :ℝregime :LocalizedRegimes S TC sample sc tb n δ_nhn :0 < nδ :ℝhδ_pos :0 < δhδ_le :δ ≤ 1conclusionconclusion 1ω ∈ 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)+ 2 * sqrt ((δ_n ^ 2 + 8 * regime.bundle_HF.regime.b * δ_n * criticalRadius (regime.bundle_HF.regime.ψ n)) * log (1 / δ) / n)+ 8 * regime.bundle_HF.regime.b * log (1 / δ) / nProof (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 : TikhonovBiasBoundAt 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) + 2 * sqrt ((δ_n ^ 2 + 8 * regime.bundle_HF.regime.b * δ_n * criticalRadius (regime.bundle_HF.regime.ψ n)) * log (1 / δ) / n) + 8 * regime.bundle_HF.regime.b * 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.norm_nonneg B.regime hδ_pos hδ_le n hn B.crit_le B.crit_pos (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.hypothesesTC :β lambda :n :ℕδ_n :ℝregime :LocalizedRegimes S TC sample sc tb n δ_nhn :0 < nδ :ℝhδ_pos :0 < δhδ_le :δ ≤ 1conclusionconclusion 1ω ∈ E :h₁ :_hh₁ :h₁ ∈ TC.Hh₂ :_hh₂ :h₂ ∈ TC.Hf :_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)+ 2 * sqrt (((regime.HF_pair_const * regime.H_diameter * δ_n + δ_n) ^ 2 + 8 * regime.bundle_HF.regime.b * (regime.HF_pair_const * regime.H_diameter * δ_n + δ_n) * criticalRadius (regime.bundle_HF.regime.ψ n)) * log (1 / δ) / n)+ 8 * regime.bundle_HF.regime.b * log (1 / δ) / nProof (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 : TikhonovBiasBoundAt 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) + 2 * sqrt (((regime.HF_pair_const * regime.H_diameter * δ_n + δ_n) ^ 2 + 8 * regime.bundle_HF.regime.b * (regime.HF_pair_const * regime.H_diameter * δ_n + δ_n) * criticalRadius (regime.bundle_HF.regime.ψ n)) * log (1 / δ) / n) + 8 * regime.bundle_HF.regime.b * 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.norm_nonneg B.regime hδ_pos hδ_le n hn hr_lb B.crit_pos (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], a fixed-level peeling floor, 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
TC :
β lambda :
n :
ℕ
δ_n :
ℝ
regime :
LocalizedRegimes S TC sample sc tb n δ_n
hn :
0 < n
δ :
ℝ
hδ_pos :
0 < δ
hδ_le :
δ ≤ 1
floor :
PeelingFloor regime δ
conclusion
conclusion 1
ω ∈ 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₂) ∂μ|
≤ 10 * regime.mF_L2_const * δ_n * ‖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 : TikhonovBiasBoundAt S β lambda sc}
{n : ℕ} {δ_n : ℝ}
(regime : LocalizedRegimes S TC sample sc tb n δ_n)
(hn : 0 < n)
{δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1)
(floor : PeelingFloor regime δ) :
∃ 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₂) ∂μ|
≤ 10 * regime.mF_L2_const * δ_n *
‖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 hslack : ∃ K : ℕ,
Rmax ≤ δ_n * (2 : ℝ) ^ K ∧
2 * sqrt
((1 + 8 * B.regime.b) * log (2 * ((K : ℝ) + 1) / δ) / n)
+ 8 * B.regime.b * log (2 * ((K : ℝ) + 1) / δ) / (n * δ_n)
≤ δ_n := by
simpa [B, Rmax] using floor.mF
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 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.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₂) ∂μ|
≤ 10 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2 := by
simpa [B, i, heval_sample, heval_pop] using hdev
have hrate :
10 * δ_n * B.norm (B.F i) + 5 * δ_n ^ 2
≤ 10 * 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 ≤ 10 * δ_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.hypothesesTC :β lambda :n :ℕδ_n :ℝregime :LocalizedRegimes S TC sample sc tb n δ_nhn :0 < nδ :ℝhδ_pos :0 < δhδ_le :δ ≤ 1conclusionconclusion 1ω ∈ 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)+ 2 * sqrt ((δ_n ^ 2 + 8 * regime.bundle_mF.regime.b * δ_n * criticalRadius (regime.bundle_mF.regime.ψ n)) * log (1 / δ) / n)+ 8 * regime.bundle_mF.regime.b * log (1 / δ) / nProof (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 : TikhonovBiasBoundAt 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) + 2 * sqrt ((δ_n ^ 2 + 8 * regime.bundle_mF.regime.b * δ_n * criticalRadius (regime.bundle_mF.regime.ψ n)) * log (1 / δ) / n) + 8 * regime.bundle_mF.regime.b * 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.norm_nonneg B.regime hδ_pos hδ_le n hn B.crit_le B.crit_pos (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.hypothesesTC :β lambda :n :ℕδ_n :ℝregime :LocalizedRegimes S TC sample sc tb n δ_nhn :0 < nδ :ℝhδ_pos :0 < δhδ_le :δ ≤ 1conclusionconclusion 1ω ∈ E :f₁ :_hf₁ :f₁ ∈ TC.Ff₂ :_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)+ 2 * sqrt (((regime.mF_L2_const * regime.F_diameter) ^ 2 + 8 * regime.bundle_mF.regime.b * (regime.mF_L2_const * regime.F_diameter) * criticalRadius (regime.bundle_mF.regime.ψ n)) * log (1 / δ) / n)+ 8 * regime.bundle_mF.regime.b * log (1 / δ) / nProof (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 : TikhonovBiasBoundAt 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) + 2 * sqrt (((regime.mF_L2_const * regime.F_diameter) ^ 2 + 8 * regime.bundle_mF.regime.b * (regime.mF_L2_const * regime.F_diameter) * criticalRadius (regime.bundle_mF.regime.ψ n)) * log (1 / δ) / n) + 8 * regime.bundle_mF.regime.b * 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.norm_nonneg B.regime hδ_pos hδ_le n hn hr_lb B.crit_pos (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.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
PerSample 2 core · 0 supporting This module combines the four localized deviation events at one sample-size index and one confidence level. ★ per_sample_empirical_process_event
Fixed-sample NPIV empirical-process event
This module combines the four localized deviation events at one sample-size
index and one confidence level. It intentionally has no countable
intersection over sample sizes, so its deviation term is
sqrt (log (4 / zeta) / n) rather than sqrt (log (2^n / zeta) / n).
structure PerSampleConfidenceFloor reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
A localized regime satisfies the fixed-confidence critical-radius floor at level zeta when each of the three objective-process envelope terms is at most the squared localization radius.
Definition (Lean source)
parameters
S :
beta lambda delta_n :
ℝ
n :
ℕ
sc :
SourceCondition S beta
TikhonovBiasBoundAt S beta lambda sc
regime :
LocalizedRegimes S TC sample sc tb n delta_n
zeta :
ℝ
assumes
HF :
2 * sqrt ((delta_n ^ 2 + 8 * regime.bundle_HF.regime.b * delta_n * criticalRadius (regime.bundle_HF.regime.ψ n)) * log (4 / zeta) / n)
+ 8 * regime.bundle_HF.regime.b * log (4 / zeta) / n
≤ delta_n ^ 2
Confidence floor for the product process.
mF :
2 * sqrt ((delta_n ^ 2 + 8 * regime.bundle_mF.regime.b * delta_n * criticalRadius (regime.bundle_mF.regime.ψ n)) * log (4 / zeta) / n)
+ 8 * regime.bundle_mF.regime.b * log (4 / zeta) / n
≤ delta_n ^ 2
Confidence floor for the moment process.
F :
2 * sqrt ((delta_n ^ 2 + 8 * regime.bundle_F.regime.b * delta_n * criticalRadius (regime.bundle_F.regime.ψ n)) * log (4 / zeta) / n)
+ 8 * regime.bundle_F.regime.b * log (4 / zeta) / n
≤ delta_n ^ 2
Confidence floor for the squared-critic process.
theorem per_sample_empirical_process_event reviewed
⚑ flagged
Causalean.Estimation.NPIV.Primal
Given a source condition, its fixed-level bias certificate, a positive fold size, a confidence level strictly between zero and one, a nonnegative regularization level, the localized regime at that one fold size, the fixed-confidence critical-radius floor, the peeling floor at one quarter of that confidence, a sample-size index, and a sample-size-dependent TRAE estimator, there is an event of probability at least 1 - zeta on which the population strong-convexity right-hand side at index n is bounded by 50 * delta n² plus the peeled centered-regularizer envelope.
Formal statement
hypotheses
TC :
split :
OneShotSplit sample
lambda_n :
ℕ → ℝ
beta :
ℝ
delta :
ℕ → ℝ
h_hat :
ℕ → Omega → S.𝒳 → ℝ
n :
ℕ
is_estimator :
IsTRAEPrimalEstimatorSequence S TC sample split lambda_n h_hat
sc :
SourceCondition S beta
tb :
TikhonovBiasBoundAt S beta (lambda_n n) sc
regime :
LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n)
hn :
1 ≤ split.n₁ n
zeta :
ℝ
hzeta_pos :
0 < zeta
hzeta_lt :
zeta < 1
hlambda :
0 ≤ lambda_n n
floor :
PerSampleConfidenceFloor regime zeta
peeling :
PeelingFloor regime (zeta / 4)
conclusion
∃ A : Set Omega,
conclusion 1
omega ∈ A :
(S.weakNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n omega)) - S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm (S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2
+ lambda_n n * ((S.strongNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n omega)))) ^ 2 - (S.strongNorm (S.hL2 tb.h_lambda_star_mem)) ^ 2)
≤ 50 * (delta n) ^ 2
+ lambda_n n * (10 * delta n * S.strongNorm (S.hL2 (TC.H_subset (is_estimator.mem_H n omega)) - S.hL2 tb.h_lambda_star_mem) + 5 * (delta n) ^ 2)
Proof (Lean source)
theorem per_sample_empirical_process_event
{S : OperatorSystem Omega mu} {TC : TRAEClasses S}
{P_W : Measure S.𝒲}
{sample : IIDSample Omega S.𝒲 mu P_W}
{split : OneShotSplit sample}
{lambda_n : ℕ → ℝ} {beta : ℝ} {delta : ℕ → ℝ}
{h_hat : ℕ → Omega → S.𝒳 → ℝ}
{n : ℕ}
(is_estimator :
IsTRAEPrimalEstimatorSequence S TC sample split lambda_n h_hat)
(sc : SourceCondition S beta)
(tb : TikhonovBiasBoundAt S beta (lambda_n n) sc)
[IsProbabilityMeasure mu]
(regime :
LocalizedRegimes S TC sample sc tb (split.n₁ n) (delta n))
(hn : 1 ≤ split.n₁ n)
{zeta : ℝ} (hzeta_pos : 0 < zeta) (hzeta_lt : zeta < 1)
(hlambda : 0 ≤ lambda_n n)
(floor : PerSampleConfidenceFloor regime zeta)
(peeling : PeelingFloor regime (zeta / 4)) :
∃ A : Set Omega,
MeasurableSet A ∧ mu A ≥ 1 - ofReal zeta ∧
∀ omega ∈ A,
(S.weakNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n omega))
- S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm
(S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2
+ lambda_n n *
((S.strongNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n omega)))) ^ 2
- (S.strongNorm (S.hL2 tb.h_lambda_star_mem)) ^ 2)
≤ 50 * (delta n) ^ 2
+ lambda_n n *
(10 * delta n *
S.strongNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n omega))
- S.hL2 tb.h_lambda_star_mem)
+ 5 * (delta n) ^ 2) := by
classical
let eta : ℝ := zeta / 4
have heta_pos : 0 < eta := by dsimp [eta]; linarith
have heta_le : eta ≤ 1 := by dsimp [eta]; linarith
have hn_pos : 0 < split.n₁ n := lt_of_lt_of_le zero_lt_one hn
obtain ⟨EHF, hEHF_meas, hEHF_mass, hEHF⟩ :=
localized_omega_event_for_HF regime hn_pos heta_pos heta_le
obtain ⟨EmF, hEmF_meas, hEmF_mass, hEmF⟩ :=
localized_omega_event_for_mF regime hn_pos heta_pos heta_le
obtain ⟨EF, hEF_meas, hEF_mass, hEF⟩ :=
localized_omega_event_for_F regime hn_pos heta_pos heta_le
obtain ⟨EH, hEH_meas, hEH_mass, hEH⟩ :=
localized_omega_event_for_H_pair_peeled
(regime := regime) hn_pos heta_pos heta_le (by simpa [eta] using peeling)
let A : Set Omega := ((EHF ∩ EmF) ∩ EF) ∩ EH
refine ⟨A, ((hEHF_meas.inter hEmF_meas).inter hEF_meas).inter hEH_meas,
?_, ?_⟩
· have h12 := measure_inter_ge_one_sub_add_of_ge hEHF_meas hEmF_meas
hEHF_mass hEmF_mass
have h123 := measure_inter_ge_one_sub_add_of_ge
(hEHF_meas.inter hEmF_meas) hEF_meas h12 hEF_mass
have h1234 := measure_inter_ge_one_sub_add_of_ge
((hEHF_meas.inter hEmF_meas).inter hEF_meas) hEH_meas h123 hEH_mass
have heta_nonneg : 0 ≤ eta := le_of_lt heta_pos
have hsum :
((ofReal eta + ofReal eta) + ofReal eta)
+ ofReal eta = ofReal zeta := by
rw [← ENNReal.ofReal_add heta_nonneg heta_nonneg]
rw [← ENNReal.ofReal_add (add_nonneg heta_nonneg heta_nonneg) heta_nonneg]
rw [← ENNReal.ofReal_add
(add_nonneg (add_nonneg heta_nonneg heta_nonneg) heta_nonneg) heta_nonneg]
congr 1
dsimp [eta]
ring
simpa [A, hsum] using h1234
· intro omega homega
rcases homega with ⟨⟨⟨homegaHF, homegamF⟩, homegaF⟩, homegaH⟩
obtain ⟨f_h, hf_h, hcl_h⟩ :=
regime.closedness (h_hat n omega) (is_estimator.mem_H n omega)
obtain ⟨f_star, hf_star, hstar_sup_le_inner⟩ :=
regime.supObjective_attained split n omega
tb.h_lambda_star_fun regime.realizability
have hinner_le_sup :
innerObjective S sample split (lambda_n n) (h_hat n omega) f_h n omega
≤ supObjective S TC sample split (lambda_n n) (h_hat n omega) n omega :=
regime.inner_le_supObjective split n omega
(h_hat n omega) (is_estimator.mem_H n omega) f_h hf_h
have hlog : 1 / eta = 4 / zeta := by
dsimp [eta]
field_simp [ne_of_gt hzeta_pos]
have hHF_h := hEHF omega homegaHF (h_hat n omega)
(is_estimator.mem_H n omega) f_h hf_h
have hmF_h := hEmF omega homegamF f_h hf_h
have hF_h := hEF omega homegaF f_h hf_h
have hHF_star := hEHF omega homegaHF tb.h_lambda_star_fun
regime.realizability f_star hf_star
have hmF_star := hEmF omega homegamF f_star hf_star
have hF_star := hEF omega homegaF 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 (regime.bundle_HF.regime.ψ (split.n₁ n))
+ 2 * sqrt
(((delta n) ^ 2 + 8 * regime.bundle_HF.regime.b * delta n *
criticalRadius (regime.bundle_HF.regime.ψ (split.n₁ n))) *
log (4 / zeta) / split.n₁ n)
+ 8 * regime.bundle_HF.regime.b * log (4 / zeta) / split.n₁ n
let rmF : ℝ :=
4 * delta n * criticalRadius (regime.bundle_mF.regime.ψ (split.n₁ n))
+ 2 * sqrt
(((delta n) ^ 2 + 8 * regime.bundle_mF.regime.b * delta n *
criticalRadius (regime.bundle_mF.regime.ψ (split.n₁ n))) *
log (4 / zeta) / split.n₁ n)
+ 8 * regime.bundle_mF.regime.b * log (4 / zeta) / split.n₁ n
let rF : ℝ :=
4 * delta n * criticalRadius (regime.bundle_F.regime.ψ (split.n₁ n))
+ 2 * sqrt
(((delta n) ^ 2 + 8 * regime.bundle_F.regime.b * delta n *
criticalRadius (regime.bundle_F.regime.ψ (split.n₁ n))) *
log (4 / zeta) / split.n₁ n)
+ 8 * regime.bundle_F.regime.b * log (4 / zeta) / split.n₁ n
have hupper_h :
2 * (∫ omega', S.m (S.W omega') f_h ∂mu)
- 2 * (∫ omega',
h_hat n omega (S.xOf (S.W omega')) *
f_h (S.zOf (S.W omega')) ∂mu)
- ∫ omega', (f_h (S.zOf (S.W omega'))) ^ 2 ∂mu
+ lambda_n n *
(((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(h_hat n omega (S.xOf (sample.Z (k : ℕ) omega))) ^ 2)
≤ innerObjective S sample split (lambda_n n)
(h_hat n omega) f_h n omega + (2 * rmF + 2 * rHF + rF) := by
exact population_regularized_le_innerObjective_add_deviation
split (lambda_n n) (h_hat n omega) f_h n omega hmF_h hHF_h hF_h
have hupper_star :
innerObjective S sample split (lambda_n n)
tb.h_lambda_star_fun f_star n omega
≤ 2 * (∫ omega', S.m (S.W omega') f_star ∂mu)
- 2 * (∫ omega',
tb.h_lambda_star_fun (S.xOf (S.W omega')) *
f_star (S.zOf (S.W omega')) ∂mu)
- ∫ omega', (f_star (S.zOf (S.W omega'))) ^ 2 ∂mu
+ lambda_n n *
(((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(tb.h_lambda_star_fun
(S.xOf (sample.Z (k : ℕ) omega))) ^ 2)
+ (2 * rmF + 2 * rHF + rF) := by
exact innerObjective_le_population_regularized_add_deviation
split (lambda_n n) tb.h_lambda_star_fun f_star n omega
hmF_star hHF_star hF_star
have hpop_h_eq :
2 * (∫ omega', S.m (S.W omega') f_h ∂mu)
- 2 * (∫ omega', h_hat n omega (S.xOf (S.W omega')) *
f_h (S.zOf (S.W omega')) ∂mu)
- ∫ omega', (f_h (S.zOf (S.W omega'))) ^ 2 ∂mu
= (S.weakNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n omega))
- S.hL2 S.h₀_mem)) ^ 2 :=
population_inner_eq_weakNorm_sq
(hh := is_estimator.mem_H n omega) (hf := hf_h) hcl_h
have hpop_star_le :
2 * (∫ omega', S.m (S.W omega') f_star ∂mu)
- 2 * (∫ omega', tb.h_lambda_star_fun (S.xOf (S.W omega')) *
f_star (S.zOf (S.W omega')) ∂mu)
- ∫ omega', (f_star (S.zOf (S.W omega'))) ^ 2 ∂mu
≤ (S.weakNorm
(S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2 :=
population_inner_le_weak (hh := regime.realizability) (hf := hf_star)
have hopt := is_estimator.opt n omega tb.h_lambda_star_fun regime.realizability
have hEP :
(S.weakNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n omega))
- S.hL2 S.h₀_mem)) ^ 2
- (S.weakNorm
(S.hL2 tb.h_lambda_star_mem - S.hL2 S.h₀_mem)) ^ 2
≤ lambda_n n *
((((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(tb.h_lambda_star_fun
(S.xOf (sample.Z (k : ℕ) omega))) ^ 2)
- (((split.n₁ n : ℕ) : ℝ)⁻¹ *
∑ k : Fin (split.n₁ n),
(h_hat n omega
(S.xOf (sample.Z (k : ℕ) omega))) ^ 2))
+ (4 * rmF + 4 * rHF + 2 * rF) := by
linarith [hupper_h, hupper_star, hpop_h_eq, hpop_star_le,
hinner_le_sup, hstar_sup_le_inner, hopt]
have hHdev := hEH omega homegaH tb.h_lambda_star_fun
regime.realizability (h_hat n omega) (is_estimator.mem_H n omega)
have hstar_sq :
(S.strongNorm (S.hL2 tb.h_lambda_star_mem)) ^ 2 =
∫ omega', (tb.h_lambda_star_fun (S.xOf (S.W omega'))) ^ 2 ∂mu :=
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 omega)))) ^ 2 =
∫ omega', (h_hat n omega (S.xOf (S.W omega'))) ^ 2 ∂mu :=
S.strongNorm_sq_hL2_eq_integral
(TC.H_subset (is_estimator.mem_H n omega))
have hHmul := mul_le_mul_of_nonneg_left hHdev hlambda
have hnorm_sub :
S.strongNorm
(S.hL2 tb.h_lambda_star_mem
- S.hL2 (TC.H_subset (is_estimator.mem_H n omega)))
= S.strongNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n omega))
- S.hL2 tb.h_lambda_star_mem) := by
simp [OperatorSystem.strongNorm, norm_sub_rev]
rw [hnorm_sub] at hHmul
have hHabs :
|lambda_n n *
(((((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(tb.h_lambda_star_fun
(S.xOf (sample.Z (k : ℕ) omega))) ^ 2)
- (((split.n₁ n : ℕ) : ℝ)⁻¹ * ∑ k : Fin (split.n₁ n),
(h_hat n omega
(S.xOf (sample.Z (k : ℕ) omega))) ^ 2))
- ((S.strongNorm (S.hL2 tb.h_lambda_star_mem)) ^ 2
- (S.strongNorm
(S.hL2 (TC.H_subset
(is_estimator.mem_H n omega)))) ^ 2))|
≤ lambda_n n *
(10 * delta n *
S.strongNorm
(S.hL2 (TC.H_subset (is_estimator.mem_H n omega))
- S.hL2 tb.h_lambda_star_mem)
+ 5 * (delta n) ^ 2) := by
simpa [abs_mul, abs_of_nonneg hlambda, hstar_sq, hhat_sq, mul_assoc]
using hHmul
have hHupper := (le_abs_self _).trans hHabs
have hdelta_pos : 0 < delta n :=
lt_of_lt_of_le regime.bundle_HF.crit_pos regime.bundle_HF.crit_le
have hdelta_nonneg : 0 ≤ delta n := hdelta_pos.le
have hcrit_HF :
delta n * criticalRadius (regime.bundle_HF.regime.ψ (split.n₁ n))
≤ (delta n) ^ 2 := by
calc
_ ≤ delta n * delta n :=
mul_le_mul_of_nonneg_left regime.bundle_HF.crit_le hdelta_nonneg
-- … truncated; follow the source link for the rest …
Regulariser 1 core · 0 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
TC :
split :
OneShotSplit sample
lambda β :
ℝ
delta :
ℕ → ℝ
h_hat :
ℕ → Ω → S.𝒳 → ℝ
IsTRAEPrimalEstimator S TC sample split lambda h_hat
sc :
SourceCondition S β
tb :
TikhonovBiasBoundAt 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 Ω,
MeasurableSet Aζ_reg
μ Aζ_reg ≥ 1 - ofReal ζ
conclusion 1
ω ∈ 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)) + 2 * sqrt ((((regimes n).H_diameter + delta n) ^ 2 + 8 * (regimes n).bundle_H.regime.b * ((regimes n).H_diameter + delta n) * criticalRadius ((regimes n).bundle_H.regime.ψ (split.n₁ n))) * log ((2 : ℝ) ^ (n + 1) / ζ) / (split.n₁ n)) + 8 * (regimes n).bundle_H.regime.b * 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 : TikhonovBiasBoundAt 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))
+ 2 * sqrt
((((regimes n).H_diameter + delta n) ^ 2 +
8 * (regimes n).bundle_H.regime.b *
((regimes n).H_diameter + delta n) *
criticalRadius
((regimes n).bundle_H.regime.ψ (split.n₁ n))) *
log ((2 : ℝ) ^ (n + 1) / ζ) / (split.n₁ n))
+ 8 * (regimes n).bundle_H.regime.b *
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