[tukamilano]

Closes #77.

Uncountable-class uniform-deviation and ERM theorems assumed
[TopologicalSpace H] [SeparableSpace H] [FirstCountableTopology H] plus
∀ x, Continuous fun h ↦ F h x, only to reduce ⨆ h to a supremum over denseSeq H.
They now take one topology-free hypothesis:

def PointwiseSeparable (F : H → 𝒳 → ℝ) : Prop :=
  ∃ g : ℕ → H, ∀ h, ∃ u : ℕ → ℕ, ∀ x,
    Tendsto (fun m ↦ F (g (u m)) x) atTop (𝓝 (F h x))

Changes

• New LearningTheory/Rademacher/PointwiseSeparable.lean
  • the definition;
  • empiricalRademacherComplexity_eq_comp_of_tendsto,
    rademacherComplexity_eq_comp_of_tendsto and uniformDeviation_eq_comp_of_tendsto, which
    reduce each quantity to F ∘ g. The population term uses dominated convergence along a
    sequence, so H needs no topology;
  • the bridge PointwiseSeparable.of_continuous, for [SeparableSpace H] [FrechetUrysohnSpace H] plus continuity. FirstCountable implies Fréchet–Urysohn by instance;
  • PointwiseSeparable.comp and PointwiseSeparable.supervisedLossClass, stability under a
    continuous loss.
• Renamed and re-proved. Every *_separable* theorem in UniformDeviation/Bounds,
  UniformDeviation/Confidence, Rademacher/Dudley and
  EmpiricalRiskMinimization/Generalization is now *_pointwiseSeparable*. Each takes
  hF_ps : PointwiseSeparable F in place of the three instances and hF_cont, and is proved by
  applying the existing countable theorem to F ∘ g.
  supervised_approxERM_excessRisk_tail_bound_of_empirical_complexity now takes
  PointwiseSeparable F and continuity of the loss.
• Deleted. The topological theorems, the *_eq / *_denseRestriction reduction lemmas in
  Bounds.lean, and denseRestriction_apply, measurable_denseRestriction_apply and
  abs_denseRestriction_le in Topology/SeparableSpace/Supremum.lean, which became unused.
  denseRestriction and the separableSpace* lemmas stay, because Probability/Process/Dudley
  and the Gaussian comparison files use them.
• Migrated. LinearPredictor/L1, LinearPredictor/L2, LipschitzParameter and both
  KernelPredictor modules keep their concrete hypotheses and go through
  PointwiseSeparable.of_continuous. The RKHS ERM parameter space now needs
  [FrechetUrysohnSpace G] instead of [FirstCountableTopology G].
• New example, FunctionClass/Threshold.lean. Threshold classifiers x ↦ 1[x ≤ t] are
  discontinuous in t, so the old route could not handle them. They are pointwise separable
  (rationals decreasing to t), which gives a confidence bound on the Kolmogorov–Smirnov
  distance from a fixed-sample Rademacher bound.
• README endpoints, FILE_TREE.md and docstrings updated.

Breaking change

The *_separable* names are gone. A caller with a continuously parametrized class replaces
hF_cont by PointwiseSeparable.of_continuous hF_cont and uses the *_pointwiseSeparable*
name.

Verification

• LEAN_NUM_THREADS=$(sysctl -n hw.ncpu) lake build: 9070 jobs, no errors, warnings or infos.
• #print axioms on the main new theorems gives only propext, Classical.choice,
  Quot.sound.
• No sorry, admit or native_decide.

🤖 Generated with Claude Code