Estimation.Orthogonal­Learning.Local­Emp­Process

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

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

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)

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

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 …

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 _