Replace separable class hypotheses with PointwiseSeparable

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

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`

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,24 +73,23 @@ 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:
 
 `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,25 +159,24 @@ 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
 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
 
 /-!

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

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