diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean
index 945a88b6..39f1caf7 100644
--- a/LeanMachineLearning.lean
+++ b/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
diff --git a/LeanMachineLearning/ForMathlib/Analysis/Calculus/Deriv/Slope.lean b/LeanMachineLearning/ForMathlib/Analysis/Calculus/Deriv/Slope.lean
new file mode 100644
index 00000000..435ff861
--- /dev/null
+++ b/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
diff --git a/LeanMachineLearning/ForMathlib/Analysis/InnerProductSpace/NormPow.lean b/LeanMachineLearning/ForMathlib/Analysis/InnerProductSpace/NormPow.lean
new file mode 100644
index 00000000..92c7c829
--- /dev/null
+++ b/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
diff --git a/LeanMachineLearning/ForMathlib/Analysis/InnerProductSpace/Projection.lean b/LeanMachineLearning/ForMathlib/Analysis/InnerProductSpace/Projection.lean
new file mode 100644
index 00000000..dc09fc5e
--- /dev/null
+++ b/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
diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Function/ConditionalExpectation/PullOut.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Function/ConditionalExpectation/PullOut.lean
new file mode 100644
index 00000000..4d9a8079
--- /dev/null
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Function/ConditionalExpectation/PullOut.lean
@@ -0,0 +1,32 @@
+/-
+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.MeasureTheory.Function.ConditionalExpectation.PullOut
+
+/-!
+# Integrability of inner products
+-/
+
+@[expose] public section
+
+open scoped ENNReal RealInnerProductSpace
+
+namespace MeasureTheory
+
+variable {Ω E : Type*} {mΩ : MeasurableSpace Ω} {mE : MeasurableSpace E} {P : Measure Ω}
+  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
+
+lemma condExp_inner_of_stronglyMeasurable_left {Ω : Type*} {m mΩ : MeasurableSpace Ω}
+    {μ : Measure Ω} {X g : Ω → E}
+    (hX : StronglyMeasurable[m] X) (hXg : Integrable (fun ω ↦ ⟪X ω, g ω⟫) μ) (hg : Integrable g μ) :
+    μ[fun ω ↦ ⟪X ω, g ω⟫ | m] =ᵐ[μ] fun ω ↦ ⟪X ω, μ[g | m] ω⟫ := by
+  filter_upwards [condExp_bilin_of_stronglyMeasurable_left (innerSL ℝ) hX hXg hg] with ω hω
+  convert hω
+  · rfl
+  · rfl
+
+end MeasureTheory
diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Function/L2Space.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Function/L2Space.lean
new file mode 100644
index 00000000..fec73192
--- /dev/null
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Function/L2Space.lean
@@ -0,0 +1,51 @@
+/-
+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.MeasureTheory.Function.L2Space
+
+/-!
+# Integrability of inner products
+-/
+
+@[expose] public section
+
+open scoped ENNReal RealInnerProductSpace
+
+namespace MeasureTheory
+
+variable {Ω E : Type*} {mΩ : MeasurableSpace Ω} {mE : MeasurableSpace E} {P : Measure Ω}
+
+lemma MemLp.eLpNorm_rpow_norm_lt_top [SeminormedAddCommGroup E]
+    {f : Ω → E} {p : ℝ≥0∞}
+    (hf : MemLp f p P) (hp_zero : p ≠ 0) (hp_top : p ≠ ∞) :
+    eLpNorm (fun x ↦ ‖f x‖ ^ p.toReal) 1 P < ∞ := by
+  simp only [eLpNorm_one_eq_lintegral_enorm, norm_nonneg, ENNReal.toReal_nonneg,
+    Real.enorm_rpow_of_nonneg, enorm_norm]
+  exact (hf.integrable_enorm_rpow hp_zero hp_top).hasFiniteIntegral
+
+lemma MemLp.integrable_inner [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+    {f g : Ω → E}
+    (hf : MemLp f 2 P) (hg : MemLp g 2 P) :
+    Integrable (fun ω ↦ ⟪f ω, g ω⟫) P := by
+  rw [← memLp_one_iff_integrable]
+  constructor
+  · exact hf.aestronglyMeasurable.inner hg.aestronglyMeasurable
+  have h x : ‖⟪f x, g x⟫‖ ≤ ‖‖f x‖ ^ (2 : ℝ) + ‖g x‖ ^ (2 : ℝ)‖ := by
+    norm_cast
+    calc ‖⟪f x, g x⟫‖ ≤ ‖f x‖ * ‖g x‖ := norm_inner_le_norm _ _
+      _ ≤ 2 * ‖f x‖ * ‖g x‖ := by
+        gcongr
+        exact le_mul_of_one_le_left (norm_nonneg _) one_le_two
+      _ ≤ ‖‖f x‖ ^ 2 + ‖g x‖ ^ 2‖ := (two_mul_le_add_sq _ _).trans (le_abs_self _)
+  refine (eLpNorm_mono h).trans_lt ((eLpNorm_add_le ?_ ?_ le_rfl).trans_lt ?_)
+  · exact (hf.norm.aemeasurable.pow_const _).aestronglyMeasurable
+  · exact (hg.norm.aemeasurable.pow_const _).aestronglyMeasurable
+  rw [ENNReal.add_lt_top]
+  exact ⟨hf.eLpNorm_rpow_norm_lt_top (by simp) (by simp),
+    hg.eLpNorm_rpow_norm_lt_top (by simp) (by simp)⟩
+
+end MeasureTheory
diff --git a/LeanMachineLearning/Online/OnlineRegret.lean b/LeanMachineLearning/Online/OnlineRegret.lean
new file mode 100644
index 00000000..4f2f1af8
--- /dev/null
+++ b/LeanMachineLearning/Online/OnlineRegret.lean
@@ -0,0 +1,58 @@
+/-
+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
+
+/-!
+# Online regret
+
+-/
+
+@[expose] public section
+
+open Filter Real Finset
+open scoped Gradient RealInnerProductSpace
+
+namespace Learning
+
+variable {E : Type*} [NormedAddCommGroup E]
+
+section OnlineRegret
+
+/-- The regret of a sequence `x : ℕ → E` compared to a point `y : E` in an online learning task
+with losses `ℓ : ℕ → E → F`. -/
+def onlineRegret {E F : Type*} [AddCommGroup F] (ℓ : ℕ → E → F) (y : E) (x : ℕ → E) (n : ℕ) : F :=
+  ∑ i ∈ range n, (ℓ i (x i) - ℓ i y)
+
+lemma apply_avg_sub_le_onlineRegret [NormedSpace ℝ E] {f : E → ℝ} (hf : ConvexOn ℝ .univ f)
+    (x : ℕ → E) (y : E) (n : ℕ) (hn : n ≠ 0) :
+    f ((n : ℝ)⁻¹ • ∑ i ∈ range n, x i) - f y ≤ (n : ℝ)⁻¹ • onlineRegret (fun _ ↦ f) y x n :=
+  hf.apply_avg_sub_le_avg_sub (by simp) _ n hn
+
+variable [InnerProductSpace ℝ E] [CompleteSpace E]
+
+lemma onlineRegret_le_onlineRegret_inner_gradient {f : ℕ → E → ℝ}
+    (hf : ∀ n, ConvexOn ℝ .univ (f n)) (hdf : ∀ n, Differentiable ℝ (f n))
+    (x : ℕ → E) (y : E) (n : ℕ) :
+    onlineRegret f y x n ≤ onlineRegret (fun n y ↦ ⟪y, ∇ (f n) (x n)⟫) y x n := by
+  simp only [onlineRegret, ← inner_sub_left]
+  gcongr with i hi
+  exact (hf i).sub_le_inner_gradient (hdf i).differentiableAt (by simp) (by simp)
+
+lemma apply_avg_sub_le_onlineRegret_inner_gradient {f : E → ℝ}
+    (hf : ConvexOn ℝ .univ f) (hdf : Differentiable ℝ f)
+    (x : ℕ → E) (y : E) (n : ℕ) (hn : n ≠ 0) :
+    f ((n : ℝ)⁻¹ • ∑ i ∈ range n, x i) - f y ≤
+      (n : ℝ)⁻¹ * (onlineRegret (fun n y ↦ ⟪y, ∇ f (x n)⟫) y x n) := by
+  simpa [onlineRegret, ← inner_sub_left] using
+    hf.apply_avg_sub_le_avg_inner hdf (by simp) (by simp) n hn
+
+end OnlineRegret
+
+end Learning
diff --git a/LeanMachineLearning/Online/OnlineToBatch.lean b/LeanMachineLearning/Online/OnlineToBatch.lean
new file mode 100644
index 00000000..401af470
--- /dev/null
+++ b/LeanMachineLearning/Online/OnlineToBatch.lean
@@ -0,0 +1,123 @@
+/-
+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.SequentialLearning.StationaryEnv
+public import Mathlib.Analysis.Calculus.Gradient.Basic
+
+import LeanMachineLearning.ForMathlib.Analysis.Calculus.Deriv.Slope
+import LeanMachineLearning.ForMathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
+import LeanMachineLearning.ForMathlib.MeasureTheory.Function.L2Space
+
+/-!
+# Online to batch conversion
+
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory Filter Real Finset
+open scoped Gradient ENNReal NNReal RealInnerProductSpace
+
+namespace Learning
+
+variable {Ω E : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P]
+  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [SecondCountableTopology E] [CompleteSpace E]
+  {mE : MeasurableSpace E} [BorelSpace E]
+  {X G : ℕ → Ω → E} {alg : Algorithm E E}
+  {ν : ℕ → Kernel E E} [∀ n, IsMarkovKernel (ν n)]
+  {f : ℕ → E → ℝ}
+
+-- todo: name
+lemma memLp_gradient (h : IsAlgEnvSeq X G alg (obliviousEnv ν) P)
+    (h_unbiased : ∀ n x, (ν n x)[id] = ∇ (f n) x)
+    (h_memLp : ∀ n, MemLp (G n) 2 P) (n : ℕ) :
+    MemLp (fun ω ↦ ∇ (f n) (X n ω)) 2 P := by
+  let M n := MeasurableSpace.comap (X n) inferInstance
+  have h_lp : MemLp P[G n | M n] 2 P := (h_memLp n).condExp (m := M n) (by simp)
+  have h_ae := h.condExp_feedback_obliviousEnv_ae_eq_integral_id n
+      ((h_memLp n).integrable (by simp))
+  refine h_lp.ae_eq <| h_ae.trans ?_
+  simp [← h_unbiased]
+
+lemma integral_inner_eq_integral_inner_gradient
+    (h : IsAlgEnvSeq X G alg (obliviousEnv ν) P)
+    (h_unbiased : ∀ n x, (ν n x)[id] = ∇ (f n) x) (h_memLp : ∀ n, MemLp (G n) 2 P)
+    (hX_lp : ∀ n, MemLp (X n) 2 P) (y : E) (n : ℕ) :
+    P[fun ω ↦ ⟪X n ω - y, G n ω⟫] = P[fun ω ↦ ⟪X n ω - y, ∇ (f n) (X n ω)⟫] := by
+  have h_obl : HasCondDistrib (G n) (X n) (ν n) P :=
+    h.hasCondDistrib_feedback_obliviousEnv n
+  calc P[fun ω ↦ ⟪X n ω - y, G n ω⟫]
+  _ = P[fun ω ↦ P[fun ω' ↦ ⟪X n ω' - y, G n ω'⟫ | mE.comap (X n)] ω] := by
+    rw [integral_condExp (h.measurable_action _).comap_le]
+  _ = P[fun ω ↦ ⟪X n ω - y, P[G n | mE.comap (X n)] ω⟫] := by
+    refine integral_congr_ae ?_
+    refine condExp_inner_of_stronglyMeasurable_left ?_ ?_ ?_
+    · refine StronglyMeasurable.sub ?_ (by fun_prop)
+      refine Measurable.stronglyMeasurable ?_
+      rw [measurable_iff_comap_le]
+    · exact MemLp.integrable_inner ((hX_lp n).sub (memLp_const _)) (h_memLp n)
+    · exact (h_memLp n).integrable (by simp)
+  _ = P[fun ω ↦ ⟪X n ω - y, (ν n (X n ω))[id]⟫] := by
+    refine integral_congr_ae ?_
+    filter_upwards [h.condExp_feedback_obliviousEnv_ae_eq_integral_id n
+      ((h_memLp n).integrable (by simp))] with ω hω using by rw [hω]
+  _ = P[fun ω ↦ ⟪X n ω - y, ∇ (f n) (X n ω)⟫] := by simp_rw [h_unbiased n]
+
+lemma integral_sub_le_integral_inner (hf : ∀ n, ConvexOn ℝ .univ (f n))
+    (hdf : ∀ n, Differentiable ℝ (f n))
+    (h_unbiased : ∀ n x, (ν n x)[id] = ∇ (f n) x) (h_memLp : ∀ n, MemLp (G n) 2 P)
+    (h : IsAlgEnvSeq X G alg (obliviousEnv ν) P)
+    (hX_lp : ∀ n, MemLp (X n) 2 P)
+    (h_int : ∀ n, Integrable (fun ω ↦ f n (X n ω)) P) -- todo: discuss this assumption
+    (y : E) (n : ℕ) :
+    P[fun ω ↦ f n (X n ω) - f n y] ≤ P[fun ω ↦ ⟪X n ω - y, G n ω⟫] := by
+  rw [integral_inner_eq_integral_inner_gradient h h_unbiased h_memLp hX_lp y n]
+  gcongr
+  · exact (h_int n).sub (integrable_const _)
+  · refine MemLp.integrable_inner ?_ ?_
+    · exact (hX_lp n).sub (memLp_const _)
+    · exact memLp_gradient h h_unbiased h_memLp n
+  · exact fun ω ↦ (hf n).sub_le_inner_gradient (hdf n).differentiableAt (by simp) (by simp)
+
+lemma integral_sum_sub_le_integral_sum_inner (hf : ∀ n, ConvexOn ℝ .univ (f n))
+    (hdf : ∀ n, Differentiable ℝ (f n))
+    (h_unbiased : ∀ n x, (ν n x)[id] = ∇ (f n) x) (h_memLp : ∀ n, MemLp (G n) 2 P)
+    (h : IsAlgEnvSeq X G alg (obliviousEnv ν) P)
+    (hX_lp : ∀ n, MemLp (X n) 2 P) (h_int : ∀ n, Integrable (fun ω ↦ f n (X n ω)) P)
+    (y : E) (n : ℕ) :
+    P[fun ω ↦ ∑ i ∈ range n, (f i (X i ω) - f i y)] ≤
+      P[fun ω ↦ ∑ i ∈ range n, ⟪X i ω - y, G i ω⟫] := by
+  rw [integral_finsetSum, integral_finsetSum]
+  rotate_left
+  · refine fun i hi ↦ MemLp.integrable_inner ?_ (h_memLp i)
+    exact (hX_lp i).sub (memLp_const _)
+  · exact fun i hi ↦ (h_int i).sub (integrable_const _)
+  refine sum_le_sum fun i hi ↦ ?_
+  exact integral_sub_le_integral_inner hf hdf h_unbiased h_memLp h hX_lp h_int y i
+
+lemma integral_apply_avg_sub_le_integral_sum_sub
+    {f : E → ℝ} (hf : ConvexOn ℝ .univ f) (hdf : Differentiable ℝ f)
+    (h_unbiased : ∀ n x, (ν n x)[id] = ∇ f x) (h_memLp : ∀ n, MemLp (G n) 2 P)
+    (h : IsAlgEnvSeq X G alg (obliviousEnv ν) P)
+    (hX_lp : ∀ n, MemLp (X n) 2 P) (h_int : ∀ n, Integrable (fun ω ↦ f (X n ω)) P)
+    (y : E) (n : ℕ) (hn : n ≠ 0)
+    (h_int_avg : Integrable (fun ω ↦ f ((n : ℝ)⁻¹ • ∑ i ∈ range n, X i ω)) P) :
+    P[fun ω ↦ f ((n : ℝ)⁻¹ • ∑ i ∈ range n, X i ω) - f y] ≤
+      (n : ℝ)⁻¹ * P[fun ω ↦ ∑ i ∈ range n, ⟪X i ω - y, G i ω⟫] := by
+  calc P[fun ω ↦ f ((n : ℝ)⁻¹ • ∑ i ∈ range n, X i ω) - f y]
+  _ ≤ (n : ℝ)⁻¹ * P[fun ω ↦ ∑ i ∈ range n, (f (X i ω) - f y)] := by
+    rw [← integral_const_mul]
+    gcongr
+    · exact h_int_avg.sub (integrable_const _)
+    · refine Integrable.const_mul (integrable_finsetSum _ fun i hi ↦ ?_) _
+      exact (h_int i).sub (integrable_const _)
+    exact fun ω ↦ hf.apply_avg_sub_le_avg_sub (by simp) y n hn
+  _ ≤ (n : ℝ)⁻¹ * P[fun ω ↦ ∑ i ∈ range n, ⟪X i ω - y, G i ω⟫] := by
+    grw [integral_sum_sub_le_integral_sum_inner (fun _ ↦ hf) (fun _ ↦ hdf) h_unbiased h_memLp h
+      hX_lp h_int y n]
+
+end Learning
diff --git a/LeanMachineLearning/Optimization/Algorithms/GradientDescent.lean b/LeanMachineLearning/Optimization/Algorithms/GradientDescent.lean
new file mode 100644
index 00000000..7c5d53b0
--- /dev/null
+++ b/LeanMachineLearning/Optimization/Algorithms/GradientDescent.lean
@@ -0,0 +1,375 @@
+/-
+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.Projection
+public import LeanMachineLearning.Online.OnlineRegret
+public import LeanMachineLearning.SequentialLearning.Deterministic
+public import LeanMachineLearning.SequentialLearning.StationaryEnv
+
+import LeanMachineLearning.ForMathlib.Analysis.Calculus.Deriv.Slope
+import LeanMachineLearning.ForMathlib.MeasureTheory.Function.L2Space
+import LeanMachineLearning.Online.OnlineToBatch
+
+/-!
+# Online and stochastic gradient descent
+
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory Filter Real Finset
+open scoped Gradient ENNReal NNReal RealInnerProductSpace
+
+namespace Learning
+
+variable {Ω E : Type*} {mΩ : MeasurableSpace Ω} {mE : MeasurableSpace E}
+  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+  {P : Measure Ω} [IsProbabilityMeasure P]
+  {x x₀ : E} {X G : ℕ → Ω → E} {γ : ℕ → ℝ} {η : ℝ}
+
+lemma measurable_proj [FiniteDimensional ℝ E] [BorelSpace E] {s : Set E}
+    (h_closed : IsClosed s) (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty) :
+  Measurable (proj s) := (continuous_proj h_closed h_convex h_nonempty).measurable
+
+protected lemma _root_.Measurable.proj [FiniteDimensional ℝ E] [BorelSpace E] {s : Set E}
+    (h_closed : IsClosed s) (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty)
+    {f : Ω → E} (hf : Measurable f) :
+    Measurable (fun ω ↦ proj s (f ω)) :=
+  (measurable_proj h_closed h_convex h_nonempty).comp hf
+
+section Linear
+
+lemma inner_eq_add (x y g : E) (hη : 0 < η) :
+    ⟪x - y, g⟫ = (2 * η)⁻¹ * (‖x - y‖ ^ 2 - ‖(x - η • g) - y‖ ^ 2) + (η / 2) * ‖g‖ ^ 2 := by
+  have hsub : (x - η • g) - y = (x - y) - η • g := by abel
+  rw [hsub, norm_sub_sq_real (x - y) (η • g)]
+  simp only [inner_smul_right, norm_smul, Real.norm_eq_abs, abs_of_pos hη]
+  field
+
+lemma inner_eq_add' (x y g : ℕ → E) (hx : ∀ n, x (n + 1) = x n - γ n • g n)
+    (hγ : ∀ n, 0 < γ n) (i : ℕ) :
+    ⟪x i - y i, g i⟫ =
+      (2 * γ i)⁻¹ * (‖x i - y i‖ ^ 2 - ‖x (i + 1) - y i‖ ^ 2) + (γ i / 2) * ‖g i‖ ^ 2 := by
+  have hsub : (x i - γ i • g i) - y i = (x i - y i) - γ i • g i := by abel
+  simp only [hx]
+  rw [hsub, norm_sub_sq_real (x i - y i) (γ i • g i)]
+  simp only [inner_smul_right, norm_smul, Real.norm_eq_abs, abs_of_pos (hγ i)]
+  specialize hγ i
+  field
+
+lemma inner_le_add_proj [FiniteDimensional ℝ E] {s : Set E} (h_closed : IsClosed s)
+    (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty) (x g : E) {y : E} (hy : y ∈ s) (hη : 0 < η) :
+    ⟪x - y, g⟫ ≤ (2 * η)⁻¹ * (‖x - y‖ ^ 2 - ‖proj s (x - η • g) - y‖ ^ 2) + (η / 2) * ‖g‖ ^ 2 := by
+  rw [inner_eq_add x y g hη]
+  gcongr
+  rw [← dist_eq_norm, ← dist_eq_norm]
+  exact dist_proj_le h_closed h_convex h_nonempty (x - η • g) hy
+
+lemma inner_le_add_proj' [FiniteDimensional ℝ E] {s : Set E} (h_closed : IsClosed s)
+    (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty) (x g : ℕ → E)
+    (hx : ∀ n, x (n + 1) = proj s (x n - γ n • g n)) {y : ℕ → E} (hy : ∀ i, y i ∈ s)
+    (hγ : ∀ i, 0 < γ i) (i : ℕ) :
+    ⟪x i - y i, g i⟫ ≤
+      (2 * γ i)⁻¹ * (‖x i - y i‖ ^ 2 - ‖x (i + 1) - y i‖ ^ 2) + (γ i / 2) * ‖g i‖ ^ 2 := by
+  grw [inner_le_add_proj h_closed h_convex h_nonempty (x i) (g i) (hy i) (hγ i)]
+  simp [hx]
+
+lemma todo (x y g : ℕ → E)
+    (h : ∀ i, ⟪x i - y i, g i⟫ ≤
+      (2 * γ i)⁻¹ * (‖x i - y i‖ ^ 2 - ‖x (i + 1) - y i‖ ^ 2) + (γ i / 2) * ‖g i‖ ^ 2) (n : ℕ) :
+    ∑ i ∈ range n, ⟪x i - y i, g i⟫ ≤
+      ∑ i ∈ range n,
+        ((2 * γ i)⁻¹ * (‖x i - y i‖ ^ 2 - ‖x (i + 1) - y i‖ ^ 2) + (γ i / 2) * ‖g i‖ ^ 2) := by
+  grw [h]
+
+-- todo: change `y` to `ℕ → E` ?
+lemma sum_inner_le_sum (x g : ℕ → E) (y : E) (hγ : ∀ n, 0 < γ n)
+    (hx : ∀ n, x (n + 1) = x n - γ n • g n) (n : ℕ) :
+    ∑ i ∈ range n, ⟪x i - y, g i⟫ ≤
+      ∑ i ∈ range n,
+        ((2 * γ i)⁻¹ * (‖x i - y‖ ^ 2 - ‖x (i + 1) - y‖ ^ 2) + (γ i / 2) * ‖g i‖ ^ 2) := by
+  refine todo x (fun _ ↦ y) g (fun i ↦ ?_) n
+  grw [inner_eq_add' x (fun _ ↦ y) g hx hγ]
+
+lemma sum_inner_le_sum_proj [FiniteDimensional ℝ E] {s : Set E} (h_closed : IsClosed s)
+    (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty) (x g : ℕ → E) (y : E) (hys : y ∈ s)
+    (hγ : ∀ n, 0 < γ n) (hx : ∀ n, x (n + 1) = proj s (x n - γ n • g n)) (n : ℕ) :
+    ∑ i ∈ range n, ⟪x i - y, g i⟫ ≤
+      ∑ i ∈ range n,
+        ((2 * γ i)⁻¹ * (‖x i - y‖ ^ 2 - ‖x (i + 1) - y‖ ^ 2) + (γ i / 2) * ‖g i‖ ^ 2) := by
+  refine todo x (fun _ ↦ y) g (fun i ↦ ?_) n
+  grw [inner_le_add_proj' h_closed h_convex h_nonempty x g hx (fun _ ↦ hys) hγ]
+
+section ConstantStep
+
+lemma todo' (x g : ℕ → E) (y : E)
+    (h : ∀ i, ⟪x i - y, g i⟫ ≤
+      (2 * η)⁻¹ * (‖x i - y‖ ^ 2 - ‖x (i + 1) - y‖ ^ 2) + (η / 2) * ‖g i‖ ^ 2) (n : ℕ) :
+    ∑ i ∈ range n, ⟪x i - y, g i⟫ ≤
+      (2 * η)⁻¹ * (‖x 0 - y‖ ^ 2 - ‖x n - y‖ ^ 2) + (η / 2) * ∑ i ∈ range n, ‖g i‖ ^ 2 := by
+  refine (todo x (fun _ ↦ y) g h n).trans_eq ?_
+  rw [sum_add_distrib, ← mul_sum, ← mul_sum, Finset.sum_range_sub' (fun i ↦ ‖x i - y‖ ^ 2) n]
+
+lemma sum_inner_le_add (x g : ℕ → E) (y : E)
+    (hη : 0 < η) (hx : ∀ n, x (n + 1) = x n - η • g n) (n : ℕ) :
+    ∑ i ∈ range n, ⟪x i - y, g i⟫ ≤
+      (2 * η)⁻¹ * (‖x 0 - y‖ ^ 2 - ‖x n - y‖ ^ 2) + (η / 2) * ∑ i ∈ range n, ‖g i‖ ^ 2 :=
+  todo' x g y (fun i ↦ (inner_eq_add' x (fun _ ↦ y) g hx (fun _ ↦ hη) i).le) n
+
+lemma todo'' (x g : ℕ → E) (y : E)
+    (h : ∀ i, ⟪x i - y, g i⟫ ≤
+      (2 * η)⁻¹ * (‖x i - y‖ ^ 2 - ‖x (i + 1) - y‖ ^ 2) + (η / 2) * ‖g i‖ ^ 2)
+    (hη : 0 < η) (n : ℕ) :
+    ∑ i ∈ range n, ⟪x i - y, g i⟫ ≤
+      (2 * η)⁻¹ * ‖x 0 - y‖ ^ 2 + (η / 2) * ∑ i ∈ range n, ‖g i‖ ^ 2 := by
+  grw [todo' x g y h n]
+  gcongr
+  exact sub_le_self _ (sq_nonneg _)
+
+/-- Lemma 14.1 in Understanding Machine Learning: From Theory to Algorithms. -/
+lemma gradient_descent_linear_regret (x g : ℕ → E) (y : E) (η : ℝ)
+    (hη : 0 < η) (hx : ∀ n, x (n + 1) = x n - η • g n) (n : ℕ) :
+    ∑ i ∈ range n, ⟪x i - y, g i⟫ ≤
+      (2 * η)⁻¹ * ‖x 0 - y‖ ^ 2 + (η / 2) * ∑ i ∈ range n, ‖g i‖ ^ 2 :=
+  todo'' x g y (fun i ↦ (inner_eq_add' x (fun _ ↦ y) g hx (fun _ ↦ hη) i).le) hη n
+
+lemma proj_gradient_descent_linear_regret [FiniteDimensional ℝ E] {s : Set E}
+    (h_closed : IsClosed s) (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty)
+    (x g : ℕ → E) {y : E} (hys : y ∈ s) (hη : 0 < η)
+    (hx : ∀ n, x (n + 1) = proj s (x n - η • g n)) (n : ℕ) :
+    ∑ i ∈ range n, ⟪x i - y, g i⟫ ≤
+      (2 * η)⁻¹ * ‖x 0 - y‖ ^ 2 + (η / 2) * ∑ i ∈ range n, ‖g i‖ ^ 2 :=
+  todo'' x g y
+    (fun i ↦ inner_le_add_proj' h_closed h_convex h_nonempty x g hx (fun _ ↦ hys) (fun _ ↦ hη) i)
+    hη n
+
+end ConstantStep
+
+lemma onlineRegret_gradientStep_le (x g : ℕ → E) (y : E) (η : ℝ)
+    (hη : 0 < η) (hx : ∀ n, x (n + 1) = x n - η • g n) (n : ℕ) :
+    onlineRegret (fun n x ↦ ⟪x, g n⟫) y x n ≤
+      (2 * η)⁻¹ * ‖x 0 - y‖ ^ 2 + (η / 2) * ∑ i ∈ range n, ‖g i‖ ^ 2 := by
+  simpa [onlineRegret, inner_sub_left] using gradient_descent_linear_regret x g y η hη hx n
+
+lemma onlineRegret_projGradStep_le [FiniteDimensional ℝ E] {s : Set E}
+    (h_closed : IsClosed s) (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty)
+    (x g : ℕ → E) {y : E} (hys : y ∈ s) (η : ℝ)
+    (hη : 0 < η) (hx : ∀ n, x (n + 1) = proj s (x n - η • g n)) (n : ℕ) :
+    onlineRegret (fun n x ↦ ⟪x, g n⟫) y x n ≤
+      (2 * η)⁻¹ * ‖x 0 - y‖ ^ 2 + (η / 2) * ∑ i ∈ range n, ‖g i‖ ^ 2 := by
+  simpa [onlineRegret, inner_sub_left] using
+    proj_gradient_descent_linear_regret h_closed h_convex h_nonempty x g hys hη hx n
+
+end Linear
+
+variable [SecondCountableTopology E] [CompleteSpace E] [BorelSpace E]
+  {f : ℕ → E → ℝ} {hf : ∀ n, Measurable (∇ (f n))}
+
+section Definition
+
+variable {env : Environment E E}
+
+/-- Online gradient descent with step sizes `γ : ℕ → ℝ` and initial point `x₀ : E`,
+without projection.
+
+It is an algorithm that chooses actions in `E` and gets feedback in `E` (gradient of the function at
+the queried point).
+The point `x (n + 1)` is defined as `x (n + 1) = x n - γ n • g n`, where `g n` is the feedback
+received at step `n`.
+Since the algorithm is expressed as a function of the history `hist : ℕ → Iic n → E × E`,
+we write `(hist ⟨n, …⟩).1` for `x n` and `(hist ⟨n, …⟩).2` for `g n`. -/
+noncomputable
+def gradientStep (γ : ℕ → ℝ) (x₀ : E) : Algorithm E E :=
+  let xn := fun (n : ℕ) (hist : Iic n → E × E) ↦ (hist ⟨n, by grind⟩).1
+  let gn := fun (n : ℕ) (hist : Iic n → E × E) ↦ (hist ⟨n, by grind⟩).2
+  detAlgorithm (fun n hist ↦ xn n hist - γ n • gn n hist) (by fun_prop) x₀
+
+lemma action_gradientStep_ae_eq (h_seq : IsAlgEnvSeq X G (gradientStep γ x₀) env P) (n : ℕ) :
+    X (n + 1) =ᵐ[P] X n - γ n • G n := h_seq.action_detAlgorithm_ae_eq n
+
+lemma action_gradientStep_ae_all_eq (h_seq : IsAlgEnvSeq X G (gradientStep γ x₀) env P) :
+    ∀ᵐ ω ∂P, X 0 ω = x₀ ∧ ∀ n, X (n + 1) ω = X n ω - γ n • G n ω :=
+  h_seq.action_detAlgorithm_ae_all_eq
+
+lemma action_ae_eq_sub_sum (h_seq : IsAlgEnvSeq X G (gradientStep γ x₀) env P) (n : ℕ) :
+    X n =ᵐ[P] fun ω ↦ x₀ - ∑ i ∈ range n, γ i • G i ω := by
+  filter_upwards [h_seq.action_detAlgorithm_ae_all_eq] with ω ⟨hω0, hω⟩
+  induction n with
+  | zero => simpa
+  | succ n ih => rw [hω n, sum_range_succ, ← sub_sub]; congr
+
+variable [FiniteDimensional ℝ E]
+  {s : Set E} {h_closed : IsClosed s} {h_convex : Convex ℝ s} {h_nonempty : s.Nonempty}
+
+/-- Projected online gradient descent with step sizes `γ : ℕ → ℝ` and initial point `x₀ : E`.
+
+It is an algorithm that chooses actions in `E` and gets feedback in `E` (gradient of the function at
+the queried point).
+The point `x (n + 1)` is defined as `x (n + 1) = proj s (x n - γ n • g n)`, where `g n` is
+the feedback received at step `n` and `proj s` is the projection onto `s`.
+Since the algorithm is expressed as a function of the history `hist : ℕ → Iic n → E × E`,
+we write `(hist ⟨n, …⟩).1` for `x n` and `(hist ⟨n, …⟩).2` for `g n`. -/
+noncomputable
+def projGradStep (s : Set E)
+    (h_closed : IsClosed s) (h_convex : Convex ℝ s) (h_nonempty : s.Nonempty)
+    (γ : ℕ → ℝ) (x₀ : E) :
+    Algorithm E E :=
+  let xn := fun (n : ℕ) (hist : Iic n → E × E) ↦ (hist ⟨n, by grind⟩).1
+  let gn := fun (n : ℕ) (hist : Iic n → E × E) ↦ (hist ⟨n, by grind⟩).2
+  detAlgorithm (fun n hist ↦ proj s (xn n hist - γ n • gn n hist))
+    (fun _ ↦ Measurable.proj h_closed h_convex h_nonempty (by fun_prop)) x₀
+
+lemma action_projGradStep_ae_eq
+    (h_seq : IsAlgEnvSeq X G (projGradStep s h_closed h_convex h_nonempty γ x₀) env P) {n : ℕ} :
+    X (n + 1) =ᵐ[P] fun ω ↦ proj s (X n ω - γ n • G n ω) := h_seq.action_detAlgorithm_ae_eq n
+
+lemma action_projGradStep_ae_all_eq
+    (h_seq : IsAlgEnvSeq X G (projGradStep s h_closed h_convex h_nonempty γ x₀) env P) :
+    ∀ᵐ ω ∂P, X 0 ω = x₀ ∧ ∀ n, X (n + 1) ω = proj s (X n ω - γ n • G n ω) :=
+  h_seq.action_detAlgorithm_ae_all_eq
+
+end Definition
+
+namespace GradientStep
+
+variable {gradKernel : ℕ → Kernel E E} [∀ n, IsMarkovKernel (gradKernel n)]
+
+lemma memLp_X (h : IsAlgEnvSeq X G (gradientStep (fun _ ↦ η) x₀) (obliviousEnv gradKernel) P)
+    (h_memLp : ∀ n, MemLp (G n) 2 P) (n : ℕ) :
+    MemLp (X n) 2 P := by
+  induction n with
+  | zero =>
+    have h0 : MemLp (fun _ ↦ x₀) 2 P := memLp_const _
+    refine h0.ae_eq ?_
+    filter_upwards [action_gradientStep_ae_all_eq h] with ω hω using hω.1.symm
+  | succ n hn =>
+    have h_sub : MemLp (fun ω ↦ X n ω - η • G n ω) 2 P := hn.sub (MemLp.const_smul (h_memLp n) _)
+    refine h_sub.ae_eq ?_
+    filter_upwards [action_gradientStep_ae_all_eq h] with ω hω using (hω.2 n).symm
+
+section Linear
+
+lemma integral_sum_inner_le (hη : 0 < η) (h_memLp : ∀ n, MemLp (G n) 2 P)
+    (h : IsAlgEnvSeq X G (gradientStep (fun _ ↦ η) x₀) (obliviousEnv gradKernel) P)
+    (y : E) (n : ℕ) :
+    P[fun ω ↦ ∑ i ∈ range n, ⟪X i ω - y, G i ω⟫] ≤
+      (2 * η)⁻¹ * ‖x₀ - y‖ ^ 2 + (η / 2) * ∑ i ∈ range n, P[fun ω ↦ ‖G i ω‖ ^ 2] := by
+  calc P[fun ω ↦ ∑ i ∈ range n, ⟪X i ω - y, G i ω⟫]
+  _ ≤ ∫ ω, (2 * η)⁻¹ * ‖x₀ - y‖ ^ 2 + (η / 2) * ∑ i ∈ range n, ‖G i ω‖ ^ 2 ∂P := by
+    refine integral_mono_ae ?_ ?_ ?_
+    · refine integrable_finsetSum _ fun i hi ↦ MemLp.integrable_inner ?_ (h_memLp i)
+      exact (memLp_X h h_memLp i).sub (memLp_const _)
+    · refine Integrable.add (integrable_const _) (Integrable.const_mul ?_ _)
+      exact integrable_finsetSum _ fun i hi ↦ (h_memLp i).integrable_norm_pow (by simp)
+    · filter_upwards [action_gradientStep_ae_all_eq h] with ω hω
+      refine (gradient_descent_linear_regret _ _ y η hη hω.2 n).trans_eq ?_
+      congr
+      exact hω.1
+  _ = (2 * η)⁻¹ * ‖x₀ - y‖ ^ 2 + (η / 2) * ∑ i ∈ range n, P[fun ω ↦ ‖G i ω‖ ^ 2] := by
+    rw [integral_add, integral_const_mul, integral_const_mul, integral_finsetSum]
+    · simp
+    · exact fun i hi ↦ (h_memLp i).integrable_norm_pow (by simp)
+    · fun_prop
+    · refine Integrable.const_mul ?_ _
+      exact integrable_finsetSum _ fun i hi ↦ (h_memLp i).integrable_norm_pow (by simp)
+
+end Linear
+
+lemma integral_sum_sub_le (hf : ∀ n, ConvexOn ℝ .univ (f n)) (hdf : ∀ n, Differentiable ℝ (f n))
+    (hη : 0 < η)
+    (h_unbiased : ∀ n x, (gradKernel n x)[id] = ∇ (f n) x) (h_memLp : ∀ n, MemLp (G n) 2 P)
+    (h : IsAlgEnvSeq X G (gradientStep (fun _ ↦ η) x₀) (obliviousEnv gradKernel) P)
+    (h_int : ∀ n, Integrable (fun ω ↦ f n (X n ω)) P) (y : E) (n : ℕ) :
+    P[fun ω ↦ ∑ i ∈ range n, (f i (X i ω) - f i y)] ≤
+      (2 * η)⁻¹ * ‖x₀ - y‖ ^ 2 + (η / 2) * ∑ i ∈ range n, P[fun ω ↦ ‖G i ω‖ ^ 2] := by
+  calc P[fun ω ↦ ∑ i ∈ range n, (f i (X i ω) - f i y)]
+  _ ≤ P[fun ω ↦ ∑ i ∈ range n, ⟪X i ω - y, G i ω⟫] :=
+    integral_sum_sub_le_integral_sum_inner hf hdf h_unbiased h_memLp h (memLp_X h h_memLp) h_int y n
+  _ ≤ (2 * η)⁻¹ * ‖x₀ - y‖ ^ 2 + (η / 2) * ∑ i ∈ range n, P[fun ω ↦ ‖G i ω‖ ^ 2] :=
+    integral_sum_inner_le hη h_memLp h y n
+
+lemma integral_onlineRegret_le
+    (hf : ∀ n, ConvexOn ℝ .univ (f n)) (hdf : ∀ n, Differentiable ℝ (f n)) (hη : 0 < η)
+    (h_unbiased : ∀ n x, (gradKernel n x)[id] = ∇ (f n) x)
+    (h_memLp : ∀ n, MemLp (G n) 2 P)
+    (h : IsAlgEnvSeq X G (gradientStep (fun _ ↦ η) x₀) (obliviousEnv gradKernel) P)
+    (h_int : ∀ n, Integrable (fun ω ↦ f n (X n ω)) P)
+    (y : E) (n : ℕ) :
+    P[fun ω ↦ onlineRegret f y (X · ω) n] ≤
+      (2 * η)⁻¹ * ‖x₀ - y‖ ^ 2 + (η / 2) * ∑ i ∈ range n, P[fun ω ↦ ‖G i ω‖ ^ 2] :=
+  integral_sum_sub_le hf hdf hη h_unbiased h_memLp h h_int y n
+
+lemma integral_apply_avg_le {f : E → ℝ} (hf : ConvexOn ℝ .univ f) (hdf : Differentiable ℝ f)
+    (hη : 0 < η)
+    (h_unbiased : ∀ n x, (gradKernel n x)[id] = ∇ f x)
+    (h_memLp : ∀ n, MemLp (G n) 2 P)
+    (h : IsAlgEnvSeq X G (gradientStep (fun _ ↦ η) x₀) (obliviousEnv gradKernel) P)
+    (h_int : ∀ n, Integrable (fun ω ↦ f (X n ω)) P)
+    (y : E) (n : ℕ) (hn : n ≠ 0)
+    (h_int_avg : Integrable (fun ω ↦ f ((n : ℝ)⁻¹ • ∑ i ∈ range n, X i ω)) P) :
+    P[fun ω ↦ f ((n : ℝ)⁻¹ • ∑ i ∈ range n, X i ω) - f y] ≤
+      (2 * η * n)⁻¹ * ‖x₀ - y‖ ^ 2 +
+      (η / (2 * n)) * ∑ i ∈ range n, P[fun ω ↦ ‖G i ω‖ ^ 2] := by
+  calc P[fun ω ↦ f ((n : ℝ)⁻¹ • ∑ i ∈ range n, X i ω) - f y]
+  _ ≤ (n : ℝ)⁻¹ * P[fun ω ↦ ∑ i ∈ range n, (f (X i ω) - f y)] := by
+    rw [← integral_const_mul]
+    gcongr
+    · exact h_int_avg.sub (integrable_const _)
+    · refine Integrable.const_mul (integrable_finsetSum _ fun i hi ↦ ?_) _
+      exact (h_int i).sub (integrable_const _)
+    exact fun ω ↦ hf.apply_avg_sub_le_avg_sub (by simp) y n hn
+  _ ≤ (2 * η * n)⁻¹ * ‖x₀ - y‖ ^ 2 +
+      (η / (2 * n)) * ∑ i ∈ range n, P[fun ω ↦ ‖G i ω‖ ^ 2] := by
+    grw [integral_sum_sub_le (fun _ ↦ hf) (fun _ ↦ hdf) hη h_unbiased h_memLp h h_int y n]
+    refine le_of_eq ?_
+    field
+
+theorem integral_apply_avg_le_const_div_sqrt {f : E → ℝ}
+    (hf : ConvexOn ℝ .univ f) (hdf : Differentiable ℝ f)
+    (h_unbiased : ∀ n x, (gradKernel n x)[id] = ∇ f x)
+    {D L : ℝ} (hD_pos : 0 < D) (hL_pos : 0 < L)
+    {y : E} (hxy_le : ‖x₀ - y‖ ≤ D) (hG_le : ∀ n ω, ‖G n ω‖ ≤ L)
+    (h_int : ∀ n, Integrable (fun ω ↦ f (X n ω)) P)
+    {n : ℕ} (hn : n ≠ 0)
+    (h_int_avg : Integrable (fun ω ↦ f ((n : ℝ)⁻¹ • ∑ i ∈ range n, X i ω)) P)
+    (h : IsAlgEnvSeq X G (gradientStep (fun _ ↦ D / (L * √n)) x₀) (obliviousEnv gradKernel) P) :
+    P[fun ω ↦ f ((n : ℝ)⁻¹ • ∑ i ∈ range n, X i ω) - f y] ≤ D * L / √n := by
+  let η := D / (L * √n)
+  have hG_lp n : MemLp (G n) 2 P := by
+    refine MemLp.mono (g := fun _ ↦ L) (memLp_const _)
+      (have := h.measurable_feedback; by fun_prop) (ae_of_all _ fun ω ↦ ?_)
+    simpa [abs_of_nonneg hL_pos.le] using hG_le n ω
+  calc P[fun ω ↦ f ((n : ℝ)⁻¹ • ∑ i ∈ range n, X i ω) - f y]
+  _ ≤ (2 * η * n)⁻¹ * ‖x₀ - y‖ ^ 2 +
+      (η / (2 * n)) * ∑ i ∈ range n, P[fun ω ↦ ‖G i ω‖ ^ 2] := by
+    refine integral_apply_avg_le hf hdf ?_ h_unbiased hG_lp h h_int y n hn h_int_avg
+    positivity
+  _ ≤ (2 * η * n)⁻¹ * D ^ 2 + (η / 2) * L ^ 2 := by
+    gcongr 1
+    · gcongr
+    · field_simp
+      rw [mul_assoc]
+      gcongr
+      calc ∑ x ∈ range n, ∫ ω, ‖G x ω‖ ^ 2 ∂P
+      _ ≤ ∑ x ∈ range n, ∫ ω, L ^ 2 ∂P := by
+        gcongr with i hi
+        · exact (hG_lp i).integrable_norm_pow (by simp)
+        · simp
+        intro ω
+        simp only
+        gcongr
+        exact hG_le _ _
+      _ = n * L ^ 2 := by simp
+  _ = D * L / √n := by
+    simp only [mul_inv_rev, inv_div, η]
+    field_simp
+    rw [Real.sq_sqrt (by positivity)]
+    ring
+
+end GradientStep
+
+end Learning
diff --git a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
index d707a586..0c8524ba 100644
--- a/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
+++ b/LeanMachineLearning/SequentialLearning/StationaryEnv.lean
@@ -77,6 +77,16 @@ variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
   {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {n N : ℕ}
   {ν : ℕ → Kernel 𝓐 𝓨} [∀ n, IsMarkovKernel (ν n)]
 
+lemma hasCondDistrib_feedback_history_action [IsObliviousEnv env]
+    (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
+    HasCondDistrib (Y (n + 1)) (fun ω ↦ (history A Y n ω, A (n + 1) ω))
+      ((feedbackCondAction env (n + 1)).prodMkLeft _) P := by
+  have hA := h.measurable_action
+  have hR' := h.measurable_feedback
+  refine ⟨by fun_prop, ?_⟩
+  have h_eq := (h.hasCondDistrib_feedback n).map_eq
+  simpa only [feedback_eq_feedbackCondAction] using h_eq
+
 lemma hasCondDistrib_feedback [IsObliviousEnv env] (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
     HasCondDistrib (Y n) (A n) (feedbackCondAction env n) P := by
   have hA := h.measurable_action
@@ -210,6 +220,21 @@ lemma condDistrib_feedback_stationaryEnv [StandardBorelSpace 𝓨] [Nonempty 
     condDistrib (Y n) (A n) P =ᵐ[P.map (A n)] ν :=
   (hasCondDistrib_feedback_stationaryEnv h n).condDistrib_eq
 
+-- todo: generalize to IsObliviousEnv
+lemma condExp_feedback_obliviousEnv_ae_eq_integral_id {E : Type*}
+    [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [CompleteSpace E]
+    {mE : MeasurableSpace E} [BorelSpace E]
+    {alg : Algorithm 𝓐 E} {Y : ℕ → Ω → E}
+    {ν : ℕ → Kernel 𝓐 E} [∀ n, IsMarkovKernel (ν n)]
+    (h : IsAlgEnvSeq A Y alg (obliviousEnv ν) P) (n : ℕ) (h_int : Integrable (Y n) P) :
+    P[Y n | m𝓐.comap (A n)] =ᵐ[P] fun ω ↦ (ν n (A n ω))[id] := by
+  have h_obl : HasCondDistrib (Y n) (A n) (ν n) P := h.hasCondDistrib_feedback_obliviousEnv n
+  have h_ae : ∀ᵐ ω ∂P, 𝓛[Y n | A n; P] (A n ω) = ν n (A n ω) :=
+    ae_of_ae_map (h.measurable_action n).aemeasurable h_obl.condDistrib_eq
+  have h_ae' : P[Y n | m𝓐.comap (A n)] =ᵐ[P] fun ω ↦ ∫ y, y ∂𝓛[Y n | A n; P] (A n ω) :=
+    condExp_ae_eq_integral_condDistrib' (h.measurable_action n) h_int
+  filter_upwards [h_ae, h_ae'] with ω hω hω' using by simp [hω', hω]
+
 /-- The feedback at time `n + 1` is conditionally independent of the history up to time `n`
 given the action at time `n + 1`. -/
 lemma condIndepFun_feedback_history_action [StandardBorelSpace Ω]