From 4d5deccbec4d3ed14f50e90d43c021b18e3ac718 Mon Sep 17 00:00:00 2001 From: tukamilano Date: Sat, 24 Oct 2026 13:58:18 +0900 Subject: [PATCH] Replace separable class hypotheses with PointwiseSeparable Uncountable-class uniform-deviation and ERM theorems assumed `[TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H]` and per-input continuity only to reduce suprema to `denseSeq H`. They now take a single topology-free hypothesis `PointwiseSeparable F`: a countable subfamily approximates the class pointwise along one subsequence for all inputs (van der Vaart-Wellner's pointwise measurable class). - Add `LearningTheory/Rademacher/PointwiseSeparable.lean`: the definition, the reductions of empirical Rademacher complexity, Rademacher complexity and uniform deviation to the subfamily (dominated convergence along a sequence), the bridge `PointwiseSeparable.of_continuous` for separable Frechet-Urysohn parameter spaces, and stability under continuous losses. - Rename every `*_separable*` theorem in UniformDeviation/Bounds, UniformDeviation/Confidence, Rademacher/Dudley and EmpiricalRiskMinimization/Generalization to `*_pointwiseSeparable*`, and delete the topological versions and the `denseSeq` reduction lemmas. - Migrate L1, L2, LipschitzParameter and both KernelPredictor modules through `PointwiseSeparable.of_continuous`. - Add `FunctionClass/Threshold.lean`: threshold classifiers, which are discontinuous in the parameter, are pointwise separable; this gives a confidence bound on the Kolmogorov-Smirnov distance. - Remove `denseRestriction` lemmas left unused in Topology/SeparableSpace/Supremum. Closes #77. Co-Authored-By: Claude Opus 5.5 --- FILE_TREE.md | 10 +- README.md | 7 +- .../Generalization.lean | 60 ++- .../KernelPredictor.lean | 10 +- .../FunctionClass/KernelPredictor.lean | 16 +- .../FunctionClass/LinearPredictor/L1.lean | 20 +- .../FunctionClass/LinearPredictor/L2.lean | 20 +- .../FunctionClass/Threshold.lean | 111 ++++++ .../LearningTheory/Rademacher/Dudley.lean | 41 +- .../Rademacher/LipschitzParameter.lean | 6 +- .../Rademacher/PointwiseSeparable.lean | 206 ++++++++++ .../LearningTheory/Rademacher/Reindex.lean | 3 +- .../UniformDeviation/Bounds.lean | 367 ++++++------------ .../UniformDeviation/Confidence.lean | 45 +-- .../Topology/SeparableSpace/Supremum.lean | 25 -- 15 files changed, 540 insertions(+), 407 deletions(-) create mode 100644 StatsMLlib/LearningTheory/FunctionClass/Threshold.lean create mode 100644 StatsMLlib/LearningTheory/Rademacher/PointwiseSeparable.lean diff --git a/FILE_TREE.md b/FILE_TREE.md index c665030..3fcf232 100644 --- a/FILE_TREE.md +++ b/FILE_TREE.md @@ -1,21 +1,21 @@ # StatsMLlib file tree This document presents the public Lean source tree after the Mathlib-style subject refactor. -`StatsMLlib/` contains 142 Lean modules under eight layer-one directories and no root-level Lean +`StatsMLlib/` contains 144 Lean modules under eight layer-one directories and no root-level Lean files. A filesystem path such as `StatsMLlib/Probability/Process/Dudley.lean` corresponds to the Lean module `StatsMLlib.Probability.Process.Dudley`. | Layer | Modules | | --- | ---: | | `Analysis` | 9 | -| `LearningTheory` | 31 | +| `LearningTheory` | 33 | | `LinearAlgebra` | 6 | | `MeasureTheory` | 4 | | `Order` | 1 | | `Probability` | 68 | | `Statistics` | 21 | | `Topology` | 2 | -| **Total** | **142** | +| **Total** | **144** | ```text StatsMLlib/ @@ -49,7 +49,8 @@ StatsMLlib/ │ │ │ ├── HiddenUnit.lean │ │ │ └── PathNorm.lean │ │ ├── HilbertPredictor.lean -│ │ └── KernelPredictor.lean +│ │ ├── KernelPredictor.lean +│ │ └── Threshold.lean │ ├── PACBayes/ │ │ ├── Basic.lean │ │ ├── Catoni.lean @@ -64,6 +65,7 @@ StatsMLlib/ │ │ ├── LipschitzParameter.lean │ │ ├── Massart.lean │ │ ├── OneStep.lean +│ │ ├── PointwiseSeparable.lean │ │ ├── Reindex.lean │ │ ├── Signs.lean │ │ └── Symmetrization.lean diff --git a/README.md b/README.md index 9f64d92..804729c 100644 --- a/README.md +++ b/README.md @@ -54,14 +54,15 @@ generalization bound. Each entry names the endpoint; every module listed carries | Model | Module | Endpoint | | --- | --- | --- | | any countable class | `LearningTheory/UniformDeviation/Confidence` | `uniform_deviation_tail_bound_countable_of_empirical_le_delta` | -| any separable class | `LearningTheory/UniformDeviation/Confidence` | `uniform_deviation_tail_bound_separable_of_empirical_le_delta` | +| any pointwise separable class | `LearningTheory/UniformDeviation/Confidence` | `uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_le_delta` | | `ℓ₂` linear predictors | `LearningTheory/FunctionClass/LinearPredictor/L2` | `linear_predictor_l2_uniform_deviation_tail_bound_delta` | | `ℓ₁/ℓ∞` linear predictors | `LearningTheory/FunctionClass/LinearPredictor/L1` | `linear_predictor_l1_uniform_deviation_tail_bound_delta` | | feature-map RKHS predictors | `LearningTheory/FunctionClass/KernelPredictor` | `rkhs_uniformDeviation_tail_bound_kernelTrace_delta` | -| via Dudley's entropy integral | `LearningTheory/Rademacher/Dudley` | `uniform_deviation_tail_bound_separable_of_dudley_delta` | +| threshold classifiers (Kolmogorov–Smirnov) | `LearningTheory/FunctionClass/Threshold` | `threshold_uniform_deviation_tail_bound_of_empirical_le_delta` | +| via Dudley's entropy integral | `LearningTheory/Rademacher/Dudley` | `uniform_deviation_tail_bound_pointwiseSeparable_of_dudley_delta` | | finite hypothesis classes | `LearningTheory/Rademacher/FiniteClass` | `uniform_deviation_tail_bound_finite_of_dudley_quarter_delta` | | Lipschitz-parametrized families | `LearningTheory/Rademacher/LipschitzParameter` | `uniform_deviation_tail_bound_lipschitzParameter_dudley_delta` | -| approximate ERM, excess risk | `LearningTheory/EmpiricalRiskMinimization/Generalization` | `approxERM_excessRisk_tail_bound_separable_of_sample_empirical_le_delta` | +| approximate ERM, excess risk | `LearningTheory/EmpiricalRiskMinimization/Generalization` | `approxERM_excessRisk_tail_bound_pointwiseSeparable_of_sample_empirical_le_delta` | | the same over an RKHS ball | `LearningTheory/EmpiricalRiskMinimization/KernelPredictor` | `rkhs_approxERM_excessRisk_tail_bound_delta` | Supporting notions: `empiricalRademacherComplexity` and `rademacherComplexity` diff --git a/StatsMLlib/LearningTheory/EmpiricalRiskMinimization/Generalization.lean b/StatsMLlib/LearningTheory/EmpiricalRiskMinimization/Generalization.lean index 0cedbd7..301ffca 100644 --- a/StatsMLlib/LearningTheory/EmpiricalRiskMinimization/Generalization.lean +++ b/StatsMLlib/LearningTheory/EmpiricalRiskMinimization/Generalization.lean @@ -42,15 +42,14 @@ Expected-complexity excess-risk tail bound for an approximate ERM: `Pr{R(A(S)) - R(hstar) ≥ 4 C + 2 ε + η} ≤ exp (-n ε² / (2 b²))`. -/ -theorem approxERM_excessRisk_tail_bound_separable_of_rademacher_le +theorem approxERM_excessRisk_tail_bound_pointwiseSeparable_of_rademacher_le [MeasurableSpace 𝒵] [Nonempty 𝒵] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] [IsProbabilityMeasure μ] (hn : 0 < n) (ℓ : H → 𝒵 → ℝ) (hℓ_meas : ∀ h, Measurable (ℓ h)) (Z : Ω → 𝒵) (hZ : Measurable Z) {b C η : ℝ} (hb : 0 < b) (hℓ_bound : ∀ h z, |ℓ h z| ≤ b) - (hℓ_cont : ∀ z : 𝒵, Continuous fun h ↦ ℓ h z) + (hℓ_ps : PointwiseSeparable ℓ) (A : (Fin n → 𝒵) → H) (hA : ∀ S, IsApproxERM η n ℓ S (A S)) (hC : rademacherComplexity n ℓ μ Z ≤ C) @@ -74,8 +73,8 @@ theorem approxERM_excessRisk_tail_bound_separable_of_rademacher_le hn (fun h ↦ (hℓ_meas h).comp hZ) hℓ_bound (Z ∘ S)) linarith _ ≤ _ := - uniform_deviation_tail_bound_separable_of_rademacher_le - (μ := μ) ℓ hℓ_meas Z hZ hb hℓ_bound hℓ_cont hC hε + uniform_deviation_tail_bound_pointwiseSeparable_of_rademacher_le + (μ := μ) ℓ hℓ_meas Z hZ hb hℓ_bound hℓ_ps hC hε /-- Observed empirical-complexity excess-risk tail bound for an approximate ERM: @@ -83,15 +82,14 @@ Observed empirical-complexity excess-risk tail bound for an approximate ERM: `Pr{R(A(S)) - R(hstar) ≥ 4 Rhatₙ(ℓ;S) + 6 ε + η} ≤ 2 exp (-n ε² / (2 b²))`. -/ -theorem approxERM_excessRisk_tail_bound_separable_of_empirical_complexity +theorem approxERM_excessRisk_tail_bound_pointwiseSeparable_of_empirical_complexity [MeasurableSpace 𝒵] [Nonempty 𝒵] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] [IsProbabilityMeasure μ] (hn : 0 < n) (ℓ : H → 𝒵 → ℝ) (hℓ_meas : ∀ h, Measurable (ℓ h)) (Z : Ω → 𝒵) (hZ : Measurable Z) {b η : ℝ} (hb : 0 < b) (hℓ_bound : ∀ h z, |ℓ h z| ≤ b) - (hℓ_cont : ∀ z : 𝒵, Continuous fun h ↦ ℓ h z) + (hℓ_ps : PointwiseSeparable ℓ) (A : (Fin n → 𝒵) → H) (hA : ∀ S, IsApproxERM η n ℓ S (A S)) (hstar : H) {ε : ℝ} (hε : 0 ≤ ε) : @@ -119,23 +117,22 @@ theorem approxERM_excessRisk_tail_bound_separable_of_empirical_complexity hn (fun h ↦ (hℓ_meas h).comp hZ) hℓ_bound (Z ∘ S)) linarith _ ≤ _ := - uniform_deviation_tail_bound_separable_of_empirical_complexity - (μ := μ) ℓ hℓ_meas Z hZ hb hℓ_bound hℓ_cont hε + uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_complexity + (μ := μ) ℓ hℓ_meas Z hZ hb hℓ_bound hℓ_ps hε /-- Confidence-parameter form of the expected-complexity excess-risk bound: `Pr{R(A(S)) - R(hstar) ≥ 4 C + 2 r(b,δ,n) + η} ≤ δ`. -/ -theorem approxERM_excessRisk_tail_bound_separable_of_rademacher_le_delta +theorem approxERM_excessRisk_tail_bound_pointwiseSeparable_of_rademacher_le_delta [MeasurableSpace 𝒵] [Nonempty 𝒵] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] [IsProbabilityMeasure μ] (hn : 0 < n) (ℓ : H → 𝒵 → ℝ) (hℓ_meas : ∀ h, Measurable (ℓ h)) (Z : Ω → 𝒵) (hZ : Measurable Z) {b C η δ : ℝ} (hb : 0 < b) (hℓ_bound : ∀ h z, |ℓ h z| ≤ b) - (hℓ_cont : ∀ z : 𝒵, Continuous fun h ↦ ℓ h z) + (hℓ_ps : PointwiseSeparable ℓ) (A : (Fin n → 𝒵) → H) (hA : ∀ S, IsApproxERM η n ℓ S (A S)) (hC : rademacherComplexity n ℓ μ Z ≤ C) @@ -162,8 +159,8 @@ theorem approxERM_excessRisk_tail_bound_separable_of_rademacher_le_delta hn (fun h ↦ (hℓ_meas h).comp hZ) hℓ_bound (Z ∘ S)) linarith _ ≤ δ := - uniform_deviation_tail_bound_separable_of_rademacher_le_delta - (μ := μ) hn ℓ hℓ_meas Z hZ hb hℓ_bound hℓ_cont hC hδ hδ_one + uniform_deviation_tail_bound_pointwiseSeparable_of_rademacher_le_delta + (μ := μ) hn ℓ hℓ_meas Z hZ hb hℓ_bound hℓ_ps hC hδ hδ_one /-- Confidence-parameter form retaining any sample-dependent empirical-complexity @@ -171,16 +168,15 @@ upper bound `C(S)`: `Pr{R(A(S)) - R(hstar) ≥ 4 C(S) + 6 r₂(b,δ,n) + η} ≤ δ`. -/ -theorem approxERM_excessRisk_tail_bound_separable_of_sample_empirical_le_delta +theorem approxERM_excessRisk_tail_bound_pointwiseSeparable_of_sample_empirical_le_delta [MeasurableSpace 𝒵] [Nonempty 𝒵] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] [IsProbabilityMeasure μ] (hn : 0 < n) (ℓ : H → 𝒵 → ℝ) (hℓ_meas : ∀ h, Measurable (ℓ h)) (Z : Ω → 𝒵) (hZ : Measurable Z) (C : (Fin n → 𝒵) → ℝ) {b η δ : ℝ} (hb : 0 < b) (hℓ_bound : ∀ h z, |ℓ h z| ≤ b) - (hℓ_cont : ∀ z : 𝒵, Continuous fun h ↦ ℓ h z) + (hℓ_ps : PointwiseSeparable ℓ) (A : (Fin n → 𝒵) → H) (hA : ∀ S, IsApproxERM η n ℓ S (A S)) (hC : ∀ S, empiricalRademacherComplexity n ℓ S ≤ C S) @@ -208,21 +204,20 @@ theorem approxERM_excessRisk_tail_bound_separable_of_sample_empirical_le_delta linarith _ ≤ δ := by simpa [sampleConfidenceRadius, confidenceRadius] using - uniform_deviation_tail_bound_separable_of_sample_empirical_le_delta - (μ := μ) hn ℓ hℓ_meas Z hZ C hb hℓ_bound hℓ_cont hC hδ hδ_one + uniform_deviation_tail_bound_pointwiseSeparable_of_sample_empirical_le_delta + (μ := μ) hn ℓ hℓ_meas Z hZ C hb hℓ_bound hℓ_ps hC hδ hδ_one /-- Exact-ERM specialization of the expected-complexity tail bound. -/ -theorem erm_excessRisk_tail_bound_separable_of_rademacher_le +theorem erm_excessRisk_tail_bound_pointwiseSeparable_of_rademacher_le [MeasurableSpace 𝒵] [Nonempty 𝒵] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] [IsProbabilityMeasure μ] (hn : 0 < n) (ℓ : H → 𝒵 → ℝ) (hℓ_meas : ∀ h, Measurable (ℓ h)) (Z : Ω → 𝒵) (hZ : Measurable Z) {b C : ℝ} (hb : 0 < b) (hℓ_bound : ∀ h z, |ℓ h z| ≤ b) - (hℓ_cont : ∀ z : 𝒵, Continuous fun h ↦ ℓ h z) + (hℓ_ps : PointwiseSeparable ℓ) (A : (Fin n → 𝒵) → H) (hA : ∀ S, IsERM n ℓ S (A S)) (hC : rademacherComplexity n ℓ μ Z ≤ C) @@ -231,8 +226,8 @@ theorem erm_excessRisk_tail_bound_separable_of_rademacher_le 4 * C + 2 * ε ≤ excessRisk ℓ μ Z (A (Z ∘ S)) hstar}).toReal ≤ (-ε ^ 2 * n / (2 * b ^ 2)).exp := by simpa using - approxERM_excessRisk_tail_bound_separable_of_rademacher_le - (μ := μ) hn ℓ hℓ_meas Z hZ hb hℓ_bound hℓ_cont A + approxERM_excessRisk_tail_bound_pointwiseSeparable_of_rademacher_le + (μ := μ) hn ℓ hℓ_meas Z hZ hb hℓ_bound hℓ_ps A (fun S ↦ (hA S).isApproxERM) hC hstar hε /-- @@ -242,7 +237,6 @@ loss class `(x,y) ↦ loss (F h x) y`. theorem supervised_approxERM_excessRisk_tail_bound_of_empirical_complexity {𝒳 𝒴 : Type*} [MeasurableSpace (𝒳 × 𝒴)] [Nonempty (𝒳 × 𝒴)] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] [IsProbabilityMeasure μ] (hn : 0 < n) (F : H → 𝒳 → ℝ) (loss : ℝ → 𝒴 → ℝ) @@ -251,8 +245,8 @@ theorem supervised_approxERM_excessRisk_tail_bound_of_empirical_complexity {b η : ℝ} (hb : 0 < b) (hclass_bound : ∀ h z, |supervisedLossClass F loss h z| ≤ b) - (hclass_cont : - ∀ z : 𝒳 × 𝒴, Continuous fun h ↦ supervisedLossClass F loss h z) + (hF_ps : PointwiseSeparable F) + (hloss_cont : ∀ y, Continuous fun u ↦ loss u y) (A : (Fin n → 𝒳 × 𝒴) → H) (hA : ∀ S, IsApproxERM η n (supervisedLossClass F loss) S (A S)) @@ -264,9 +258,9 @@ theorem supervised_approxERM_excessRisk_tail_bound_of_empirical_complexity excessRisk (supervisedLossClass F loss) μ Z (A (Z ∘ S)) hstar}).toReal ≤ 2 * (-ε ^ 2 * n / (2 * b ^ 2)).exp := - approxERM_excessRisk_tail_bound_separable_of_empirical_complexity + approxERM_excessRisk_tail_bound_pointwiseSeparable_of_empirical_complexity (μ := μ) hn (supervisedLossClass F loss) hclass_meas Z hZ - hb hclass_bound hclass_cont A hA hstar hε + hb hclass_bound (hF_ps.supervisedLossClass hloss_cont) A hA hstar hε /-! ## Examples @@ -307,7 +301,7 @@ probability through `Measure.real`. /-- Main sample-dependent excess-risk example for an approximate ERM. -/ example [MeasurableSpace 𝒵] [Nonempty 𝒵] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] + [TopologicalSpace H] [SeparableSpace H] [FrechetUrysohnSpace H] [IsProbabilityMeasure μ] (ℓ : H → 𝒵 → ℝ) (hℓ_meas : ∀ h, Measurable (ℓ h)) (X : Ω → 𝒵) (hX : Measurable X) @@ -321,8 +315,8 @@ example (μⁿ {S : Fin n → Ω | 4 * C (X ∘ S) + 6 * sampleConfidenceRadius b δ n + η ≤ excessRisk ℓ μ X (A (X ∘ S)) hstar}).toReal ≤ δ := by - exact approxERM_excessRisk_tail_bound_separable_of_sample_empirical_le_delta - (μ := μ) hn ℓ hℓ_meas X hX C hb hℓ_bound hℓ_cont + exact approxERM_excessRisk_tail_bound_pointwiseSeparable_of_sample_empirical_le_delta + (μ := μ) hn ℓ hℓ_meas X hX C hb hℓ_bound (PointwiseSeparable.of_continuous hℓ_cont) A hA hC hstar hδ hδ_one /-! diff --git a/StatsMLlib/LearningTheory/EmpiricalRiskMinimization/KernelPredictor.lean b/StatsMLlib/LearningTheory/EmpiricalRiskMinimization/KernelPredictor.lean index bfff8c0..cb73d31 100644 --- a/StatsMLlib/LearningTheory/EmpiricalRiskMinimization/KernelPredictor.lean +++ b/StatsMLlib/LearningTheory/EmpiricalRiskMinimization/KernelPredictor.lean @@ -13,8 +13,8 @@ import StatsMLlib.LearningTheory.Rademacher.Reindex This module combines the contraction theorem with the feature-map RKHS trace estimate and the approximate-ERM oracle inequality, giving a loss-to-excess-risk -endpoint for a weight family indexed by an arbitrary separable, first-countable -parameter space. The uniform bound the contraction step needs comes from the +endpoint for a weight family indexed by an arbitrary separable Fréchet–Urysohn +(for example, metric) parameter space. The uniform bound the contraction step needs comes from the kernel diagonal bound. -/ @@ -31,7 +31,7 @@ variable {𝒳 : Type v} {𝒴 : Type w} variable {E : Type x} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] variable {G : Type y} [Nonempty G] - [TopologicalSpace G] [SeparableSpace G] [FirstCountableTopology G] + [TopologicalSpace G] [SeparableSpace G] [FrechetUrysohnSpace G] variable {μ : Measure Ω} local notation "μⁿ" => Measure.pi (fun _ ↦ μ) @@ -167,12 +167,12 @@ theorem rkhs_approxERM_excessRisk_tail_bound_delta exact (hloss_cont z.2).comp ((continuous_rkhsPredictor_weight Φ z.1).comp hweights) have htail := - approxERM_excessRisk_tail_bound_separable_of_sample_empirical_le_delta + approxERM_excessRisk_tail_bound_pointwiseSeparable_of_sample_empirical_le_delta (μ := μ) hn lossClass (by simpa only [lossClass, predictor] using hclass_meas) Z hZ C hb (by simpa only [lossClass, predictor] using hclass_bound) - hclass_cont + (PointwiseSeparable.of_continuous hclass_cont) A (by simpa only [lossClass, predictor] using hA) hC gstar hδ hδ_one diff --git a/StatsMLlib/LearningTheory/FunctionClass/KernelPredictor.lean b/StatsMLlib/LearningTheory/FunctionClass/KernelPredictor.lean index 76f2b1a..b4cb675 100644 --- a/StatsMLlib/LearningTheory/FunctionClass/KernelPredictor.lean +++ b/StatsMLlib/LearningTheory/FunctionClass/KernelPredictor.lean @@ -231,13 +231,13 @@ theorem rkhs_rademacherComplexity_le r * Λ / Real.sqrt (n : ℝ) := by let : Nonempty (Metric.closedBall (0 : H) Λ) := (Metric.nonempty_closedBall.mpr hΛ).to_subtype - apply rademacherComplexity_le_of_empirical_le_separable + apply rademacherComplexity_le_of_empirical_le_pointwiseSeparable (F := rkhsPredictor Φ) (X := X) · intro w exact (measurable_rkhsPredictor_input Φ hΦ w).comp hX · exact mul_nonneg hr hΛ · exact fun w x ↦ abs_rkhsPredictor_le Φ hΛ hr hdiag w x - · exact continuous_rkhsPredictor_weight Φ + · exact PointwiseSeparable.of_continuous (continuous_rkhsPredictor_weight Φ) · exact rkhs_empiricalRademacherComplexity_le Φ Λ r hΛ hr hdiag /-- @@ -260,13 +260,13 @@ theorem rkhs_uniformDeviation_expectation_le 2 * (r * Λ / Real.sqrt (n : ℝ)) := by let : Nonempty (Metric.closedBall (0 : H) Λ) := (Metric.nonempty_closedBall.mpr hΛ).to_subtype - apply uniform_deviation_expectation_le_of_empirical_le_separable + apply uniform_deviation_expectation_le_of_empirical_le_pointwiseSeparable (F := rkhsPredictor Φ) hn · exact fun w ↦ measurable_rkhsPredictor_input Φ hΦ w · exact hX · exact mul_nonneg hr hΛ · exact fun w x ↦ abs_rkhsPredictor_le Φ hΛ hr hdiag w x - · exact continuous_rkhsPredictor_weight Φ + · exact PointwiseSeparable.of_continuous (continuous_rkhsPredictor_weight Φ) · exact rkhs_empiricalRademacherComplexity_le Φ Λ r hΛ hr hdiag /-- @@ -297,13 +297,13 @@ theorem rkhs_uniformDeviation_tail_bound_delta μ X (X ∘ S)}).toReal ≤ δ := by let : Nonempty (Metric.closedBall (0 : H) Λ) := (Metric.nonempty_closedBall.mpr hΛ.le).to_subtype - apply uniform_deviation_tail_bound_separable_of_empirical_le_delta + apply uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_le_delta (μ := μ) hn (F := rkhsPredictor Φ) · exact fun w ↦ measurable_rkhsPredictor_input Φ hΦ w · exact hX · exact mul_pos hr hΛ · exact fun w x ↦ abs_rkhsPredictor_le Φ hΛ.le hr.le hdiag w x - · exact continuous_rkhsPredictor_weight Φ + · exact PointwiseSeparable.of_continuous (continuous_rkhsPredictor_weight Φ) · exact rkhs_empiricalRademacherComplexity_le Φ Λ r hΛ.le hr.le hdiag · exact hδ @@ -333,7 +333,7 @@ theorem rkhs_uniformDeviation_tail_bound_kernelTrace_delta μ X (X ∘ S)}).toReal ≤ δ := by let : Nonempty (Metric.closedBall (0 : H) Λ) := (Metric.nonempty_closedBall.mpr hΛ.le).to_subtype - exact uniform_deviation_tail_bound_separable_of_sample_empirical_le_delta + exact uniform_deviation_tail_bound_pointwiseSeparable_of_sample_empirical_le_delta (μ := μ) hn (rkhsPredictor Φ : Metric.closedBall (0 : H) Λ → 𝒳 → ℝ) @@ -342,7 +342,7 @@ theorem rkhs_uniformDeviation_tail_bound_kernelTrace_delta (fun S ↦ Λ * (n : ℝ)⁻¹ * Real.sqrt (kernelTrace Φ S)) (mul_pos hr hΛ) (fun w x ↦ abs_rkhsPredictor_le Φ hΛ.le hr.le hdiag w x) - (continuous_rkhsPredictor_weight Φ) + (PointwiseSeparable.of_continuous (continuous_rkhsPredictor_weight Φ)) (rkhs_empiricalRademacherComplexity_le_kernelTrace Φ Λ hΛ.le) hδ hδ_one diff --git a/StatsMLlib/LearningTheory/FunctionClass/LinearPredictor/L1.lean b/StatsMLlib/LearningTheory/FunctionClass/LinearPredictor/L1.lean index 0fa2482..28f7168 100644 --- a/StatsMLlib/LearningTheory/FunctionClass/LinearPredictor/L1.lean +++ b/StatsMLlib/LearningTheory/FunctionClass/LinearPredictor/L1.lean @@ -911,13 +911,13 @@ theorem linear_predictor_l1_rademacher_complexity_bound ≤ (Xinf * W / Real.sqrt (n : ℝ)) * Real.sqrt (2 * Real.log (2 * d)) := by let : Nonempty (L1Ball (d := d) W) := nonempty_L1Ball hW - apply rademacherComplexity_le_of_empirical_le_separable + apply rademacherComplexity_le_of_empirical_le_pointwiseSeparable (F := linearPredictorL1) (X := Z) · intro w exact (continuous_linearPredictorL1_input w).measurable.comp hZ · exact mul_nonneg hX hW · exact fun w x ↦ abs_linearPredictorL1_le hX w x - · exact continuous_linearPredictorL1_weight + · exact PointwiseSeparable.of_continuous continuous_linearPredictorL1_weight · exact linear_predictor_l1_empirical_bound d n Xinf W hX hW d_pos n_pos @@ -940,13 +940,13 @@ theorem linear_predictor_l1_uniform_deviation_expectation_bound Real.sqrt (2 * Real.log (2 * d))) := by let : Nonempty (L1Ball (d := d) W) := nonempty_L1Ball hW let : Nonempty (LinftyBall (d := d) Xinf) := nonempty_LinftyBall hX - apply uniform_deviation_expectation_le_of_empirical_le_separable + apply uniform_deviation_expectation_le_of_empirical_le_pointwiseSeparable (F := linearPredictorL1) n_pos · exact fun w ↦ (continuous_linearPredictorL1_input w).measurable · exact hZ · exact mul_nonneg hX hW · exact fun w x ↦ abs_linearPredictorL1_le hX w x - · exact continuous_linearPredictorL1_weight + · exact PointwiseSeparable.of_continuous continuous_linearPredictorL1_weight · exact linear_predictor_l1_empirical_bound d n Xinf W hX hW d_pos n_pos @@ -972,13 +972,13 @@ theorem linear_predictor_l1_uniform_deviation_tail_bound ≤ (-ε ^ 2 * n / (2 * (Xinf * W) ^ 2)).exp := by let : Nonempty (L1Ball (d := d) W) := nonempty_L1Ball hW.le let : Nonempty (LinftyBall (d := d) Xinf) := nonempty_LinftyBall hX.le - apply uniform_deviation_tail_bound_separable_of_empirical_le + apply uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_le (F := linearPredictorL1) · exact fun w ↦ (continuous_linearPredictorL1_input w).measurable · exact hZ · exact mul_pos hX hW · exact fun w x ↦ abs_linearPredictorL1_le hX.le w x - · exact continuous_linearPredictorL1_weight + · exact PointwiseSeparable.of_continuous continuous_linearPredictorL1_weight · exact linear_predictor_l1_empirical_bound d n Xinf W hX.le hW.le d_pos n_pos · exact hε @@ -1009,13 +1009,13 @@ theorem linear_predictor_l1_uniform_deviation_tail_bound_delta μ Z (Z ∘ S)}).toReal ≤ δ := by let : Nonempty (L1Ball (d := d) W) := nonempty_L1Ball hW.le let : Nonempty (LinftyBall (d := d) Xinf) := nonempty_LinftyBall hX.le - apply uniform_deviation_tail_bound_separable_of_empirical_le_delta + apply uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_le_delta (μ := μ) n_pos (F := linearPredictorL1) · exact fun w ↦ (continuous_linearPredictorL1_input w).measurable · exact hZ · exact mul_pos hX hW · exact fun w x ↦ abs_linearPredictorL1_le hX.le w x - · exact continuous_linearPredictorL1_weight + · exact PointwiseSeparable.of_continuous continuous_linearPredictorL1_weight · exact linear_predictor_l1_empirical_bound d n Xinf W hX.le hW.le d_pos n_pos · exact hδ @@ -1047,7 +1047,7 @@ theorem linear_predictor_l1_uniform_deviation_tail_bound_of_sample_delta let : Nonempty (L1Ball (d := d) W) := nonempty_L1Ball hW.le let : Nonempty (LinftyBall (d := d) Xinf) := nonempty_LinftyBall hX.le exact - uniform_deviation_tail_bound_separable_of_sample_empirical_le_delta + uniform_deviation_tail_bound_pointwiseSeparable_of_sample_empirical_le_delta (μ := μ) (n := n) n_pos (linearPredictorL1 : L1Ball (d := d) W → LinftyBall (d := d) Xinf → ℝ) @@ -1058,7 +1058,7 @@ theorem linear_predictor_l1_uniform_deviation_tail_bound_of_sample_delta Real.sqrt (2 * Real.log (2 * d))) (mul_pos hX hW) (fun w x ↦ abs_linearPredictorL1_le hX.le w x) - continuous_linearPredictorL1_weight + (PointwiseSeparable.of_continuous continuous_linearPredictorL1_weight) (linear_predictor_l1_empirical_bound_of_sample d n Xinf W hW.le d_pos n_pos) hδ hδ_one diff --git a/StatsMLlib/LearningTheory/FunctionClass/LinearPredictor/L2.lean b/StatsMLlib/LearningTheory/FunctionClass/LinearPredictor/L2.lean index 25f922b..3de4fa5 100644 --- a/StatsMLlib/LearningTheory/FunctionClass/LinearPredictor/L2.lean +++ b/StatsMLlib/LearningTheory/FunctionClass/LinearPredictor/L2.lean @@ -551,13 +551,13 @@ theorem linear_predictor_l2_rademacher_complexity_bound ≤ X * W / Real.sqrt (n : ℝ) := by let : Nonempty (Metric.closedBall (0 : EuclideanSpace ℝ (Fin d)) W) := (Metric.nonempty_closedBall.mpr hW).to_subtype - apply rademacherComplexity_le_of_empirical_le_separable + apply rademacherComplexity_le_of_empirical_le_pointwiseSeparable (F := linearPredictorL2) (X := Z) · intro w exact (continuous_linearPredictorL2_input w).measurable.comp hZ · exact mul_nonneg hX hW · exact fun w x ↦ abs_linearPredictorL2_le hW w x - · exact continuous_linearPredictorL2_weight + · exact PointwiseSeparable.of_continuous continuous_linearPredictorL2_weight · exact linear_predictor_l2_empirical_bound d n W X hX hW /-- @@ -581,13 +581,13 @@ theorem linear_predictor_l2_uniform_deviation_expectation_bound (Metric.nonempty_closedBall.mpr hW).to_subtype let : Nonempty (Metric.closedBall (0 : EuclideanSpace ℝ (Fin d)) X) := (Metric.nonempty_closedBall.mpr hX).to_subtype - apply uniform_deviation_expectation_le_of_empirical_le_separable + apply uniform_deviation_expectation_le_of_empirical_le_pointwiseSeparable (F := linearPredictorL2) hn · exact fun w ↦ (continuous_linearPredictorL2_input w).measurable · exact hZ · exact mul_nonneg hX hW · exact fun w x ↦ abs_linearPredictorL2_le hW w x - · exact continuous_linearPredictorL2_weight + · exact PointwiseSeparable.of_continuous continuous_linearPredictorL2_weight · exact linear_predictor_l2_empirical_bound d n W X hX hW /-- @@ -612,13 +612,13 @@ theorem linear_predictor_l2_uniform_deviation_tail_bound (Metric.nonempty_closedBall.mpr hW.le).to_subtype let : Nonempty (Metric.closedBall (0 : EuclideanSpace ℝ (Fin d)) X) := (Metric.nonempty_closedBall.mpr hX.le).to_subtype - apply uniform_deviation_tail_bound_separable_of_empirical_le + apply uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_le (F := linearPredictorL2) · exact fun w ↦ (continuous_linearPredictorL2_input w).measurable · exact hZ · exact mul_pos hX hW · exact fun w x ↦ abs_linearPredictorL2_le hW.le w x - · exact continuous_linearPredictorL2_weight + · exact PointwiseSeparable.of_continuous continuous_linearPredictorL2_weight · exact linear_predictor_l2_empirical_bound d n W X hX.le hW.le · exact hε @@ -647,13 +647,13 @@ theorem linear_predictor_l2_uniform_deviation_tail_bound_delta (Metric.nonempty_closedBall.mpr hW.le).to_subtype let : Nonempty (Metric.closedBall (0 : EuclideanSpace ℝ (Fin d)) X) := (Metric.nonempty_closedBall.mpr hX.le).to_subtype - apply uniform_deviation_tail_bound_separable_of_empirical_le_delta + apply uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_le_delta (μ := μ) hn (F := linearPredictorL2) · exact fun w ↦ (continuous_linearPredictorL2_input w).measurable · exact hZ · exact mul_pos hX hW · exact fun w x ↦ abs_linearPredictorL2_le hW.le w x - · exact continuous_linearPredictorL2_weight + · exact PointwiseSeparable.of_continuous continuous_linearPredictorL2_weight · exact linear_predictor_l2_empirical_bound d n W X hX.le hW.le · exact hδ · exact hδ_one @@ -688,7 +688,7 @@ theorem linear_predictor_l2_uniform_deviation_tail_bound_of_sample_delta let : Nonempty (Metric.closedBall (0 : EuclideanSpace ℝ (Fin d)) X) := (Metric.nonempty_closedBall.mpr hX.le).to_subtype have htail := - uniform_deviation_tail_bound_separable_of_sample_empirical_le_delta + uniform_deviation_tail_bound_pointwiseSeparable_of_sample_empirical_le_delta (μ := μ) (n := n) hn (linearPredictorL2 : Metric.closedBall (0 : EuclideanSpace ℝ (Fin d)) W → @@ -701,7 +701,7 @@ theorem linear_predictor_l2_uniform_deviation_tail_bound_of_sample_delta (∑ k : Fin n, ‖(S k : EuclideanSpace ℝ (Fin d))‖ ^ 2)) (mul_pos hX hW) (fun w x ↦ abs_linearPredictorL2_le hW.le w x) - continuous_linearPredictorL2_weight + (PointwiseSeparable.of_continuous continuous_linearPredictorL2_weight) (linear_predictor_l2_empirical_bound_of_sample d n W X hW.le) hδ hδ_one simpa only [Function.comp_apply] using htail diff --git a/StatsMLlib/LearningTheory/FunctionClass/Threshold.lean b/StatsMLlib/LearningTheory/FunctionClass/Threshold.lean new file mode 100644 index 0000000..d855754 --- /dev/null +++ b/StatsMLlib/LearningTheory/FunctionClass/Threshold.lean @@ -0,0 +1,111 @@ +/- +Copyright (c) 2026 Kei Tsukamoto. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kei Tsukamoto +-/ +import StatsMLlib.LearningTheory.UniformDeviation.Confidence + +/-! +# Threshold classifiers on the real line + +The class of threshold classifiers `x ↦ 1[x ≤ t]`, indexed by `t : ℝ`, is the basic 0-1 loss +class that is not continuous in its parameter, so no topology on the index space reduces its +suprema to a countable subclass. It is nevertheless pointwise separable: approximating `t` from +above by rationals converges at every input, including `x = t`. + +Its uniform deviation `sup_t |Fₙ(t) - F(t)|` is the Kolmogorov–Smirnov distance between the +empirical and population distribution functions, so the endpoint below is a +Rademacher-complexity form of the Glivenko–Cantelli theorem. + +## Main definitions + +* `thresholdClass`: the threshold classifiers `x ↦ 1[x ≤ t]`. + +## Main results + +* `pointwiseSeparable_thresholdClass`: the class is pointwise separable. +* `threshold_uniform_deviation_tail_bound_of_empirical_le_delta`: a confidence bound on the + Kolmogorov–Smirnov distance from a fixed-sample Rademacher bound. +-/ + +open Filter Topology MeasureTheory ProbabilityTheory + +universe u + +variable {n : ℕ} {Ω : Type u} [MeasurableSpace Ω] {μ : Measure Ω} + +local notation "μⁿ" => Measure.pi (fun _ ↦ μ) + +/-- The threshold classifier `x ↦ 1[x ≤ t]`. -/ +noncomputable def thresholdClass (t x : ℝ) : ℝ := + if x ≤ t then 1 else 0 + +lemma abs_thresholdClass_le (t x : ℝ) : |thresholdClass t x| ≤ 1 := by + unfold thresholdClass + split_ifs <;> norm_num + +lemma measurable_thresholdClass (t : ℝ) : Measurable (thresholdClass t) := + Measurable.ite (measurableSet_le measurable_id measurable_const) + measurable_const measurable_const + +/-- +Threshold classifiers form a pointwise separable class: rationals `r m` decreasing to `t` give +`1[x ≤ r m] → 1[x ≤ t]` at every input `x`. +-/ +theorem pointwiseSeparable_thresholdClass : PointwiseSeparable thresholdClass := by + obtain ⟨q, hq⟩ := exists_surjective_nat ℚ + refine ⟨fun m ↦ (q m : ℝ), fun t ↦ ?_⟩ + have hr : ∀ m : ℕ, ∃ r : ℚ, t < r ∧ (r : ℝ) < t + 1 / ((m : ℝ) + 1) := fun m ↦ + exists_rat_btwn (lt_add_of_pos_right t (by positivity)) + choose r hr_gt hr_lt using hr + choose u hu using fun m ↦ hq (r m) + refine ⟨u, fun x ↦ ?_⟩ + simp only [hu] + by_cases hx : x ≤ t + · have h1 : (fun m ↦ thresholdClass (r m) x) = fun _ ↦ 1 := + funext fun m ↦ by simp [thresholdClass, hx.trans (hr_gt m).le] + rw [h1, show thresholdClass t x = 1 by simp [thresholdClass, hx]] + exact tendsto_const_nhds + · have hxt : t < x := lt_of_not_ge hx + have hlim : Tendsto (fun m ↦ (r m : ℝ)) atTop (𝓝 t) := by + have hupper : Tendsto (fun m : ℕ ↦ t + 1 / ((m : ℝ) + 1)) atTop (𝓝 t) := by + simpa using tendsto_one_div_add_atTop_nhds_zero_nat.const_add t + exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hupper + (fun m ↦ (hr_gt m).le) (fun m ↦ (hr_lt m).le) + have hev : ∀ᶠ m in atTop, (r m : ℝ) < x := hlim.eventually (gt_mem_nhds hxt) + rw [show thresholdClass t x = 0 by simp [thresholdClass, hx]] + refine tendsto_const_nhds.congr' ?_ + filter_upwards [hev] with m hm + simp [thresholdClass, not_le.mpr hm] + +/-- +Confidence bound on the Kolmogorov–Smirnov distance `sup_t |Fₙ(t) - F(t)|` from a fixed-sample +bound `C` on the empirical Rademacher complexity of threshold classifiers. +-/ +theorem threshold_uniform_deviation_tail_bound_of_empirical_le_delta + [IsProbabilityMeasure μ] (hn : 0 < n) + (X : Ω → ℝ) (hX : Measurable X) + {C δ : ℝ} (hC : ∀ S : Fin n → ℝ, empiricalRademacherComplexity n thresholdClass S ≤ C) + (hδ : 0 < δ) (hδ_one : δ ≤ 1) : + (μⁿ {S : Fin n → Ω | + 2 * C + Real.sqrt (2 * Real.log (1 / δ) / n) ≤ + uniformDeviation n thresholdClass μ X (X ∘ S)}).toReal ≤ δ := by + simpa only [one_mul] using + uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_le_delta + (μ := μ) hn thresholdClass measurable_thresholdClass X hX one_pos + abs_thresholdClass_le pointwiseSeparable_thresholdClass hC hδ hδ_one + +/-! ## Examples + +Worked uses of this module's public API. They are elaborated with the library, so they +double as acceptance tests that these statements stay usable as written. +-/ + +/-- The Kolmogorov–Smirnov confidence bound for threshold classifiers. -/ +example [IsProbabilityMeasure μ] (hn : 0 < n) (X : Ω → ℝ) (hX : Measurable X) + {C δ : ℝ} (hC : ∀ S : Fin n → ℝ, empiricalRademacherComplexity n thresholdClass S ≤ C) + (hδ : 0 < δ) (hδ_one : δ ≤ 1) : + (μⁿ {S : Fin n → Ω | + 2 * C + Real.sqrt (2 * Real.log (1 / δ) / n) ≤ + uniformDeviation n thresholdClass μ X (X ∘ S)}).toReal ≤ δ := + threshold_uniform_deviation_tail_bound_of_empirical_le_delta hn X hX hC hδ hδ_one diff --git a/StatsMLlib/LearningTheory/Rademacher/Dudley.lean b/StatsMLlib/LearningTheory/Rademacher/Dudley.lean index 14b0b72..140764d 100644 --- a/StatsMLlib/LearningTheory/Rademacher/Dudley.lean +++ b/StatsMLlib/LearningTheory/Rademacher/Dudley.lean @@ -2121,12 +2121,12 @@ A sample-uniform Dudley estimate bounds expected Rademacher complexity: `(∀ S, Dα(F,S) ≤ C) → Rₙ(F;μ) ≤ C`. -/ theorem rademacher_complexity_le_dudley_of_uniform_entropy - [Nonempty ι] [TopologicalSpace ι] [SeparableSpace ι] + [Nonempty ι] [IsProbabilityMeasure μ] (f : ι → 𝒳 → ℝ) (X : Ω → 𝒳) (hf : ∀ h, Measurable (f h ∘ X)) {b c α C : ℝ} (hb : 0 ≤ b) (hf_bound : ∀ h x, |f h x| ≤ b) - (hf_cont : ∀ x : 𝒳, Continuous fun h ↦ f h x) + (hf_ps : PointwiseSeparable f) (hn : 0 < n) (hα : 0 < α) (hαc : α < c / 2) (htb : ∀ S : Fin n → 𝒳, TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace f S))) @@ -2134,8 +2134,8 @@ theorem rademacher_complexity_le_dudley_of_uniform_entropy (hentropy : ∀ S : Fin n → 𝒳, dudleyEntropyEstimate f S (htb S) α c ≤ C) : rademacherComplexity n f μ X ≤ C := by - apply rademacherComplexity_le_of_empirical_le_separable - f X hf hb hf_bound hf_cont + apply rademacherComplexity_le_of_empirical_le_pointwiseSeparable + f X hf hb hf_bound hf_ps intro S exact (dudley_entropy_integral_bound_abs hα (htb S) hn (hnorm S) hαc).trans (hentropy S) @@ -2146,14 +2146,13 @@ A sample-uniform Dudley estimate yields `Pr{UDₙ ≥ 2 C + ε} ≤ exp (-n ε² / (2b²))`. -/ -theorem uniform_deviation_tail_bound_separable_of_uniform_dudley +theorem uniform_deviation_tail_bound_pointwiseSeparable_of_uniform_dudley [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty ι] - [TopologicalSpace ι] [SeparableSpace ι] [FirstCountableTopology ι] [IsProbabilityMeasure μ] (f : ι → 𝒳 → ℝ) (hf : ∀ h, Measurable (f h)) (X : Ω → 𝒳) (hX : Measurable X) {b c α C : ℝ} (hb : 0 < b) (hf_bound : ∀ h x, |f h x| ≤ b) - (hf_cont : ∀ x : 𝒳, Continuous fun h ↦ f h x) + (hf_ps : PointwiseSeparable f) (hn : 0 < n) (hα : 0 < α) (hαc : α < c / 2) (htb : ∀ S : Fin n → 𝒳, TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace f S))) @@ -2164,8 +2163,8 @@ theorem uniform_deviation_tail_bound_separable_of_uniform_dudley (μⁿ {S | 2 * C + ε ≤ uniformDeviation n f μ X (X ∘ S)}).toReal ≤ (-ε ^ 2 * n / (2 * b ^ 2)).exp := by - apply uniform_deviation_tail_bound_separable_of_empirical_le - (F := f) hf X hX hb hf_bound hf_cont + apply uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_le + (F := f) hf X hX hb hf_bound hf_ps · intro S exact (dudley_entropy_integral_bound_abs hα (htb S) hn (hnorm S) hαc).trans (hentropy S) @@ -2177,14 +2176,13 @@ Sample-dependent Dudley generalization estimate: `Pr{UDₙ ≥ 2 Dα(F,S) + 3ε} ≤ 2 exp (-n ε² / (2b²))`. -/ -theorem uniform_deviation_tail_bound_separable_of_dudley +theorem uniform_deviation_tail_bound_pointwiseSeparable_of_dudley [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty ι] - [TopologicalSpace ι] [SeparableSpace ι] [FirstCountableTopology ι] [IsProbabilityMeasure μ] (f : ι → 𝒳 → ℝ) (hf : ∀ h, Measurable (f h)) (X : Ω → 𝒳) (hX : Measurable X) {b c α : ℝ} (hb : 0 < b) (hf_bound : ∀ h x, |f h x| ≤ b) - (hf_cont : ∀ x : 𝒳, Continuous fun h ↦ f h x) + (hf_ps : PointwiseSeparable f) (hn : 0 < n) (hα : 0 < α) (hαc : α < c / 2) (htb : ∀ S : Fin n → 𝒳, TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace f S))) @@ -2195,10 +2193,10 @@ theorem uniform_deviation_tail_bound_separable_of_dudley 3 * ε ≤ uniformDeviation n f μ X (X ∘ S)}).toReal ≤ 2 * (-ε ^ 2 * n / (2 * b ^ 2)).exp := by exact - uniform_deviation_tail_bound_separable_of_sample_empirical_le + uniform_deviation_tail_bound_pointwiseSeparable_of_sample_empirical_le (μ := μ) f hf X hX (fun S ↦ dudleyEntropyEstimate f S (htb S) α c) - hb hf_bound hf_cont + hb hf_bound hf_ps (fun S ↦ dudley_entropy_integral_bound_abs hα (htb S) hn (hnorm S) hαc) hε @@ -2209,14 +2207,13 @@ Confidence form of the sample-dependent Dudley estimate: `Pr{UDₙ ≥ 2 Dα(F,S) + 3b √(2 log(2/δ)/n)} ≤ δ`. -/ -theorem uniform_deviation_tail_bound_separable_of_dudley_delta +theorem uniform_deviation_tail_bound_pointwiseSeparable_of_dudley_delta [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty ι] - [TopologicalSpace ι] [SeparableSpace ι] [FirstCountableTopology ι] [IsProbabilityMeasure μ] (f : ι → 𝒳 → ℝ) (hf : ∀ h, Measurable (f h)) (X : Ω → 𝒳) (hX : Measurable X) {b c α : ℝ} (hb : 0 < b) (hf_bound : ∀ h x, |f h x| ≤ b) - (hf_cont : ∀ x : 𝒳, Continuous fun h ↦ f h x) + (hf_ps : PointwiseSeparable f) (hn : 0 < n) (hα : 0 < α) (hαc : α < c / 2) (htb : ∀ S : Fin n → 𝒳, TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace f S))) @@ -2227,10 +2224,10 @@ theorem uniform_deviation_tail_bound_separable_of_dudley_delta 3 * (b * Real.sqrt (2 * Real.log (2 / δ) / n)) ≤ uniformDeviation n f μ X (X ∘ S)}).toReal ≤ δ := by exact - uniform_deviation_tail_bound_separable_of_sample_empirical_le_delta + uniform_deviation_tail_bound_pointwiseSeparable_of_sample_empirical_le_delta (μ := μ) hn f hf X hX (fun S ↦ dudleyEntropyEstimate f S (htb S) α c) - hb hf_bound hf_cont + hb hf_bound hf_ps (fun S ↦ dudley_entropy_integral_bound_abs hα (htb S) hn (hnorm S) hαc) hδ hδ_one @@ -2271,7 +2268,7 @@ required in this form. /-- Main sample-dependent Dudley entropy-integral example. -/ example [MeasurableSpace 𝒳] [Nonempty 𝒳] - [TopologicalSpace ι] [SeparableSpace ι] [FirstCountableTopology ι] + [TopologicalSpace ι] [SeparableSpace ι] [FrechetUrysohnSpace ι] [IsProbabilityMeasure μ] (F : ι → 𝒳 → ℝ) (hF_meas : ∀ h, Measurable (F h)) (X : Ω → 𝒳) (hX : Measurable X) @@ -2286,8 +2283,8 @@ example 2 * dudleyEntropyEstimate F (X ∘ S) (htb (X ∘ S)) α c + 3 * (b * Real.sqrt (2 * Real.log (2 / δ) / n)) ≤ uniformDeviation n F μ X (X ∘ S)}).toReal ≤ δ := by - exact uniform_deviation_tail_bound_separable_of_dudley_delta - F hF_meas X hX hb hF_bound hF_cont hn hα hαc + exact uniform_deviation_tail_bound_pointwiseSeparable_of_dudley_delta + F hF_meas X hX hb hF_bound (PointwiseSeparable.of_continuous hF_cont) hn hα hαc htb hnorm hδ hδ_one end Generalization diff --git a/StatsMLlib/LearningTheory/Rademacher/LipschitzParameter.lean b/StatsMLlib/LearningTheory/Rademacher/LipschitzParameter.lean index 94300a1..e038b57 100644 --- a/StatsMLlib/LearningTheory/Rademacher/LipschitzParameter.lean +++ b/StatsMLlib/LearningTheory/Rademacher/LipschitzParameter.lean @@ -361,7 +361,7 @@ end # Generalization bounds for one-dimensional Lipschitz families The explicit interval grid and Dudley estimate are inserted into the -sample-dependent separable-class bridge. The final threshold contains only +sample-dependent pointwise-separable-class bridge. The final threshold contains only `ceil (2 W L / α)`, not a covering number or a total-boundedness proof. -/ @@ -406,10 +406,10 @@ theorem uniform_deviation_tail_bound_lipschitzParameter_dudley_delta intro t s rw [Subtype.dist_eq, Real.dist_eq] exact hF_lip t s x - apply uniform_deviation_tail_bound_separable_of_sample_empirical_le_delta + apply uniform_deviation_tail_bound_pointwiseSeparable_of_sample_empirical_le_delta (μ := μ) hn F hF_meas X hX (fun _ ↦ lipschitzParameterDudleyEstimate n W L α c) - hb hF_bound hF_cont + hb hF_bound (PointwiseSeparable.of_continuous hF_cont) · intro S exact empiricalRademacherComplexity_le_lipschitzParameterDudleyEstimate hn hW hL hα hαc F hF_lip S (hNorm S) diff --git a/StatsMLlib/LearningTheory/Rademacher/PointwiseSeparable.lean b/StatsMLlib/LearningTheory/Rademacher/PointwiseSeparable.lean new file mode 100644 index 0000000..a1766bb --- /dev/null +++ b/StatsMLlib/LearningTheory/Rademacher/PointwiseSeparable.lean @@ -0,0 +1,206 @@ +/- +Copyright (c) 2026 Kei Tsukamoto. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kei Tsukamoto +-/ +import StatsMLlib.LearningTheory.Rademacher.Complexity +import StatsMLlib.LearningTheory.UniformDeviation.Defs +import StatsMLlib.LearningTheory.EmpiricalRiskMinimization.Defs +import StatsMLlib.Analysis.FiniteSample +import Mathlib.MeasureTheory.Integral.DominatedConvergence +import Mathlib.Topology.Sequences + +/-! +# Pointwise separable function classes + +A function class `F : H → 𝒳 → ℝ` is *pointwise separable* if a countable subfamily +`g : ℕ → H` approximates every member of the class pointwise along a sequence, with one +sequence serving all inputs `x` at once. This is the "pointwise measurable class" condition of +van der Vaart and Wellner, *Weak Convergence and Empirical Processes*, Example 2.3.4. + +For a uniformly bounded class, the condition reduces the suprema over `H` that define empirical +Rademacher complexity, Rademacher complexity, and uniform deviation to suprema over `ℕ`. The +reduction for uniform deviation uses dominated convergence along a sequence, so `H` carries no +topology. Like `StatsMLlib.LearningTheory.Rademacher.Reindex`, these lemmas change the index of a +class while preserving the three central quantities. + +Continuity in the parameter is one sufficient condition (`PointwiseSeparable.of_continuous`), +but it is not necessary: threshold classes `x ↦ 1[x ≤ t]` are pointwise separable although they +are discontinuous in `t`. + +## Main definitions + +* `PointwiseSeparable`: a countable subfamily approximates the class pointwise. + +## Main results + +* `empiricalRademacherComplexity_eq_comp_of_tendsto`, + `rademacherComplexity_eq_comp_of_tendsto`, `uniformDeviation_eq_comp_of_tendsto`: the + reductions to the countable subfamily. +* `PointwiseSeparable.of_continuous`: a class continuous in a separable Fréchet–Urysohn + parameter space is pointwise separable. +* `PointwiseSeparable.comp`, `PointwiseSeparable.supervisedLossClass`: stability under + composition with a continuous outer map, such as a loss. +-/ + +open Filter Topology Set MeasureTheory ProbabilityTheory +open scoped BigOperators + +universe u v w x + +variable {Ω : Type u} [MeasurableSpace Ω] {H : Type v} {𝒳 : Type w} + +/-- +A function class `F` is pointwise separable if some sequence `g` of hypotheses approximates every +hypothesis `h` pointwise along a subsequence `g ∘ u`, the same subsequence for every input. +-/ +def PointwiseSeparable (F : H → 𝒳 → ℝ) : Prop := + ∃ g : ℕ → H, ∀ h, ∃ u : ℕ → ℕ, ∀ x, + Tendsto (fun m ↦ F (g (u m)) x) atTop (𝓝 (F h x)) + +/-- +A bounded indexed supremum equals the supremum along a sequence `g` when every value is a limit +of values along `g`. +-/ +theorem ciSup_eq_ciSup_comp_of_tendsto [Nonempty H] {Φ : H → ℝ} (g : ℕ → H) + (hΦ : BddAbove (range Φ)) + (hlim : ∀ h, ∃ u : ℕ → ℕ, Tendsto (fun m ↦ Φ (g (u m))) atTop (𝓝 (Φ h))) : + ⨆ h, Φ h = ⨆ m, Φ (g m) := by + have hg : BddAbove (range fun m ↦ Φ (g m)) := + hΦ.mono (by rintro _ ⟨m, rfl⟩; exact ⟨g m, rfl⟩) + apply le_antisymm + · apply ciSup_le + intro h + obtain ⟨u, hu⟩ := hlim h + exact le_of_tendsto' hu fun m ↦ le_ciSup hg (u m) + · exact ciSup_le fun m ↦ le_ciSup hΦ (g m) + +section Reduction + +variable {n : ℕ} + +/-- A sample average of a family bounded by `b` is bounded by `|b|`, also for `n = 0`. -/ +private lemma abs_sampleAverage_le (a : Fin n → 𝒳 → ℝ) (S : Fin n → 𝒳) {b : ℝ} + (ha : ∀ k x, |a k x| ≤ b) : + |(n : ℝ)⁻¹ * ∑ k : Fin n, a k (S k)| ≤ |b| := by + rcases Nat.eq_zero_or_pos n with hn | hn + · subst hn + simp + · exact (abs_normalized_fin_sum_le hn a S ha).trans (le_abs_self b) + +/-- +For a uniformly bounded class, empirical Rademacher complexity is unchanged by restricting to a +sequence that approximates the class pointwise. +-/ +theorem empiricalRademacherComplexity_eq_comp_of_tendsto [Nonempty H] + (F : H → 𝒳 → ℝ) (g : ℕ → H) + (hg : ∀ h, ∃ u : ℕ → ℕ, ∀ x, Tendsto (fun m ↦ F (g (u m)) x) atTop (𝓝 (F h x))) + {b : ℝ} (hF : ∀ h x, |F h x| ≤ b) (S : Fin n → 𝒳) : + empiricalRademacherComplexity n F S = empiricalRademacherComplexity n (F ∘ g) S := by + dsimp only [empiricalRademacherComplexity] + congr 1 + refine Finset.sum_congr rfl fun σ _ ↦ ?_ + refine ciSup_eq_ciSup_comp_of_tendsto + (Φ := fun h ↦ |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F h (S k)|) g ?_ ?_ + · refine ⟨|b|, ?_⟩ + rintro _ ⟨h, rfl⟩ + exact abs_sampleAverage_le (fun k x ↦ (σ k : ℝ) * F h x) S + (fun k x ↦ by simpa [abs_mul, abs_sigma] using hF h x) + · intro h + obtain ⟨u, hu⟩ := hg h + refine ⟨u, (continuous_abs.tendsto _).comp ?_⟩ + exact ((tendsto_finsetSum _ fun k _ ↦ (hu (S k)).const_mul _).const_mul _) + +/-- +For a uniformly bounded class, Rademacher complexity is unchanged by restricting to a sequence +that approximates the class pointwise. +-/ +theorem rademacherComplexity_eq_comp_of_tendsto [Nonempty H] + (F : H → 𝒳 → ℝ) (g : ℕ → H) + (hg : ∀ h, ∃ u : ℕ → ℕ, ∀ x, Tendsto (fun m ↦ F (g (u m)) x) atTop (𝓝 (F h x))) + {b : ℝ} (hF : ∀ h x, |F h x| ≤ b) (μ : Measure Ω) (X : Ω → 𝒳) : + rademacherComplexity n F μ X = rademacherComplexity n (F ∘ g) μ X := by + dsimp only [rademacherComplexity] + congr 1 + funext ω + exact empiricalRademacherComplexity_eq_comp_of_tendsto F g hg hF (X ∘ ω) + +/-- +For a uniformly bounded measurable class, uniform deviation is unchanged by restricting to a +sequence that approximates the class pointwise. The population term converges by dominated +convergence along the approximating sequence. +-/ +theorem uniformDeviation_eq_comp_of_tendsto [Nonempty H] + (F : H → 𝒳 → ℝ) (g : ℕ → H) + (hg : ∀ h, ∃ u : ℕ → ℕ, ∀ x, Tendsto (fun m ↦ F (g (u m)) x) atTop (𝓝 (F h x))) + {b : ℝ} (hF : ∀ h x, |F h x| ≤ b) + (μ : Measure Ω) [IsFiniteMeasure μ] (X : Ω → 𝒳) + (hF_meas : ∀ h, Measurable (F h ∘ X)) (S : Fin n → 𝒳) : + uniformDeviation n F μ X S = uniformDeviation n (F ∘ g) μ X S := by + dsimp only [uniformDeviation] + refine ciSup_eq_ciSup_comp_of_tendsto + (Φ := fun h ↦ |(n : ℝ)⁻¹ * ∑ k : Fin n, F h (S k) - μ[fun ω ↦ F h (X ω)]|) g ?_ ?_ + · refine ⟨|b| + b * μ.real univ, ?_⟩ + rintro _ ⟨h, rfl⟩ + have hint : |μ[fun ω ↦ F h (X ω)]| ≤ b * μ.real univ := by + simpa [Real.norm_eq_abs] using + norm_integral_le_of_norm_le_const (μ := μ) (f := fun ω ↦ F h (X ω)) + (Filter.Eventually.of_forall fun ω ↦ by simpa [Real.norm_eq_abs] using hF h (X ω)) + exact (abs_sub _ _).trans + (add_le_add (abs_sampleAverage_le (fun _ x ↦ F h x) S (fun _ x ↦ hF h x)) hint) + · intro h + obtain ⟨u, hu⟩ := hg h + refine ⟨u, (continuous_abs.tendsto _).comp ?_⟩ + refine Tendsto.sub + ((tendsto_finsetSum _ fun k _ ↦ hu (S k)).const_mul _) ?_ + exact tendsto_integral_of_dominated_convergence (fun _ ↦ b) + (fun m ↦ (hF_meas (g (u m))).aestronglyMeasurable) (integrable_const b) + (fun m ↦ Filter.Eventually.of_forall fun ω ↦ by + simpa [Real.norm_eq_abs] using hF (g (u m)) (X ω)) + (Filter.Eventually.of_forall fun ω ↦ hu (X ω)) + +end Reduction + +namespace PointwiseSeparable + +/-- +A class indexed by a separable Fréchet–Urysohn space and continuous in the parameter at every +input is pointwise separable, along a dense sequence. First-countable spaces, in particular +metric spaces, are Fréchet–Urysohn. +-/ +theorem of_continuous [TopologicalSpace H] [TopologicalSpace.SeparableSpace H] + [FrechetUrysohnSpace H] [Nonempty H] + {F : H → 𝒳 → ℝ} (hF : ∀ x, Continuous fun h ↦ F h x) : + PointwiseSeparable F := by + refine ⟨TopologicalSpace.denseSeq H, fun h ↦ ?_⟩ + have hmem : h ∈ closure (range (TopologicalSpace.denseSeq H)) := by + rw [(TopologicalSpace.denseRange_denseSeq H).closure_eq] + exact mem_univ h + obtain ⟨a, ha, hlim⟩ := mem_closure_iff_seq_limit.mp hmem + choose u hu using ha + refine ⟨u, fun x ↦ ?_⟩ + simp only [hu] + exact ((hF x).tendsto h).comp hlim + +/-- +Pointwise separability is preserved by reading the class at `π z` and post-composing with a map +`ψ z` that is continuous for every `z`. +-/ +theorem comp {𝒵 : Type*} {F : H → 𝒳 → ℝ} (hF : PointwiseSeparable F) + (π : 𝒵 → 𝒳) {ψ : 𝒵 → ℝ → ℝ} (hψ : ∀ z, Continuous (ψ z)) : + PointwiseSeparable fun h z ↦ ψ z (F h (π z)) := by + obtain ⟨g, hg⟩ := hF + refine ⟨g, fun h ↦ ?_⟩ + obtain ⟨u, hu⟩ := hg h + exact ⟨u, fun z ↦ ((hψ z).tendsto _).comp (hu (π z))⟩ + +/-- +A supervised loss class built from a pointwise separable predictor class and a loss continuous +in the prediction is pointwise separable. +-/ +theorem supervisedLossClass {𝒴 : Type*} {F : H → 𝒳 → ℝ} (hF : PointwiseSeparable F) + {loss : ℝ → 𝒴 → ℝ} (hloss : ∀ y, Continuous fun u ↦ loss u y) : + PointwiseSeparable (_root_.supervisedLossClass F loss) := + hF.comp Prod.fst (ψ := fun z u ↦ loss u z.2) fun z ↦ hloss z.2 + +end PointwiseSeparable diff --git a/StatsMLlib/LearningTheory/Rademacher/Reindex.lean b/StatsMLlib/LearningTheory/Rademacher/Reindex.lean index e96babf..91c6883 100644 --- a/StatsMLlib/LearningTheory/Rademacher/Reindex.lean +++ b/StatsMLlib/LearningTheory/Rademacher/Reindex.lean @@ -12,7 +12,8 @@ import StatsMLlib.Order.IndexedSupremum # Reindexing function classes These lemmas distinguish a purely set-theoretic change of hypothesis index -from the topological `denseRestriction` bridge. Pulling a class back along +from the approximating-sequence reduction of +`StatsMLlib.LearningTheory.Rademacher.PointwiseSeparable`. Pulling a class back along an arbitrary map can only decrease empirical complexity; a surjective map does not change the class and hence preserves all three central quantities. -/ diff --git a/StatsMLlib/LearningTheory/UniformDeviation/Bounds.lean b/StatsMLlib/LearningTheory/UniformDeviation/Bounds.lean index 5b21893..cc800d4 100644 --- a/StatsMLlib/LearningTheory/UniformDeviation/Bounds.lean +++ b/StatsMLlib/LearningTheory/UniformDeviation/Bounds.lean @@ -7,7 +7,7 @@ import StatsMLlib.LearningTheory.Rademacher.Complexity import StatsMLlib.LearningTheory.UniformDeviation.Defs import StatsMLlib.Probability.Concentration.McDiarmid import StatsMLlib.LearningTheory.UniformDeviation.BoundedDifference -import StatsMLlib.Topology.SeparableSpace.Supremum +import StatsMLlib.LearningTheory.Rademacher.PointwiseSeparable import StatsMLlib.MeasureTheory.Measure.Real /-! @@ -23,7 +23,8 @@ This module uses `uniformDeviation` and the expected Rademacher complexity of a ## Main results * `uniform_deviation_tail_bound_countable`: tail bound for a countable function class. -* `uniform_deviation_tail_bound_separable`: tail bound for a separable function class. +* `uniform_deviation_tail_bound_pointwiseSeparable`: tail bound for a pointwise separable + function class. -/ section @@ -144,104 +145,6 @@ theorem uniform_deviation_tail_bound_countable_of_pos uniform_deviation_tail_bound_countable (μ := μ) f hf X hX (le_of_lt hb) hf' ht' hε _ = _ := by dsimp only [t]; field_simp -open TopologicalSpace - -lemma empiricalRademacherComplexity_eq - [Nonempty ι] [TopologicalSpace ι] [SeparableSpace ι] - (n : ℕ) {f : ι → (𝒳 → ℝ)} (hf : ∀ x : 𝒳, Continuous fun i ↦ f i x) (S : Fin n → 𝒳) : - empiricalRademacherComplexity n f S = empiricalRademacherComplexity n (f ∘ denseSeq ι) S := by - dsimp [empiricalRademacherComplexity] - congr - ext i - apply separableSpaceSup_eq_real - continuity - -lemma RademacherComplexity_eq - [Nonempty ι] [TopologicalSpace ι] [SeparableSpace ι] - (n : ℕ) (f : ι → (𝒳 → ℝ)) (hf : ∀ x : 𝒳, Continuous fun i ↦ f i x) - (μ : Measure Ω) (X : Ω → 𝒳) : - rademacherComplexity n f μ X = rademacherComplexity n (f ∘ denseSeq ι) μ X := by - dsimp [rademacherComplexity] - congr - ext i - exact empiricalRademacherComplexity_eq n hf (X ∘ i) - -lemma uniformDeviation_eq - [MeasurableSpace 𝒳] - [Nonempty ι] [TopologicalSpace ι] [SeparableSpace ι] [FirstCountableTopology ι] - (n : ℕ) (f : ι → 𝒳 → ℝ) - (hf : ∀ i, Measurable (f i)) - (X : Ω → 𝒳) (hX : Measurable X) - {b : ℝ} (hf' : ∀ i x, |f i x| ≤ b) - (hf'' : ∀ x : 𝒳, Continuous fun i ↦ f i x) - (μ : Measure Ω) [IsFiniteMeasure μ] : - uniformDeviation n f μ X = uniformDeviation n (f ∘ denseSeq ι) μ X := by - ext y - dsimp [uniformDeviation] - apply separableSpaceSup_eq_real - apply Continuous.abs - apply Continuous.sub - · continuity - · have : ∀ (x : ι), ∀ᵐ (a : Ω) ∂μ, ‖f x (X a)‖ ≤ b := by - intro i - filter_upwards with ω - exact hf' i (X ω) - apply MeasureTheory.continuous_of_dominated _ this - · apply MeasureTheory.integrable_const - · filter_upwards with ω - continuity - · intro i - apply Measurable.aestronglyMeasurable - measurability - -/-- (Main Theorem) Separable-class tail bound obtained via reduction to a countable dense -subclass. -/ -theorem uniform_deviation_tail_bound_separable - [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty ι] - [TopologicalSpace ι] [SeparableSpace ι] [FirstCountableTopology ι] - [IsProbabilityMeasure μ] - (f : ι → 𝒳 → ℝ) (hf : ∀ i, Measurable (f i)) - (X : Ω → 𝒳) (hX : Measurable X) - {b : ℝ} (hb : 0 ≤ b) (hf' : ∀ i x, |f i x| ≤ b) - (hf'' : ∀ x : 𝒳, Continuous fun i ↦ f i x) - {t : ℝ} (ht' : t * b ^ 2 ≤ 1 / 2) - {ε : ℝ} (hε : 0 ≤ ε) : - (μⁿ (fun ω ↦ 2 * rademacherComplexity n f μ X + ε ≤ uniformDeviation n f μ X (X ∘ ω))).toReal ≤ - (- ε ^ 2 * t * n).exp := by - let f' := f ∘ denseSeq ι - calc - _ = (μⁿ (fun ω ↦ 2 * rademacherComplexity n f' μ X + ε ≤ - uniformDeviation n f' μ X (X ∘ ω))).toReal := by - congr - ext ω - rw [RademacherComplexity_eq n f hf'' μ X] - rw [uniformDeviation_eq n f hf X hX hf' hf'' μ] - _ ≤ (- ε ^ 2 * t * n).exp := by - apply uniform_deviation_tail_bound_countable f' _ X hX hb _ ht' hε - · intro i - measurability - · exact fun i x ↦ hf' (denseSeq ι i) x - -/-- (Main Theorem) Optimized separable-class tail bound with `t = 1 / (2 * b^2)`. -/ -theorem uniform_deviation_tail_bound_separable_of_pos - [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty ι] - [TopologicalSpace ι] [SeparableSpace ι] [FirstCountableTopology ι] - [IsProbabilityMeasure μ] - (f : ι → 𝒳 → ℝ) (hf : ∀ i, Measurable (f i)) - (X : Ω → 𝒳) (hX : Measurable X) - {b : ℝ} (hb : 0 < b) (hf' : ∀ i x, |f i x| ≤ b) - (hf'' : ∀ x : 𝒳, Continuous fun i ↦ f i x) - {ε : ℝ} (hε : 0 ≤ ε) : - (μⁿ (fun ω ↦ 2 * rademacherComplexity n f μ X + ε ≤ uniformDeviation n f μ X (X ∘ ω))).toReal ≤ - (- ε ^ 2 * n / (2 * b ^ 2)).exp := by - let t := 1 / (2 * b ^ 2) - have ht' : t * b ^ 2 ≤ 1 / 2 := le_of_eq (by dsimp only [t]; field_simp) - calc - _ ≤ (- ε ^ 2 * t * n).exp := - uniform_deviation_tail_bound_separable (μ := μ) f hf X hX (le_of_lt hb) hf' hf'' ht' hε - _ = _ := by dsimp only [t]; field_simp - - private lemma normalized_two_mul_bound_mcdiarmid_scale (hn : 0 < n) {b t : ℝ} (ht : t * b ^ 2 ≤ 1 / 2) : ((n : ℝ) * t / 2) * (n : ℝ) * ((n : ℝ)⁻¹ * 2 * b) ^ 2 ≤ 1 := by @@ -477,147 +380,107 @@ theorem uniform_deviation_tail_bound_countable_of_sample_empirical_le (μ := μ) f hf X hX hb hf' hε --- The separable results below are indexed by a topological hypothesis space `H`, --- while the countable results above use a bare index type `ι`. The two play --- different roles, so both names are kept. +-- The pointwise-separable results below are indexed by a hypothesis space `H`, +-- while the countable results above use a bare index type `ι`. Each result below +-- restricts the class to an approximating sequence and applies a countable result. variable {H : Type v} /-- -Empirical Rademacher complexity is unchanged after restricting a continuous -family to the chosen countable dense sequence. +(Main Theorem) Tail bound for a pointwise separable class, obtained by restricting the class to +an approximating sequence. -/ -lemma empiricalRademacherComplexity_denseRestriction - [Nonempty H] [TopologicalSpace H] [SeparableSpace H] - (n : ℕ) {F : H → 𝒳 → ℝ} - (hF : ∀ x : 𝒳, Continuous fun h ↦ F h x) (S : Fin n → 𝒳) : - empiricalRademacherComplexity n F S = - empiricalRademacherComplexity n (denseRestriction F) S := by - dsimp [empiricalRademacherComplexity] - congr - ext σ - apply separableSpaceSup_eq_real - continuity - -/-- -Expected Rademacher complexity is unchanged after restriction to -`denseRestriction F`. --/ -lemma rademacherComplexity_denseRestriction - [Nonempty H] [TopologicalSpace H] [SeparableSpace H] - (n : ℕ) (F : H → 𝒳 → ℝ) - (hF : ∀ x : 𝒳, Continuous fun h ↦ F h x) - (μ : Measure Ω) (X : Ω → 𝒳) : - rademacherComplexity n F μ X = - rademacherComplexity n (denseRestriction F) μ X := by - dsimp [rademacherComplexity] - congr - ext S - exact empiricalRademacherComplexity_denseRestriction n hF (X ∘ S) +theorem uniform_deviation_tail_bound_pointwiseSeparable + [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] [IsProbabilityMeasure μ] + (F : H → 𝒳 → ℝ) (hF_meas : ∀ h, Measurable (F h)) + (X : Ω → 𝒳) (hX : Measurable X) + {b : ℝ} (hb : 0 ≤ b) (hF_bound : ∀ h x, |F h x| ≤ b) + (hF_ps : PointwiseSeparable F) + {t : ℝ} (ht' : t * b ^ 2 ≤ 1 / 2) + {ε : ℝ} (hε : 0 ≤ ε) : + (μⁿ (fun ω ↦ 2 * rademacherComplexity n F μ X + ε ≤ uniformDeviation n F μ X (X ∘ ω))).toReal ≤ + (- ε ^ 2 * t * n).exp := by + obtain ⟨g, hg⟩ := hF_ps + simp only [rademacherComplexity_eq_comp_of_tendsto F g hg hF_bound μ X, + uniformDeviation_eq_comp_of_tendsto F g hg hF_bound μ X fun h ↦ (hF_meas h).comp hX] + exact uniform_deviation_tail_bound_countable (F ∘ g) (fun i ↦ hF_meas (g i)) X hX hb + (fun i x ↦ hF_bound (g i) x) ht' hε + +/-- (Main Theorem) Optimized pointwise-separable tail bound with `t = 1 / (2 * b^2)`. -/ +theorem uniform_deviation_tail_bound_pointwiseSeparable_of_pos + [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] [IsProbabilityMeasure μ] + (F : H → 𝒳 → ℝ) (hF_meas : ∀ h, Measurable (F h)) + (X : Ω → 𝒳) (hX : Measurable X) + {b : ℝ} (hb : 0 < b) (hF_bound : ∀ h x, |F h x| ≤ b) + (hF_ps : PointwiseSeparable F) + {ε : ℝ} (hε : 0 ≤ ε) : + (μⁿ (fun ω ↦ 2 * rademacherComplexity n F μ X + ε ≤ uniformDeviation n F μ X (X ∘ ω))).toReal ≤ + (- ε ^ 2 * n / (2 * b ^ 2)).exp := by + let t := 1 / (2 * b ^ 2) + have ht' : t * b ^ 2 ≤ 1 / 2 := le_of_eq (by dsimp only [t]; field_simp) + calc + _ ≤ (- ε ^ 2 * t * n).exp := + uniform_deviation_tail_bound_pointwiseSeparable (μ := μ) F hF_meas X hX (le_of_lt hb) + hF_bound hF_ps ht' hε + _ = _ := by dsimp only [t]; field_simp /-- -A uniform fixed-sample bound for a separable class lifts to expected -Rademacher complexity through `denseRestriction`. +A uniform fixed-sample bound for a pointwise separable class lifts to expected Rademacher +complexity. -/ -theorem rademacherComplexity_le_of_empirical_le_separable - [Nonempty H] [TopologicalSpace H] [SeparableSpace H] - [IsProbabilityMeasure μ] +theorem rademacherComplexity_le_of_empirical_le_pointwiseSeparable + [Nonempty H] [IsProbabilityMeasure μ] (F : H → 𝒳 → ℝ) (X : Ω → 𝒳) (hF_meas : ∀ h, Measurable (F h ∘ X)) {b C : ℝ} (hb : 0 ≤ b) (hF_bound : ∀ h x, |F h x| ≤ b) - (hF_cont : ∀ x : 𝒳, Continuous fun h ↦ F h x) + (hF_ps : PointwiseSeparable F) (hC : ∀ S : Fin n → 𝒳, empiricalRademacherComplexity n F S ≤ C) : rademacherComplexity n F μ X ≤ C := by - rw [rademacherComplexity_denseRestriction n F hF_cont μ X] - apply rademacherComplexity_le_of_empirical_le_countable - (f := denseRestriction F) (μ := μ) - · exact fun i ↦ hF_meas (denseSeq H i) + obtain ⟨g, hg⟩ := hF_ps + rw [rademacherComplexity_eq_comp_of_tendsto F g hg hF_bound μ X] + apply rademacherComplexity_le_of_empirical_le_countable (f := F ∘ g) (μ := μ) + · exact fun i ↦ hF_meas (g i) · exact hb - · exact abs_denseRestriction_le hF_bound + · exact fun i x ↦ hF_bound (g i) x · intro S - rw [← empiricalRademacherComplexity_denseRestriction n hF_cont S] + rw [← empiricalRademacherComplexity_eq_comp_of_tendsto F g hg hF_bound S] exact hC S /-- -Uniform deviation is unchanged after restricting a continuous and uniformly -bounded family to `denseRestriction F`. --/ -lemma uniformDeviation_denseRestriction - [MeasurableSpace 𝒳] - [Nonempty H] [TopologicalSpace H] [SeparableSpace H] - [FirstCountableTopology H] - (n : ℕ) (F : H → 𝒳 → ℝ) - (hF_meas : ∀ h, Measurable (F h)) - (X : Ω → 𝒳) (hX : Measurable X) - {b : ℝ} (hF_bound : ∀ h x, |F h x| ≤ b) - (hF_cont : ∀ x : 𝒳, Continuous fun h ↦ F h x) - (μ : Measure Ω) [IsFiniteMeasure μ] : - uniformDeviation n F μ X = - uniformDeviation n (denseRestriction F) μ X := by - ext S - dsimp [uniformDeviation] - apply separableSpaceSup_eq_real - apply Continuous.abs - apply Continuous.sub - · continuity - · have hdominated : - ∀ h : H, ∀ᵐ ω : Ω ∂μ, ‖F h (X ω)‖ ≤ b := by - intro h - filter_upwards with ω - exact hF_bound h (X ω) - apply MeasureTheory.continuous_of_dominated _ hdominated - · exact MeasureTheory.integrable_const _ - · filter_upwards with ω - continuity - · intro h - exact (hF_meas h).comp hX |>.aestronglyMeasurable - -/-- -Expected uniform-deviation bound for a separable class from a deterministic +Expected uniform-deviation bound for a pointwise separable class from a deterministic fixed-sample empirical Rademacher bound. -/ -theorem uniform_deviation_expectation_le_of_empirical_le_separable - [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] - [IsProbabilityMeasure μ] +theorem uniform_deviation_expectation_le_of_empirical_le_pointwiseSeparable + [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] [IsProbabilityMeasure μ] (hn : 0 < n) (F : H → 𝒳 → ℝ) (hF_meas : ∀ h, Measurable (F h)) (X : Ω → 𝒳) (hX : Measurable X) {b C : ℝ} (hb : 0 ≤ b) (hF_bound : ∀ h x, |F h x| ≤ b) - (hF_cont : ∀ x : 𝒳, Continuous fun h ↦ F h x) + (hF_ps : PointwiseSeparable F) (hC : ∀ S : Fin n → 𝒳, empiricalRademacherComplexity n F S ≤ C) : μⁿ[fun S : Fin n → Ω ↦ uniformDeviation n F μ X (X ∘ S)] ≤ 2 * C := by - calc - μⁿ[fun S : Fin n → Ω ↦ uniformDeviation n F μ X (X ∘ S)] = - μⁿ[fun S : Fin n → Ω ↦ - uniformDeviation n (denseRestriction F) μ X (X ∘ S)] := by - apply integral_congr_ae - filter_upwards with S - exact congrFun - (uniformDeviation_denseRestriction - n F hF_meas X hX hF_bound hF_cont μ) (X ∘ S) - _ ≤ 2 * C := by - apply uniform_deviation_expectation_le_of_empirical_le_countable - (f := denseRestriction F) (μ := μ) hn X - · exact fun i ↦ (hF_meas (denseSeq H i)).comp hX - · exact hb - · exact abs_denseRestriction_le hF_bound - · intro S - rw [← empiricalRademacherComplexity_denseRestriction n hF_cont S] - exact hC S + obtain ⟨g, hg⟩ := hF_ps + simp only [uniformDeviation_eq_comp_of_tendsto F g hg hF_bound μ X + fun h ↦ (hF_meas h).comp hX] + apply uniform_deviation_expectation_le_of_empirical_le_countable + (f := F ∘ g) (μ := μ) hn X + · exact fun i ↦ (hF_meas (g i)).comp hX + · exact hb + · exact fun i x ↦ hF_bound (g i) x + · intro S + rw [← empiricalRademacherComplexity_eq_comp_of_tendsto F g hg hF_bound S] + exact hC S /-- -Replace expected Rademacher complexity in the separable-class tail bound by -any deterministic upper bound `C`. +Replace expected Rademacher complexity in the pointwise-separable tail bound by any +deterministic upper bound `C`. -/ -theorem uniform_deviation_tail_bound_separable_of_rademacher_le - [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] - [IsProbabilityMeasure μ] +theorem uniform_deviation_tail_bound_pointwiseSeparable_of_rademacher_le + [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] [IsProbabilityMeasure μ] (F : H → 𝒳 → ℝ) (hF_meas : ∀ h, Measurable (F h)) (X : Ω → 𝒳) (hX : Measurable X) {b C : ℝ} (hb : 0 < b) (hF_bound : ∀ h x, |F h x| ≤ b) - (hF_cont : ∀ x : 𝒳, Continuous fun h ↦ F h x) + (hF_ps : PointwiseSeparable F) (hC : rademacherComplexity n F μ X ≤ C) {ε : ℝ} (hε : 0 ≤ ε) : (μⁿ {S | @@ -631,77 +494,61 @@ theorem uniform_deviation_tail_bound_separable_of_rademacher_le intro S gcongr _ ≤ _ := - uniform_deviation_tail_bound_separable_of_pos - (μ := μ) F hF_meas X hX hb hF_bound hF_cont hε + uniform_deviation_tail_bound_pointwiseSeparable_of_pos + (μ := μ) F hF_meas X hX hb hF_bound hF_ps hε /-- -Separable-class tail bound with a deterministic fixed-sample upper bound on -empirical Rademacher complexity. +Pointwise-separable tail bound with a deterministic fixed-sample upper bound on empirical +Rademacher complexity. -/ -theorem uniform_deviation_tail_bound_separable_of_empirical_le - [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] - [IsProbabilityMeasure μ] +theorem uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_le + [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] [IsProbabilityMeasure μ] (F : H → 𝒳 → ℝ) (hF_meas : ∀ h, Measurable (F h)) (X : Ω → 𝒳) (hX : Measurable X) {b C : ℝ} (hb : 0 < b) (hF_bound : ∀ h x, |F h x| ≤ b) - (hF_cont : ∀ x : 𝒳, Continuous fun h ↦ F h x) + (hF_ps : PointwiseSeparable F) (hC : ∀ S : Fin n → 𝒳, empiricalRademacherComplexity n F S ≤ C) {ε : ℝ} (hε : 0 ≤ ε) : (μⁿ {S | 2 * C + ε ≤ uniformDeviation n F μ X (X ∘ S)}).toReal ≤ (-ε ^ 2 * n / (2 * b ^ 2)).exp := by - apply uniform_deviation_tail_bound_separable_of_rademacher_le - (μ := μ) F hF_meas X hX hb hF_bound hF_cont _ hε - exact rademacherComplexity_le_of_empirical_le_separable - F X (fun h ↦ (hF_meas h).comp hX) hb.le hF_bound hF_cont hC + apply uniform_deviation_tail_bound_pointwiseSeparable_of_rademacher_le + (μ := μ) F hF_meas X hX hb hF_bound hF_ps _ hε + exact rademacherComplexity_le_of_empirical_le_pointwiseSeparable + F X (fun h ↦ (hF_meas h).comp hX) hb.le hF_bound hF_ps hC /-- -Sample-dependent separable-class tail bound retaining the observed empirical -Rademacher complexity in the threshold. +Sample-dependent pointwise-separable tail bound retaining the observed empirical Rademacher +complexity in the threshold. -/ -theorem uniform_deviation_tail_bound_separable_of_empirical_complexity - [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] - [IsProbabilityMeasure μ] +theorem uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_complexity + [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] [IsProbabilityMeasure μ] (F : H → 𝒳 → ℝ) (hF_meas : ∀ h, Measurable (F h)) (X : Ω → 𝒳) (hX : Measurable X) {b : ℝ} (hb : 0 < b) (hF_bound : ∀ h x, |F h x| ≤ b) - (hF_cont : ∀ x : 𝒳, Continuous fun h ↦ F h x) + (hF_ps : PointwiseSeparable F) {ε : ℝ} (hε : 0 ≤ ε) : (μⁿ {S : Fin n → Ω | 2 * empiricalRademacherComplexity n F (X ∘ S) + 3 * ε ≤ uniformDeviation n F μ X (X ∘ S)}).toReal ≤ 2 * (-ε ^ 2 * n / (2 * b ^ 2)).exp := by - calc - _ = (μⁿ {S : Fin n → Ω | - 2 * empiricalRademacherComplexity n (denseRestriction F) (X ∘ S) + - 3 * ε ≤ - uniformDeviation n (denseRestriction F) μ X (X ∘ S)}).toReal := by - congr - ext S - rw [empiricalRademacherComplexity_denseRestriction n hF_cont (X ∘ S)] - rw [uniformDeviation_denseRestriction - n F hF_meas X hX hF_bound hF_cont μ] - _ ≤ _ := - uniform_deviation_tail_bound_countable_of_empirical_complexity - (μ := μ) (denseRestriction F) - (measurable_denseRestriction_apply hF_meas) - X hX hb (abs_denseRestriction_le hF_bound) hε + obtain ⟨g, hg⟩ := hF_ps + simp only [empiricalRademacherComplexity_eq_comp_of_tendsto F g hg hF_bound, + uniformDeviation_eq_comp_of_tendsto F g hg hF_bound μ X fun h ↦ (hF_meas h).comp hX] + exact uniform_deviation_tail_bound_countable_of_empirical_complexity + (μ := μ) (F ∘ g) (fun i ↦ hF_meas (g i)) X hX hb (fun i x ↦ hF_bound (g i) x) hε /-- -Sample-dependent separable-class tail bound with a pointwise upper bound -`C S` on empirical Rademacher complexity. +Sample-dependent pointwise-separable tail bound with a pointwise upper bound `C S` on empirical +Rademacher complexity. -/ -theorem uniform_deviation_tail_bound_separable_of_sample_empirical_le - [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] - [IsProbabilityMeasure μ] +theorem uniform_deviation_tail_bound_pointwiseSeparable_of_sample_empirical_le + [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] [IsProbabilityMeasure μ] (F : H → 𝒳 → ℝ) (hF_meas : ∀ h, Measurable (F h)) (X : Ω → 𝒳) (hX : Measurable X) (C : (Fin n → 𝒳) → ℝ) {b : ℝ} (hb : 0 < b) (hF_bound : ∀ h x, |F h x| ≤ b) - (hF_cont : ∀ x : 𝒳, Continuous fun h ↦ F h x) + (hF_ps : PointwiseSeparable F) (hC : ∀ S : Fin n → 𝒳, empiricalRademacherComplexity n F S ≤ C S) {ε : ℝ} (hε : 0 ≤ ε) : (μⁿ {S : Fin n → Ω | @@ -717,8 +564,8 @@ theorem uniform_deviation_tail_bound_separable_of_sample_empirical_le gcongr exact hC (X ∘ S) _ ≤ _ := - uniform_deviation_tail_bound_separable_of_empirical_complexity - (μ := μ) F hF_meas X hX hb hF_bound hF_cont hε + uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_complexity + (μ := μ) F hF_meas X hX hb hF_bound hF_ps hε /-! ## Examples @@ -742,14 +589,16 @@ $$ $$ Thus this single statement exhibits the three commonly used variants -requested at once: a separable hypothesis class, a high-probability estimate, -and empirical rather than expected Rademacher complexity. +requested at once: an uncountable hypothesis class, a high-probability estimate, +and empirical rather than expected Rademacher complexity. A class continuous in a +separable metric parameter enters through `PointwiseSeparable.of_continuous`. -/ -/-- Basic separable high-probability bound using observed empirical complexity. -/ +/-- Basic high-probability bound for a continuously parametrized class, using observed +empirical complexity. -/ example [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] + [TopologicalSpace H] [TopologicalSpace.SeparableSpace H] [FrechetUrysohnSpace H] [IsProbabilityMeasure μ] (F : H → 𝒳 → ℝ) (hF_meas : ∀ h, Measurable (F h)) (X : Ω → 𝒳) (hX : Measurable X) @@ -760,7 +609,7 @@ example 2 * empiricalRademacherComplexity n F (X ∘ S) + 3 * ε ≤ uniformDeviation n F μ X (X ∘ S)}).toReal ≤ 2 * (-ε ^ 2 * n / (2 * b ^ 2)).exp := by - exact uniform_deviation_tail_bound_separable_of_empirical_complexity - (μ := μ) F hF_meas X hX hb hF_bound hF_cont hε + exact uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_complexity + (μ := μ) F hF_meas X hX hb hF_bound (PointwiseSeparable.of_continuous hF_cont) hε end diff --git a/StatsMLlib/LearningTheory/UniformDeviation/Confidence.lean b/StatsMLlib/LearningTheory/UniformDeviation/Confidence.lean index 327d951..19bddb3 100644 --- a/StatsMLlib/LearningTheory/UniformDeviation/Confidence.lean +++ b/StatsMLlib/LearningTheory/UniformDeviation/Confidence.lean @@ -11,7 +11,7 @@ import StatsMLlib.Probability.Concentration.Confidence This module turns the `ε`-tail bounds of `StatsMLlib.LearningTheory.UniformDeviation.Bounds`, for both countable and -separable classes, into statements with failure probability `0 < δ ≤ 1`. +pointwise separable classes, into statements with failure probability `0 < δ ≤ 1`. -/ section @@ -151,18 +151,17 @@ theorem uniform_deviation_tail_bound_countable_of_sample_empirical_le_delta two_mul_exp_neg_sampleConfidenceRadius_sq hn hb hδ hδ_one /-- -Separable-class confidence bound from an upper bound `C` on expected +Pointwise-separable-class confidence bound from an upper bound `C` on expected Rademacher complexity. -/ -theorem uniform_deviation_tail_bound_separable_of_rademacher_le_delta +theorem uniform_deviation_tail_bound_pointwiseSeparable_of_rademacher_le_delta [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] [IsProbabilityMeasure μ] (hn : 0 < n) (F : H → 𝒳 → ℝ) (hF_meas : ∀ h, Measurable (F h)) (X : Ω → 𝒳) (hX : Measurable X) {b C δ : ℝ} (hb : 0 < b) (hF_bound : ∀ h x, |F h x| ≤ b) - (hF_cont : ∀ x : 𝒳, Continuous fun h ↦ F h x) + (hF_ps : PointwiseSeparable F) (hC : rademacherComplexity n F μ X ≤ C) (hδ : 0 < δ) (hδ_one : δ ≤ 1) : (μⁿ {S : Fin n → Ω | @@ -171,57 +170,55 @@ theorem uniform_deviation_tail_bound_separable_of_rademacher_le_delta calc _ ≤ (-deterministicConfidenceRadius b δ n ^ 2 * n / (2 * b ^ 2)).exp := - uniform_deviation_tail_bound_separable_of_rademacher_le - (μ := μ) F hF_meas X hX hb hF_bound hF_cont hC + uniform_deviation_tail_bound_pointwiseSeparable_of_rademacher_le + (μ := μ) F hF_meas X hX hb hF_bound hF_ps hC (deterministicConfidenceRadius_nonneg hb.le) _ = δ := exp_neg_deterministicConfidenceRadius_sq hn hb hδ hδ_one /-- -Confidence-parameter form of the deterministic-threshold separable-class +Confidence-parameter form of the deterministic-threshold pointwise-separable-class generalization bound. The displayed radius unfolds to `b * √(2 * log (1 / δ) / n)`. -/ -theorem uniform_deviation_tail_bound_separable_of_empirical_le_delta +theorem uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_le_delta [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] [IsProbabilityMeasure μ] (hn : 0 < n) (F : H → 𝒳 → ℝ) (hF_meas : ∀ h, Measurable (F h)) (X : Ω → 𝒳) (hX : Measurable X) {b C δ : ℝ} (hb : 0 < b) (hF_bound : ∀ h x, |F h x| ≤ b) - (hF_cont : ∀ x : 𝒳, Continuous fun h ↦ F h x) + (hF_ps : PointwiseSeparable F) (hC : ∀ S : Fin n → 𝒳, empiricalRademacherComplexity n F S ≤ C) (hδ : 0 < δ) (hδ_one : δ ≤ 1) : (μⁿ {S : Fin n → Ω | 2 * C + b * Real.sqrt (2 * Real.log (1 / δ) / n) ≤ uniformDeviation n F μ X (X ∘ S)}).toReal ≤ δ := by simpa [deterministicConfidenceRadius, confidenceRadius] using - uniform_deviation_tail_bound_separable_of_rademacher_le_delta - (μ := μ) hn F hF_meas X hX hb hF_bound hF_cont - (rademacherComplexity_le_of_empirical_le_separable - F X (fun h ↦ (hF_meas h).comp hX) hb.le hF_bound hF_cont hC) + uniform_deviation_tail_bound_pointwiseSeparable_of_rademacher_le_delta + (μ := μ) hn F hF_meas X hX hb hF_bound hF_ps + (rademacherComplexity_le_of_empirical_le_pointwiseSeparable + F X (fun h ↦ (hF_meas h).comp hX) hb.le hF_bound hF_ps hC) hδ hδ_one /-- -Confidence-parameter form of the sample-dependent separable-class +Confidence-parameter form of the sample-dependent pointwise-separable-class generalization bound. The concentration radius unfolds to `b * √(2 * log (2 / δ) / n)` because the proof uses a union bound. -/ -theorem uniform_deviation_tail_bound_separable_of_sample_empirical_le_delta +theorem uniform_deviation_tail_bound_pointwiseSeparable_of_sample_empirical_le_delta [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] [IsProbabilityMeasure μ] (hn : 0 < n) (F : H → 𝒳 → ℝ) (hF_meas : ∀ h, Measurable (F h)) (X : Ω → 𝒳) (hX : Measurable X) (C : (Fin n → 𝒳) → ℝ) {b δ : ℝ} (hb : 0 < b) (hF_bound : ∀ h x, |F h x| ≤ b) - (hF_cont : ∀ x : 𝒳, Continuous fun h ↦ F h x) + (hF_ps : PointwiseSeparable F) (hC : ∀ S : Fin n → 𝒳, empiricalRademacherComplexity n F S ≤ C S) (hδ : 0 < δ) (hδ_one : δ ≤ 1) : (μⁿ {S : Fin n → Ω | @@ -229,8 +226,8 @@ theorem uniform_deviation_tail_bound_separable_of_sample_empirical_le_delta 3 * (b * Real.sqrt (2 * Real.log (2 / δ) / n)) ≤ uniformDeviation n F μ X (X ∘ S)}).toReal ≤ δ := by have htail := - uniform_deviation_tail_bound_separable_of_sample_empirical_le - (μ := μ) F hF_meas X hX C hb hF_bound hF_cont hC + uniform_deviation_tail_bound_pointwiseSeparable_of_sample_empirical_le + (μ := μ) F hF_meas X hX C hb hF_bound hF_ps hC (sampleConfidenceRadius_nonneg (n := n) (δ := δ) hb.le) calc _ = (μⁿ {S : Fin n → Ω | @@ -251,7 +248,7 @@ double as acceptance tests that these statements stay usable as written. example [MeasurableSpace 𝒳] [Nonempty 𝒳] [Nonempty H] - [TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] + [TopologicalSpace H] [SeparableSpace H] [FrechetUrysohnSpace H] [IsProbabilityMeasure μ] (F : H → 𝒳 → ℝ) (hF_meas : ∀ h, Measurable (F h)) (X : Ω → 𝒳) (hX : Measurable X) @@ -263,7 +260,7 @@ example (μⁿ {S : Fin n → Ω | 2 * C + b * Real.sqrt (2 * Real.log (1 / δ) / n) ≤ uniformDeviation n F μ X (X ∘ S)}).toReal ≤ δ := by - exact uniform_deviation_tail_bound_separable_of_empirical_le_delta - (μ := μ) hn F hF_meas X hX hb hF_bound hF_cont hC hδ hδ_one + exact uniform_deviation_tail_bound_pointwiseSeparable_of_empirical_le_delta + (μ := μ) hn F hF_meas X hX hb hF_bound (PointwiseSeparable.of_continuous hF_cont) hC hδ hδ_one end diff --git a/StatsMLlib/Topology/SeparableSpace/Supremum.lean b/StatsMLlib/Topology/SeparableSpace/Supremum.lean index 0900b43..23b3a37 100644 --- a/StatsMLlib/Topology/SeparableSpace/Supremum.lean +++ b/StatsMLlib/Topology/SeparableSpace/Supremum.lean @@ -8,7 +8,6 @@ import Mathlib.Order.ConditionallyCompleteLattice.Indexed import Mathlib.Topology.Order.Lattice import Mathlib.Basic.Real.Basic import Mathlib.Topology.Algebra.Ring.Real -import Mathlib.MeasureTheory.MeasurableSpace.Basic universe u v w @@ -115,30 +114,6 @@ noncomputable abbrev denseRestriction (F : H → α) : ℕ → α := F ∘ denseSeq H -@[simp] -lemma denseRestriction_apply - {H : Type u} {α : Type w} - [TopologicalSpace H] [SeparableSpace H] [Nonempty H] - (F : H → α) (i : ℕ) : - denseRestriction F i = F (denseSeq H i) := - rfl - -lemma measurable_denseRestriction_apply - {H : Type u} {α : Type w} {β : Type*} - [TopologicalSpace H] [SeparableSpace H] [Nonempty H] - [MeasurableSpace α] [MeasurableSpace β] - {F : H → α → β} (hF : ∀ h, Measurable (F h)) (i : ℕ) : - Measurable (denseRestriction F i) := - hF (denseSeq H i) - -lemma abs_denseRestriction_le - {H : Type u} {α : Type w} - [TopologicalSpace H] [SeparableSpace H] [Nonempty H] - {F : H → α → ℝ} {b : ℝ} - (hF : ∀ h x, |F h x| ≤ b) : - ∀ i x, |denseRestriction F i x| ≤ b := - fun i x ↦ hF (denseSeq H i) x - /-- Canonical form of `separableSpaceSup_eq_real`: the supremum of a continuous family over a separable space is the supremum of its restriction to the chosen countable dense sequence. -/