Stochastic gradient descent

LeanMachineLearning.lean

@@ -1,5 +1,10 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
+public import LeanMachineLearning.ForMathlib.Analysis.Calculus.Deriv.Slope
+public import LeanMachineLearning.ForMathlib.Analysis.InnerProductSpace.NormPow
+public import LeanMachineLearning.ForMathlib.Analysis.InnerProductSpace.Projection
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Function.L2Space
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Measurable
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Order.Lattice
@@ -29,6 +34,9 @@ public import LeanMachineLearning.Online.Bandit.BayesRegret
 public import LeanMachineLearning.Online.Bandit.Regret
 public import LeanMachineLearning.Online.Bandit.RewardByCountMeasure
 public import LeanMachineLearning.Online.Bandit.SumRewards
+public import LeanMachineLearning.Online.OnlineRegret
+public import LeanMachineLearning.Online.OnlineToBatch
+public import LeanMachineLearning.Optimization.Algorithms.GradientDescent
 public import LeanMachineLearning.SequentialLearning.Algorithm
 public import LeanMachineLearning.SequentialLearning.AlgorithmDensity
 public import LeanMachineLearning.SequentialLearning.AlgorithmDensityBayes

LeanMachineLearning/ForMathlib/Analysis/Calculus/Deriv/Slope.lean

@@ -0,0 +1,150 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.Analysis.Calculus.Gradient.Basic
+
+import Mathlib.Analysis.Calculus.Deriv.Comp
+import Mathlib.Analysis.Calculus.Deriv.Mul
+import Mathlib.Analysis.Calculus.Deriv.Slope
+import Mathlib.Analysis.Calculus.LocalExtr.Basic
+
+/-!
+# Convexity lemmas about derivatives and gradients
+
+-/
+
+@[expose] public section
+
+open Finset Filter
+open scoped Gradient RealInnerProductSpace Topology
+
+namespace ConvexOn
+
+variable {E : Type*} [NormedAddCommGroup E] {f : E → ℝ} {x y : E} {s : Set E}
+
+lemma fderiv_sub_le_sub [NormedSpace ℝ E] (hf : ConvexOn ℝ s f)
+    (hfx : DifferentiableAt ℝ f x) (y : E) (hx : x ∈ s) (hy : y ∈ s) :
+    fderiv ℝ f x (y - x) ≤ f y - f x := by
+  have h_convex t (ht : t ∈ Set.Ioo (0 : ℝ) 1) :
+      f (x + t • (y - x)) ≤ t * f y + (1 - t) * f x := by
+    have h1 : x + t • (y - x) = (1 - t) • x + t • y := by module
+    have h2 : f ((1 - t) • x + t • y) ≤ (1 - t) • f x + t • f y :=
+      hf.2 hx hy (by grind) (by grind) (by simp)
+    simp only [smul_eq_mul] at h2
+    grind
+  have h_path_deriv : HasDerivAt (fun t : ℝ ↦ f (x + t • (y - x)))
+      (fderiv ℝ f x (y - x)) 0 := by
+    have h1 : HasDerivAt (fun t : ℝ ↦ x + t • (y - x)) (y - x) 0 := by
+      simpa using (hasDerivAt_id (0 : ℝ)).smul_const (y - x)
+    have h2 : HasFDerivAt f (fderiv ℝ f x) (x + (0 : ℝ) • (y - x)) := by
+      simpa using hfx.hasFDerivAt
+    exact h2.comp_hasDerivAt _ h1
+  refine le_of_tendsto h_path_deriv.tendsto_slope_zero_right (Filter.eventually_of_mem
+    (Ioo_mem_nhdsGT_of_mem ⟨le_rfl, zero_lt_one⟩) fun t ht ↦ ?_)
+  simp [inv_mul_le_iff₀ ht.1]
+  grind
+
+lemma add_fderiv_le [NormedSpace ℝ E] (hf : ConvexOn ℝ s f)
+    (hfx : DifferentiableAt ℝ f x) (hx : x ∈ s) (hy : y ∈ s) :
+    f x + fderiv ℝ f x (y - x) ≤ f y := by
+  suffices fderiv ℝ f x (y - x) ≤ f y - f x by grind
+  exact hf.fderiv_sub_le_sub hfx y hx hy
+
+lemma add_inner_gradient_le [InnerProductSpace ℝ E] [CompleteSpace E] (hf : ConvexOn ℝ s f)
+    (hfx : DifferentiableAt ℝ f x) (hx : x ∈ s) (hy : y ∈ s) :
+    f x + ⟪y - x, ∇ f x⟫ ≤ f y := by
+  rw [gradient, real_inner_comm, InnerProductSpace.toDual_symm_apply]
+  exact hf.add_fderiv_le hfx hx hy
+
+lemma le_add_fderiv [NormedSpace ℝ E] (hf : ConvexOn ℝ s f)
+    (hfx : DifferentiableAt ℝ f x) (hx : x ∈ s) (hy : y ∈ s) :
+    f x ≤ f y + fderiv ℝ f x (x - y) := by
+  have h_add_le := hf.add_fderiv_le hfx hx hy
+  grind
+
+lemma le_add_inner_gradient [InnerProductSpace ℝ E] [CompleteSpace E] (hf : ConvexOn ℝ s f)
+    (hfx : DifferentiableAt ℝ f x) (hx : x ∈ s) (hy : y ∈ s) :
+    f x ≤ f y + ⟪x - y, ∇ f x⟫ := by
+  rw [gradient, real_inner_comm, InnerProductSpace.toDual_symm_apply]
+  exact le_add_fderiv hf hfx hx hy
+
+lemma sub_le_fderiv [NormedSpace ℝ E] (hf : ConvexOn ℝ s f)
+    (hfx : DifferentiableAt ℝ f x) (hx : x ∈ s) (hy : y ∈ s) :
+    f x - f y ≤ fderiv ℝ f x (x - y) := by
+  have h_le := hf.le_add_fderiv hfx hx hy
+  grind
+
+lemma sub_le_inner_gradient [InnerProductSpace ℝ E] [CompleteSpace E] (hf : ConvexOn ℝ s f)
+    (hfx : DifferentiableAt ℝ f x) (hx : x ∈ s) (hy : y ∈ s) :
+    f x - f y ≤ ⟪x - y, ∇ f x⟫ := by
+  rw [gradient, real_inner_comm, InnerProductSpace.toDual_symm_apply]
+  exact sub_le_fderiv hf hfx hx hy
+
+lemma isMinOn_of_fderiv_nonneg [NormedSpace ℝ E] (hf : ConvexOn ℝ s f)
+    (hfx : DifferentiableAt ℝ f x) (hx : x ∈ s) (h_nonneg : ∀ y ∈ s, 0 ≤ fderiv ℝ f x (y - x)) :
+    IsMinOn f s x := by
+  intro y hy
+  have h_le := hf.le_add_fderiv hfx hx hy
+  specialize h_nonneg y hy
+  grind
+
+lemma isMinOn_of_inner_gradient_nonneg [InnerProductSpace ℝ E] [CompleteSpace E]
+    (hf : ConvexOn ℝ s f) (hfx : DifferentiableAt ℝ f x) (hx : x ∈ s)
+    (h_nonneg : ∀ y ∈ s, 0 ≤ ⟪y - x, ∇ f x⟫) :
+    IsMinOn f s x := by
+  refine isMinOn_of_fderiv_nonneg hf hfx hx fun y hy ↦ ?_
+  convert h_nonneg y hy
+  rw [gradient, ← InnerProductSpace.toDual_symm_apply, real_inner_comm]
+
+lemma fderiv_nonneg_of_isMinOn [NormedSpace ℝ E] (hs : Convex ℝ s)
+    (hfx : DifferentiableAt ℝ f x) (hx : x ∈ s) (h_min : IsMinOn f s x) {y : E} (hy : y ∈ s) :
+    0 ≤ fderiv ℝ f x (y - x) := by
+  refine IsLocalMinOn.hasFDerivWithinAt_nonneg h_min.localize (y := y - x)
+    hfx.hasFDerivAt.hasFDerivWithinAt ?_
+  refine sub_mem_posTangentConeAt_of_openSegment_subset ?_
+  exact StarConvex.openSegment_subset (hs hx) hy
+
+lemma inner_gradient_nonneg_of_isMinOn [InnerProductSpace ℝ E] [CompleteSpace E] (hs : Convex ℝ s)
+    (hfx : DifferentiableAt ℝ f x) (hx : x ∈ s) (h_min : IsMinOn f s x) {y : E} (hy : y ∈ s) :
+    0 ≤ ⟪y - x, ∇ f x⟫ := by
+  rw [gradient, real_inner_comm, InnerProductSpace.toDual_symm_apply]
+  exact fderiv_nonneg_of_isMinOn hs hfx hx h_min hy
+
+lemma isMinOn_iff_fderiv_nonneg [NormedSpace ℝ E] (hs : Convex ℝ s)
+    (hf : ConvexOn ℝ s f) (hfx : DifferentiableAt ℝ f x) (hx : x ∈ s) :
+    IsMinOn f s x ↔ ∀ y ∈ s, 0 ≤ fderiv ℝ f x (y - x) :=
+  ⟨fderiv_nonneg_of_isMinOn hs hfx hx, hf.isMinOn_of_fderiv_nonneg hfx hx⟩
+
+lemma isMinOn_iff_inner_gradient_nonneg [InnerProductSpace ℝ E] [CompleteSpace E] (hs : Convex ℝ s)
+    (hf : ConvexOn ℝ s f) (hfx : DifferentiableAt ℝ f x) (hx : x ∈ s) :
+    IsMinOn f s x ↔ ∀ y ∈ s, 0 ≤ ⟪y - x, ∇ f x⟫ :=
+  ⟨inner_gradient_nonneg_of_isMinOn hs hfx hx, hf.isMinOn_of_inner_gradient_nonneg hfx hx⟩
+
+lemma apply_avg_sub_le_avg_sub [NormedSpace ℝ E] (hf : ConvexOn ℝ s f)
+    {x : ℕ → E} (hx : ∀ i, x i ∈ s) (y : E) (n : ℕ) (hn : n ≠ 0) :
+    f ((n : ℝ)⁻¹ • ∑ i ∈ range n, x i) - f y ≤ (n : ℝ)⁻¹ • ∑ i ∈ range n, (f (x i) - f y) := by
+  calc f ((n : ℝ)⁻¹ • ∑ i ∈ range n, x i) - f y
+  _ ≤ (n : ℝ)⁻¹ • ∑ i ∈ range n, f (x i) - f y := by
+    simp_rw [smul_sum]
+    grw [hf.map_sum_le (fun _ _ ↦ by positivity) (by simp; field) (fun i _ ↦ hx i)]
+  _ = (n : ℝ)⁻¹ * ∑ i ∈ range n, (f (x i) - f y) := by
+    simp_rw [smul_eq_mul, mul_sum, mul_sub, sum_sub_distrib]
+    rw [← sum_mul]
+    simp
+    field
+
+lemma apply_avg_sub_le_avg_inner [InnerProductSpace ℝ E] [CompleteSpace E]
+    (hf : ConvexOn ℝ s f) (hdf : Differentiable ℝ f) {x : ℕ → E} (hx : ∀ i, x i ∈ s)
+    (hy : y ∈ s) (n : ℕ) (hn : n ≠ 0) :
+    f ((n : ℝ)⁻¹ • ∑ i ∈ range n, x i) - f y ≤ (n : ℝ)⁻¹ * ∑ i ∈ range n, ⟪x i - y, ∇ f (x i)⟫ := by
+  calc f ((n : ℝ)⁻¹ • ∑ i ∈ range n, x i) - f y
+  _ ≤ (n : ℝ)⁻¹ * ∑ i ∈ range n, (f (x i) - f y) := apply_avg_sub_le_avg_sub hf hx y n hn
+  _ ≤ (n : ℝ)⁻¹ * ∑ i ∈ range n, ⟪x i - y, ∇ f (x i)⟫ := by
+    gcongr
+    exact hf.sub_le_inner_gradient hdf.differentiableAt (hx i) hy
+
+end ConvexOn

LeanMachineLearning/ForMathlib/Analysis/InnerProductSpace/NormPow.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.Analysis.Calculus.Gradient.Basic
+
+import LeanMachineLearning.ForMathlib.Analysis.Calculus.Deriv.Slope
+import Mathlib.Analysis.InnerProductSpace.NormPow
+
+/-!
+# Differentiability of the norm to a power
+
+-/
+
+@[expose] public section
+
+open scoped Gradient
+
+variable {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+  [NormedAddCommGroup F] [NormedSpace ℝ F]
+
+lemma Differentiable.norm_pow {f : F → E} (hf : Differentiable ℝ f) {p : ℕ} (hp : 1 < p) :
+    Differentiable ℝ (fun x ↦ ‖f x‖ ^ p) := by
+  suffices Differentiable ℝ (fun x ↦ ‖f x‖ ^ (p : ℝ)) by
+    convert this using 1
+    simp
+  exact hf.norm_rpow (by simp [hp])
+
+lemma gradient_norm_sub_sq [CompleteSpace E] (x y : E) :
+    ∇ (fun z ↦ ‖z - x‖ ^ 2) y = 2 • (y - x) := by
+  have h := ((hasFDerivAt_id y).sub_const x).norm_sq.hasGradientAt.gradient
+  simp only [id_eq, map_sub, ContinuousLinearMap.comp_id, map_nsmul] at h
+  rw [h]
+  congr
+  · exact (InnerProductSpace.toDual ℝ E).symm_apply_apply _
+  · exact (InnerProductSpace.toDual ℝ E).symm_apply_apply _
+
+lemma gradient_dist_sq [CompleteSpace E] (x y : E) : ∇ (fun z ↦ dist x z ^ 2) y = 2 • (y - x) := by
+  simp only [dist_eq_norm, norm_sub_rev x]
+  exact gradient_norm_sub_sq x y

LeanMachineLearning/ForMathlib/Analysis/InnerProductSpace/Projection.lean

@@ -0,0 +1,170 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import LeanMachineLearning.ForMathlib.Analysis.InnerProductSpace.NormPow
+public import Mathlib.Analysis.Calculus.Gradient.Basic
+public import Mathlib.Analysis.InnerProductSpace.NormPow
+
+import LeanMachineLearning.ForMathlib.Analysis.Calculus.Deriv.Slope
+
+/-!
+# Projection on a nonempty closed convex set in an inner product space
+
+-/
+
+@[expose] public section
+
+open Real Finset Metric
+open scoped RealInnerProductSpace Gradient
+
+namespace Learning
+
+section Definition
+
+variable {E : Type*} [PseudoMetricSpace E] {s : Set E}
+
+open Classical in
+/-- Projection on a set: closest point to `x` in the set `s`, taking an arbitrary value if there is
+no such point. -/
+noncomputable
+def proj [Zero E] (s : Set E) (x : E) : E :=
+  if h : ∃ y ∈ s, IsMinOn (dist x) s y then h.choose else 0
+
+/-- If the set is closed and nonempty, then the projection exists. -/
+lemma _root_.IsClosed.exists_isMinOn_dist [ProperSpace E]
+    (h_closed : IsClosed s) (h_nonempty : s.Nonempty) (x : E) :
+    ∃ y ∈ s, IsMinOn (dist x) s y := by
+  have h_cont : Continuous (dist x) := by fun_prop
+  obtain ⟨z, hz⟩ := h_nonempty
+  have h_compact : IsCompact (closedBall x (dist x z) ∩ s) :=
+    IsCompact.inter_right (isCompact_closedBall _ _) h_closed
+  have h3 : (closedBall x (dist x z) ∩ s).Nonempty := ⟨z, ⟨by simp [dist_comm], hz⟩⟩
+  obtain ⟨y, hy, hy_min⟩ := h_compact.exists_isMinOn h3 h_cont.continuousOn
+  refine ⟨y, hy.2, ?_⟩
+  intro u hu
+  simp only [Set.mem_ofPred_eq]
+  by_cases h1 : u ∈ closedBall x (dist x z)
+  · specialize hy_min ⟨h1, hu⟩
+    grind
+  · simp only [mem_closedBall, not_le, Set.mem_inter_iff] at h1 hy
+    grind [dist_comm]
+
+/-- If the set is closed and nonempty, then the projection belongs to the set. -/
+lemma _root_.IsClosed.proj_mem [Zero E] [ProperSpace E]
+    (h_closed : IsClosed s) (h_nonempty : s.Nonempty) (x : E) :
+    proj s x ∈ s := by
+  have h := h_closed.exists_isMinOn_dist h_nonempty x
+  rw [proj, dite_eq_left h]
+  exact h.choose_spec.1
+
+lemma isMinOn_proj_of_exists [Zero E] {x : E} (h : ∃ y ∈ s, IsMinOn (dist x) s y) :
+    IsMinOn (dist x) s (proj s x) := by
+  rw [proj, dite_eq_left h]
+  exact h.choose_spec.2
+
+/-- If the set is closed and nonempty, then the projection is a minimizer of the distance. -/
+lemma _root_.IsClosed.isMinOn_proj [Zero E] [ProperSpace E]
+    (h_closed : IsClosed s) (h_nonempty : s.Nonempty) (x : E) :
+    IsMinOn (dist x) s (proj s x) :=
+  isMinOn_proj_of_exists (h_closed.exists_isMinOn_dist h_nonempty x)
+
+/-- If `x ∈ s`, then the projection of `x` onto `s` is `x`. -/
+@[simp]
+lemma proj_of_mem {E : Type*} [MetricSpace E] [Zero E] {s : Set E} {x : E}
+    (hx : x ∈ s) :
+    proj s x = x := by
+  have h_min : IsMinOn (dist x) s x := fun y hy ↦ by simp
+  have h_min_proj := isMinOn_proj_of_exists ⟨x, hx, h_min⟩ hx
+  symm
+  simpa using h_min_proj
+
+end Definition
+
+lemma _root_.IsClosed.isMinOn_norm_sq_proj {E : Type*} [NormedAddCommGroup E] [ProperSpace E]
+    {s : Set E} (h_closed : IsClosed s) (h_nonempty : s.Nonempty) (x : E) :
+    IsMinOn (fun y ↦ ‖y - x‖ ^ 2) s (proj s x) := by
+  intro y hy
+  simp only [Set.mem_ofPred_eq, sq_le_sq, abs_dist, ← dist_eq_norm, dist_comm _ x]
+  exact h_closed.isMinOn_proj h_nonempty x hy
+
+section Convex
+
+variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
+  {s : Set E}
+
+lemma inner_proj_nonpos (h_closed : IsClosed s) (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty)
+    (x : E) {y : E} (hy : y ∈ s) :
+    ⟪proj s x - x, proj s x - y⟫ ≤ 0 := by
+  suffices 0 ≤ 2 * ⟪proj s x - x, y - proj s x⟫ by
+    simp only [Nat.ofNat_pos, mul_nonneg_iff_of_pos_left] at this
+    rwa [← neg_sub y, inner_neg_right, neg_nonpos]
+  have h_inner := ConvexOn.inner_gradient_nonneg_of_isMinOn h_convex ?_ ?_ ?_ (x := proj s x)
+    (y := y) (f := fun z ↦ ‖z - x‖ ^ 2) hy
+  · rw [real_inner_comm, ← inner_smul_right]
+    convert h_inner using 2
+    symm
+    convert gradient_norm_sub_sq x (proj s x)
+    exact ofNat_smul_eq_nsmul ℝ 2 (proj s x - x)
+  · refine Differentiable.differentiableAt ?_
+    refine Differentiable.norm_pow ?_ (by simp)
+    fun_prop
+  · exact h_closed.proj_mem h_nonempty x
+  · exact h_closed.isMinOn_norm_sq_proj h_nonempty x
+
+lemma inner_proj_nonneg (h_closed : IsClosed s) (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty)
+    (x : E) {y : E} (hy : y ∈ s) :
+    0 ≤ ⟪proj s x - x, y - proj s x⟫ := by
+  rw [← neg_sub _ y, inner_neg_right, neg_nonneg]
+  exact inner_proj_nonpos h_closed h_convex h_nonempty x hy
+
+lemma dist_proj_proj_le (h_closed : IsClosed s) (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty)
+    (x y : E) :
+    dist (proj s x) (proj s y) ≤ dist x y := by
+  suffices dist (proj s x) (proj s y) ^ 2 ≤ dist x y ^ 2 by simpa [sq_le_sq] using this
+  have h_eq : ‖x - y‖ ^ 2 = ‖proj s x - proj s y‖ ^ 2 + ‖x - y + proj s y - proj s x‖ ^ 2 +
+      2 * ⟪proj s x - x, proj s y - proj s x⟫ + 2 * ⟪proj s y - y, proj s x - proj s y⟫ := by
+    calc ‖x - y‖ ^ 2
+    _ = ‖proj s x - proj s y + (x - y + proj s y - proj s x)‖ ^ 2 := by congr; abel
+    _ = ‖proj s x - proj s y‖ ^ 2 + ‖x - y + proj s y - proj s x‖ ^ 2 +
+        2 * ⟪proj s x - proj s y, x - y + proj s y - proj s x⟫ := by
+      rw [norm_add_sq (𝕜 := ℝ)]
+      simp only [RCLike.re_to_real]
+      ring
+    _ = ‖proj s x - proj s y‖ ^ 2 + ‖x - y + proj s y - proj s x‖ ^ 2 +
+        2 * ⟪proj s x - x, proj s y - proj s x⟫ + 2 * ⟪proj s y - y, proj s x - proj s y⟫ := by
+      simp_rw [add_assoc]
+      congr
+      rw [← mul_add, ← neg_sub _ (proj s y), inner_neg_right, add_comm (- _), ← sub_eq_add_neg,
+        ← inner_sub_left, real_inner_comm]
+      congr 2
+      abel
+  simp_rw [dist_eq_norm, h_eq, add_assoc]
+  refine le_add_of_nonneg_right ?_
+  have h1 : 0 ≤ ⟪proj s x - x, proj s y - proj s x⟫ :=
+    inner_proj_nonneg h_closed h_convex h_nonempty x (h_closed.proj_mem h_nonempty y)
+  have h2 : 0 ≤ ⟪proj s y - y, proj s x - proj s y⟫ :=
+    inner_proj_nonneg h_closed h_convex h_nonempty y (h_closed.proj_mem h_nonempty x)
+  positivity
+
+lemma dist_proj_le (h_closed : IsClosed s) (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty)
+    (x : E) {y : E} (hy : y ∈ s) :
+    dist (proj s x) y ≤ dist x y := by
+  nth_rw 1 [← proj_of_mem hy]
+  exact dist_proj_proj_le h_closed h_convex h_nonempty x y
+
+lemma lipschitzWith_proj (h_closed : IsClosed s) (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty) :
+    LipschitzWith 1 (proj s) := by
+  intro x y
+  simp only [ENNReal.coe_one, one_mul, edist_dist]
+  grw [dist_proj_proj_le h_closed h_convex h_nonempty x y]
+
+lemma continuous_proj (h_closed : IsClosed s) (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty) :
+  Continuous (proj s) := (lipschitzWith_proj h_closed h_convex h_nonempty).continuous
+
+end Convex
+
+end Learning