Estimation.OrthogonalLearning.LocalEmpProcess
Local empirical-process modulus machinery for orthogonal learning, derived from Rademacher, localized, fixed-nuisance, and random-nuisance regimes.
Local 1 core · 0 supporting This file states the local empirical-process modulus assumption used in orthogonal statistical learning: with high probability, empirical excess risk is uniformly close to population excess risk at a rate depending on th
Local Empirical-Process Modulus
This file states the local empirical-process modulus assumption used in orthogonal statistical learning: with high probability, empirical excess risk is uniformly close to population excess risk at a rate depending on the distance to the population target. The predicate serves as the bridge from empirical-process theory to oracle inequalities for plug-in estimators.
def LocalEmpProcessModulus reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Given an orthogonal statistical-learning system, an independent and identically distributed sample with the system's population law, a one-shot sample split, a rate sequence, a confidence tolerance, and a nuisance function, the local empirical-process modulus condition holds exactly when, for every sample size, there exists an event that is measurable, has measure at least , with subtraction truncated at zero, and on which, uniformly over the target class, the population excess risk minus the fold-B empirical excess risk is at most times the distance from the distinguished target plus .
Definition (Lean source)
parameters
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
S_iid :
IIDSample Ω Z μ P_Z
split :
OneShotSplit S_iid
ρ :
ℕ → ℝ
δ :
ℝ
g :
G
n :
ℕ
def
LocalEmpProcessModulus S S_iid split ρ δ g :
Prop
given by
clause 1
ω ∈ E :
θ ∈ S.Θ_set :
(S.L θ g - S.L S.θ₀ g)
- (empRiskFoldB S S_iid split n ω θ g - empRiskFoldB S S_iid split n ω S.θ₀ g)
≤ ρ n * ‖θ - S.θ₀‖ + (ρ n) ^ 2
Rademacher 7 core · 1 supporting This file obtains a local empirical-process bound for orthogonal statistical learning from global control of the Rademacher complexity of the centred loss class. ★ foldB_pi_law★ localEmpProcessModulus_of_bounded_rademacher★ localEmpProcessModulus_of_bounded_rademacher_ae
Global Rademacher Modulus
This file obtains a local empirical-process bound for orthogonal statistical learning from global control of the Rademacher complexity of the centred loss class. It supplies versions for losses bounded everywhere or almost everywhere, and treats the degenerate case in which the target class contains one element.
lemma foldB_pi_law reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Fold-B joint-law identification (public alias). For an IID sample S split via split, at any fold size n, the joint distribution of the fold-B subsample, mapped from μ via ω ↦ (i ↦ S.Z i ω) indexed by i ∈ split.foldB n, equals the product measure Measure.pi (fun _ ↦ P).
Formal statement
hypotheses
conclusion
μ.map (fun ω (i : split.foldB n) => S.Z i ω) = Measure.pi (fun _ : split.foldB n => P)
Proof (Lean source)
lemma foldB_pi_law [IsProbabilityMeasure μ] [IsProbabilityMeasure P]
(S : IIDSample Ω X μ P) (split : OneShotSplit S) (n : ℕ) :
μ.map (fun ω (i : split.foldB n) => S.Z i ω) =
Measure.pi (fun _ : split.foldB n => P) :=
oneShot_iid S split n
def RademacherBound reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Given an orthogonal statistical-learning system, an independent and identically distributed sample with the system's population law, a one-shot sample split, a nuisance function, a sequence of targets in the target class, and a real sequence, the Rademacher-complexity bound holds exactly when, for every sample size, the proposed bound is nonnegative and the Rademacher complexity of the centred loss class indexed by that target sequence on fold B, computed under the ambient sample measure using the zeroth observation coordinate, is at most the proposed bound.
Definition (Lean source)
parameters
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
S_iid :
IIDSample Ω Z μ P_Z
split :
OneShotSplit S_iid
g :
G
idx :
ℕ → S.Θ_set
R :
ℕ → ℝ
n :
ℕ
def
RademacherBound S S_iid split g idx R :
Prop
given by
clause 1
0 ≤ R n
clause 2
rademacherComplexity (split.foldB n).card (fun (k : ℕ) z => S.ℓ z (idx k).val g - S.ℓ z S.θ₀ g) μ (S_iid.Z 0)
≤ R n
def UniformlyBoundedLoss reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Given an orthogonal statistical-learning system, a nuisance function, and a real bound, the uniform bounded-loss condition holds exactly when, for every observation and every target in the target class, the absolute loss at that nuisance function is at most the bound.
Definition (Lean source)
parameters
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
g :
G
b :
ℝ
z :
θ ∈ S.Θ_set :
def
UniformlyBoundedLoss S g b :
Prop
given by
|S.ℓ z θ g| ≤ b
def UniformlyBoundedLossAE reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Given an orthogonal statistical-learning system, a nuisance function, and a real bound, the almost-everywhere uniform bounded-loss condition holds exactly when, outside a set of population probability zero, every target in the target class has absolute loss at that nuisance function at most the bound.
Definition (Lean source)
parameters
def
UniformlyBoundedLossAE S g b :
Prop
given by
∀ᵐ z ∂P_Z, ∀ θ ∈ S.Θ_set, |S.ℓ z θ g| ≤ b
def LossContinuousOnΘset reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Given an orthogonal statistical-learning system and a nuisance function, the target-continuity condition for the loss holds exactly when, for every observation, the loss as a function of the target is continuous on the system's target class at that fixed nuisance function.
Definition (Lean source)
parameters
def
LossContinuousOnΘset S g :
Prop
given by
Continuous (fun (θ : S.Θ_set) => S.ℓ z θ.val g)
theorem localEmpProcessModulus_of_bounded_rademacher reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Bounded-loss Rademacher bridge theorem. Assume b is nonnegative, that the loss magnitude is uniformly bounded by b over the parameter set, and that the loss is continuous in the parameter on the parameter set. Given a sequence R n that is nonnegative and upper-bounds the population Rademacher complexity of the centred loss class on the fold-B sample at every sample size, then for any confidence level 0 < δ ≤ 1 the local empirical-process modulus condition holds, with rate ρ n := √(2 · b) when the fold-B sample is empty and ρ n := √(2 · R n + 2 · b · √(2 · log(1/δ) / |foldB n|)) otherwise.
Formal statement
hypotheses
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
S_iid :
IIDSample Ω Z μ P_Z
split :
OneShotSplit S_iid
b :
ℝ
hb :
0 ≤ b
g :
G
hg_bdd :
UniformlyBoundedLoss S g b
hg_cont :
idx :
ℕ → S.Θ_set
idx_dense :
DenseRange idx
R :
ℕ → ℝ
hR :
RademacherBound S S_iid split g idx R
δ :
ℝ
hδ :
0 < δ
hδ' :
δ ≤ 1
conclusion
LocalEmpProcessModulus S S_iid split (fun n => sqrt (if (split.foldB n).card = 0 then 2 * b else 2 * R n + 2 * b * sqrt (2 * log (1 / δ) / (split.foldB n).card))) δ g
Proof (Lean source)
theorem localEmpProcessModulus_of_bounded_rademacher
(S : LearningSystem Ω μ Z P_Z Θ G)
[IsProbabilityMeasure μ]
(S_iid : IIDSample Ω Z μ P_Z)
(split : OneShotSplit S_iid)
{b : ℝ} (hb : 0 ≤ b) (g : G)
(hg_bdd : UniformlyBoundedLoss S g b)
(hg_cont : LossContinuousOnΘset S g)
(idx : ℕ → S.Θ_set)
(idx_dense : DenseRange idx)
(R : ℕ → ℝ)
(hR : RademacherBound S S_iid split g idx R)
{δ : ℝ} (hδ : 0 < δ) (hδ' : δ ≤ 1) :
LocalEmpProcessModulus S S_iid split
(fun n => sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card))) δ g := by
intro n
classical
haveI : IsProbabilityMeasure P_Z := by
rw [← S_iid.law]
exact Measure.isProbabilityMeasure_map (S_iid.meas 0).aemeasurable
have hR_nonneg : 0 ≤ R n := (hR n).1
by_cases hm0 : (split.foldB n).card = 0
· refine ⟨Set.univ, MeasurableSet.univ, ?_, ?_⟩
· rw [measure_univ]
exact tsub_le_self
· intro ω _ θ hθ
have hfold_empty : split.foldB n = ∅ := Finset.card_eq_zero.mp hm0
have hpop : S.L θ g - S.L S.θ₀ g ≤ 2 * b :=
populationRisk_sub_le_two_mul_bound S hb hg_bdd hθ
have hρsq :
(sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card))) ^ 2
= 2 * b := by
rw [Real.sq_sqrt]
· simp [hm0]
· have : 0 ≤ 2 * b := by nlinarith
simpa [hm0] using this
have hρ_nonneg :
0 ≤ sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card)) :=
Real.sqrt_nonneg _
have hnorm_nonneg : 0 ≤ ‖θ - S.θ₀‖ := norm_nonneg _
calc
(S.L θ g - S.L S.θ₀ g)
- (empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g)
= S.L θ g - S.L S.θ₀ g := by
simp [empRiskFoldB, hfold_empty]
_ ≤ 2 * b := hpop
_ = (sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card))) ^ 2 := hρsq.symm
_ ≤ sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card)) * ‖θ - S.θ₀‖
+ (sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card))) ^ 2 := by
nlinarith [mul_nonneg hρ_nonneg hnorm_nonneg]
· have hm_pos_nat : 0 < (split.foldB n).card := Nat.pos_of_ne_zero hm0
have hm_pos : 0 < ((split.foldB n).card : ℝ) := Nat.cast_pos.mpr hm_pos_nat
by_cases hb0 : b = 0
· refine ⟨Set.univ, MeasurableSet.univ, ?_, ?_⟩
· rw [measure_univ]
exact tsub_le_self
· intro ω _ θ hθ
have hloss_zero : ∀ z θ', θ' ∈ S.Θ_set → S.ℓ z θ' g = 0 := by
intro z θ' hθ'
have habs : |S.ℓ z θ' g| = 0 := by
apply le_antisymm
· simpa [hb0] using hg_bdd z θ' hθ'
· exact abs_nonneg _
exact abs_eq_zero.mp habs
have hLθ : S.L θ g = 0 := by
have habs := populationRisk_abs_le_of_uniform S hb hg_bdd hθ
exact abs_eq_zero.mp (le_antisymm (by simpa [hb0] using habs) (abs_nonneg _))
have hL0 : S.L S.θ₀ g = 0 := by
have habs := populationRisk_abs_le_of_uniform S hb hg_bdd S.θ₀_mem
exact abs_eq_zero.mp (le_antisymm (by simpa [hb0] using habs) (abs_nonneg _))
have hempθ : empRiskFoldB S S_iid split n ω θ g = 0 := by
simp [empRiskFoldB, hloss_zero, hθ]
have hemp0 : empRiskFoldB S S_iid split n ω S.θ₀ g = 0 := by
simp [empRiskFoldB, hloss_zero, S.θ₀_mem]
have hρ_nonneg :
0 ≤ sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card)) :=
Real.sqrt_nonneg _
have hnorm_nonneg : 0 ≤ ‖θ - S.θ₀‖ := norm_nonneg _
have hρsq_nonneg :
0 ≤ (sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card))) ^ 2 := sq_nonneg _
calc
(S.L θ g - S.L S.θ₀ g)
- (empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g) = 0 := by
simp [hLθ, hL0, hempθ, hemp0]
_ ≤ sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card)) * ‖θ - S.θ₀‖
+ (sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card))) ^ 2 := by
nlinarith [mul_nonneg hρ_nonneg hnorm_nonneg, hρsq_nonneg]
· have hb_pos : 0 < b := lt_of_le_of_ne hb (Ne.symm hb0)
let m : ℕ := (split.foldB n).card
let fθ : S.Θ_set → Z → ℝ := fun θ z => S.ℓ z θ.val g - S.ℓ z S.θ₀ g
haveI : Nonempty Z := nonempty_of_isProbabilityMeasure P_Z
haveI : Nonempty S.Θ_set := ⟨⟨S.θ₀, S.θ₀_mem⟩⟩
haveI : SeparableSpace S.Θ_set := by
exact ⟨⟨Set.range idx, Set.countable_range idx, idx_dense⟩⟩
have hf_meas : ∀ θ : S.Θ_set, Measurable (fθ θ) := by
intro θ
exact (S.ℓ_meas θ.val g).sub (S.ℓ_meas S.θ₀ g)
have hf_bdd : ∀ θ : S.Θ_set, ∀ z : Z, |fθ θ z| ≤ 2 * b := by
intro θ z
have h1 : |S.ℓ z θ.val g| ≤ b := hg_bdd z θ.val θ.property
have h2 : |S.ℓ z S.θ₀ g| ≤ b := hg_bdd z S.θ₀ S.θ₀_mem
have h := abs_sub (S.ℓ z θ.val g) (S.ℓ z S.θ₀ g)
dsimp [fθ]
linarith
have hf_cont : ∀ z : Z, Continuous fun θ : S.Θ_set => fθ θ z := by
intro z
exact (hg_cont z).sub continuous_const
let ε : ℝ := 2 * b * sqrt (2 * log (1 / δ) / m)
let τ : ℝ := 2 * R n + ε
have hε_nonneg : 0 ≤ ε := by
dsimp [ε]
positivity
have htail := uniform_deviation_tail_bound_separable_of_pos
(μ := P_Z) (n := m) (f := fθ) hf_meas (X := id) measurable_id
(b := 2 * b) (by linarith) hf_bdd hf_cont (ε := ε) hε_nonneg
have hrad_full_le : rademacherComplexity m fθ P_Z id ≤ R n := by
have hfull_dense :
rademacherComplexity m fθ P_Z id =
rademacherComplexity m (fθ ∘ idx) P_Z id :=
rademacherComplexity_eq_denseRange idx_dense m fθ hf_cont P_Z id
have hmap :
rademacherComplexity m (fθ ∘ idx) P_Z id =
rademacherComplexity m (fθ ∘ idx) μ (S_iid.Z 0) := by
have hmap' :
rademacherComplexity m (fθ ∘ idx) (μ.map (S_iid.Z 0)) id =
rademacherComplexity m (fθ ∘ idx) μ (S_iid.Z 0) :=
rademacherComplexity_map_id m (fθ ∘ idx)
(by
intro k
exact (hf_meas (idx k))) μ (S_iid.Z 0) (S_iid.meas 0)
simpa [S_iid.law] using hmap'
calc
rademacherComplexity m fθ P_Z id
= rademacherComplexity m (fθ ∘ idx) P_Z id := hfull_dense
_ = rademacherComplexity m (fθ ∘ idx) μ (S_iid.Z 0) := hmap
_ ≤ R n := (hR n).2
let badZ : Set (Fin m → Z) :=
{s | 2 • rademacherComplexity m fθ P_Z id + ε ≤
uniformDeviation m fθ P_Z id (id ∘ s)}
let EZ : Set (Fin m → Z) := badZᶜ
have hbad_meas : MeasurableSet badZ := by
have hUD_eq :
uniformDeviation m fθ P_Z id =
uniformDeviation m (fθ ∘ denseSeq S.Θ_set) P_Z id :=
-- … truncated; follow the source link for the rest …
theorem localEmpProcessModulus_of_bounded_rademacher_ae reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Almost-everywhere bounded-loss bridge. Assume b is nonnegative, that the loss magnitude is bounded by b at P_Z-almost-every observation, over the parameter set, and that the loss is continuous in the parameter on the parameter set. Given a sequence R n that is nonnegative and upper-bounds the population Rademacher complexity of the centred loss class on the fold-B sample at every sample size, and that the target parameter minimizes, over the parameter set, the population risk of the loss — evaluated at the model's baseline nuisance and clamped to [-b, b], then for any confidence level 0 < δ ≤ 1 the local empirical-process modulus condition holds, with rate ρ n := √(2 · b) when the fold-B sample is empty and ρ n := √(2 · R n + 2 · b · √(2 · log(1/δ) / |foldB n|)) otherwise.
Formal statement
hypotheses
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
S_iid :
IIDSample Ω Z μ P_Z
split :
OneShotSplit S_iid
b :
ℝ
hb :
0 ≤ b
g :
G
hg_bdd_ae :
UniformlyBoundedLossAE S g b
hg_cont :
idx :
ℕ → S.Θ_set
idx_dense :
DenseRange idx
R :
ℕ → ℝ
hR :
RademacherBound S S_iid split g idx R
hclamp_minimizes :
δ :
ℝ
hδ :
0 < δ
hδ' :
δ ≤ 1
conclusion
LocalEmpProcessModulus S S_iid split (fun n => sqrt (if (split.foldB n).card = 0 then 2 * b else 2 * R n + 2 * b * sqrt (2 * log (1 / δ) / (split.foldB n).card))) δ g
Proof (Lean source)
theorem localEmpProcessModulus_of_bounded_rademacher_ae
(S : LearningSystem Ω μ Z P_Z Θ G)
[IsProbabilityMeasure μ]
(S_iid : IIDSample Ω Z μ P_Z)
(split : OneShotSplit S_iid)
{b : ℝ} (hb : 0 ≤ b) (g : G)
(hg_bdd_ae : UniformlyBoundedLossAE S g b)
(hg_cont : LossContinuousOnΘset S g)
(idx : ℕ → S.Θ_set)
(idx_dense : DenseRange idx)
(R : ℕ → ℝ)
(hR : RademacherBound S S_iid split g idx R)
(hclamp_minimizes : ∀ θ ∈ S.Θ_set,
∫ z, max (-b) (min b (S.ℓ z S.θ₀ S.g₀)) ∂P_Z
≤ ∫ z, max (-b) (min b (S.ℓ z θ S.g₀)) ∂P_Z)
{δ : ℝ} (hδ : 0 < δ) (hδ' : δ ≤ 1) :
LocalEmpProcessModulus S S_iid split
(fun n => sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card))) δ g := by
intro n
classical
haveI : IsProbabilityMeasure P_Z := by
rw [← S_iid.law]
exact Measure.isProbabilityMeasure_map (S_iid.meas 0).aemeasurable
by_cases hm0 : (split.foldB n).card = 0
· refine ⟨Set.univ, MeasurableSet.univ, ?_, ?_⟩
· rw [measure_univ]
exact tsub_le_self
· intro ω _ θ hθ
have hfold_empty : split.foldB n = ∅ := Finset.card_eq_zero.mp hm0
have hpop : S.L θ g - S.L S.θ₀ g ≤ 2 * b :=
populationRisk_sub_le_two_mul_bound_ae S hb hg_bdd_ae hθ
have hρsq :
(sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card))) ^ 2
= 2 * b := by
rw [Real.sq_sqrt]
· simp [hm0]
· have : 0 ≤ 2 * b := by nlinarith
simpa [hm0] using this
have hρ_nonneg :
0 ≤ sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card)) :=
Real.sqrt_nonneg _
have hnorm_nonneg : 0 ≤ ‖θ - S.θ₀‖ := norm_nonneg _
calc
(S.L θ g - S.L S.θ₀ g)
- (empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g)
= S.L θ g - S.L S.θ₀ g := by
simp [empRiskFoldB, hfold_empty]
_ ≤ 2 * b := hpop
_ = (sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card))) ^ 2 := hρsq.symm
_ ≤ sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card)) * ‖θ - S.θ₀‖
+ (sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card))) ^ 2 := by
nlinarith [mul_nonneg hρ_nonneg hnorm_nonneg]
· let clamp : ℝ → ℝ := fun t => max (-b) (min b t)
let Sc : LearningSystem Ω μ Z P_Z Θ G :=
{ S with
ℓ := fun z θ g' => clamp (S.ℓ z θ g')
ℓ_meas := fun θ g' => by
dsimp [clamp]
exact measurable_const.max (measurable_const.min (S.ℓ_meas θ g'))
θ₀_minimizes := by
intro θ hθ
simpa [clamp] using hclamp_minimizes θ hθ }
have hclamp_abs : ∀ t : ℝ, |clamp t| ≤ b := by
intro t
rw [abs_le]
constructor
· dsimp [clamp]
exact le_max_left (-b) (min b t)
· dsimp [clamp]
exact max_le (by linarith) (min_le_left b t)
have hclamp_eq_of_abs_le : ∀ {t : ℝ}, |t| ≤ b → clamp t = t := by
intro t ht
have ht_low : -b ≤ t := (abs_le.mp ht).1
have ht_high : t ≤ b := (abs_le.mp ht).2
dsimp [clamp]
rw [min_eq_right ht_high, max_eq_right ht_low]
have hSc_bdd : UniformlyBoundedLoss Sc g b := by
intro z θ hθ
simpa [Sc] using hclamp_abs (S.ℓ z θ g)
have hSc_cont : LossContinuousOnΘset Sc g := by
intro z
dsimp [Sc, clamp]
exact continuous_const.max (continuous_const.min (hg_cont z))
have hℓ_ae : ∀ θ, θ ∈ S.Θ_set →
(fun z => S.ℓ z θ g) =ᵐ[P_Z] fun z => Sc.ℓ z θ g := by
intro θ hθ
filter_upwards [hg_bdd_ae] with z hz
simpa [Sc] using (hclamp_eq_of_abs_le (hz θ hθ)).symm
have hℓ_all_ae : ∀ᵐ z ∂P_Z,
∀ θ ∈ S.Θ_set, S.ℓ z θ g = Sc.ℓ z θ g := by
filter_upwards [hg_bdd_ae] with z hz θ hθ
simpa [Sc] using (hclamp_eq_of_abs_le (hz θ hθ)).symm
have hL_eq : ∀ θ, θ ∈ S.Θ_set → S.L θ g = Sc.L θ g := by
intro θ hθ
dsimp [LearningSystem.L]
exact integral_congr_ae (hℓ_ae θ hθ)
let idxc : ℕ → Sc.Θ_set := fun k => ⟨(idx k).val, by
simp [Sc, (idx k).property]⟩
have idxc_dense : DenseRange idxc := by
simpa [idxc, Sc] using idx_dense
have hRc : RademacherBound Sc S_iid split g idxc R := by
intro m
refine ⟨(hR m).1, ?_⟩
have hcenter_ae : ∀ k : ℕ,
(fun ω => S.ℓ (S_iid.Z 0 ω) (idx k).val g
- S.ℓ (S_iid.Z 0 ω) S.θ₀ g) =ᵐ[μ]
fun ω => Sc.ℓ (S_iid.Z 0 ω) (idx k).val g
- Sc.ℓ (S_iid.Z 0 ω) Sc.θ₀ g := by
intro k
have hidx_base : (fun z => S.ℓ z (idx k).val g) =ᵐ[P_Z]
fun z => Sc.ℓ z (idx k).val g :=
hℓ_ae (idx k).val (idx k).property
have hzero_base : (fun z => S.ℓ z S.θ₀ g) =ᵐ[P_Z]
fun z => Sc.ℓ z S.θ₀ g :=
hℓ_ae S.θ₀ S.θ₀_mem
have hidx' : (fun ω => S.ℓ (S_iid.Z 0 ω) (idx k).val g) =ᵐ[μ]
fun ω => Sc.ℓ (S_iid.Z 0 ω) (idx k).val g := by
have hmap : ∀ᵐ z ∂μ.map (S_iid.Z 0),
S.ℓ z (idx k).val g = Sc.ℓ z (idx k).val g := by
rw [S_iid.law]
exact hidx_base
exact ae_of_ae_map (S_iid.meas 0).aemeasurable hmap
have hzero' : (fun ω => S.ℓ (S_iid.Z 0 ω) S.θ₀ g) =ᵐ[μ]
fun ω => Sc.ℓ (S_iid.Z 0 ω) Sc.θ₀ g := by
have hmap : ∀ᵐ z ∂μ.map (S_iid.Z 0),
S.ℓ z S.θ₀ g = Sc.ℓ z S.θ₀ g := by
rw [S_iid.law]
exact hzero_base
exact ae_of_ae_map (S_iid.meas 0).aemeasurable hmap
exact hidx'.sub hzero'
have hcongr :
rademacherComplexity (split.foldB m).card
(fun k z => S.ℓ z (idx k).val g - S.ℓ z S.θ₀ g)
μ (S_iid.Z 0) =
rademacherComplexity (split.foldB m).card
(fun k z => Sc.ℓ z (idxc k).val g - Sc.ℓ z Sc.θ₀ g)
μ (S_iid.Z 0) :=
by
simpa [idxc] using
rademacherComplexity_congr_ae (split.foldB m).card
(fun k z => S.ℓ z (idx k).val g - S.ℓ z S.θ₀ g)
(fun k z => Sc.ℓ z (idx k).val g - Sc.ℓ z Sc.θ₀ g)
μ (S_iid.Z 0) hcenter_ae
calc
rademacherComplexity (split.foldB m).card
(fun k z => Sc.ℓ z (idxc k).val g - Sc.ℓ z Sc.θ₀ g)
μ (S_iid.Z 0)
= rademacherComplexity (split.foldB m).card
(fun k z => S.ℓ z (idx k).val g - S.ℓ z S.θ₀ g)
μ (S_iid.Z 0) := hcongr.symm
_ ≤ R m := (hR m).2
have hmod_c := localEmpProcessModulus_of_bounded_rademacher
Sc S_iid split hb g hSc_bdd hSc_cont idxc idxc_dense R hRc hδ hδ'
rcases hmod_c n with ⟨Ec, hEc_meas, hEc_prob, hEc_bound⟩
let Gs : Set Ω :=
{ω | ∀ i ∈ split.foldB n, ∀ θ ∈ S.Θ_set,
S.ℓ (S_iid.Z i ω) θ g = Sc.ℓ (S_iid.Z i ω) θ g}
have hsample_all_ae : ∀ i : ℕ, ∀ᵐ ω ∂μ,
∀ θ ∈ S.Θ_set,
S.ℓ (S_iid.Z i ω) θ g = Sc.ℓ (S_iid.Z i ω) θ g := by
intro i
have hlaw_i : μ.map (S_iid.Z i) = P_Z := by
rw [← (S_iid.identDist i).map_eq, S_iid.law]
have hbase : ∀ᵐ z ∂P_Z,
∀ θ ∈ S.Θ_set, S.ℓ z θ g = Sc.ℓ z θ g := hℓ_all_ae
have hmap : ∀ᵐ z ∂μ.map (S_iid.Z i),
∀ θ ∈ S.Θ_set, S.ℓ z θ g = Sc.ℓ z θ g := by
simpa [hlaw_i] using hbase
exact ae_of_ae_map (S_iid.meas i).aemeasurable hmap
have hGs_ae : ∀ᵐ ω ∂μ, ω ∈ Gs := by
have hfin : ∀ᵐ ω ∂μ, ∀ i ∈ split.foldB n,
∀ θ ∈ S.Θ_set,
S.ℓ (S_iid.Z i ω) θ g = Sc.ℓ (S_iid.Z i ω) θ g := by
simpa using (Finset.eventually_all (split.foldB n)).2
(fun i _hi => hsample_all_ae i)
simpa [Gs] using hfin
have hGs_null : μ Gsᶜ = 0 := ae_iff.mp hGs_ae
rcases exists_measurable_superset_of_null hGs_null with
⟨N, hGs_compl_subset_N, hN_meas, hN_null⟩
refine ⟨Ec \ N, hEc_meas.diff hN_meas, ?_, ?_⟩
· rw [measure_diff_null hN_null]
exact hEc_prob
· intro ω hω θ hθ
have hωEc : ω ∈ Ec := hω.1
have hωG : ω ∈ Gs := by
by_contra hnot
exact hω.2 (hGs_compl_subset_N hnot)
have hLθ : S.L θ g = Sc.L θ g := hL_eq θ hθ
have hL0 : S.L S.θ₀ g = Sc.L Sc.θ₀ g := by
simpa [Sc] using hL_eq S.θ₀ S.θ₀_mem
have hempθ :
empRiskFoldB S S_iid split n ω θ g =
empRiskFoldB Sc S_iid split n ω θ g := by
dsimp [empRiskFoldB]
congr 1
exact Finset.sum_congr rfl fun i hi => hωG i hi θ hθ
have hemp0 :
empRiskFoldB S S_iid split n ω S.θ₀ g =
empRiskFoldB Sc S_iid split n ω Sc.θ₀ g := by
dsimp [empRiskFoldB]
congr 1
exact Finset.sum_congr rfl fun i hi => by
simpa [Sc] using hωG i hi S.θ₀ S.θ₀_mem
calc
(S.L θ g - S.L S.θ₀ g)
- (empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g)
= (Sc.L θ g - Sc.L Sc.θ₀ g)
- (empRiskFoldB Sc S_iid split n ω θ g
- empRiskFoldB Sc S_iid split n ω Sc.θ₀ g) := by
-- … truncated; follow the source link for the rest …
1 supporting declaration (lemmas, instances)
-
localEmpProcessModulus_singletontheorem — Trivial finite class. When Θ_set = {θ₀} (the class collapses to the truth), the modulus inequality holds with ρ n := 0.hypothesesΘ :sharedType u_3G :sharedType u_4S :LearningSystem Ω μ Z P_Z Θ GS_iid :IIDSample Ω Z μ P_Zsplit :OneShotSplit S_iidg :Ghsing :S.Θ_set = {S.θ₀}δ :ℝ_hδ :0 < δconclusionLocalEmpProcessModulus S S_iid split (fun _ => 0) δ gProof (Lean source)
theorem localEmpProcessModulus_singleton (S : LearningSystem Ω μ Z P_Z Θ G) (S_iid : IIDSample Ω Z μ P_Z) (split : OneShotSplit S_iid) [IsProbabilityMeasure μ] (g : G) (hsing : S.Θ_set = {S.θ₀}) {δ : ℝ} (_hδ : 0 < δ) : LocalEmpProcessModulus S S_iid split (fun _ => 0) δ g := by intro n refine ⟨Set.univ, MeasurableSet.univ, ?_, ?_⟩ · rw [measure_univ] exact tsub_le_self · intro ω _ θ hθ have hθ' : θ ∈ ({S.θ₀} : Set Θ) := by simpa [hsing] using hθ rcases hθ' with rfl simp
Localized 7 core · 1 supporting This file derives local empirical-process moduli for orthogonal statistical learning from localized Rademacher-complexity conditions. ★ localEmpProcessModulus_of_localized_bounded★ localEmpProcessModulus_of_localized_bounded_ae★ localEmpProcessModulus_of_localized_sharp★ localEmpProcessModulus_of_localized_sharp_ae
Localized Rademacher Moduli
This file derives local empirical-process moduli for orthogonal statistical learning from localized Rademacher-complexity conditions. It supplies both a bounded-loss fallback and a sharp critical-radius result, including an almost-everywhere version obtained by clamping the centered loss.
def LocalizedRademacherRegime reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
For an orthogonal statistical-learning system, an independent and identically distributed sample from its observation law, a one-shot sample split, a nuisance function, a sequence indexing candidate targets, a norm on real-valued observation functions, a family of real complexity envelopes, and a real bound, the localized Rademacher regime requires: the bound is nonnegative; the centered loss is bounded in absolute value by that bound for every observation and candidate target; each complexity envelope is sub-root; and at every sample size, the envelope upper-bounds the population Rademacher complexity of the indexed centered-loss class on the split's validation fold.
Definition (Lean source)
parameters
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
_S_iid :
IIDSample Ω Z μ P_Z
_split :
OneShotSplit _S_iid
g :
G
idx :
ℕ → S.Θ_set
norm :
(Z → ℝ) → ℝ
ψ :
ℕ → ℝ → ℝ
b :
ℝ
def
LocalizedRademacherRegime S _S_iid _split g idx norm ψ b :
Prop
given by
clause 1
0 ≤ b
clause 2
z :
θ ∈ S.Θ_set :
|S.ℓ z θ g - S.ℓ z S.θ₀ g| ≤ b
clause 4
n :
ℕ
RademacherUpperBound (fun (k : ℕ) (z : Z) => S.ℓ z (idx k).val g - S.ℓ z S.θ₀ g) norm P_Z (id : Z → Z) (_split.foldB n).card (ψ (_split.foldB n).card)
def LocalizedRademacherRegimeAE reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
For an orthogonal statistical-learning system, an independent and identically distributed sample from its observation law, a one-shot sample split, a nuisance function, a sequence indexing candidate targets, a norm on real-valued observation functions, a family of real complexity envelopes, and a real bound, the almost-everywhere localized Rademacher regime requires: the bound is nonnegative; for almost every observation under the observation law, the centered loss is bounded in absolute value by that bound for every candidate target; each complexity envelope is sub-root; and at every sample size, the envelope upper-bounds the population Rademacher complexity of the indexed centered-loss class on the split's validation fold.
Definition (Lean source)
parameters
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
_S_iid :
IIDSample Ω Z μ P_Z
_split :
OneShotSplit _S_iid
g :
G
idx :
ℕ → S.Θ_set
norm :
(Z → ℝ) → ℝ
ψ :
ℕ → ℝ → ℝ
b :
ℝ
def
LocalizedRademacherRegimeAE S _S_iid _split g idx norm ψ b :
Prop
given by
clause 1
0 ≤ b
clause 2
∀ᵐ z ∂P_Z, ∀ θ ∈ S.Θ_set, |S.ℓ z θ g - S.ℓ z S.θ₀ g| ≤ b
clause 4
n :
ℕ
RademacherUpperBound (fun (k : ℕ) (z : Z) => S.ℓ z (idx k).val g - S.ℓ z S.θ₀ g) norm P_Z (id : Z → Z) (_split.foldB n).card (ψ (_split.foldB n).card)
theorem localEmpProcessModulus_of_localized_bounded reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Uniform-bound fallback bridge. Under a localized Rademacher regime — a uniform bound b on the centred pointwise loss difference together with a sub-root Rademacher- complexity envelope ψ, and given that the population excess risk at every admissible parameter is likewise bounded by b, then for any confidence level 0 < δ ≤ 1 the local empirical-process modulus condition holds, with the constant envelope ρ n := √(2 · b).
Formal statement
hypotheses
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
S_iid :
IIDSample Ω Z μ P_Z
split :
OneShotSplit S_iid
Nonempty S.Θ_set
g :
G
idx :
ℕ → S.Θ_set
norm :
(Z → ℝ) → ℝ
ψ :
ℕ → ℝ → ℝ
b :
ℝ
hreg :
LocalizedRademacherRegime S S_iid split g idx norm ψ b
hpop_center :
∀ θ ∈ S.Θ_set, |S.L θ g - S.L S.θ₀ g| ≤ b
δ :
ℝ
_hδ :
0 < δ
_hδ' :
δ ≤ 1
conclusion
LocalEmpProcessModulus S S_iid split (fun _n => sqrt (2 * b)) δ g
Proof (Lean source)
theorem localEmpProcessModulus_of_localized_bounded
(S : LearningSystem Ω μ Z P_Z Θ G) [IsProbabilityMeasure μ]
(S_iid : IIDSample Ω Z μ P_Z) (split : OneShotSplit S_iid)
[Nonempty S.Θ_set]
(g : G)
(idx : ℕ → S.Θ_set)
{norm : (Z → ℝ) → ℝ}
{ψ : ℕ → ℝ → ℝ} {b : ℝ}
(hreg : LocalizedRademacherRegime S S_iid split g idx norm ψ b)
(hpop_center : ∀ θ ∈ S.Θ_set, |S.L θ g - S.L S.θ₀ g| ≤ b)
{δ : ℝ} (_hδ : 0 < δ) (_hδ' : δ ≤ 1) :
LocalEmpProcessModulus S S_iid split
(fun _n => sqrt (2 * b)) δ g := by
intro n
classical
obtain ⟨hb, hbound, _hsub, _hub⟩ := hreg
refine ⟨Set.univ, MeasurableSet.univ, ?_, ?_⟩
· rw [measure_univ]
exact tsub_le_self
· intro ω _ θ hθ
have hpop_abs : |S.L θ g - S.L S.θ₀ g| ≤ b := hpop_center θ hθ
have hemp_abs :
|empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g| ≤ b :=
empRiskFoldB_centered_abs_le S S_iid split hb hbound n ω hθ
have hmain :
(S.L θ g - S.L S.θ₀ g)
- (empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g) ≤ 2 * b := by
have hpop_le : S.L θ g - S.L S.θ₀ g ≤ b :=
(le_abs_self _).trans hpop_abs
have hemp_ge :
-b ≤ empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g :=
(abs_le.mp hemp_abs).1
linarith
have hρsq :
(sqrt (2 * b)) ^ 2 = 2 * b := by
rw [Real.sq_sqrt]
nlinarith
have hρ_nonneg : 0 ≤ sqrt (2 * b) := Real.sqrt_nonneg _
have hnorm_nonneg : 0 ≤ ‖θ - S.θ₀‖ := norm_nonneg _
calc
(S.L θ g - S.L S.θ₀ g)
- (empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g)
≤ 2 * b := hmain
_ = (sqrt (2 * b)) ^ 2 := hρsq.symm
_ ≤ sqrt (2 * b) * ‖θ - S.θ₀‖ + (sqrt (2 * b)) ^ 2 := by
nlinarith [mul_nonneg hρ_nonneg hnorm_nonneg]
theorem localEmpProcessModulus_of_localized_bounded_ae reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Almost-everywhere uniform-bound fallback bridge. Under an almost-everywhere localized Rademacher regime — a P_Z-a.e. bound b on the centred pointwise loss difference together with a sub-root Rademacher-complexity envelope ψ, and given that the population excess risk at every admissible parameter is likewise bounded by b, then for any confidence level 0 < δ ≤ 1 the local empirical-process modulus condition holds, with the constant envelope ρ n := √(2 · b).
Formal statement
hypotheses
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
S_iid :
IIDSample Ω Z μ P_Z
split :
OneShotSplit S_iid
Nonempty S.Θ_set
g :
G
idx :
ℕ → S.Θ_set
norm :
(Z → ℝ) → ℝ
ψ :
ℕ → ℝ → ℝ
b :
ℝ
hreg :
LocalizedRademacherRegimeAE S S_iid split g idx norm ψ b
hpop_center :
∀ θ ∈ S.Θ_set, |S.L θ g - S.L S.θ₀ g| ≤ b
δ :
ℝ
_hδ :
0 < δ
_hδ' :
δ ≤ 1
conclusion
LocalEmpProcessModulus S S_iid split (fun _n => sqrt (2 * b)) δ g
Proof (Lean source)
theorem localEmpProcessModulus_of_localized_bounded_ae
(S : LearningSystem Ω μ Z P_Z Θ G) [IsProbabilityMeasure μ]
(S_iid : IIDSample Ω Z μ P_Z) (split : OneShotSplit S_iid)
[Nonempty S.Θ_set]
(g : G)
(idx : ℕ → S.Θ_set)
{norm : (Z → ℝ) → ℝ}
{ψ : ℕ → ℝ → ℝ} {b : ℝ}
(hreg : LocalizedRademacherRegimeAE S S_iid split g idx norm ψ b)
(hpop_center : ∀ θ ∈ S.Θ_set, |S.L θ g - S.L S.θ₀ g| ≤ b)
{δ : ℝ} (_hδ : 0 < δ) (_hδ' : δ ≤ 1) :
LocalEmpProcessModulus S S_iid split
(fun _n => sqrt (2 * b)) δ g := by
intro n
classical
obtain ⟨hb, hbound_ae, _hsub, _hub⟩ := hreg
let Gn : Set Ω :=
{ω | ∀ i ∈ split.foldB n, ∀ θ ∈ S.Θ_set,
|S.ℓ (S_iid.Z i ω) θ g - S.ℓ (S_iid.Z i ω) S.θ₀ g| ≤ b}
have hsample_all_ae : ∀ i : ℕ, ∀ᵐ ω ∂μ,
∀ θ ∈ S.Θ_set,
|S.ℓ (S_iid.Z i ω) θ g - S.ℓ (S_iid.Z i ω) S.θ₀ g| ≤ b := by
intro i
have hlaw_i : μ.map (S_iid.Z i) = P_Z := by
rw [← (S_iid.identDist i).map_eq, S_iid.law]
have hmap : ∀ᵐ z ∂μ.map (S_iid.Z i),
∀ θ ∈ S.Θ_set, |S.ℓ z θ g - S.ℓ z S.θ₀ g| ≤ b := by
simpa [hlaw_i] using hbound_ae
exact ae_of_ae_map (S_iid.meas i).aemeasurable hmap
have hGn_ae : ∀ᵐ ω ∂μ, ω ∈ Gn := by
have hfin : ∀ᵐ ω ∂μ, ∀ i ∈ split.foldB n,
∀ θ ∈ S.Θ_set,
|S.ℓ (S_iid.Z i ω) θ g - S.ℓ (S_iid.Z i ω) S.θ₀ g| ≤ b := by
simpa using (Finset.eventually_all (split.foldB n)).2
(fun i _hi => hsample_all_ae i)
simpa [Gn] using hfin
have hGn_null : μ Gnᶜ = 0 := ae_iff.mp hGn_ae
rcases exists_measurable_superset_of_null hGn_null with
⟨N, hGn_compl_subset_N, hN_meas, hN_null⟩
refine ⟨Set.univ \ N, MeasurableSet.univ.diff hN_meas, ?_, ?_⟩
· rw [measure_diff_null hN_null, measure_univ]
exact tsub_le_self
· intro ω hω θ hθ
have hωG : ω ∈ Gn := by
by_contra hnot
exact hω.2 (hGn_compl_subset_N hnot)
have hpop_abs : |S.L θ g - S.L S.θ₀ g| ≤ b := hpop_center θ hθ
have hemp_abs :
|empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g| ≤ b :=
empRiskFoldB_centered_abs_le_ae S S_iid split hb n ω
(by simpa [Gn] using hωG) hθ
have hmain :
(S.L θ g - S.L S.θ₀ g)
- (empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g) ≤ 2 * b := by
have hpop_le : S.L θ g - S.L S.θ₀ g ≤ b :=
(le_abs_self _).trans hpop_abs
have hemp_ge :
-b ≤ empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g :=
(abs_le.mp hemp_abs).1
linarith
have hρsq :
(sqrt (2 * b)) ^ 2 = 2 * b := by
rw [Real.sq_sqrt]
nlinarith
have hρ_nonneg : 0 ≤ sqrt (2 * b) := Real.sqrt_nonneg _
have hnorm_nonneg : 0 ≤ ‖θ - S.θ₀‖ := norm_nonneg _
calc
(S.L θ g - S.L S.θ₀ g)
- (empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g)
≤ 2 * b := hmain
_ = (sqrt (2 * b)) ^ 2 := hρsq.symm
_ ≤ sqrt (2 * b) * ‖θ - S.θ₀‖ + (sqrt (2 * b)) ^ 2 := by
nlinarith [mul_nonneg hρ_nonneg hnorm_nonneg]
def CenteredClampedThetaMinimizes reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
For an orthogonal statistical-learning system and a real clamp radius, the centered clamped target-minimization condition states that every candidate target has auxiliary population risk at least that of the designated target, where its excess loss relative to the designated target is clamped to .
Definition (Lean source)
parameters
def
CenteredClampedThetaMinimizes S b :
Prop
theorem localEmpProcessModulus_of_localized_sharp reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Localized critical-radius modulus, countable-class Foster–Syrgkanis form. Fix a countable, densely-indexed target class on which the loss is continuous in the parameter for every observation and a localized Rademacher regime holds — a uniform centred-loss bound and a sub-root Rademacher-complexity envelope ψ. Suppose the Lipschitz constant L is nonnegative, that the chosen function-space norm of the centred loss difference at each parameter is bounded by L · ‖θ − θ₀‖, that the loss at each parameter is measurable and integrable under P_Z, and that the same centred loss difference has diameter at most Rmax in that norm. Assume the critical radius of ψ at every fold-B sample size satisfies criticalRadius (ψ m) ≤ Rmax and criticalRadius (ψ m) > 0, together with the sub-root fixed-point inequality ψ m (criticalRadius (ψ m)) ≤ criticalRadius (ψ m) ^ 2; that ψ upper-bounds the population Rademacher complexity of the star-hulled centred loss class on a fold-B-sized sample; and the technical regularity conditions that the empirical Rademacher supremum is bounded above and the upper empirical Rademacher complexity process is integrable. For any confidence level 0 < δ ≤ 1, assume the Foster–Syrgkanis peeling-absorption condition that at every dyadic shell count covering Rmax, the McDiarmid concentration slack at the union-bound-adjusted confidence is dominated by the squared critical radius. Then the local empirical-process modulus condition holds, with envelope ρ n := (8 · L + 3) · criticalRadius (ψ |foldB n|) (falling back to √(2 · b) when the fold-B sample is empty).
Formal statement
hypotheses
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
S_iid :
IIDSample Ω Z μ P_Z
split :
OneShotSplit S_iid
Nonempty S.Θ_set
Countable S.Θ_set
g :
G
_hg_cont :
∀ z, Continuous fun (θ : S.Θ_set) => S.ℓ z θ.val g
idx :
ℕ → S.Θ_set
_idx_dense :
DenseRange idx
norm :
(Z → ℝ) → ℝ
ψ :
ℕ → ℝ → ℝ
b L Rmax :
ℝ
hreg :
LocalizedRademacherRegime S S_iid split g idx norm ψ b
hL_nonneg :
0 ≤ L
hF_lip :
∀ θ ∈ S.Θ_set, norm (fun z => S.ℓ z θ g - S.ℓ z S.θ₀ g) ≤ L * ‖θ - S.θ₀‖
hℓ_meas :
∀ θ ∈ S.Θ_set, Measurable (fun z => S.ℓ z θ g)
hℓ_int :
∀ θ ∈ S.Θ_set, Integrable (fun z => S.ℓ z θ g) P_Z
hF_diam :
∀ θ ∈ S.Θ_set, norm (fun z => S.ℓ z θ g - S.ℓ z S.θ₀ g) ≤ Rmax
n-dependent critical-radius hypotheses (ψ m is the envelope at sample size m).
hRmax_lb :
∀ m : ℕ, criticalRadius (ψ m) ≤ Rmax
hcrit_pos :
∀ m : ℕ, 0 < criticalRadius (ψ m)
hcrit_fp :
∀ m : ℕ, ψ m (criticalRadius (ψ m)) ≤ (criticalRadius (ψ m)) ^ 2
hψ_ub :
∀ m : ℕ,
RademacherUpperBound (fun (θ : S.Θ_set) (z : Z) => S.ℓ z θ.val g - S.ℓ z S.θ₀ g) norm P_Z (id : Z → Z) m (ψ m)
BddAbove hypothesis needed by the bridge lemma inside `localized_uniform_deviation`.
_hrad_bdd :
∀ m r,
∀ S_fin : Fin m → Z,
∀ σ : Signs m,
BddAbove (Set.range fun p : starHullParam S.Θ_set => |(m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * starHullZeroOut (fun (θ : S.Θ_set) (z : Z) => S.ℓ z θ.val g - S.ℓ z S.θ₀ g) norm r p (S_fin k)|)
Integrability of the upper empirical Rademacher process; consumed by the bridge lemma inside `localized_uniform_deviation`.
hrad_int :
∀ m r,
Integrable (fun ω : Fin m → Z => empiricalRademacherComplexity m (starHullZeroOut (fun (θ : S.Θ_set) (z : Z) => S.ℓ z θ.val g - S.ℓ z S.θ₀ g) norm r) ((id : Z → Z) ∘ ω)) (Measure.pi (fun _ => P_Z))
δ :
ℝ
hδ :
0 < δ
hδ' :
δ ≤ 1
Foster–Syrgkanis Lemma 29 critical-radius lower bound (peeling-aware): for any dyadic shell count `K` covering `Rmax`, the McDiarmid slack at the union-bound-adjusted confidence `δ / (2 (K + 1))` is dominated by the squared critical radius. The `K + 1` accounts for the union over `K + 1` dyadic shells in the peeling argument; the factor `2` keeps the intersection event mass `≥ 1 − δ` strictly. This absorbs every `b · √(log(·)/m)` term into the `δ_n²` part of the modulus inequality.
hδ_dom :
∀ n K : ℕ
if
0 < (split.foldB n).card
and
Rmax ≤ (criticalRadius (ψ (split.foldB n).card)) * (2 : ℝ) ^ K
then
≤ (criticalRadius (ψ (split.foldB n).card)) ^ 2
conclusion
LocalEmpProcessModulus S S_iid split (fun n => if (split.foldB n).card = 0 then sqrt (2 * b) else (8 * L + 3) * criticalRadius (ψ (split.foldB n).card)) δ g
Proof (Lean source)
theorem localEmpProcessModulus_of_localized_sharp
(S : LearningSystem Ω μ Z P_Z Θ G) [IsProbabilityMeasure μ]
(S_iid : IIDSample Ω Z μ P_Z) (split : OneShotSplit S_iid)
[Nonempty S.Θ_set] [Countable S.Θ_set]
(g : G)
(_hg_cont : ∀ z, Continuous fun (θ : S.Θ_set) => S.ℓ z θ.val g)
(idx : ℕ → S.Θ_set)
(_idx_dense : DenseRange idx)
{norm : (Z → ℝ) → ℝ}
{ψ : ℕ → ℝ → ℝ} {b L Rmax : ℝ}
(hreg : LocalizedRademacherRegime S S_iid split g idx norm ψ b)
(hL_nonneg : 0 ≤ L)
(hF_lip : ∀ θ ∈ S.Θ_set,
norm (fun z => S.ℓ z θ g - S.ℓ z S.θ₀ g) ≤ L * ‖θ - S.θ₀‖)
(hℓ_meas : ∀ θ ∈ S.Θ_set, Measurable (fun z => S.ℓ z θ g))
(hℓ_int : ∀ θ ∈ S.Θ_set, Integrable (fun z => S.ℓ z θ g) P_Z)
(hF_diam : ∀ θ ∈ S.Θ_set,
norm (fun z => S.ℓ z θ g - S.ℓ z S.θ₀ g) ≤ Rmax)
-- n-dependent critical-radius hypotheses (ψ m is the envelope at sample size m).
(hRmax_lb : ∀ m : ℕ, criticalRadius (ψ m) ≤ Rmax)
(hcrit_pos : ∀ m : ℕ, 0 < criticalRadius (ψ m))
(hcrit_fp : ∀ m : ℕ, ψ m (criticalRadius (ψ m)) ≤ (criticalRadius (ψ m)) ^ 2)
(hψ_ub : ∀ m : ℕ,
RademacherUpperBound
(fun (θ : S.Θ_set) (z : Z) => S.ℓ z θ.val g - S.ℓ z S.θ₀ g)
norm P_Z (id : Z → Z) m (ψ m))
-- BddAbove hypothesis needed by the bridge lemma inside `localized_uniform_deviation`.
(_hrad_bdd : ∀ m r, ∀ S_fin : Fin m → Z, ∀ σ : Signs m,
BddAbove (Set.range fun p : starHullParam S.Θ_set =>
|(m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) *
starHullZeroOut
(fun (θ : S.Θ_set) (z : Z) => S.ℓ z θ.val g - S.ℓ z S.θ₀ g)
norm r p (S_fin k)|))
-- Integrability of the upper empirical Rademacher process; consumed by the
-- bridge lemma inside `localized_uniform_deviation`.
(hrad_int : ∀ m r,
Integrable
(fun ω : Fin m → Z =>
empiricalRademacherComplexity m
(starHullZeroOut
(fun (θ : S.Θ_set) (z : Z) => S.ℓ z θ.val g - S.ℓ z S.θ₀ g)
norm r) ((id : Z → Z) ∘ ω))
(Measure.pi (fun _ => P_Z)))
{δ : ℝ} (hδ : 0 < δ) (hδ' : δ ≤ 1)
-- Foster–Syrgkanis Lemma 29 critical-radius lower bound (peeling-aware):
-- for any dyadic shell count `K` covering `Rmax`, the McDiarmid slack at
-- the union-bound-adjusted confidence `δ / (2 (K + 1))` is dominated by
-- the squared critical radius. The `K + 1` accounts for the union over
-- `K + 1` dyadic shells in the peeling argument; the factor `2` keeps the
-- intersection event mass `≥ 1 − δ` strictly. This absorbs every
-- `b · √(log(·)/m)` term into the `δ_n²` part of the modulus inequality.
(hδ_dom : ∀ n K : ℕ, 0 < (split.foldB n).card →
Rmax ≤ (criticalRadius (ψ (split.foldB n).card)) * (2 : ℝ) ^ K →
b * sqrt
(2 * log (2 * ((K : ℝ) + 1) / δ) / (split.foldB n).card)
≤ (criticalRadius (ψ (split.foldB n).card)) ^ 2) :
LocalEmpProcessModulus S S_iid split
(fun n =>
if (split.foldB n).card = 0 then sqrt (2 * b)
else (8 * L + 3) * criticalRadius (ψ (split.foldB n).card)) δ g := by
intro n
classical
obtain ⟨hb, hbound, hsub, _hub_idx⟩ := hreg
haveI : IsProbabilityMeasure P_Z := by
rw [← S_iid.law]
exact Measure.isProbabilityMeasure_map (S_iid.meas 0).aemeasurable
by_cases hm0 : (split.foldB n).card = 0
· refine ⟨Set.univ, MeasurableSet.univ, ?_, ?_⟩
· rw [measure_univ]
exact tsub_le_self
· intro ω _ θ hθ
have hfold_empty : split.foldB n = ∅ := Finset.card_eq_zero.mp hm0
have hcenter_int :
Integrable (fun z => S.ℓ z θ g - S.ℓ z S.θ₀ g) P_Z :=
(hℓ_int θ hθ).sub (hℓ_int S.θ₀ S.θ₀_mem)
have hmean_eq :
(∫ z, S.ℓ z θ g - S.ℓ z S.θ₀ g ∂P_Z) =
S.L θ g - S.L S.θ₀ g := by
change (∫ z, S.ℓ z θ g - S.ℓ z S.θ₀ g ∂P_Z) =
(∫ z, S.ℓ z θ g ∂P_Z) - (∫ z, S.ℓ z S.θ₀ g ∂P_Z)
exact integral_sub (hℓ_int θ hθ) (hℓ_int S.θ₀ S.θ₀_mem)
have hpop_abs : |S.L θ g - S.L S.θ₀ g| ≤ b := by
rw [← hmean_eq]
calc
|∫ z, S.ℓ z θ g - S.ℓ z S.θ₀ g ∂P_Z|
≤ ∫ z, |S.ℓ z θ g - S.ℓ z S.θ₀ g| ∂P_Z :=
abs_integral_le_integral_abs
_ ≤ ∫ _z, b ∂P_Z := by
apply integral_mono
· exact hcenter_int.abs
· exact integrable_const b
· intro z
exact hbound z θ hθ
_ = b := by simp
have hρsq :
(if (split.foldB n).card = 0 then sqrt (2 * b)
else (8 * L + 3) * criticalRadius (ψ (split.foldB n).card)) ^ 2 =
2 * b := by
rw [if_pos hm0, Real.sq_sqrt]
nlinarith
have hρ_nonneg :
0 ≤
(if (split.foldB n).card = 0 then sqrt (2 * b)
else (8 * L + 3) * criticalRadius (ψ (split.foldB n).card)) := by
rw [if_pos hm0]
exact Real.sqrt_nonneg _
have hnorm_nonneg : 0 ≤ ‖θ - S.θ₀‖ := norm_nonneg _
calc
(S.L θ g - S.L S.θ₀ g)
- (empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g)
= S.L θ g - S.L S.θ₀ g := by
simp [empRiskFoldB, hfold_empty]
_ ≤ b := (le_abs_self _).trans hpop_abs
_ ≤ 2 * b := by nlinarith
_ =
(if (split.foldB n).card = 0 then sqrt (2 * b)
else (8 * L + 3) * criticalRadius (ψ (split.foldB n).card)) ^ 2 :=
hρsq.symm
_ ≤
(if (split.foldB n).card = 0 then sqrt (2 * b)
else (8 * L + 3) * criticalRadius (ψ (split.foldB n).card)) *
‖θ - S.θ₀‖
+
(if (split.foldB n).card = 0 then sqrt (2 * b)
else (8 * L + 3) * criticalRadius (ψ (split.foldB n).card)) ^ 2 := by
nlinarith [mul_nonneg hρ_nonneg hnorm_nonneg]
· have hm_pos_nat : 0 < (split.foldB n).card := Nat.pos_of_ne_zero hm0
let m : ℕ := (split.foldB n).card
let δn : ℝ := criticalRadius (ψ m)
haveI : Nonempty Z := nonempty_of_isProbabilityMeasure P_Z
let F : S.Θ_set → Z → ℝ :=
fun θ z => S.ℓ z θ.val g - S.ℓ z S.θ₀ g
have hF_meas_full : ∀ θ : S.Θ_set, Measurable (F θ) := by
intro θ
exact (hℓ_meas θ.val θ.property).sub (hℓ_meas S.θ₀ S.θ₀_mem)
let Rloc : LocalizedRegime Z S.Θ_set Z F norm P_Z (id : Z → Z) :=
{ b := b
b_nonneg := hb
bound := by
intro θ z
exact hbound z θ.val θ.property
ψ := ψ
ψ_subRoot := hsub
ψ_ub := by
intro m'
simpa [F] using hψ_ub m' }
have hdev_Rmax :
∃ E : Set (Fin m → Z), MeasurableSet E ∧
Measure.pi (fun _ => P_Z) E ≥ 1 - ofReal δ ∧
∀ ω ∈ E, ∀ θ : S.Θ_set, norm (F θ) ≤ Rmax →
|(m : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin m => F θ ((id : Z → Z) (ω k)))
- P_Z[fun z => F θ ((id : Z → Z) z)]|
≤ 4 * Rmax * criticalRadius (Rloc.ψ m)
+ Rloc.b * sqrt (2 * log (1 / δ) / m) := by
exact localized_uniform_deviation F norm P_Z (id : Z → Z)
measurable_id hF_meas_full Rloc hδ hδ' m
(by simpa [m] using hm_pos_nat) (r := Rmax) (by simpa [Rloc] using hRmax_lb m)
(by simpa [Rloc] using hcrit_pos m) (by simpa [Rloc] using hcrit_fp m)
(by simpa [F] using _hrad_bdd m Rmax)
(by simpa [F, Function.comp_def] using hrad_int m Rmax)
have hnonempty_modulus :
∃ E : Set Ω, MeasurableSet E ∧ μ E ≥ 1 - ofReal δ ∧
∀ ω ∈ E, ∀ θ ∈ S.Θ_set,
(S.L θ g - S.L S.θ₀ g)
- (empRiskFoldB S S_iid split n ω θ g
- empRiskFoldB S S_iid split n ω S.θ₀ g)
≤ ((8 * L + 3) * δn) * ‖θ - S.θ₀‖
+ ((8 * L + 3) * δn) ^ 2 := by
have hpeelingK : ∃ K : ℕ, Rmax ≤ δn * (2 : ℝ) ^ K := by
have hδn_pos : 0 < δn := hcrit_pos m
-- 2^K → ∞, so for K large enough, δn · 2^K ≥ Rmax.
rcases pow_unbounded_of_one_lt (Rmax / δn) (by norm_num : (1 : ℝ) < 2) with ⟨K, hK⟩
refine ⟨K, ?_⟩
rw [div_lt_iff₀ hδn_pos] at hK
linarith [hK]
-- … truncated; follow the source link for the rest …
theorem localEmpProcessModulus_of_localized_sharp_ae reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Almost-everywhere countable-class localized bridge. Fix a countable, densely-indexed target class on which the loss is continuous in the parameter for every observation and the chosen function-space norm is invariant under P_Z-a.e. equality of its argument. Assume an almost-everywhere localized Rademacher regime holds — a uniform centred-loss bound and a sub-root Rademacher-complexity envelope ψ, that the Lipschitz constant L is nonnegative, that the norm of the centred loss difference at each parameter is bounded by L · ‖θ − θ₀‖, that the loss at each parameter is measurable and integrable under P_Z, and that the same centred loss difference has diameter at most Rmax in that norm. Assume the critical radius of ψ at every fold-B sample size satisfies criticalRadius (ψ m) ≤ Rmax and criticalRadius (ψ m) > 0, together with the sub-root fixed-point inequality ψ m (criticalRadius (ψ m)) ≤ criticalRadius (ψ m) ^ 2; that ψ upper-bounds the population Rademacher complexity of the star-hulled centred loss class on a fold-B-sized sample; the technical regularity conditions that the empirical Rademacher supremum is bounded above and the upper empirical Rademacher complexity process is integrable; and that the population-optimal parameter minimizes the auxiliary population risk with the centred excess loss clamped to [-b, b]. For any confidence level 0 < δ ≤ 1, assume the Foster–Syrgkanis peeling-absorption condition that at every dyadic shell count covering Rmax, the McDiarmid concentration slack at the union-bound-adjusted confidence is dominated by the squared critical radius. Then the local empirical-process modulus condition holds, with envelope ρ n := (8 · L + 3) · criticalRadius (ψ |foldB n|) (falling back to √(2 · b) when the fold-B sample is empty).
Formal statement
hypotheses
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
S_iid :
IIDSample Ω Z μ P_Z
split :
OneShotSplit S_iid
Nonempty S.Θ_set
Countable S.Θ_set
g :
G
_hg_cont :
∀ z, Continuous fun (θ : S.Θ_set) => S.ℓ z θ.val g
idx :
ℕ → S.Θ_set
_idx_dense :
DenseRange idx
norm :
(Z → ℝ) → ℝ
hnorm_ae :
∀ F F' : Z → ℝ
if
F =ᵐ[P_Z] F'
then
norm F = norm F'
ψ :
ℕ → ℝ → ℝ
b L Rmax :
ℝ
hreg :
LocalizedRademacherRegimeAE S S_iid split g idx norm ψ b
hL_nonneg :
0 ≤ L
hF_lip :
∀ θ ∈ S.Θ_set, norm (fun z => S.ℓ z θ g - S.ℓ z S.θ₀ g) ≤ L * ‖θ - S.θ₀‖
hℓ_meas :
∀ θ ∈ S.Θ_set, Measurable (fun z => S.ℓ z θ g)
hℓ_int :
∀ θ ∈ S.Θ_set, Integrable (fun z => S.ℓ z θ g) P_Z
hF_diam :
∀ θ ∈ S.Θ_set, norm (fun z => S.ℓ z θ g - S.ℓ z S.θ₀ g) ≤ Rmax
hRmax_lb :
∀ m : ℕ, criticalRadius (ψ m) ≤ Rmax
hcrit_pos :
∀ m : ℕ, 0 < criticalRadius (ψ m)
hcrit_fp :
∀ m : ℕ, ψ m (criticalRadius (ψ m)) ≤ (criticalRadius (ψ m)) ^ 2
hψ_ub :
∀ m : ℕ,
RademacherUpperBound (fun (θ : S.Θ_set) (z : Z) => S.ℓ z θ.val g - S.ℓ z S.θ₀ g) norm P_Z (id : Z → Z) m (ψ m)
hrad_bdd :
∀ m r,
∀ S_fin : Fin m → Z,
∀ σ : Signs m,
BddAbove (Set.range fun p : starHullParam S.Θ_set => |(m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * starHullZeroOut (fun (θ : S.Θ_set) (z : Z) => S.ℓ z θ.val g - S.ℓ z S.θ₀ g) norm r p (S_fin k)|)
hrad_int :
∀ m r,
Integrable (fun ω : Fin m → Z => empiricalRademacherComplexity m (starHullZeroOut (fun (θ : S.Θ_set) (z : Z) => S.ℓ z θ.val g - S.ℓ z S.θ₀ g) norm r) ((id : Z → Z) ∘ ω)) (Measure.pi (fun _ => P_Z))
hclamp_minimizes :
δ :
ℝ
hδ :
0 < δ
hδ' :
δ ≤ 1
hδ_dom :
∀ n K : ℕ
if
0 < (split.foldB n).card
and
Rmax ≤ (criticalRadius (ψ (split.foldB n).card)) * (2 : ℝ) ^ K
then
≤ (criticalRadius (ψ (split.foldB n).card)) ^ 2
conclusion
LocalEmpProcessModulus S S_iid split (fun n => if (split.foldB n).card = 0 then sqrt (2 * b) else (8 * L + 3) * criticalRadius (ψ (split.foldB n).card)) δ g
Proof (Lean source)
theorem localEmpProcessModulus_of_localized_sharp_ae
(S : LearningSystem Ω μ Z P_Z Θ G) [IsProbabilityMeasure μ]
(S_iid : IIDSample Ω Z μ P_Z) (split : OneShotSplit S_iid)
[Nonempty S.Θ_set] [Countable S.Θ_set]
(g : G)
(_hg_cont : ∀ z, Continuous fun (θ : S.Θ_set) => S.ℓ z θ.val g)
(idx : ℕ → S.Θ_set)
(_idx_dense : DenseRange idx)
{norm : (Z → ℝ) → ℝ}
(hnorm_ae : ∀ F F' : Z → ℝ, F =ᵐ[P_Z] F' → norm F = norm F')
{ψ : ℕ → ℝ → ℝ} {b L Rmax : ℝ}
(hreg : LocalizedRademacherRegimeAE S S_iid split g idx norm ψ b)
(hL_nonneg : 0 ≤ L)
(hF_lip : ∀ θ ∈ S.Θ_set,
norm (fun z => S.ℓ z θ g - S.ℓ z S.θ₀ g) ≤ L * ‖θ - S.θ₀‖)
(hℓ_meas : ∀ θ ∈ S.Θ_set, Measurable (fun z => S.ℓ z θ g))
(hℓ_int : ∀ θ ∈ S.Θ_set, Integrable (fun z => S.ℓ z θ g) P_Z)
(hF_diam : ∀ θ ∈ S.Θ_set,
norm (fun z => S.ℓ z θ g - S.ℓ z S.θ₀ g) ≤ Rmax)
(hRmax_lb : ∀ m : ℕ, criticalRadius (ψ m) ≤ Rmax)
(hcrit_pos : ∀ m : ℕ, 0 < criticalRadius (ψ m))
(hcrit_fp : ∀ m : ℕ, ψ m (criticalRadius (ψ m)) ≤ (criticalRadius (ψ m)) ^ 2)
(hψ_ub : ∀ m : ℕ,
RademacherUpperBound
(fun (θ : S.Θ_set) (z : Z) => S.ℓ z θ.val g - S.ℓ z S.θ₀ g)
norm P_Z (id : Z → Z) m (ψ m))
(hrad_bdd : ∀ m r, ∀ S_fin : Fin m → Z, ∀ σ : Signs m,
BddAbove (Set.range fun p : starHullParam S.Θ_set =>
|(m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) *
starHullZeroOut
(fun (θ : S.Θ_set) (z : Z) => S.ℓ z θ.val g - S.ℓ z S.θ₀ g)
norm r p (S_fin k)|))
(hrad_int : ∀ m r,
Integrable
(fun ω : Fin m → Z =>
empiricalRademacherComplexity m
(starHullZeroOut
(fun (θ : S.Θ_set) (z : Z) => S.ℓ z θ.val g - S.ℓ z S.θ₀ g)
norm r) ((id : Z → Z) ∘ ω))
(Measure.pi (fun _ => P_Z)))
(hclamp_minimizes : CenteredClampedThetaMinimizes S b)
{δ : ℝ} (hδ : 0 < δ) (hδ' : δ ≤ 1)
(hδ_dom : ∀ n K : ℕ, 0 < (split.foldB n).card →
Rmax ≤ (criticalRadius (ψ (split.foldB n).card)) * (2 : ℝ) ^ K →
b * sqrt
(2 * log (2 * ((K : ℝ) + 1) / δ) / (split.foldB n).card)
≤ (criticalRadius (ψ (split.foldB n).card)) ^ 2) :
LocalEmpProcessModulus S S_iid split
(fun n =>
if (split.foldB n).card = 0 then sqrt (2 * b)
else (8 * L + 3) * criticalRadius (ψ (split.foldB n).card)) δ g := by
classical
obtain ⟨hb, hbound_ae, hsub, hub_idx⟩ := hreg
haveI : IsProbabilityMeasure P_Z := by
rw [← S_iid.law]
exact Measure.isProbabilityMeasure_map (S_iid.meas 0).aemeasurable
let clamp : ℝ → ℝ := fun t => max (-b) (min b t)
let Sc : LearningSystem Ω μ Z P_Z Θ G :=
{ S with
ℓ := fun z θ g' =>
S.ℓ z S.θ₀ g' + clamp (S.ℓ z θ g' - S.ℓ z S.θ₀ g')
ℓ_meas := fun θ g' => by
dsimp [clamp]
exact (S.ℓ_meas S.θ₀ g').add
(measurable_const.max
(measurable_const.min ((S.ℓ_meas θ g').sub (S.ℓ_meas S.θ₀ g'))))
θ₀_minimizes := by
intro θ hθ
simpa [CenteredClampedThetaMinimizes, clamp] using hclamp_minimizes θ hθ }
have hclamp_abs : ∀ t : ℝ, |clamp t| ≤ b := by
intro t
rw [abs_le]
constructor
· dsimp [clamp]
exact le_max_left (-b) (min b t)
· dsimp [clamp]
exact max_le (by linarith) (min_le_left b t)
have hclamp_zero : clamp 0 = 0 := by
dsimp [clamp]
rw [min_eq_right hb, max_eq_right]
linarith
have hclamp_eq_of_abs_le : ∀ {t : ℝ}, |t| ≤ b → clamp t = t := by
intro t ht
have ht_low : -b ≤ t := (abs_le.mp ht).1
have ht_high : t ≤ b := (abs_le.mp ht).2
dsimp [clamp]
rw [min_eq_right ht_high, max_eq_right ht_low]
have hSc_center :
∀ z θ, θ ∈ S.Θ_set →
Sc.ℓ z θ g - Sc.ℓ z Sc.θ₀ g =
clamp (S.ℓ z θ g - S.ℓ z S.θ₀ g) := by
intro z θ _hθ
dsimp [Sc]
have hzero_arg : S.ℓ z S.θ₀ g - S.ℓ z S.θ₀ g = 0 := by ring
rw [hzero_arg]
rw [hclamp_zero]
ring
have hSc_bound :
∀ z, ∀ θ ∈ Sc.Θ_set, |Sc.ℓ z θ g - Sc.ℓ z Sc.θ₀ g| ≤ b := by
intro z θ hθ
rw [hSc_center z θ (by simpa [Sc] using hθ)]
exact hclamp_abs _
let Fs : S.Θ_set → Z → ℝ :=
fun θ z => S.ℓ z θ.val g - S.ℓ z S.θ₀ g
let Fc : S.Θ_set → Z → ℝ :=
fun θ z => Sc.ℓ z θ.val g - Sc.ℓ z Sc.θ₀ g
have hcenter_all_ae :
∀ᵐ z ∂P_Z, ∀ θ : S.Θ_set, Fs θ z = Fc θ z := by
filter_upwards [hbound_ae] with z hz θ
have hc := hclamp_eq_of_abs_le (hz θ.val θ.property)
calc
Fs θ z = S.ℓ z θ.val g - S.ℓ z S.θ₀ g := rfl
_ = clamp (S.ℓ z θ.val g - S.ℓ z S.θ₀ g) := hc.symm
_ = Fc θ z := by
dsimp [Fc]
rw [hSc_center z θ.val θ.property]
have hstar_all_ae :
∀ r : ℝ, ∀ᵐ z ∂P_Z, ∀ p : starHullParam S.Θ_set,
starHullZeroOut Fs norm r p z = starHullZeroOut Fc norm r p z := by
intro r
filter_upwards [hcenter_all_ae] with z hz p
have hstar_ae : starHullEval Fs p =ᵐ[P_Z] starHullEval Fc p := by
filter_upwards [hcenter_all_ae] with z' hz'
dsimp [starHullEval]
rw [hz' p.2]
have hnorm_eq : norm (starHullEval Fs p) = norm (starHullEval Fc p) :=
hnorm_ae _ _ hstar_ae
have hpval : starHullEval Fs p z = starHullEval Fc p z := by
dsimp [starHullEval]
rw [hz p.2]
by_cases hp : norm (starHullEval Fs p) ≤ r
· have hpc : norm (starHullEval Fc p) ≤ r := hnorm_eq ▸ hp
change
(if norm (starHullEval Fs p) ≤ r then starHullEval Fs p z else 0) =
(if norm (starHullEval Fc p) ≤ r then starHullEval Fc p z else 0)
rw [if_pos hp, if_pos hpc]
exact hpval
· have hpc : ¬ norm (starHullEval Fc p) ≤ r := by
intro hc
exact hp (hnorm_eq.symm ▸ hc)
change
(if norm (starHullEval Fs p) ≤ r then starHullEval Fs p z else 0) =
(if norm (starHullEval Fc p) ≤ r then starHullEval Fc p z else 0)
rw [if_neg hp, if_neg hpc]
have hℓ_all_ae :
∀ᵐ z ∂P_Z, ∀ θ ∈ S.Θ_set, S.ℓ z θ g = Sc.ℓ z θ g := by
filter_upwards [hbound_ae] with z hz θ hθ
have hc := hclamp_eq_of_abs_le (hz θ hθ)
dsimp [Sc]
rw [hc]
ring
have hL_eq : ∀ θ, θ ∈ S.Θ_set → S.L θ g = Sc.L θ g := by
intro θ hθ
dsimp [LearningSystem.L]
apply integral_congr_ae
filter_upwards [hℓ_all_ae] with z hz
exact hz θ hθ
have hSc_lip : ∀ θ ∈ Sc.Θ_set,
norm (fun z => Sc.ℓ z θ g - Sc.ℓ z Sc.θ₀ g) ≤ L * ‖θ - Sc.θ₀‖ := by
intro θ hθ
have hθS : θ ∈ S.Θ_set := by simpa [Sc] using hθ
have hae : (fun z => Sc.ℓ z θ g - Sc.ℓ z Sc.θ₀ g) =ᵐ[P_Z]
fun z => S.ℓ z θ g - S.ℓ z S.θ₀ g := by
filter_upwards [hcenter_all_ae] with z hz
exact (hz ⟨θ, hθS⟩).symm
rw [hnorm_ae _ _ hae]
simpa [Sc] using hF_lip θ hθS
have hSc_diam : ∀ θ ∈ Sc.Θ_set,
norm (fun z => Sc.ℓ z θ g - Sc.ℓ z Sc.θ₀ g) ≤ Rmax := by
intro θ hθ
have hθS : θ ∈ S.Θ_set := by simpa [Sc] using hθ
have hae : (fun z => Sc.ℓ z θ g - Sc.ℓ z Sc.θ₀ g) =ᵐ[P_Z]
fun z => S.ℓ z θ g - S.ℓ z S.θ₀ g := by
filter_upwards [hcenter_all_ae] with z hz
exact (hz ⟨θ, hθS⟩).symm
rw [hnorm_ae _ _ hae]
simpa [Sc] using hF_diam θ hθS
have hSc_ψ_ub : ∀ m : ℕ,
RademacherUpperBound
(fun (θ : Sc.Θ_set) (z : Z) => Sc.ℓ z θ.val g - Sc.ℓ z Sc.θ₀ g)
norm P_Z (id : Z → Z) m (ψ m) := by
intro m r hr
have hcongr :
rademacherComplexity m (starHullZeroOut Fs norm r) P_Z (id : Z → Z) =
rademacherComplexity m (starHullZeroOut Fc norm r) P_Z (id : Z → Z) :=
rademacherComplexity_congr_ae_all m
(starHullZeroOut Fs norm r) (starHullZeroOut Fc norm r)
P_Z (id : Z → Z) (by simpa using hstar_all_ae r)
calc
rademacherComplexity m
(starHullZeroOut
(fun (θ : Sc.Θ_set) (z : Z) => Sc.ℓ z θ.val g - Sc.ℓ z Sc.θ₀ g)
norm r) P_Z (id : Z → Z)
= rademacherComplexity m (starHullZeroOut Fc norm r) P_Z (id : Z → Z) := by
rfl
_ = rademacherComplexity m (starHullZeroOut Fs norm r) P_Z (id : Z → Z) :=
hcongr.symm
_ ≤ ψ m r := by
simpa [Fs] using hψ_ub m r hr
let idxc : ℕ → Sc.Θ_set := fun k => ⟨(idx k).val, by
simp [Sc, (idx k).property]⟩
have idxc_dense : DenseRange idxc := by
simpa [idxc, Sc] using _idx_dense
have hSc_reg : LocalizedRademacherRegime Sc S_iid split g idxc norm ψ b := by
refine ⟨hb, hSc_bound, hsub, ?_⟩
intro n r hr
have hidx_all_ae :
∀ r : ℝ, ∀ᵐ z ∂P_Z, ∀ p : starHullParam ℕ,
starHullZeroOut
(fun (k : ℕ) (z : Z) => S.ℓ z (idx k).val g - S.ℓ z S.θ₀ g)
norm r p z =
starHullZeroOut
(fun (k : ℕ) (z : Z) => Sc.ℓ z (idx k).val g - Sc.ℓ z Sc.θ₀ g)
norm r p z := by
intro r'
filter_upwards [hcenter_all_ae] with z hz p
have hstar_ae :
-- … truncated; follow the source link for the rest …
1 supporting declaration (lemmas, instances)
-
localEmpProcessModulus_of_localized_singletontheorem — Trivial finite class. When Θ_set = {θ₀} the modulus inequality holds with ρ n := 0 (the centred excess risk is identically zero). Mirrors localEmpProcessModulus_singleton in the global-Rademacher bridge.hypothesesΘ :sharedType u_3G :sharedType u_4S :LearningSystem Ω μ Z P_Z Θ GS_iid :IIDSample Ω Z μ P_Zsplit :OneShotSplit S_iidg :Ghsing :S.Θ_set = {S.θ₀}δ :ℝ_hδ :0 < δconclusionLocalEmpProcessModulus S S_iid split (fun _ => 0) δ gProof (Lean source)
theorem localEmpProcessModulus_of_localized_singleton (S : LearningSystem Ω μ Z P_Z Θ G) (S_iid : IIDSample Ω Z μ P_Z) (split : OneShotSplit S_iid) [IsProbabilityMeasure μ] (g : G) (hsing : S.Θ_set = {S.θ₀}) {δ : ℝ} (_hδ : 0 < δ) : LocalEmpProcessModulus S S_iid split (fun _ => 0) δ g := by intro n refine ⟨Set.univ, MeasurableSet.univ, ?_, ?_⟩ · rw [measure_univ] exact tsub_le_self · intro ω _ θ hθ have hθ' : θ ∈ ({S.θ₀} : Set Θ) := by simpa [hsing] using hθ rcases hθ' with rfl simp
RandomNuisance 5 core · 4 supporting The fixed-nuisance bridge localEmpProcessModulus_of_bounded_rademacher (OrthogonalLearning/LocalEmpProcess/Rademacher.lean) controls the centred excess-risk process for a *fixed* nuisance g : G. ★ localEmpProcessModulus_random_of_bounded_rademacher
Random-nuisance empirical-process modulus (cross-fitting lift)
The fixed-nuisance bridge localEmpProcessModulus_of_bounded_rademacher
(OrthogonalLearning/LocalEmpProcess/Rademacher.lean) controls the centred
excess-risk process for a fixed nuisance g : G. Cross-fitting feeds a
random, fold-A-measurable nuisance
ĥ : ℕ → Ω → G into the fold-B evaluation, so the high-probability modulus
event becomes a random object: at sample n and sample point ω the bad set is
selected by ĥ n ω.
LocalEmpProcessModulusRandom is the random-g analogue of
LocalEmpProcessModulus — exactly the hMod hypothesis of
oracle_inequality_drLearner_random_nuisance.
The proof structure factors the fixed-nuisance Rademacher argument into
g-parametric lemmas, then lifts them with the cross-fit conditioning keystone
randomParam_event_le:
* foldBCoord / foldBCoord_law — the fold-B coordinate map Y : Ω → (Fin m → Z)
with law Measure.pi P_Z (independent of g);
* badDataSet g — despite the historical name, this is the product-sample
bad event for nuisance g, not an observed data set. Its
Measure.pi P_Z-mass is ≤ δ (badDataSet_mass_le, using McDiarmid and
symmetrization);
* modulus_of_not_badData g — on the complement, the modulus inequality holds
uniformly over Θ_set;
* randomParam_event_le — conditions on fold A, integrates the per-ĥ n ω
mass bound against the fold-A marginal, with no loss in the probability budget.
The fold-A-measurability of ĥ n and the joint measurability of
(ω, s) ↦ s ∈ badDataSet (ĥ n ω) enter as named regularity hypotheses, in the
same spirit as RademacherBound / LossContinuousOnΘset.
def LocalEmpProcessModulusRandom reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Given an orthogonal statistical-learning system, an independent and identically distributed sample with the system's population law, a one-shot sample split, a rate sequence, a confidence tolerance, and a sample-dependent nuisance estimator, the random-nuisance local empirical-process modulus condition holds exactly when, for every sample size, there exists an event that is measurable, has measure at least , with subtraction truncated at zero, and on which, uniformly over the target class, the population excess risk at the realized nuisance estimate minus the fold-B empirical excess risk is at most times the distance from the distinguished target plus .
Definition (Lean source)
parameters
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
S_iid :
IIDSample Ω Z μ P_Z
split :
OneShotSplit S_iid
ρ :
ℕ → ℝ
δ :
ℝ
ĥ :
ℕ → Ω → G
n :
ℕ
def
LocalEmpProcessModulusRandom S S_iid split ρ δ ĥ :
Prop
given by
clause 1
ω ∈ E :
θ ∈ S.Θ_set :
(S.L θ (ĥ n ω) - S.L S.θ₀ (ĥ n ω))
- (empRiskFoldB S S_iid split n ω θ (ĥ n ω) - empRiskFoldB S S_iid split n ω S.θ₀ (ĥ n ω))
≤ ρ n * ‖θ - S.θ₀‖ + (ρ n) ^ 2
def foldBCoord reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Given an independent and identically distributed sample, a one-shot sample split, and a sample size, the fold-B coordinate map sends each sample realization to its fold-B observations, indexed in their canonical finite order.
def badDataSet reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Given an orthogonal statistical-learning system, an independent and identically distributed sample with the system's population law, a one-shot sample split, a sample size, a loss bound, a confidence tolerance, a candidate complexity-bound sequence, and a nuisance function, the product-sample bad event is the set of fold-B observation vectors for which twice the centred-loss Rademacher complexity plus , where is the fold-B size, does not exceed the centred-loss uniform deviation.
Definition (Lean source)
parameters
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
S_iid :
IIDSample Ω Z μ P_Z
split :
OneShotSplit S_iid
n :
ℕ
b δ :
ℝ
_R :
ℕ → ℝ
g :
G
def modulusRadius reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Given an independent and identically distributed sample, a one-shot sample split, a loss bound, a confidence tolerance, and a complexity-bound sequence, the deterministic modulus-radius sequence assigns to every sample size the value when fold B is empty, and otherwise the value , where is the fold-B size.
Definition (Lean source)
theorem localEmpProcessModulus_random_of_bounded_rademacher reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Cross-fit lift of the empirical-process modulus to a random nuisance. Let ĥ be a fold-A-measurable random nuisance sequence. Assume b is strictly positive, that at every sample size and sample point the loss magnitude at the realised nuisance ĥ n ω is uniformly bounded by b, and that the loss at that realised nuisance is continuous in the parameter. Given a sequence R n that Rademacher-controls the centred loss class at every realisation ĥ n ω, and a confidence level 0 < δ ≤ 1. Suppose further that the σ-algebra m_A n generating the fold-A information is coarser than the ambient σ-algebra, that fold A is independent of the fold-B coordinate block under this σ-algebra, and that the nuisance-indexed bad event depends jointly measurably on the fold-A outcome and the fold-B sample. Then the random-nuisance local empirical-process modulus condition holds, at rate ρ n := √(2·b) on empty folds and ρ n := √(2·R n + 2·b·√(2·log(1/δ)/|foldB n|)) otherwise, evaluated at the random nuisance ĥ.
Formal statement
hypotheses
Θ :
Type u_3
G :
Type u_4
S :
LearningSystem Ω μ Z P_Z Θ G
S_iid :
IIDSample Ω Z μ P_Z
split :
OneShotSplit S_iid
b :
ℝ
hb_pos :
0 < b
ĥ :
ℕ → Ω → G
hg_bdd :
∀ n ω, UniformlyBoundedLoss S (ĥ n ω) b
hg_cont :
∀ n ω, LossContinuousOnΘset S (ĥ n ω)
idx :
ℕ → S.Θ_set
idx_dense :
DenseRange idx
R :
ℕ → ℝ
hR :
∀ n ω, RademacherBound S S_iid split (ĥ n ω) idx R
δ :
ℝ
hδ :
0 < δ
hδ' :
δ ≤ 1
m_A :
ℕ → MeasurableSpace Ω
hm_A_le :
∀ n, m_A n ≤ (inferInstance : MeasurableSpace Ω)
hindep :
∀ n,
@Indep Ω (m_A n) (comap (foldBCoord S_iid split n) inferInstance) (inferInstance : MeasurableSpace Ω) μ
hbad_joint :
∀ n,
@MeasurableSet (Ω × (Fin (split.foldB n).card → Z)) ((m_A n).prod inferInstance) {p | p.2 ∈ badDataSet S S_iid split n b δ R (ĥ n p.1)}
conclusion
LocalEmpProcessModulusRandom S S_iid split (modulusRadius split b δ R) δ ĥ
Proof (Lean source)
theorem localEmpProcessModulus_random_of_bounded_rademacher
(S : LearningSystem Ω μ Z P_Z Θ G)
[IsProbabilityMeasure μ] [IsProbabilityMeasure P_Z]
(S_iid : IIDSample Ω Z μ P_Z)
(split : OneShotSplit S_iid)
{b : ℝ} (hb_pos : 0 < b)
(ĥ : ℕ → Ω → G)
(hg_bdd : ∀ n ω, UniformlyBoundedLoss S (ĥ n ω) b)
(hg_cont : ∀ n ω, LossContinuousOnΘset S (ĥ n ω))
(idx : ℕ → S.Θ_set) (idx_dense : DenseRange idx)
(R : ℕ → ℝ) (hR : ∀ n ω, RademacherBound S S_iid split (ĥ n ω) idx R)
{δ : ℝ} (hδ : 0 < δ) (hδ' : δ ≤ 1)
(m_A : ℕ → MeasurableSpace Ω)
(hm_A_le : ∀ n, m_A n ≤ (inferInstance : MeasurableSpace Ω))
(hindep : ∀ n, @Indep Ω (m_A n)
(comap (foldBCoord S_iid split n) inferInstance)
(inferInstance : MeasurableSpace Ω) μ)
(hbad_joint : ∀ n, @MeasurableSet (Ω × (Fin (split.foldB n).card → Z))
((m_A n).prod inferInstance)
{p | p.2 ∈ badDataSet S S_iid split n b δ R (ĥ n p.1)}) :
LocalEmpProcessModulusRandom S S_iid split (modulusRadius split b δ R) δ ĥ := by
intro n
classical
by_cases hm0 : (split.foldB n).card = 0
· -- Empty fold-B: trivial event Set.univ.
refine ⟨Set.univ, MeasurableSet.univ, ?_, ?_⟩
· rw [measure_univ]
exact tsub_le_self
· intro ω _ θ hθ
have hfold_empty : split.foldB n = ∅ := Finset.card_eq_zero.mp hm0
-- inline population bound S.L θ ĥ - S.L θ₀ ĥ ≤ 2 b
have habs : ∀ θ' ∈ S.Θ_set, |S.L θ' (ĥ n ω)| ≤ b := by
intro θ' hθ'
calc
|S.L θ' (ĥ n ω)| = |∫ z, S.ℓ z θ' (ĥ n ω) ∂P_Z| := rfl
_ ≤ ∫ z, |S.ℓ z θ' (ĥ n ω)| ∂P_Z := abs_integral_le_integral_abs
_ ≤ ∫ _z, b ∂P_Z := by
apply integral_mono
· exact Integrable.of_bound (S.ℓ_meas θ' (ĥ n ω)).abs.aestronglyMeasurable b
(by
filter_upwards with z
simpa [Real.norm_eq_abs] using hg_bdd n ω z θ' hθ')
· exact integrable_const b
· intro z
exact hg_bdd n ω z θ' hθ'
_ = b := by simp
have hpop : S.L θ (ĥ n ω) - S.L S.θ₀ (ĥ n ω) ≤ 2 * b := by
have hθ_abs := habs θ hθ
have hθ₀_abs := habs S.θ₀ S.θ₀_mem
have hθ_le : S.L θ (ĥ n ω) ≤ b := (le_abs_self _).trans hθ_abs
have hθ₀_ge : -b ≤ S.L S.θ₀ (ĥ n ω) := (abs_le.mp hθ₀_abs).1
linarith
have hρsq :
(sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card))) ^ 2
= 2 * b := by
rw [Real.sq_sqrt]
· simp [hm0]
· have : 0 ≤ 2 * b := by nlinarith
simpa [hm0] using this
have hρ_nonneg :
0 ≤ sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card)) :=
Real.sqrt_nonneg _
have hnorm_nonneg : 0 ≤ ‖θ - S.θ₀‖ := norm_nonneg _
change (S.L θ (ĥ n ω) - S.L S.θ₀ (ĥ n ω))
- (empRiskFoldB S S_iid split n ω θ (ĥ n ω)
- empRiskFoldB S S_iid split n ω S.θ₀ (ĥ n ω))
≤ modulusRadius split b δ R n * ‖θ - S.θ₀‖
+ (modulusRadius split b δ R n) ^ 2
unfold modulusRadius
calc
(S.L θ (ĥ n ω) - S.L S.θ₀ (ĥ n ω))
- (empRiskFoldB S S_iid split n ω θ (ĥ n ω)
- empRiskFoldB S S_iid split n ω S.θ₀ (ĥ n ω))
= S.L θ (ĥ n ω) - S.L S.θ₀ (ĥ n ω) := by
simp [empRiskFoldB, hfold_empty]
_ ≤ 2 * b := hpop
_ = (sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card))) ^ 2 := hρsq.symm
_ ≤ sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card)) * ‖θ - S.θ₀‖
+ (sqrt
(if (split.foldB n).card = 0 then 2 * b
else 2 * R n + 2 * b *
sqrt (2 * log (1 / δ) / (split.foldB n).card))) ^ 2 := by
nlinarith [mul_nonneg hρ_nonneg hnorm_nonneg]
· -- Nonempty fold-B: cross-fit conditioning via randomParam_event_le.
have hm_pos : 0 < (split.foldB n).card := Nat.pos_of_ne_zero hm0
set Bad : Ω → Set (Fin (split.foldB n).card → Z) :=
fun ω => badDataSet S S_iid split n b δ R (ĥ n ω) with hBad_def
haveI : IsProbabilityMeasure (Measure.pi (fun _ : Fin (split.foldB n).card => P_Z)) := by
infer_instance
have hsec : ∀ ω, Measure.pi (fun _ : Fin (split.foldB n).card => P_Z) (Bad ω)
≤ ofReal δ :=
fun ω => badDataSet_mass_le S S_iid split hb_pos (ĥ n ω) (hg_bdd n ω) (hg_cont n ω)
idx idx_dense R (hR n ω) hδ hδ' n hm_pos
have hkey : μ {ω | foldBCoord S_iid split n ω ∈ Bad ω} ≤ ofReal δ :=
randomParam_event_le (foldBCoord_meas split n) (foldBCoord_law split n)
(m_A n) (hm_A_le n) (hindep n) Bad (hbad_joint n) hsec
-- measurability of the bad event
have hmeas_bad : MeasurableSet {ω | foldBCoord S_iid split n ω ∈ Bad ω} := by
have hset_eq :
{ω | foldBCoord S_iid split n ω ∈ Bad ω}
= (fun ω => (ω, foldBCoord S_iid split n ω)) ⁻¹'
{p : Ω × (Fin (split.foldB n).card → Z) | p.2 ∈ Bad p.1} := rfl
rw [hset_eq]
have hms : MeasurableSet[(inferInstance : MeasurableSpace Ω).prod inferInstance]
{p : Ω × (Fin (split.foldB n).card → Z) | p.2 ∈ Bad p.1} := by
have hle : (m_A n).prod (inferInstance : MeasurableSpace (Fin (split.foldB n).card → Z))
≤ (inferInstance : MeasurableSpace Ω).prod inferInstance := by
unfold prod
exact sup_le_sup_right (comap_mono (hm_A_le n)) _
exact hle _ (hbad_joint n)
exact (measurable_id.prodMk (foldBCoord_meas split n)) hms
refine ⟨{ω | foldBCoord S_iid split n ω ∉ Bad ω},
hmeas_bad.compl, ?_, ?_⟩
· -- μ E ≥ 1 - ofReal δ
have hEc : {ω | foldBCoord S_iid split n ω ∉ Bad ω}
= {ω | foldBCoord S_iid split n ω ∈ Bad ω}ᶜ := rfl
rw [hEc, measure_compl hmeas_bad (measure_ne_top μ _), measure_univ]
rw [ge_iff_le]
exact tsub_le_tsub_left hkey 1
· -- on-event modulus bound
intro ω hω θ hθ
have hoff : foldBCoord S_iid split n ω ∉ badDataSet S S_iid split n b δ R (ĥ n ω) := hω
exact modulus_of_not_badData S S_iid split hb_pos (ĥ n ω) (hg_bdd n ω) (hg_cont n ω)
idx idx_dense R (hR n ω) hδ hδ' n ω hm_pos hoff θ hθ
4 supporting declarations (lemmas, instances)
-
foldBCoord_lawtheorem — Fold-B coordinate law. μ.map (foldBCoord n) = Measure.pi P_Z. This identifies the validation-fold coordinates as an i.i.d. product sample.hypothesessplit :OneShotSplit S_iidn :ℕconclusionμ.map (foldBCoord S_iid split n) = Measure.pi (fun _ : Fin (split.foldB n).card => P_Z)Proof (Lean source)
theorem foldBCoord_law {S_iid : IIDSample Ω Z μ P_Z} [IsProbabilityMeasure μ] [IsProbabilityMeasure P_Z] (split : OneShotSplit S_iid) (n : ℕ) : μ.map (foldBCoord S_iid split n) = Measure.pi (fun _ : Fin (split.foldB n).card => P_Z) := by set m := (split.foldB n).card with hm let e : Fin m ≃o split.foldB n := (split.foldB n).orderIsoOfFin rfl let YB : Ω → split.foldB n → Z := fun ω i => S_iid.Z i.val ω let T : (split.foldB n → Z) ≃ᵐ (Fin m → Z) := MeasurableEquiv.piCongrLeft (fun _ : Fin m => Z) e.symm.toEquiv have hY_eq : foldBCoord S_iid split n = T ∘ YB := by funext ω j simpa [foldBCoord, YB, T, e] using (MeasurableEquiv.piCongrLeft_apply_apply (e := e.symm.toEquiv) (β := fun _ : Fin m => Z) (x := fun i : split.foldB n => S_iid.Z i.val ω) (i := e j)).symm rw [hY_eq, ← Measure.map_map T.measurable (measurable_pi_lambda YB fun i => S_iid.meas i.val)] rw [foldB_pi_law S_iid split n] simpa [T] using Measure.pi_map_piCongrLeft (e := e.symm.toEquiv) (β := fun _ : Fin m => Z) (μ := fun _ : Fin m => P_Z) -
badDataSet_mass_letheorem — Mass bound. The product-space bad set has Measure.pi P_Z-mass ≤ δ. The proof uses the deterministic fixed-nuisance construction from Rademacher.lean: McDiarmid concentration, symmetrization, and separable lifting.hypothesesΘ :sharedType u_3G :sharedType u_4S :LearningSystem Ω μ Z P_Z Θ GS_iid :IIDSample Ω Z μ P_Zsplit :OneShotSplit S_iidb :ℝhb_pos :0 < bg :Ghg_bdd :UniformlyBoundedLoss S g bhg_cont :idx :ℕ → S.Θ_setidx_dense :DenseRange idxR :ℕ → ℝ_hR :RademacherBound S S_iid split g idx Rδ :ℝhδ :0 < δhδ' :δ ≤ 1n :ℕhm_pos :0 < (split.foldB n).cardconclusionMeasure.pi (fun _ : Fin (split.foldB n).card => P_Z) (badDataSet S S_iid split n b δ R g)≤ ofReal δProof (Lean source)
theorem badDataSet_mass_le (S : LearningSystem Ω μ Z P_Z Θ G) [IsProbabilityMeasure μ] [IsProbabilityMeasure P_Z] (S_iid : IIDSample Ω Z μ P_Z) (split : OneShotSplit S_iid) {b : ℝ} (hb_pos : 0 < b) (g : G) (hg_bdd : UniformlyBoundedLoss S g b) (hg_cont : LossContinuousOnΘset S g) (idx : ℕ → S.Θ_set) (idx_dense : DenseRange idx) (R : ℕ → ℝ) (_hR : RademacherBound S S_iid split g idx R) {δ : ℝ} (hδ : 0 < δ) (hδ' : δ ≤ 1) (n : ℕ) (hm_pos : 0 < (split.foldB n).card) : Measure.pi (fun _ : Fin (split.foldB n).card => P_Z) (badDataSet S S_iid split n b δ R g) ≤ ENNReal.ofReal δ := by simp only [badDataSet] let m : ℕ := (split.foldB n).card let fθ : S.Θ_set → Z → ℝ := fun θ z => S.ℓ z θ.val g - S.ℓ z S.θ₀ g haveI : Nonempty Z := nonempty_of_isProbabilityMeasure P_Z haveI : Nonempty S.Θ_set := ⟨⟨S.θ₀, S.θ₀_mem⟩⟩ haveI : SeparableSpace S.Θ_set := by exact ⟨⟨Set.range idx, Set.countable_range idx, idx_dense⟩⟩ have hf_meas : ∀ θ : S.Θ_set, Measurable (fθ θ) := by intro θ exact (S.ℓ_meas θ.val g).sub (S.ℓ_meas S.θ₀ g) have hf_bdd : ∀ θ : S.Θ_set, ∀ z : Z, |fθ θ z| ≤ 2 * b := by intro θ z have h1 : |S.ℓ z θ.val g| ≤ b := hg_bdd z θ.val θ.property have h2 : |S.ℓ z S.θ₀ g| ≤ b := hg_bdd z S.θ₀ S.θ₀_mem have h := abs_sub (S.ℓ z θ.val g) (S.ℓ z S.θ₀ g) dsimp [fθ] linarith have hf_cont : ∀ z : Z, Continuous fun θ : S.Θ_set => fθ θ z := by intro z exact (hg_cont z).sub continuous_const let ε : ℝ := 2 * b * sqrt (2 * log (1 / δ) / m) have hε_nonneg : 0 ≤ ε := by dsimp [ε] positivity have hm_pos' : 0 < m := hm_pos have htail := uniform_deviation_tail_bound_separable_of_pos (μ := P_Z) (n := m) (f := fθ) hf_meas (X := id) measurable_id (b := 2 * b) (by linarith) hf_bdd hf_cont (ε := ε) hε_nonneg change Measure.pi (fun _ : Fin m => P_Z) {s | 2 • rademacherComplexity m fθ P_Z id + ε ≤ uniformDeviation m fθ P_Z id (id ∘ s)} ≤ ENNReal.ofReal δ have hbad_toReal : (Measure.pi (fun _ : Fin m => P_Z) {s | 2 • rademacherComplexity m fθ P_Z id + ε ≤ uniformDeviation m fθ P_Z id (id ∘ s)}).toReal ≤ δ := by have hle_exp := htail have hexp_le : exp (-ε ^ 2 * m / (2 * (2 * b) ^ 2)) ≤ δ := by have hδ_nonneg : 0 ≤ δ := le_of_lt hδ have hlog_nonneg : 0 ≤ log (1 / δ) := by apply Real.log_nonneg have : (1 : ℝ) ≤ 1 / δ := by rw [le_div_iff₀ hδ] simpa using hδ' exact this have hsqrt_sq : (sqrt (2 * log (1 / δ) / m)) ^ 2 = 2 * log (1 / δ) / m := by rw [Real.sq_sqrt] positivity have hcalc : -ε ^ 2 * m / (2 * (2 * b) ^ 2) = log δ := by have hεsq : ε ^ 2 = 4 * b ^ 2 * (2 * log (1 / δ) / m) := by dsimp [ε] rw [mul_pow, hsqrt_sq] ring have hloginv : log (1 / δ) = -log δ := by rw [one_div, Real.log_inv] rw [hεsq, hloginv] have hmne : (m : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hm_pos'.ne' have hbne : (b : ℝ) ≠ 0 := hb_pos.ne' field_simp ring rw [hcalc, Real.exp_log hδ] exact hle_exp.trans hexp_le rw [ENNReal.le_ofReal_iff_toReal_le (measure_ne_top _ _) (le_of_lt hδ)] exact hbad_toReal -
modulus_of_not_badDatatheorem — On-event modulus. Off the bad set, the modulus inequality holds uniformly over Θ_set for a fixed nuisance g, using the same bounded-loss Rademacher radius as the deterministic bridge in Rademacher.lean.hypothesesΘ :sharedType u_3G :sharedType u_4S :LearningSystem Ω μ Z P_Z Θ GS_iid :IIDSample Ω Z μ P_Zsplit :OneShotSplit S_iidb :ℝhb_pos :0 < bg :Ghg_bdd :UniformlyBoundedLoss S g bhg_cont :idx :ℕ → S.Θ_setidx_dense :DenseRange idxR :ℕ → ℝhR :RademacherBound S S_iid split g idx Rδ :ℝ_hδ :0 < δ_hδ' :δ ≤ 1n :ℕω :Ωhm_pos :0 < (split.foldB n).cardhoff :foldBCoord S_iid split n ω ∉ badDataSet S S_iid split n b δ R gθ :Θhθ :θ ∈ S.Θ_setconclusion(S.L θ g - S.L S.θ₀ g)- (empRiskFoldB S S_iid split n ω θ g - empRiskFoldB S S_iid split n ω S.θ₀ g)≤ modulusRadius split b δ R n * ‖θ - S.θ₀‖ + (modulusRadius split b δ R n) ^ 2Proof (Lean source)
theorem modulus_of_not_badData (S : LearningSystem Ω μ Z P_Z Θ G) [IsProbabilityMeasure μ] (S_iid : IIDSample Ω Z μ P_Z) (split : OneShotSplit S_iid) {b : ℝ} (hb_pos : 0 < b) (g : G) (hg_bdd : UniformlyBoundedLoss S g b) (hg_cont : LossContinuousOnΘset S g) (idx : ℕ → S.Θ_set) (idx_dense : DenseRange idx) (R : ℕ → ℝ) (hR : RademacherBound S S_iid split g idx R) {δ : ℝ} (_hδ : 0 < δ) (_hδ' : δ ≤ 1) (n : ℕ) (ω : Ω) (hm_pos : 0 < (split.foldB n).card) (hoff : foldBCoord S_iid split n ω ∉ badDataSet S S_iid split n b δ R g) (θ : Θ) (hθ : θ ∈ S.Θ_set) : (S.L θ g - S.L S.θ₀ g) - (empRiskFoldB S S_iid split n ω θ g - empRiskFoldB S S_iid split n ω S.θ₀ g) ≤ modulusRadius split b δ R n * ‖θ - S.θ₀‖ + (modulusRadius split b δ R n) ^ 2 := by classical haveI : IsProbabilityMeasure P_Z := by rw [← S_iid.law] exact Measure.isProbabilityMeasure_map (S_iid.meas 0).aemeasurable have hR_nonneg : 0 ≤ R n := (hR n).1 have hm0 : (split.foldB n).card ≠ 0 := hm_pos.ne' have hm_pos' : 0 < ((split.foldB n).card : ℝ) := Nat.cast_pos.mpr hm_pos set m : ℕ := (split.foldB n).card with hm_def let fθ : S.Θ_set → Z → ℝ := fun θ z => S.ℓ z θ.val g - S.ℓ z S.θ₀ g haveI : Nonempty Z := nonempty_of_isProbabilityMeasure P_Z haveI : Nonempty S.Θ_set := ⟨⟨S.θ₀, S.θ₀_mem⟩⟩ haveI : SeparableSpace S.Θ_set := by exact ⟨⟨Set.range idx, Set.countable_range idx, idx_dense⟩⟩ have hf_meas : ∀ θ : S.Θ_set, Measurable (fθ θ) := by intro θ exact (S.ℓ_meas θ.val g).sub (S.ℓ_meas S.θ₀ g) have hf_bdd : ∀ θ : S.Θ_set, ∀ z : Z, |fθ θ z| ≤ 2 * b := by intro θ z have h1 : |S.ℓ z θ.val g| ≤ b := hg_bdd z θ.val θ.property have h2 : |S.ℓ z S.θ₀ g| ≤ b := hg_bdd z S.θ₀ S.θ₀_mem have h := abs_sub (S.ℓ z θ.val g) (S.ℓ z S.θ₀ g) dsimp [fθ] linarith have hf_cont : ∀ z : Z, Continuous fun θ : S.Θ_set => fθ θ z := by intro z exact (hg_cont z).sub continuous_const let ε : ℝ := 2 * b * sqrt (2 * log (1 / δ) / m) have hε_nonneg : 0 ≤ ε := by dsimp [ε] positivity have hsep_sup : ∀ {f : S.Θ_set → ℝ}, Continuous f → ⨆ x : S.Θ_set, f x = ⨆ k : ℕ, f (idx k) := by intro f hf have hclosure : closure (range f) = closure (range (f ∘ idx)) := by rw [Set.range_comp f idx] apply Set.Subset.antisymm · have hsub : range f ⊆ closure (f '' range idx) := hf.range_subset_closure_image_dense idx_dense exact closure_minimal hsub isClosed_closure · apply closure_mono exact Set.image_subset_range f (range idx) by_cases hbdd : BddAbove (range f) · calc ⨆ x : S.Θ_set, f x = sSup (closure (range f)) := by exact sSup_eq_closure_sSup (Set.range_nonempty f) hbdd _ = sSup (closure (range (f ∘ idx))) := by rw [hclosure] _ = ⨆ k : ℕ, f (idx k) := by have hbdd_idx : BddAbove (range (f ∘ idx)) := by rw [Set.range_comp f idx] exact BddAbove.mono (Set.image_subset_range f (range idx)) hbdd exact (sSup_eq_closure_sSup (Set.range_nonempty (f ∘ idx)) hbdd_idx).symm · have hbdd_idx : ¬ BddAbove (range (f ∘ idx)) := by intro h have hclosure_bdd : BddAbove (closure (range (f ∘ idx))) := bddAbove_closure.mpr h rw [← hclosure] at hclosure_bdd exact hbdd (bddAbove_closure.mp hclosure_bdd) calc ⨆ x : S.Θ_set, f x = 0 := Real.iSup_of_not_bddAbove hbdd _ = ⨆ k : ℕ, f (idx k) := (Real.iSup_of_not_bddAbove hbdd_idx).symm have hemp_dense : ∀ sample : Fin m → Z, empiricalRademacherComplexity m fθ sample = empiricalRademacherComplexity m (fθ ∘ idx) sample := by intro sample dsimp [empiricalRademacherComplexity] congr ext σ exact hsep_sup (by apply Continuous.abs apply Continuous.const_mul exact continuous_finset_sum univ fun k _ => continuous_const.mul (hf_cont (sample k))) have hrad_full_le : rademacherComplexity m fθ P_Z id ≤ R n := by have hfull_dense : rademacherComplexity m fθ P_Z id = rademacherComplexity m (fθ ∘ idx) P_Z id := by dsimp [rademacherComplexity] congr ext ω' exact hemp_dense (id ∘ ω') have hmap : rademacherComplexity m (fθ ∘ idx) P_Z id = rademacherComplexity m (fθ ∘ idx) μ (S_iid.Z 0) := by have hmap' : rademacherComplexity m (fθ ∘ idx) (μ.map (S_iid.Z 0)) id = rademacherComplexity m (fθ ∘ idx) μ (S_iid.Z 0) := by dsimp [rademacherComplexity] let Φ : (Fin m → Ω) → (Fin m → Z) := fun ω' i => S_iid.Z 0 (ω' i) have hmapΦ : Measure.map Φ (Measure.pi fun _ : Fin m => μ) = Measure.pi fun _ : Fin m => μ.map (S_iid.Z 0) := by dsimp [Φ] rw [Measure.pi_map_pi] intro _ exact (S_iid.meas 0).aemeasurable rw [← hmapΦ] rw [integral_map] · rfl · exact (measurable_pi_lambda Φ (fun i => (S_iid.meas 0).comp (measurable_pi_apply i))).aemeasurable · apply Measurable.aestronglyMeasurable apply measurable_const.mul apply Finset.univ.measurable_sum intro σ _ apply Measurable.iSup intro i apply Measurable.abs apply measurable_const.mul apply Finset.univ.measurable_sum intro k _ apply measurable_const.mul exact (hf_meas (idx i)).comp (measurable_pi_apply k) simpa [S_iid.law] using hmap' calc rademacherComplexity m fθ P_Z id = rademacherComplexity m (fθ ∘ idx) P_Z id := hfull_dense _ = rademacherComplexity m (fθ ∘ idx) μ (S_iid.Z 0) := hmap _ ≤ R n := by simpa [m, fθ, Function.comp_def] using (hR n).2 let e : Fin m ≃o split.foldB n := (split.foldB n).orderIsoOfFin rfl let Y : Ω → Fin m → Z := fun ω j => S_iid.Z (e j).val ω have hgood : ¬ (2 • rademacherComplexity m fθ P_Z id + ε ≤ uniformDeviation m fθ P_Z id (id ∘ Y ω)) := by have hoff' := hoff simp only [badDataSet, Set.mem_setOf_eq] at hoff' exact hoff' let θs : S.Θ_set := ⟨θ, hθ⟩ have hdev_lt : uniformDeviation m fθ P_Z id (Y ω) < 2 * R n + ε := by have hnot : uniformDeviation m fθ P_Z id (Y ω) < 2 • rademacherComplexity m fθ P_Z id + ε := by rw [not_le] at hgood simpa using hgood have hrad_two : 2 • rademacherComplexity m fθ P_Z id + ε ≤ 2 * R n + ε := by simpa [two_nsmul] using add_le_add_right (mul_le_mul_of_nonneg_left hrad_full_le (by norm_num : (0 : ℝ) ≤ 2)) ε exact hnot.trans_le hrad_two have hpoint_le_dev : |(m : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin m => fθ θs (Y ω k)) - P_Z[fun z => fθ θs (id z)]| ≤ uniformDeviation m fθ P_Z id (Y ω) := by dsimp [uniformDeviation] apply le_ciSup (f := fun i : S.Θ_set => |(m : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin m => fθ i (Y ω k)) - P_Z[fun z => fθ i (id z)]|) rw [bddAbove_def] use 4 * b intro y hy rcases hy with ⟨θ', rfl⟩ have hsample : |(m : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin m => fθ θ' (Y ω k))| ≤ 2 * b := by calc _ = (m : ℝ)⁻¹ * |Finset.univ.sum fun k : Fin m => fθ θ' (Y ω k)| := by rw [abs_mul, abs_of_nonneg] exact inv_nonneg.mpr (Nat.cast_nonneg _) _ ≤ (m : ℝ)⁻¹ * (Finset.univ.sum fun _ : Fin m => 2 * b) := by apply mul_le_mul_of_nonneg_left · exact Finset.abs_sum_le_sum_abs _ _ |>.trans (Finset.sum_le_sum fun k _ => hf_bdd θ' (Y ω k)) · positivity _ = 2 * b := by rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, ← mul_assoc, inv_mul_cancel₀ hm_pos'.ne', one_mul] have hmean : |P_Z[fun z => fθ θ' (id z)]| ≤ 2 * b := by calc _ ≤ ∫ z, |fθ θ' z| ∂P_Z := abs_integral_le_integral_abs _ ≤ ∫ _z, 2 * b ∂P_Z := by apply integral_mono · exact Integrable.of_bound ((hf_meas θ').abs.aestronglyMeasurable) (2 * b) (by filter_upwards with z simpa [Real.norm_eq_abs] using hf_bdd θ' z) · exact integrable_const (2 * b) · intro z exact hf_bdd θ' z _ = 2 * b := by simp calc |(m : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin m => fθ θ' (Y ω k)) - P_Z[fun z => fθ θ' (id z)]| ≤ |(m : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin m => fθ θ' (Y ω k))| + |P_Z[fun z => fθ θ' (id z)]| := abs_sub _ _ _ ≤ 4 * b := by linarith have hcenter_abs : |(empRiskFoldB S S_iid split n ω θ g - empRiskFoldB S S_iid split n ω S.θ₀ g) - (S.L θ g - S.L S.θ₀ g)| ≤ 2 * R n + ε := by have hsum_reindex : (Finset.univ.sum fun k : Fin m => fθ θs (Y ω k)) = ∑ i ∈ split.foldB n, (S.ℓ (S_iid.Z i ω) θ g - S.ℓ (S_iid.Z i ω) S.θ₀ g) := by have hsum_subtype : (Finset.univ.sum fun k : Fin m => fθ θs (Y ω k)) = ∑ i : split.foldB n, (S.ℓ (S_iid.Z i.val ω) θ g - S.ℓ (S_iid.Z i.val ω) S.θ₀ g) := Fintype.sum_equiv e.toEquiv (fun k => fθ θs (Y ω k)) (fun i : split.foldB n => S.ℓ (S_iid.Z i.val ω) θ g - S.ℓ (S_iid.Z i.val ω) S.θ₀ g) (by intro k; rfl) have hsum_attach : (∑ i : split.foldB n, (S.ℓ (S_iid.Z i.val ω) θ g - S.ℓ (S_iid.Z i.val ω) S.θ₀ g)) = ∑ i ∈ split.foldB n, (S.ℓ (S_iid.Z i ω) θ g - S.ℓ (S_iid.Z i ω) S.θ₀ g) := by simpa using Finset.sum_attach (s := split.foldB n) (f := fun i => S.ℓ (S_iid.Z i ω) θ g - S.ℓ (S_iid.Z i ω) S.θ₀ g) exact hsum_subtype.trans hsum_attach have hmean_eq : (∫ z, fθ θs z ∂P_Z) = S.L θ g - S.L S.θ₀ g := by have hintθ : Integrable (fun z => S.ℓ z θ g) P_Z := Integrable.of_bound (S.ℓ_meas θ g).aestronglyMeasurable b (by filter_upwards with z simpa [Real.norm_eq_abs] using hg_bdd z θ hθ) have hint0 : Integrable (fun z => S.ℓ z S.θ₀ g) P_Z := Integrable.of_bound (S.ℓ_meas S.θ₀ g).aestronglyMeasurable b (by filter_upwards with z simpa [Real.norm_eq_abs] using hg_bdd z S.θ₀ S.θ₀_mem) change (∫ z, S.ℓ z θ g - S.ℓ z S.θ₀ g ∂P_Z) = S.L θ g - S.L S.θ₀ g change (∫ z, S.ℓ z θ g - S.ℓ z S.θ₀ g ∂P_Z) = (∫ z, S.ℓ z θ g ∂P_Z) - (∫ z, S.ℓ z S.θ₀ g ∂P_Z) exact integral_sub hintθ hint0 have hpoint := hpoint_le_dev.trans (le_of_lt hdev_lt) have hpoint' : |(m : ℝ)⁻¹ * -- … truncated; follow the source link for the rest … -
foldBCoord_meastheorem — The fold-B coordinate map is measurable.Proof (Lean source)
@[fun_prop] theorem foldBCoord_meas {S_iid : IIDSample Ω Z μ P_Z} (split : OneShotSplit S_iid) (n : ℕ) : Measurable (foldBCoord S_iid split n) := by apply measurable_pi_lambda intro j exact S_iid.meas _
RandomParam 1 core · 0 supporting This file supplies the measure-theoretic conditioning step used in cross-fitting. ★ randomParam_event_le
Cross-Fit Random Parameter Conditioning
This file supplies the measure-theoretic conditioning step used in cross-fitting. It shows that a fold-A-measurable random choice of a fold-B event inherits the same probability bound as each fixed fold-B event, using independence between the training and validation folds.
The main theorem randomParam_event_le is the cross-fit conditioning lemma:
if the fold-B coordinate map has law ν, the fold-A sigma-algebra is
independent of that coordinate block, and every selected bad set has
ν-mass at most δ, then the random event selected by fold-A data has
μ-mass at most δ.
theorem randomParam_event_le reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Cross-fit conditioning keystone. Let Y be measurable with pushforward law μ.map Y = ν, and let m_A be a sub-σ-algebra with m_A ≤ mΩ that is independent of the σ-algebra generated by Y. Suppose the family of "bad" subsets of β indexed by ω has an m_A-measurable joint dependence on (ω, ·) and each individual bad set has ν-mass at most δ. Then the random event where Y ω falls in the ω-dependent bad set also has μ-mass at most δ.
Formal statement
hypotheses
Ω β :
Y :
Ω → β
hY :
@Measurable Ω β mΩ mβ Y
ν :
hY_law :
μ.map Y = ν
m_A :
hm_A_le :
m_A ≤ mΩ
δ :
ℝ
Bad :
Ω → Set β
hBad :
@MeasurableSet (Ω × β) (m_A.prod mβ) {p : Ω × β | p.2 ∈ Bad p.1}
hsec :
∀ ω, ν (Bad ω) ≤ ofReal δ
conclusion
μ {ω | Y ω ∈ Bad ω} ≤ ofReal δ
Proof (Lean source)
theorem randomParam_event_le
{Ω β : Type*} [mΩ : MeasurableSpace Ω] [mβ : MeasurableSpace β]
{μ : Measure Ω} [IsProbabilityMeasure μ]
{Y : Ω → β} (hY : @Measurable Ω β mΩ mβ Y)
{ν : Measure β} [IsProbabilityMeasure ν] (hY_law : μ.map Y = ν)
(m_A : MeasurableSpace Ω) (hm_A_le : m_A ≤ mΩ)
(hindep : @Indep Ω m_A (comap Y mβ) mΩ μ)
{δ : ℝ}
(Bad : Ω → Set β)
(hBad : @MeasurableSet (Ω × β) (m_A.prod mβ) {p : Ω × β | p.2 ∈ Bad p.1})
(hsec : ∀ ω, ν (Bad ω) ≤ ofReal δ) :
μ {ω | Y ω ∈ Bad ω} ≤ ofReal δ := by
classical
have hJ_meas : @Measurable Ω (Ω × β) mΩ (m_A.prod mβ) (fun ω => (ω, Y ω)) := by
apply Measurable.prod
· exact measurable_id'' hm_A_le
· exact hY
-- Product factorisation `μ.map (ω ↦ (ω, Y ω)) = (μ.trim m_A).prod ν`.
have hmap : @Measure.map Ω (Ω × β) mΩ (m_A.prod mβ)
(fun ω => (ω, Y ω)) μ
= @Measure.prod Ω β m_A mβ (μ.trim hm_A_le) ν := by
have h :=
@indep_trim_prod_map_eq Ω β mΩ mβ μ _ m_A hm_A_le Y
hY.aemeasurable hindep
rw [hY_law] at h
exact h
-- The random event is the `(ω ↦ (ω, Y ω))`-preimage of the joint bad set.
have hmass :
μ {ω | Y ω ∈ Bad ω}
= (@Measure.prod Ω β m_A mβ (μ.trim hm_A_le) ν) {p : Ω × β | p.2 ∈ Bad p.1} := by
have hpre : {ω | Y ω ∈ Bad ω}
= (fun ω => (ω, Y ω)) ⁻¹' {p : Ω × β | p.2 ∈ Bad p.1} := rfl
rw [hpre,
← @Measure.map_apply Ω (Ω × β) mΩ (m_A.prod mβ) μ
(fun ω => (ω, Y ω)) hJ_meas {p : Ω × β | p.2 ∈ Bad p.1} hBad,
hmap]
rw [hmass,
@Measure.prod_apply Ω β m_A mβ (μ.trim hm_A_le) ν _ {p : Ω × β | p.2 ∈ Bad p.1} hBad]
-- Integrate the section bound against the fold-A probability marginal.
have hsec' : ∀ ω, ν (Prod.mk ω ⁻¹' {p : Ω × β | p.2 ∈ Bad p.1}) ≤ ofReal δ := by
intro ω
have he : Prod.mk ω ⁻¹' {p : Ω × β | p.2 ∈ Bad p.1} = Bad ω := by
ext s; simp
rw [he]; exact hsec ω
calc
∫⁻ ω, ν (Prod.mk ω ⁻¹' {p : Ω × β | p.2 ∈ Bad p.1}) ∂(μ.trim hm_A_le)
≤ ∫⁻ _ : Ω, ofReal δ ∂(μ.trim hm_A_le) := lintegral_mono hsec'
_ = ofReal δ * (μ.trim hm_A_le) univ := by rw [lintegral_const]
_ = ofReal δ := by
rw [trim_measurableSet_eq hm_A_le MeasurableSet.univ, measure_univ, mul_one]