diff --git a/LeanPool/LongTails.lean b/LeanPool/LongTails.lean new file mode 100644 index 000000000..a5d1316d7 --- /dev/null +++ b/LeanPool/LongTails.lean @@ -0,0 +1,22 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ + + + +module + +public import LeanPool.LongTails.Theorems.GeneralizedSelfNormalizedConvex + +/-! +# Gradient-only acceleration for generalized-smooth convex optimization + +Source: url:https://github.com/k3nfalt/longtails/tree/269cbc764dd36851fd0b64f2f950f329ee127de4 +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +Status: verified +Main declarations: `LongTails.OracleTemplate.GeneralizedAccelerated.SelfNormalized.result` +Tags: convex-optimization, gradient-methods, oracle-complexity, hilbert-spaces +MSC: 90C25, 90C30, 68Q25 +-/ diff --git a/LeanPool/LongTails/Algorithms/DampedGeneralizedAccelerated.lean b/LeanPool/LongTails/Algorithms/DampedGeneralizedAccelerated.lean new file mode 100644 index 000000000..7728fec71 --- /dev/null +++ b/LeanPool/LongTails/Algorithms/DampedGeneralizedAccelerated.lean @@ -0,0 +1,125 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import LeanPool.LongTails.Setups.GeneralizedSmoothAndConvex +public import Mathlib.Analysis.SpecialFunctions.Sqrt + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +namespace LongTails.OracleTemplate.GeneralizedAccelerated + +open LongTails.Setups.GeneralizedSmoothAndConvex + +/-- The reported point, auxiliary center, accumulated weight and curvature guess. -/ +structure Iterate (E : Type*) where + /-- Accumulated accelerated weight. -/ + A : ℝ + /-- Point reported after the step. -/ + x : E + /-- Auxiliary center in the energy potential. -/ + z : E + /-- Current estimate of the local curvature. -/ + guess : ℝ + +/-- A first gradient query and the state needed to consume the second query. -/ +structure Pending (E : Type*) where + /-- Iterate before the current pair of queries. -/ + previous : Iterate E + /-- Tentative accelerated weight. -/ + weight : ℝ + /-- Interpolation point used for the first query. -/ + y : E + /-- Curvature computed from the first gradient. -/ + curvature : ℝ + /-- Local step at which the second gradient is queried. -/ + point : E + +/-- The initialization, first-query and second-query phases of the accelerated algorithm. -/ +inductive State (E : Type*) where + | start (A : ℝ) (x : E) + | ready (s : Iterate E) + | pending (p : Pending E) + +/-- The positive root of the accelerated weight equation for a curvature guess. -/ +noncomputable def tentativeWeight {E : Type*} (s : Iterate E) : ℝ := + (1 + Real.sqrt (1 + 4 * s.guess * s.A)) / (2 * s.guess) + +/-- The weighted interpolation of the reported point and auxiliary center. -/ +noncomputable def coupling {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + (s : Iterate E) : E := + let a := tentativeWeight s + (s.A / (s.A + a)) • s.x + (a / (s.A + a)) • s.z + +/-- A gradient-dependent curvature bound used to choose a safe local step. -/ +noncomputable def localCurvature {E : Type*} [NormedAddCommGroup E] + (L0 L1 : ℝ) (g : E) : ℝ := + 4 * (L0 + L1 * ‖g‖) + +/-- Form a local gradient step and retain its data for the second gradient query. -/ +noncomputable def prepare {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + (L0 L1 : ℝ) (s : Iterate E) (y g : E) : Pending E := + let M := localCurvature L0 L1 g + ⟨s, tentativeWeight s, y, M, y - (1 / M) • g⟩ + +/-- Consume the second gradient, damping the update when the curvature guess is too small. -/ +noncomputable def finish {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + (p : Pending E) (g : E) : Iterate E := by + classical + exact + if p.curvature ≤ p.previous.guess then + ⟨p.previous.A + p.weight, p.point, p.previous.z - p.weight • g, + p.previous.guess / 16⟩ + else + let γ := p.previous.guess / p.curvature + let a := γ * p.weight + let A := p.previous.A + a + ⟨A, ((1 - γ) * p.previous.A / A) • p.previous.x + + (γ * (p.previous.A + p.weight) / A) • p.point, + p.previous.z - a • g, 16 * p.previous.guess⟩ + +/-- One accelerated step, using gradients at the interpolation point and the local step. -/ +noncomputable def step {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + (L0 L1 : ℝ) (g : E → E) (s : Iterate E) : Iterate E := + let p := prepare L0 L1 s (coupling s) (g (coupling s)) + finish p (g p.point) + +/-- Initialize the energy weight from the radius and objective-gap bounds. -/ +noncomputable def initialIterate {E : Type*} [NormedAddCommGroup E] + (L0 L1 R Δ : ℝ) (x0 : E) (g : E → E) : Iterate E := + ⟨R ^ 2 / (2 * Δ), x0, x0, localCurvature L0 L1 (g x0)⟩ + +/-- The accelerated iterate after a fixed number of two-gradient steps. -/ +noncomputable def run {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + (L0 L1 : ℝ) (g : E → E) (s : Iterate E) : ℕ → Iterate E + | 0 => s + | n + 1 => step L0 L1 g (run L0 L1 g s n) + +/-- The oracle state machine implementing damped acceleration without objective queries. -/ +noncomputable def algorithm (p : Public) : Algorithm p.E p.E p.E where + State := State p.E + initial _ := .start (p.R ^ 2 / (2 * p.Δ)) p.x0 + query := fun state => (0, match state with + | .start _ x => x + | .ready s => coupling s + | .pending s => s.point) + update + | .start A x, g => + let s : Iterate p.E := ⟨A, x, x, localCurvature p.L0 p.L1 g⟩ + .pending (prepare p.L0 p.L1 s x g) + | .ready s, g => .pending (prepare p.L0 p.L1 s (coupling s) g) + | .pending s, g => .ready (finish s g) + output + | .start _ x => x + | .ready s => s.x + | .pending s => s.previous.x + +end LongTails.OracleTemplate.GeneralizedAccelerated diff --git a/LeanPool/LongTails/Algorithms/Gd.lean b/LeanPool/LongTails/Algorithms/Gd.lean new file mode 100644 index 000000000..babfe8632 --- /dev/null +++ b/LeanPool/LongTails/Algorithms/Gd.lean @@ -0,0 +1,30 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import LeanPool.LongTails.Template +public import Mathlib.Analysis.InnerProductSpace.Basic + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +namespace LongTails.OracleTemplate.Gradient + +/-- Ordinary gradient descent with constant step size equal to the reciprocal smoothness. -/ +noncomputable def gd {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : + ℝ × E → Algorithm E E E 1 + | (L, x0) => { + State := E + initial _ := x0 + query x := (0, x) + update x reply := x - (1 / L) • reply + output x := x } + +end LongTails.OracleTemplate.Gradient diff --git a/LeanPool/LongTails/Imports.lean b/LeanPool/LongTails/Imports.lean new file mode 100644 index 000000000..b2e25db91 --- /dev/null +++ b/LeanPool/LongTails/Imports.lean @@ -0,0 +1,26 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Pool contributors +-/ +module -- shake: keep-all --deprecated_module: ignore + +-- Generated project imports; run `lake exe mk_all`. +public import LeanPool.LongTails +public import LeanPool.LongTails.Algorithms.DampedGeneralizedAccelerated +public import LeanPool.LongTails.Algorithms.Gd +public import LeanPool.LongTails.Proofs.DampedGeneralizedDynamics +public import LeanPool.LongTails.Proofs.DampedGeneralizedExecution +public import LeanPool.LongTails.Proofs.Execution +public import LeanPool.LongTails.Proofs.GdConvex +public import LeanPool.LongTails.Proofs.GeneralizedAcceleratedEnergy +public import LeanPool.LongTails.Proofs.GeneralizedCharging +public import LeanPool.LongTails.Proofs.GeneralizedConvergence +public import LeanPool.LongTails.Proofs.GeneralizedGradientStep +public import LeanPool.LongTails.Proofs.GeneralizedLogCharging +public import LeanPool.LongTails.Proofs.GeneralizedMixedRate +public import LeanPool.LongTails.Proofs.GeneralizedSelfNormalizedConvergence +public import LeanPool.LongTails.Setups.GeneralizedSmoothAndConvex +public import LeanPool.LongTails.Setups.SmoothAndConvex +public import LeanPool.LongTails.Template +public import LeanPool.LongTails.Theorems.GeneralizedSelfNormalizedConvex diff --git a/LeanPool/LongTails/Proofs/DampedGeneralizedDynamics.lean b/LeanPool/LongTails/Proofs/DampedGeneralizedDynamics.lean new file mode 100644 index 000000000..ac92b7522 --- /dev/null +++ b/LeanPool/LongTails/Proofs/DampedGeneralizedDynamics.lean @@ -0,0 +1,405 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import LeanPool.LongTails.Proofs.GeneralizedGradientStep +public import LeanPool.LongTails.Proofs.GeneralizedAcceleratedEnergy +public import Mathlib.Tactic.NormNum.RealSqrt + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +open Set InnerProductSpace +open scoped RealInnerProductSpace + +namespace LongTails.OracleTemplate.GeneralizedAccelerated + +open LongTails.Setups.GeneralizedSmoothAndConvex + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] + +omit [InnerProductSpace ℝ E] [CompleteSpace E] in +omit [NormedAddCommGroup E] in +lemma tentativeWeight_pos (s : Iterate E) (hguess : 0 < s.guess) : + 0 < tentativeWeight s := by + unfold tentativeWeight + positivity + +omit [InnerProductSpace ℝ E] [CompleteSpace E] in +omit [NormedAddCommGroup E] in +lemma tentativeWeight_equation (s : Iterate E) (hA : 0 ≤ s.A) + (hguess : 0 < s.guess) : + s.guess * tentativeWeight s ^ 2 = s.A + tentativeWeight s := by + have hs := Real.sq_sqrt (show 0 ≤ 1 + 4 * s.guess * s.A by positivity) + unfold tentativeWeight + field_simp + ring_nf at hs ⊢ + nlinarith + +omit [CompleteSpace E] in +lemma coupling_same (A M : ℝ) (x : E) (hA : 0 ≤ A) (hM : 0 < M) : + coupling (⟨A, x, x, M⟩ : Iterate E) = x := by + have ha := tentativeWeight_pos (⟨A, x, x, M⟩ : Iterate E) hM + have hsum : A + tentativeWeight (⟨A, x, x, M⟩ : Iterate E) ≠ 0 := + ne_of_gt (by linarith) + unfold coupling + simp only + rw [← add_smul, ← add_div, div_self hsum, one_smul] + +lemma damping_bounds {M G : ℝ} (hM : 0 < M) (hG : 0 < G) : + 0 < min 1 (G / M) ∧ min 1 (G / M) ≤ 1 ∧ min 1 (G / M) * M ≤ G := by + refine ⟨lt_min zero_lt_one (div_pos hG hM), min_le_left _ _, ?_⟩ + calc + min 1 (G / M) * M ≤ (G / M) * M := + mul_le_mul_of_nonneg_right (min_le_right _ _) hM.le + _ = G := div_mul_cancel₀ _ hM.ne' + +omit [CompleteSpace E] in +lemma finish_uniform (p : Pending E) (g : E) + (hA : 0 ≤ p.previous.A) (ha : 0 < p.weight) + (hM : 0 < p.curvature) (hG : 0 < p.previous.guess) : + let γ := min 1 (p.previous.guess / p.curvature) + let B := p.previous.A + γ * p.weight + (finish p g).A = B ∧ + (finish p g).x = ((1 - γ) * p.previous.A / B) • p.previous.x + + (γ * (p.previous.A + p.weight) / B) • p.point ∧ + (finish p g).z = p.previous.z - (γ * p.weight) • g ∧ + 0 < (finish p g).guess := by + dsimp only + unfold finish + split_ifs with h + · have hd : 1 ≤ p.previous.guess / p.curvature := (le_div_iff₀ hM).mpr (by simpa) + rw [min_eq_left hd] + have hsum : p.previous.A + p.weight ≠ 0 := ne_of_gt (by linarith) + simp [hsum, div_pos hG (by norm_num : (0 : ℝ) < 16)] + · have hd : p.previous.guess / p.curvature ≤ 1 := + (div_le_one hM).mpr (le_of_lt (lt_of_not_ge h)) + rw [min_eq_right hd] + exact ⟨rfl, rfl, rfl, by positivity⟩ + +omit [CompleteSpace E] in +lemma step_weights {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) + (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) : + let M := localCurvature L0 L1 (g (coupling s)) + let γ := min 1 (s.guess / M) + (step L0 L1 g s).A = s.A + γ * tentativeWeight s ∧ + s.A < (step L0 L1 g s).A ∧ + (step L0 L1 g s).A ≤ s.A + tentativeWeight s ∧ + 0 < (step L0 L1 g s).guess := by + let p := prepare L0 L1 s (coupling s) (g (coupling s)) + have hM := localCurvature_pos hL0 hL1 (g (coupling s)) + have ha := tentativeWeight_pos s hG + have hd := damping_bounds hM hG + have hf := finish_uniform p (g p.point) hA ha hM hG + refine ⟨hf.1, ?_, ?_, hf.2.2.2⟩ + · change s.A < (finish p (g p.point)).A + rw [hf.1] + exact lt_add_of_pos_right _ (mul_pos hd.1 ha) + · change (finish p (g p.point)).A ≤ _ + rw [hf.1] + have hm := mul_le_mul_of_nonneg_right hd.2.1 ha.le + dsimp [p, prepare] at * + linarith + +lemma down_growth {G A a : ℝ} (hG : 0 < G) (hA : 0 ≤ A) (ha : 0 < a) + (he : G * a ^ 2 = A + a) : + 1 / (2 * Real.sqrt G) ≤ Real.sqrt (A + a) - Real.sqrt A := by + have hnew : 0 < A + a := by positivity + have hroot := congrArg Real.sqrt he + rw [Real.sqrt_mul hG.le, Real.sqrt_sq ha.le] at hroot + have hGroot := Real.sqrt_pos.mpr hG + have hnewroot := Real.sqrt_pos.mpr hnew + have hsq := Real.sq_sqrt hA + have hsqnew := Real.sq_sqrt hnew.le + have hmon := Real.sqrt_le_sqrt (show A ≤ A + a by linarith) + have hprod := mul_nonneg (Real.sqrt_nonneg G) (sq_nonneg (Real.sqrt (A + a) - Real.sqrt A)) + have hscaled : Real.sqrt (A + a) ≤ + (2 * Real.sqrt G * (Real.sqrt (A + a) - Real.sqrt A)) * Real.sqrt (A + a) := by + nlinarith [mul_pos hGroot ha] + have hcancel := (mul_le_mul_iff_left₀ hnewroot).mp + (show 1 * Real.sqrt (A + a) ≤ + (2 * Real.sqrt G * (Real.sqrt (A + a) - Real.sqrt A)) * Real.sqrt (A + a) by + nlinarith only [hscaled]) + apply (div_le_iff₀ (show 0 < 2 * Real.sqrt G by positivity)).mpr + nlinarith only [hcancel] + +lemma step_energy {f : E → ℝ} {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) + (hc : ConvexOn ℝ univ f) (hg : ∀ x, HasGradientAt f (g x) x) + (hgd : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) + (s : Iterate E) (u : E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) : + let y := coupling s + let M := localCurvature L0 L1 (g y) + let w := y - (1 / M) • g y + let γ := min 1 (s.guess / M) + let next := step L0 L1 g s + next.A * (f next.x - f u) + 1 / 2 * ‖next.z - u‖ ^ 2 + + γ * (s.A + tentativeWeight s) * (3 * M / 8) * ‖w - y‖ ^ 2 ≤ + s.A * (f s.x - f u) + 1 / 2 * ‖s.z - u‖ ^ 2 := by + let y := coupling s + let M := localCurvature L0 L1 (g y) + let w := y - (1 / M) • g y + let γ := min 1 (s.guess / M) + have hM : 0 < M := localCurvature_pos hL0 hL1 _ + have ha := tentativeWeight_pos s hG + have hd := damping_bounds hM hG + have hw : γ * tentativeWeight s ^ 2 * M ≤ s.A + tentativeWeight s := by + have hm := mul_le_mul_of_nonneg_right hd.2.2 (sq_nonneg (tentativeWeight s)) + rw [← tentativeWeight_equation s hA hG] + nlinarith only [hm] + have hf := finish_uniform (prepare L0 L1 s y (g y)) (g w) hA ha hM hG + dsimp only [prepare] at hf + dsimp only + change (finish _ _).A * (f (finish _ _).x - f u) + + 1 / 2 * ‖(finish _ _).z - u‖ ^ 2 + _ ≤ _ + dsimp only [prepare, y, M, w] at hf ⊢ + rw [hf.1, hf.2.1, hf.2.2.1] + exact damped_step hM hc hg s.x s.z u w hA ha hd.1 hd.2.1 hw + (local_step_residual hL0 hL1 hgd hH y) + +/-- The objective-gap and squared-distance potential for accelerated convergence. -/ +noncomputable def energy (f : E → ℝ) (u : E) (s : Iterate E) : ℝ := + s.A * (f s.x - f u) + 1 / 2 * ‖s.z - u‖ ^ 2 + +/-- The nonnegative energy decrease charged to one accelerated step. -/ +noncomputable def dissipation (L0 L1 : ℝ) (g : E → E) (s : Iterate E) : ℝ := + let y := coupling s + let M := localCurvature L0 L1 (g y) + let w := y - (1 / M) • g y + min 1 (s.guess / M) * (s.A + tentativeWeight s) * (3 * M / 8) * ‖w - y‖ ^ 2 + +omit [CompleteSpace E] in +lemma dissipation_nonneg {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) + (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) : + 0 ≤ dissipation L0 L1 g s := by + have hM := localCurvature_pos hL0 hL1 (g (coupling s)) + have ha := tentativeWeight_pos s hG + dsimp [dissipation] + positivity + +omit [CompleteSpace E] in +lemma run_valid {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) + (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) (n : ℕ) : + 0 ≤ (run L0 L1 g s n).A ∧ 0 < (run L0 L1 g s n).guess := by + induction n with + | zero => exact ⟨hA, hG⟩ + | succ n ih => + have hs := step_weights (g := g) hL0 hL1 (run L0 L1 g s n) ih.1 ih.2 + exact ⟨(ih.1.trans hs.2.1.le), hs.2.2.2⟩ + +lemma run_energy {f : E → ℝ} {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) + (hc : ConvexOn ℝ univ f) (hg : ∀ x, HasGradientAt f (g x) x) + (hgd : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) + (s : Iterate E) (u : E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) (n : ℕ) : + energy f u (run L0 L1 g s n) + + ∑ k ∈ Finset.range n, dissipation L0 L1 g (run L0 L1 g s k) ≤ energy f u s := by + induction n with + | zero => simp [run] + | succ n ih => + have hv := run_valid (g := g) hL0 hL1 s hA hG n + have hs := step_energy hL0 hL1 hc hg hgd hH (run L0 L1 g s n) u hv.1 hv.2 + change energy f u (run L0 L1 g s (n + 1)) + + dissipation L0 L1 g (run L0 L1 g s n) ≤ energy f u (run L0 L1 g s n) at hs + rw [Finset.sum_range_succ] + linarith + +omit [CompleteSpace E] in +lemma run_weight_mono {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) + (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) : + Monotone (fun n => (run L0 L1 g s n).A) := by + apply monotone_nat_of_le_succ + intro n + have hv := run_valid (g := g) hL0 hL1 s hA hG n + exact (step_weights (g := g) hL0 hL1 _ hv.1 hv.2).2.1.le + +omit [CompleteSpace E] in +lemma step_guess {g : E → E} {L0 L1 : ℝ} (s : Iterate E) : + (step L0 L1 g s).guess = + if localCurvature L0 L1 (g (coupling s)) ≤ s.guess then s.guess / 16 else 16 * s.guess := by + by_cases h : localCurvature L0 L1 (g (coupling s)) ≤ s.guess <;> + simp [step, finish, prepare, h] + +omit [CompleteSpace E] in +lemma step_inverse_sqrt_guess {g : E → E} {L0 L1 : ℝ} + (s : Iterate E) (hG : 0 < s.guess) : + 1 / Real.sqrt (step L0 L1 g s).guess = + if localCurvature L0 L1 (g (coupling s)) ≤ s.guess + then 4 * (1 / Real.sqrt s.guess) else (1 / Real.sqrt s.guess) / 4 := by + rw [step_guess] + split_ifs <;> simp [Real.sqrt_div, Real.sqrt_mul, hG.le] + <;> norm_num <;> ring + +omit [CompleteSpace E] in +lemma step_down_growth {g : E → E} {L0 L1 : ℝ} + (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) + (hdown : localCurvature L0 L1 (g (coupling s)) ≤ s.guess) : + 1 / (2 * Real.sqrt s.guess) ≤ + Real.sqrt (step L0 L1 g s).A - Real.sqrt s.A := by + have hweight : (step L0 L1 g s).A = s.A + tentativeWeight s := by + simp [step, finish, prepare, hdown] + rw [hweight] + exact down_growth hG hA (tentativeWeight_pos s hG) (tentativeWeight_equation s hA hG) + +omit [CompleteSpace E] in +lemma down_sum_le_sqrt {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) + (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) (N : ℕ) : + (∑ i ∈ Finset.range N, + if localCurvature L0 L1 (g (coupling (run L0 L1 g s i))) ≤ (run L0 L1 g s i).guess + then 1 / Real.sqrt (run L0 L1 g s i).guess else 0) ≤ + 2 * Real.sqrt (run L0 L1 g s N).A := by + induction N with + | zero => simp + | succ n ih => + rw [Finset.sum_range_succ] + have hv := run_valid (g := g) hL0 hL1 s hA hG n + split_ifs with hd + · have hs := step_down_growth (run L0 L1 g s n) hv.1 hv.2 hd + have he : 1 / (2 * Real.sqrt (run L0 L1 g s n).guess) = + (1 / Real.sqrt (run L0 L1 g s n).guess) / 2 := by ring + rw [he] at hs + change _ ≤ 2 * Real.sqrt (step L0 L1 g (run L0 L1 g s n)).A + linarith + · have hs := Real.sqrt_le_sqrt + (step_weights (g := g) hL0 hL1 (run L0 L1 g s n) hv.1 hv.2).2.1.le + change _ ≤ 2 * Real.sqrt (step L0 L1 g (run L0 L1 g s n)).A + linarith + +omit [CompleteSpace E] in +lemma step_high_dissipation {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 < L1) + (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) + (hup : s.guess ≤ localCurvature L0 L1 (g (coupling s))) + (hhigh : 8 * L0 < localCurvature L0 L1 (g (coupling s))) : + (step L0 L1 g s).A * s.guess ≤ + (512 / 3) * L1 ^ 2 * dissipation L0 L1 g s := by + let M := localCurvature L0 L1 (g (coupling s)) + let d := ‖coupling s - (1 / M) • g (coupling s) - coupling s‖ + have hM : 0 < M := localCurvature_pos hL0 hL1.le _ + have hmin : min 1 (s.guess / M) = s.guess / M := + min_eq_right ((div_le_one hM).mpr hup) + have hmove : 1 / (8 * L1) ≤ d := + (local_step_movement hL0 hL1 (coupling s) (g (coupling s))).resolve_left + (not_le_of_gt hhigh) + have hm : 1 ≤ 8 * L1 * d := by + have ht := (div_le_iff₀ (show 0 < 8 * L1 by positivity)).mp hmove + nlinarith only [ht] + have hs : 1 ≤ 64 * L1 ^ 2 * d ^ 2 := by nlinarith [sq_nonneg (8 * L1 * d - 1)] + have ha := tentativeWeight_pos s hG + have hd : dissipation L0 L1 g s = (3 / 8) * s.guess * (s.A + tentativeWeight s) * d ^ 2 := by + change min 1 (s.guess / M) * (s.A + tentativeWeight s) * (3 * M / 8) * d ^ 2 = _ + rw [hmin] + field_simp + have hmul := mul_le_mul_of_nonneg_left hs + (show 0 ≤ s.guess * (s.A + tentativeWeight s) by positivity) + have hw := mul_le_mul_of_nonneg_right + (step_weights (g := g) hL0 hL1.le s hA hG).2.2.1 hG.le + rw [hd] + nlinarith only [hmul, hw] + +omit [InnerProductSpace ℝ E] [CompleteSpace E] in +lemma initial_energy {f : E → ℝ} {g : E → E} {L0 L1 R Δ : ℝ} + (hΔ : 0 < Δ) (x0 u : E) + (hdist : ‖x0 - u‖ ≤ R) (hgap : f x0 - f u ≤ Δ) : + energy f u (initialIterate L0 L1 R Δ x0 g) ≤ R ^ 2 := by + have hgap' := mul_le_mul_of_nonneg_left hgap + (show 0 ≤ R ^ 2 / (2 * Δ) by positivity) + have he : R ^ 2 / (2 * Δ) * Δ = R ^ 2 / 2 := by field_simp + rw [he] at hgap' + have hnorm := pow_le_pow_left₀ (norm_nonneg _) hdist 2 + dsimp [energy, initialIterate] + linarith + +omit [InnerProductSpace ℝ E] [CompleteSpace E] in +lemma energy_nonneg {f : E → ℝ} {u : E} (hmin : IsMinOn f univ u) + (s : Iterate E) (hA : 0 ≤ s.A) : 0 ≤ energy f u s := by + have hg : 0 ≤ f s.x - f u := sub_nonneg.mpr (hmin (mem_univ _)) + exact add_nonneg (mul_nonneg hA hg) (by positivity) + +lemma run_dissipation_le {f : E → ℝ} {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) + (hc : ConvexOn ℝ univ f) (hg : ∀ x, HasGradientAt f (g x) x) + (hgd : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) + (s : Iterate E) (u : E) (hmin : IsMinOn f univ u) + (hA : 0 ≤ s.A) (hG : 0 < s.guess) (N : ℕ) : + (∑ i ∈ Finset.range N, dissipation L0 L1 g (run L0 L1 g s i)) ≤ energy f u s := by + have he := run_energy hL0 hL1 hc hg hgd hH s u hA hG N + have hn := energy_nonneg hmin (run L0 L1 g s N) (run_valid (g := g) hL0 hL1 s hA hG N).1 + linarith + +lemma run_high_sum_le {f : E → ℝ} {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 < L1) + (hc : ConvexOn ℝ univ f) (hg : ∀ x, HasGradientAt f (g x) x) + (hgd : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) + (s : Iterate E) (u : E) (hmin : IsMinOn f univ u) + (hA : 0 ≤ s.A) (hG : 0 < s.guess) (N : ℕ) + (Q : Finset ℕ) (hQ : Q ⊆ Finset.range N) + (hup : ∀ i ∈ Q, (run L0 L1 g s i).guess ≤ + localCurvature L0 L1 (g (coupling (run L0 L1 g s i)))) + (hhigh : ∀ i ∈ Q, 8 * L0 < localCurvature L0 L1 (g (coupling (run L0 L1 g s i)))) : + (∑ i ∈ Q, (run L0 L1 g s (i + 1)).A * (run L0 L1 g s i).guess) ≤ + (512 / 3) * L1 ^ 2 * energy f u s := by + have hd := run_dissipation_le hL0 hL1.le hc hg hgd hH s u hmin hA hG N + have hsub := Finset.sum_le_sum_of_subset_of_nonneg hQ + (fun i _ _ => dissipation_nonneg (g := g) hL0 hL1.le (run L0 L1 g s i) + (run_valid (g := g) hL0 hL1.le s hA hG i).1 + (run_valid (g := g) hL0 hL1.le s hA hG i).2) + calc + _ ≤ ∑ i ∈ Q, (512 / 3) * L1 ^ 2 * dissipation L0 L1 g (run L0 L1 g s i) := by + apply Finset.sum_le_sum + intro i hi + have hv := run_valid (g := g) hL0 hL1.le s hA hG i + exact step_high_dissipation hL0 hL1 _ hv.1 hv.2 (hup i hi) (hhigh i hi) + _ = (512 / 3) * L1 ^ 2 * (∑ i ∈ Q, dissipation L0 L1 g (run L0 L1 g s i)) := + (Finset.mul_sum _ _ _).symm + _ ≤ (512 / 3) * L1 ^ 2 * energy f u s := + mul_le_mul_of_nonneg_left (hsub.trans hd) (by positivity) + +omit [CompleteSpace E] in +lemma initial_first_down {g : E → E} {L0 L1 R Δ : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hΔ : 0 < Δ) (x0 : E) : + let s := initialIterate L0 L1 R Δ x0 g + localCurvature L0 L1 (g (coupling s)) = s.guess := by + have he := coupling_same (R ^ 2 / (2 * Δ)) (localCurvature L0 L1 (g x0)) x0 + (by positivity) (localCurvature_pos hL0 hL1 _) + simp only [initialIterate, he] + +/-- A failed target accuracy bounds the accumulated weight using the common energy estimate. -/ +lemma run_weight_le_of_inaccurate {f : E → ℝ} {g : E → E} {L0 L1 R ε : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) + (hc : ConvexOn ℝ univ f) (hg : ∀ x, HasGradientAt f (g x) x) + (hgd : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) + (s : Iterate E) (u : E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) + (hE : energy f u s ≤ R ^ 2) (hε : 0 < ε) (N : ℕ) + (hfail : ε < f (run L0 L1 g s N).x - f u) : + (run L0 L1 g s N).A ≤ R ^ 2 / ε := by + have hweight := (run_valid (g := g) hL0 hL1 s hA hG N).1 + have hm := mul_le_mul_of_nonneg_left hfail.le hweight + have he := run_energy hL0 hL1 hc hg hgd hH s u hA hG N + have hsum : 0 ≤ ∑ k ∈ Finset.range N, dissipation L0 L1 g (run L0 L1 g s k) := by + apply Finset.sum_nonneg + intro k _ + have hv := run_valid (g := g) hL0 hL1 s hA hG k + exact dissipation_nonneg hL0 hL1 _ hv.1 hv.2 + dsimp only [energy] at he hE + apply (le_div_iff₀ hε).mpr + linarith only [hm, he, hE, hsum, sq_nonneg ‖(run L0 L1 g s N).z - u‖] + +end LongTails.OracleTemplate.GeneralizedAccelerated diff --git a/LeanPool/LongTails/Proofs/DampedGeneralizedExecution.lean b/LeanPool/LongTails/Proofs/DampedGeneralizedExecution.lean new file mode 100644 index 000000000..06697352c --- /dev/null +++ b/LeanPool/LongTails/Proofs/DampedGeneralizedExecution.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import LeanPool.LongTails.Proofs.DampedGeneralizedDynamics +public import LeanPool.LongTails.Proofs.Execution + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +namespace LongTails.OracleTemplate.GeneralizedAccelerated + +open LongTails.Setups.GeneralizedSmoothAndConvex + +lemma two_queries (p : Public) (g : p.E → p.E) (s : Iterate p.E) : + (fun state => (algorithm p).update state (g (((algorithm p).query state).2)))^[2] + (.ready s) = .ready (step p.L0 p.L1 g s) := rfl + +lemma first_two_queries (p : Public) (g : p.E → p.E) + (hL0 : 0 < p.L0) (hL1 : 0 ≤ p.L1) (hΔ : 0 < p.Δ) : + (fun state => (algorithm p).update state (g (((algorithm p).query state).2)))^[2] + ((algorithm p).initial ()) = + .ready (step p.L0 p.L1 g (initialIterate p.L0 p.L1 p.R p.Δ p.x0 g)) := by + have hc := coupling_same (p.R ^ 2 / (2 * p.Δ)) + (localCurvature p.L0 p.L1 (g p.x0)) p.x0 (by positivity) + (localCurvature_pos hL0 hL1 _) + simp only [step, initialIterate, hc] + rfl + +lemma execute_algorithm (p : Public) (g : p.E → p.E) + (hL0 : 0 < p.L0) (hL1 : 0 ≤ p.L1) (hΔ : 0 < p.Δ) (N : ℕ) : + execute { answer := fun _ (_, x) _ => g x } (algorithm p) (fun _ => (2 * N)) = + (run p.L0 p.L1 g (initialIterate p.L0 p.L1 p.R p.Δ p.x0 g) N).x := by + let T := fun state => (algorithm p).update state (g (((algorithm p).query state).2)) + have hi : ∀ n, T^[2 * (n + 1)] ((algorithm p).initial ()) = + .ready (run p.L0 p.L1 g (initialIterate p.L0 p.L1 p.R p.Δ p.x0 g) (n + 1)) := by + intro n + induction n with + | zero => exact first_two_queries p g hL0 hL1 hΔ + | succ n ih => + rw [show 2 * (n + 1 + 1) = 2 + 2 * (n + 1) by omega, + Function.iterate_add_apply, ih] + exact two_queries p g _ + erw [execute_iterate] + cases N with + | zero => rfl + | succ n => + change (algorithm p).output (T^[2 * (n + 1)] ((algorithm p).initial ())) = _ + rw [hi] + rfl + +lemma execute_gradient_oracle (p : Public) (f : p.E → ℝ) (g : p.E → p.E) + (oracle : Oracle p.E p.E) + (hg : ∀ x, HasGradientAt f (g x) x) + (horacle : ∀ k seed x, HasGradientAt f (oracle.answer k (0, x) seed) x) + (hL0 : 0 < p.L0) (hL1 : 0 ≤ p.L1) (hΔ : 0 < p.Δ) (N : ℕ) + (seed : (algorithm p).Seed) (oracleSeed : (k : ℕ) → oracle.Seed k) : + execute oracle (algorithm p) (fun _ => (2 * N)) seed oracleSeed = + (run p.L0 p.L1 g (initialIterate p.L0 p.L1 p.R p.Δ p.x0 g) N).x := by + have hanswer : ∀ k x sample, oracle.answer k (0, x) sample = g x := + fun k x sample => (horacle k sample x).unique (hg x) + rw [execute_eq_of_answer_eq oracle g hanswer] + cases seed + exact execute_algorithm p g hL0 hL1 hΔ N + +end LongTails.OracleTemplate.GeneralizedAccelerated diff --git a/LeanPool/LongTails/Proofs/Execution.lean b/LeanPool/LongTails/Proofs/Execution.lean new file mode 100644 index 000000000..f345fb759 --- /dev/null +++ b/LeanPool/LongTails/Proofs/Execution.lean @@ -0,0 +1,143 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import LeanPool.LongTails.Template +public import Mathlib.Logic.Function.Iterate +public import Mathlib.Tactic.SplitIfs + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +open MeasureTheory + +namespace LongTails.OracleTemplate + +lemma execute_eq_of_answer_eq {Query Reply Output : Type*} + (oracle : Oracle Query Reply 1) (g : Query → Reply) + (h : ∀ k query seed, oracle.answer k (0, query) seed = g query) + (A : Algorithm Query Reply Output 1) (K : ℕ) (seed : A.Seed) + (oracleSeed : (k : ℕ) → oracle.Seed k) : + execute oracle A (fun _ => K) seed oracleSeed = + execute { answer := fun _ query _ => g query.2 } A (fun _ => K) seed := by + unfold execute + congr 1 + funext k query + obtain ⟨i, query⟩ := query + have hi : i = 0 := Subsingleton.elim _ _ + subst i + exact h k query (oracleSeed k) + +lemma execute_indexed {Query Reply Output : Type*} (oracle : Oracle Query Reply) + (A : Algorithm Query Reply Output) (K : ℕ) (seed : A.Seed) + (ξ : (k : ℕ) → oracle.Seed k) : + execute oracle A (fun _ => K) seed ξ = + A.output ((fun sc : A.State × ℕ => + (A.update sc.1 (oracle.answer sc.2 (A.query sc.1) (ξ sc.2)), sc.2 + 1))^[K] + (A.initial seed, 0)).1 := by + unfold execute + simp only [Fin.sum_univ_one] + generalize A.initial seed = state + generalize (0 : ℕ) = call + induction K generalizing state call with + | zero => rfl + | succ k ih => + rw [Function.iterate_succ_apply] + change (if k + 1 = 0 then _ else _) = _ + simp only [Nat.add_eq_zero_iff, Nat.one_ne_zero, and_false, ite_false] + have hr : Function.update (fun _ : Fin 1 => k + 1) (A.query state).1 k = fun _ => k := by + funext i + have hi : i = (A.query state).1 := Subsingleton.elim _ _ + subst i + simp + simp only [Nat.add_sub_cancel] + rw [hr] + exact ih _ _ + +lemma execute_iterate {Query Reply Output : Type*} (oracle : Query → Reply) + (A : Algorithm Query Reply Output 1) (K : ℕ) (seed : A.Seed) : + execute { answer := fun _ query _ => oracle query.2 } A (fun _ => K) seed = + A.output ((fun s => A.update s (oracle (A.query s).2))^[K] (A.initial seed)) := by + rw [execute_indexed] + congr 1 + generalize A.initial seed = state + generalize (0 : ℕ) = call + induction K generalizing state call with + | zero => rfl + | succ K ih => + rw [Function.iterate_succ_apply, Function.iterate_succ_apply] + exact ih _ _ + +lemma execute_eq_of_safe_prefix {Query Reply Output : Type*} {n : ℕ} + (O : Oracle Query Reply n) (A : Algorithm Query Reply Output n) + (budget : Fin n → ℕ) (seed : A.Seed) (ξ : (k : ℕ) → O.Seed k) + (state : ℕ → A.State) (remaining : ℕ → Fin n → ℕ) (T : ℕ) (output : Output) + (hstate : state 0 = A.initial seed) + (hstep : ∀ k, state (k + 1) = A.update (state k) (O.answer k (A.query (state k)) (ξ k))) + (hremaining : remaining 0 = budget) + (hconsume : ∀ k, remaining (k + 1) = Function.update (remaining k) + (A.query (state k)).1 (remaining k (A.query (state k)).1 - 1)) + (hsafe : ∀ k, k < T → 0 < remaining k (A.query (state k)).1) + (houtput : ∀ k, T ≤ k → A.output (state k) = output) + (hT : T ≤ ∑ i, budget i) : execute O A budget seed ξ = output := by + unfold execute + generalize hf : (∑ i, budget i) = fuel + have hbound : T ≤ fuel := hf ▸ hT + rw [← hstate, ← hremaining] + generalize hc : (0 : ℕ) = call + have hb : T ≤ call + fuel := by omega + clear hf hbound hc hT + induction fuel generalizing call with + | zero => exact houtput call (by omega) + | succ fuel ih => + change (if remaining call (A.query (state call)).1 = 0 then _ else _) = output + split_ifs with hz + · exact houtput call (by by_contra h; have := hsafe call (by omega); omega) + · dsimp only + rw [← hstep, ← hconsume] + exact ih (call + 1) (by omega) + +lemma convergence_of_public_budget {S : Setup} (B : S.Public → ℕ) + (h : ∃ make : (p : S.Public) → Algorithm (S.Query p) (S.Reply p) (S.Output p) S.numOracles, + (∀ p, S.valid p → ∀ I O, S.admissible p I O → + let A := make (S.publicInput p) + S.successful p I + (fun seed : A.Seed × ((k : ℕ) → O.Seed k) => + execute O A (fun _ => B (S.publicInput p)) seed.1 seed.2) + ⟨(A.law : Measure _).prod (O.law : Measure _), inferInstance⟩) ∧ + ∀ p, S.valid p → S.allowedAlgorithm (S.publicInput p) (make (S.publicInput p))) : + Convergence S (fun p _ => B (S.publicInput p)) := h + +lemma convergence_of_call_budget {S : Setup} (budget : S.Params → ℕ) + (h : ∃ make : (p : S.Public) → Algorithm (S.Query p) (S.Reply p) (S.Output p) S.numOracles, + (∀ p, S.valid p → ∀ K, budget p ≤ K → ∀ I O, S.admissible p I O → + let A := make (S.publicInput p) + S.successful p I + (fun seed : A.Seed × ((k : ℕ) → O.Seed k) => execute O A (fun _ => K) seed.1 seed.2) + ⟨(A.law : Measure _).prod (O.law : Measure _), inferInstance⟩) ∧ + ∀ p, S.valid p → S.allowedAlgorithm (S.publicInput p) (make (S.publicInput p))) : + Convergence S (fun p _ => budget p) := by + obtain ⟨make, correct, allowed⟩ := h + exact ⟨make, fun p hp => correct p hp (budget p) le_rfl, allowed⟩ + +lemma convergence_of_block_budget {S : Setup} (B : S.Params → ℕ) (m : S.Public → ℕ) + (h : ∃ make : (p : S.Public) → Algorithm (S.Query p) (S.Reply p) (S.Output p) S.numOracles, + (∀ p, S.valid p → ∀ N, B p ≤ N → ∀ I O, S.admissible p I O → + let A := make (S.publicInput p) + S.successful p I + (fun seed : A.Seed × ((k : ℕ) → O.Seed k) => + execute O A (fun _ => m (S.publicInput p) * N) seed.1 seed.2) + ⟨(A.law : Measure _).prod (O.law : Measure _), inferInstance⟩) ∧ + ∀ p, S.valid p → S.allowedAlgorithm (S.publicInput p) (make (S.publicInput p))) : + Convergence S (fun p _ => m (S.publicInput p) * B p) := by + obtain ⟨make, correct, allowed⟩ := h + exact ⟨make, fun p hp => correct p hp (B p) le_rfl, allowed⟩ + +end LongTails.OracleTemplate diff --git a/LeanPool/LongTails/Proofs/GdConvex.lean b/LeanPool/LongTails/Proofs/GdConvex.lean new file mode 100644 index 000000000..37f497f27 --- /dev/null +++ b/LeanPool/LongTails/Proofs/GdConvex.lean @@ -0,0 +1,190 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import LeanPool.LongTails.Algorithms.Gd +public import LeanPool.LongTails.Proofs.Execution +public import LeanPool.LongTails.Setups.SmoothAndConvex +public import Mathlib.Analysis.Calculus.MeanValue +public import Mathlib.Analysis.Calculus.Deriv.Pow +public import Mathlib.Analysis.Convex.Deriv +public import Mathlib.Tactic.Convert +public import Mathlib.Tactic.FieldSimp +public import Mathlib.Tactic.Linarith +public import Mathlib.Tactic.Module +public import Mathlib.Tactic.NormNum +public import Mathlib.Tactic.Positivity +public import Mathlib.Tactic.Ring + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +open Set InnerProductSpace +open scoped RealInnerProductSpace + +namespace LongTails.OracleTemplate.Gradient + +open LongTails.Setups.SmoothAndConvex + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] + +omit [CompleteSpace E] in +lemma execute_gd (oracle : E → E) (L : ℝ) (x0 : E) (K : ℕ) : + execute { answer := fun _ query _ => oracle query.2 } (gd (L, x0)) (fun _ => K) = + (fun x => x - (1 / L) • oracle x)^[K] x0 := by + exact execute_iterate oracle (gd (L, x0)) K () + +lemma smooth_upper_bound {f : E → ℝ} {oracle : E → E} {L : ℝ} + (hg : ∀ x, HasGradientAt f (oracle x) x) + (hlip : ∀ x y, ‖oracle x - oracle y‖ ≤ L * ‖x - y‖) (x y : E) : + f y ≤ f x + ⟪oracle x, y - x⟫ + L / 2 * ‖y - x‖ ^ 2 := by + let d := y - x + let F := fun t : ℝ => f (x + t • d) + let F' := fun t : ℝ => ⟪oracle (x + t • d), d⟫ + have hF : ∀ t, HasDerivAt F (F' t) t := by + intro t + have h := (hg _).hasFDerivAt.comp_hasDerivAt t + ((hasDerivAt_id t).smul_const d |>.const_add x) + simp only [id_eq, one_smul, toDual_apply_apply] at h + exact h + let B := fun t : ℝ => f x + t * ⟪oracle x, d⟫ + t ^ 2 * (L / 2 * ‖d‖ ^ 2) + have hB : ∀ t, HasDerivAt B (⟪oracle x, d⟫ + L * ‖d‖ ^ 2 * t) t := by + intro t + convert ((hasDerivAt_id t).mul_const ⟪oracle x, d⟫ |>.const_add (f x)).add + (((hasDerivAt_id t).pow 2).mul_const (L / 2 * ‖d‖ ^ 2)) using 1 + · funext s + dsimp [B] + · dsimp + ring + have hderiv : ∀ t ∈ Ico (0 : ℝ) 1, F' t ≤ ⟪oracle x, d⟫ + L * ‖d‖ ^ 2 * t := by + intro t ht + have h := (real_inner_le_norm (oracle (x + t • d) - oracle x) d).trans + (mul_le_mul_of_nonneg_right (hlip (x + t • d) x) (norm_nonneg d)) + simp only [add_sub_cancel_left, norm_smul, Real.norm_eq_abs, + abs_of_nonneg ht.1, inner_sub_left] at h + dsimp [F'] + nlinarith + have h := image_le_of_deriv_right_le_deriv_boundary + (fun t _ => (hF t).continuousAt.continuousWithinAt) + (fun t _ => (hF t).hasDerivWithinAt) + (show F 0 ≤ B 0 by simp [F, B]) + (fun t _ => (hB t).continuousAt.continuousWithinAt) + (fun t _ => (hB t).hasDerivWithinAt) hderiv + (show (1 : ℝ) ∈ Icc 0 1 by constructor <;> norm_num) + simpa [F, B, d] using h + +lemma convex_support {f : E → ℝ} {oracle : E → E} + (hc : ConvexOn ℝ Set.univ f) (hg : ∀ x, HasGradientAt f (oracle x) x) + (x y : E) : ⟪oracle x, y - x⟫ ≤ f y - f x := by + have hconv := hc.comp_affineMap (AffineMap.lineMap x y) + have hd : HasFDerivAt f ((toDual ℝ E) (oracle x)) + ((AffineMap.lineMap x y) (0 : ℝ)) := by + simpa using (hg x).hasFDerivAt + have hline : HasDerivAt (f ∘ AffineMap.lineMap x y) ⟪oracle x, y - x⟫ (0 : ℝ) := by + simpa using hd.comp_hasDerivAt (0 : ℝ) + (AffineMap.hasDerivAt_lineMap (a := x) (b := y) (x := (0 : ℝ))) + have h := hconv.le_slope_of_hasDerivAt (x := 0) (y := 1) + (by simp) (by simp) (by norm_num) hline + simpa [slope_def_field] using h + +lemma descent {f : E → ℝ} {oracle : E → E} {L : ℝ} + (hL : 0 < L) (hg : ∀ x, HasGradientAt f (oracle x) x) + (hlip : ∀ x y, ‖oracle x - oracle y‖ ≤ L * ‖x - y‖) (x : E) : + f (x - (1 / L) • oracle x) ≤ f x - ‖oracle x‖ ^ 2 / (2 * L) := by + have h := smooth_upper_bound hg hlip x (x - (1 / L) • oracle x) + have he : x - (1 / L) • oracle x - x = -(1 / L) • oracle x := by module + rw [he] at h + simp only [inner_smul_right, real_inner_self_eq_norm_sq, norm_smul, + Real.norm_eq_abs, abs_neg, abs_of_pos (one_div_pos.mpr hL)] at h + convert h using 1 + field_simp + ring + +private lemma convex_step {f : E → ℝ} {oracle : E → E} {L : ℝ} + (hL : 0 < L) (hc : ConvexOn ℝ Set.univ f) + (hg : ∀ x, HasGradientAt f (oracle x) x) + (hlip : ∀ x y, ‖oracle x - oracle y‖ ≤ L * ‖x - y‖) (x u : E) : + f (x - (1 / L) • oracle x) - f u ≤ + L / 2 * (‖x - u‖ ^ 2 - ‖x - (1 / L) • oracle x - u‖ ^ 2) := by + have hd := descent hL hg hlip x + have hs := convex_support hc hg x u + have he : x - (1 / L) • oracle x - u = (x - u) - (1 / L) • oracle x := by module + rw [he, norm_sub_sq_real (x - u) ((1 / L) • oracle x)] + simp only [norm_smul, Real.norm_eq_abs, mul_pow, sq_abs, inner_smul_right] + have hi : ⟪x - u, oracle x⟫ = -⟪oracle x, u - x⟫ := by + rw [real_inner_comm, ← inner_neg_right] + congr 1 + module + rw [hi] + have hne : L ≠ 0 := ne_of_gt hL + have heq : L / 2 * + (‖x - u‖ ^ 2 - (‖x - u‖ ^ 2 - 2 * ((1 / L) * -⟪oracle x, u - x⟫) + + (1 / L) ^ 2 * ‖oracle x‖ ^ 2)) = + -⟪oracle x, u - x⟫ - ‖oracle x‖ ^ 2 / (2 * L) := by field_simp; ring + rw [heq] + linarith + +lemma gd_accuracy (f : E → ℝ) (oracle : E → E) + (L R ε : ℝ) (x0 xstar : E) + (hL : 0 < L) (hR : 0 ≤ R) (hε : 0 < ε) + (hc : ConvexOn ℝ Set.univ f) + (hg : ∀ x, HasGradientAt f (oracle x) x) + (hlip : ∀ x y, ‖oracle x - oracle y‖ ≤ L * ‖x - y‖) + (hdist : ‖x0 - xstar‖ ≤ R) + (K : ℕ) + (hbudget : max 1 ⌈L * R ^ 2 / (2 * ε)⌉₊ ≤ K) : + f (execute { answer := fun _ query _ => oracle query.2 } (gd (L, x0)) (fun _ => K)) - + f xstar ≤ ε := by + let T := fun x => x - (1 / L) • oracle x + let x := fun k => T^[k] x0 + have hx : ∀ k, x (k + 1) = x k - (1 / L) • oracle (x k) := by + intro k + exact Function.iterate_succ_apply' T k x0 + have hsum : ∀ n, (∑ k ∈ Finset.range n, (f (x (k + 1)) - f xstar)) ≤ + L / 2 * (‖x0 - xstar‖ ^ 2 - ‖x n - xstar‖ ^ 2) := by + intro n + induction n with + | zero => simp [x] + | succ n ih => + have hs := convex_step hL hc hg hlip (x n) xstar + rw [← hx n] at hs + rw [Finset.sum_range_succ] + linarith + have hmono : Antitone (fun k => f (x k)) := by + apply antitone_nat_of_succ_le + intro k + have hd := descent hL hg hlip (x k) + rw [← hx k] at hd + have hn : 0 ≤ ‖oracle (x k)‖ ^ 2 / (2 * L) := by positivity + linarith + rw [execute_gd] + change f (x K) - f xstar ≤ ε + have hK : 0 < K := lt_of_lt_of_le Nat.zero_lt_one ((le_max_left _ _).trans hbudget) + have hKr : (0 : ℝ) < K := by exact_mod_cast hK + have hle := Finset.sum_le_sum (s := Finset.range K) + (fun k hk => sub_le_sub_right + (hmono (by have := Finset.mem_range.mp hk; omega : k + 1 ≤ K)) (f xstar)) + simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul] at hle + have hrate : f (x K) - f xstar ≤ L * ‖x0 - xstar‖ ^ 2 / (2 * (K : ℝ)) := by + apply (le_div_iff₀ (show 0 < 2 * (K : ℝ) by positivity)).mpr + have hs := hsum K + nlinarith [sq_nonneg ‖x K - xstar‖] + have hceil : L * R ^ 2 / (2 * ε) ≤ (K : ℝ) := + (Nat.le_ceil _).trans (Nat.cast_le.mpr ((le_max_right 1 _).trans hbudget)) + have hR2 : ‖x0 - xstar‖ ^ 2 ≤ R ^ 2 := by + nlinarith [norm_nonneg (x0 - xstar)] + have hbound : L * ‖x0 - xstar‖ ^ 2 / (2 * (K : ℝ)) ≤ ε := by + apply (div_le_iff₀ (show 0 < 2 * (K : ℝ) by positivity)).mpr + have hh := (div_le_iff₀ (show 0 < 2 * ε by positivity)).mp hceil + have hnum := mul_le_mul_of_nonneg_left hR2 hL.le + nlinarith + exact hrate.trans hbound + +end LongTails.OracleTemplate.Gradient diff --git a/LeanPool/LongTails/Proofs/GeneralizedAcceleratedEnergy.lean b/LeanPool/LongTails/Proofs/GeneralizedAcceleratedEnergy.lean new file mode 100644 index 000000000..33a3f70be --- /dev/null +++ b/LeanPool/LongTails/Proofs/GeneralizedAcceleratedEnergy.lean @@ -0,0 +1,112 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import LeanPool.LongTails.Proofs.GdConvex + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +open Set InnerProductSpace +open scoped RealInnerProductSpace + +namespace LongTails.OracleTemplate.GeneralizedAccelerated + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] + +omit [CompleteSpace E] in +lemma ms_inner {M : ℝ} (hM : 0 < M) (g d : E) + (hr : ‖g + M • d‖ ≤ M / 2 * ‖d‖) : + ⟪g, d⟫ ≤ -(3 * M / 8) * ‖d‖ ^ 2 - ‖g‖ ^ 2 / (2 * M) := by + have hsq : ‖g + M • d‖ ^ 2 ≤ (M / 2 * ‖d‖) ^ 2 := + pow_le_pow_left₀ (norm_nonneg _) hr 2 + rw [norm_add_sq_real] at hsq + simp only [inner_smul_right, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs] at hsq + have hM0 := hM.ne' + field_simp + nlinarith + +lemma damped_step {f : E → ℝ} {g : E → E} {M A a γ : ℝ} + (hM : 0 < M) (hc : ConvexOn ℝ univ f) + (hg : ∀ x, HasGradientAt f (g x) x) + (x z u w : E) (hA : 0 ≤ A) (ha : 0 < a) + (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hweight : γ * a ^ 2 * M ≤ A + a) + (hr : let y := (A / (A + a)) • x + (a / (A + a)) • z + ‖g w + M • (w - y)‖ ≤ M / 2 * ‖w - y‖) : + let y := (A / (A + a)) • x + (a / (A + a)) • z + let B := A + γ * a + let xnew := ((1 - γ) * A / B) • x + (γ * (A + a) / B) • w + B * (f xnew - f u) + 1 / 2 * ‖z - (γ * a) • g w - u‖ ^ 2 + + γ * (A + a) * (3 * M / 8) * ‖w - y‖ ^ 2 ≤ + A * (f x - f u) + 1 / 2 * ‖z - u‖ ^ 2 := by + let y := (A / (A + a)) • x + (a / (A + a)) • z + let B := A + γ * a + let xnew := ((1 - γ) * A / B) • x + (γ * (A + a) / B) • w + change ‖g w + M • (w - y)‖ ≤ M / 2 * ‖w - y‖ at hr + change B * (f xnew - f u) + 1 / 2 * ‖z - (γ * a) • g w - u‖ ^ 2 + + γ * (A + a) * (3 * M / 8) * ‖w - y‖ ^ 2 ≤ _ + have hB : 0 < B := by dsimp [B]; positivity + have hAa : 0 < A + a := by positivity + have hx := Gradient.convex_support hc hg w x + have hu := Gradient.convex_support hc hg w u + have hid : A • (x - w) + a • (u - w) = + a • (u - z) + (A + a) • (y - w) := by + dsimp [y] + match_scalars + all_goals field_simp [hAa.ne'] <;> ring + have hi := congrArg (fun v => ⟪g w, v⟫) hid + simp only [inner_add_right, inner_smul_right] at hi + have hneg (v₁ v₂ : E) : ⟪g w, v₁ - v₂⟫ = -⟪g w, v₂ - v₁⟫ := by + rw [← inner_neg_right] + congr 1 + module + rw [hneg u z, hneg y w] at hi + have hs : (A + a) * (f w - f u) ≤ A * (f x - f u) + + a * ⟪g w, z - u⟫ + (A + a) * ⟪g w, w - y⟫ := by + have hx' := mul_le_mul_of_nonneg_left hx hA + have hu' := mul_le_mul_of_nonneg_left hu ha.le + nlinarith + have hsum : (1 - γ) * A / B + γ * (A + a) / B = 1 := by + dsimp [B] + field_simp; ring + have hmix := hc.2 (mem_univ x) (mem_univ w) + (show 0 ≤ (1 - γ) * A / B by positivity) + (show 0 ≤ γ * (A + a) / B by positivity) hsum + change f xnew ≤ _ at hmix + have hmix' := mul_le_mul_of_nonneg_left hmix hB.le + have hmix'' : B * (f xnew - f u) ≤ + (1 - γ) * A * (f x - f u) + γ * (A + a) * (f w - f u) := by + have he : B * (((1 - γ) * A / B) • f x + + (γ * (A + a) / B) • f w) = + (1 - γ) * A * f x + γ * (A + a) * f w := by + simp only [smul_eq_mul] + field_simp + rw [he] at hmix' + dsimp [B] at hmix' ⊢ + nlinarith + have hs' := mul_le_mul_of_nonneg_left hs hγ.le + have hinner := ms_inner hM (g w) (w - y) hr + have hinner' := mul_le_mul_of_nonneg_left hinner + (show 0 ≤ γ * (A + a) by positivity) + have hweight' := mul_le_mul_of_nonneg_right hweight + (show 0 ≤ γ * ‖g w‖ ^ 2 by positivity) + have hn : z - (γ * a) • g w - u = (z - u) - (γ * a) • g w := by module + rw [hn, norm_sub_sq_real] + simp only [inner_smul_right, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs] + rw [← real_inner_comm (z - u) (g w)] + have hcancel : γ ^ 2 * a ^ 2 * ‖g w‖ ^ 2 / 2 ≤ + γ * (A + a) * (‖g w‖ ^ 2 / (2 * M)) := by + rw [← mul_div_assoc] + apply (le_div_iff₀ (show 0 < 2 * M by positivity)).mpr + nlinarith only [hweight'] + dsimp [B] at hmix'' ⊢ + nlinarith only [hmix'', hs', hinner', hcancel] + +end LongTails.OracleTemplate.GeneralizedAccelerated diff --git a/LeanPool/LongTails/Proofs/GeneralizedCharging.lean b/LeanPool/LongTails/Proofs/GeneralizedCharging.lean new file mode 100644 index 000000000..266c64de2 --- /dev/null +++ b/LeanPool/LongTails/Proofs/GeneralizedCharging.lean @@ -0,0 +1,270 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import Mathlib.Algebra.BigOperators.Group.List.Basic +public import Mathlib.Basic.Real.Basic +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Data.List.Nodup +public import Mathlib.Tactic.Linarith +public import Mathlib.Tactic.Ring + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +namespace LongTails.OracleTemplate.GeneralizedAccelerated + +/-- An active block and earlier blocks used to count curvature updates. -/ +structure ChargingState where + /-- Start index and count of the active charging block. -/ + active : ℕ × ℕ + /-- Completed charging blocks, in reverse chronological order. -/ + past : List (ℕ × ℕ) + +/-- Partition the iteration history into blocks starting at upward curvature changes. -/ +def charging (up : ℕ → Bool) : ℕ → ChargingState + | 0 => ⟨(0, 0), []⟩ + | n + 1 => + let s := charging up n + if up (n + 1) then ⟨(n + 1, 1), s.active :: s.past⟩ + else ⟨(s.active.1, s.active.2 + 1), s.past⟩ + +/-- The exponentially weighted inverse-curvature mass of a block. -/ +noncomputable def chargeValue (w : ℕ → ℝ) (b : ℕ × ℕ) : ℝ := + 2 ^ b.2 * w b.1 + +/-- The sum of the active and completed block charges. -/ +noncomputable def chargeTotal (w : ℕ → ℝ) (s : ChargingState) : ℝ := + chargeValue w s.active + (s.past.map (chargeValue w)).sum + +/-- The inverse-curvature mass accumulated at downward curvature changes. -/ +noncomputable def downMass (up : ℕ → Bool) (w : ℕ → ℝ) (n : ℕ) : ℝ := + ∑ i ∈ Finset.range (n + 1), if up i then 0 else w i + +lemma charging_mass_succ (up : ℕ → Bool) (w : ℕ → ℝ) (n : ℕ) : + downMass up w (n + 1) = downMass up w n + (if up (n + 1) then 0 else w (n + 1)) := by + exact Finset.sum_range_succ _ _ + +lemma charging_up {up : ℕ → Bool} (w : ℕ → ℝ) {n : ℕ} (h : up (n + 1) = true) : + chargeValue w (charging up (n + 1)).active = 2 * w (n + 1) ∧ + chargeTotal w (charging up (n + 1)) = chargeTotal w (charging up n) + 2 * w (n + 1) := by + simp [charging, h, chargeValue, chargeTotal] + ring + +lemma charging_down {up : ℕ → Bool} (w : ℕ → ℝ) {n : ℕ} (h : up (n + 1) = false) : + chargeValue w (charging up (n + 1)).active = 2 * chargeValue w (charging up n).active ∧ + chargeTotal w (charging up (n + 1)) = + chargeTotal w (charging up n) + chargeValue w (charging up n).active := by + simp only [charging, h, Bool.false_eq_true, ↓reduceIte, chargeValue, pow_succ, + chargeTotal] + constructor <;> ring + +lemma charging_potential {up : ℕ → Bool} {w : ℕ → ℝ} + (hfirst : up 0 = false) (hw : ∀ n, 0 ≤ w n) + (hnext : ∀ n, w (n + 1) = if up n then w n / 4 else 4 * w n) (n : ℕ) : + chargeValue w (charging up n).active ≤ 16 * w n ∧ + (up n = true → chargeValue w (charging up n).active = 2 * w n) ∧ + chargeTotal w (charging up n) + (8 / 3) * w (n + 1) ≤ 16 * downMass up w n := by + induction n with + | zero => + have hn := hnext 0 + simp only [hfirst, Bool.false_eq_true, ↓reduceIte] at hn + simp only [charging, chargeValue, pow_zero, one_mul, chargeTotal, + List.map_nil, List.sum_nil, add_zero, downMass, Finset.sum_range_succ, + Finset.sum_range_zero, zero_add, hfirst, Bool.false_eq_true, ↓reduceIte, + false_implies, true_and] + constructor <;> nlinarith [hw 0] + | succ n ih => + have hm := charging_mass_succ up w n + have hn := hnext (n + 1) + cases hu : up (n + 1) with + | true => + obtain ⟨ha, hs⟩ := charging_up w hu + simp only [hu, ↓reduceIte, add_zero] at hm hn + refine ⟨?_, fun _ => ha, ?_⟩ + · rw [ha] + nlinarith [hw (n + 1)] + · rw [hs, hn, hm] + linarith [ih.2.2] + | false => + obtain ⟨ha, hs⟩ := charging_down w hu + simp only [hu, Bool.false_eq_true, ↓reduceIte] at hm hn + have hlast : chargeValue w (charging up n).active ≤ 8 * w (n + 1) := by + have hp := hnext n + cases hpup : up n with + | false => + simp only [hpup, Bool.false_eq_true, ↓reduceIte] at hp + nlinarith [ih.1, hw n] + | true => + simp only [hpup, ↓reduceIte] at hp + rw [ih.2.1 hpup] + linarith + refine ⟨?_, by simp [], ?_⟩ + · rw [ha] + linarith + · rw [hs, hn, hm] + linarith [ih.2.2] + +lemma charging_total_le {up : ℕ → Bool} {w : ℕ → ℝ} + (hfirst : up 0 = false) (hw : ∀ n, 0 ≤ w n) + (hnext : ∀ n, w (n + 1) = if up n then w n / 4 else 4 * w n) (n : ℕ) : + chargeTotal w (charging up n) ≤ 16 * downMass up w n := by + have h := (charging_potential hfirst hw hnext n).2.2 + nlinarith [hw (n + 1)] + +/-- The active block followed by all completed blocks. -/ +def chargingEntries (s : ChargingState) : List (ℕ × ℕ) := s.active :: s.past + +lemma charging_indices (up : ℕ → Bool) (n : ℕ) : + (charging up n).active.1 ≤ n ∧ + (∀ b ∈ (charging up n).past, b.1 < (charging up n).active.1) ∧ + (chargingEntries (charging up n)).Pairwise (fun a b => b.1 < a.1) ∧ + (∀ b ∈ chargingEntries (charging up n), b.1 = 0 ∨ up b.1 = true) := by + induction n with + | zero => simp [charging, chargingEntries] + | succ n ih => + cases hu : up (n + 1) with + | false => + simp only [charging, hu, Bool.false_eq_true, ↓reduceIte, chargingEntries, + List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at ih ⊢ + exact ⟨by omega, ih.2.1, ⟨ih.2.2.1.1, ih.2.2.1.2⟩, + ih.2.2.2.1, ih.2.2.2.2⟩ + | true => + have hb : ∀ b ∈ chargingEntries (charging up n), b.1 < n + 1 := by + intro b h + rcases List.mem_cons.mp h with h | h + · subst b; omega + · have ht := ih.2.1 b h; omega + change _ ∧ _ ∧ _ ∧ _ + simp only [charging, hu, ↓reduceIte, chargingEntries] + refine ⟨le_rfl, hb, List.pairwise_cons.mpr ⟨hb, ih.2.2.1⟩, ?_⟩ + intro b h + rcases List.mem_cons.mp h with h | h + · subst b; exact Or.inr hu + · exact ih.2.2.2 b h + +lemma charging_index_le (up : ℕ → Bool) (n : ℕ) (b : ℕ × ℕ) + (hb : b ∈ chargingEntries (charging up n)) : b.1 ≤ n := by + have h := charging_indices up n + rcases List.mem_cons.mp hb with hb | hb + · subst b; exact h.1 + · exact (h.2.1 b hb).le.trans h.1 + +/-- The total charge from blocks whose start precedes a given iteration. -/ +noncomputable def chargePrefix (w : ℕ → ℝ) (s : ChargingState) (t : ℕ) : ℝ := + (((chargingEntries s).filter (fun b => b.1 < t)).map (chargeValue w)).sum + +lemma charging_prefix_bound {up : ℕ → Bool} {w B : ℕ → ℝ} + (hB0 : 0 ≤ B 0) (hB : Monotone B) (htotal : ∀ n, chargeTotal w (charging up n) ≤ B n) (n : ℕ) : + ∀ b ∈ chargingEntries (charging up n), chargePrefix w (charging up n) b.1 ≤ B b.1 := by + induction n with + | zero => + intro b hb + simp only [charging, chargingEntries, List.mem_cons, List.not_mem_nil, or_false] at hb + subst b + simpa [chargePrefix, charging, chargingEntries] using hB0 + | succ n ih => + intro b hb + cases hu : up (n + 1) with + | true => + have he : chargingEntries (charging up (n + 1)) = + (n + 1, 1) :: chargingEntries (charging up n) := by + simp [charging, hu, chargingEntries] + rw [he] at hb + rcases List.mem_cons.mp hb with hb | hb + · subst b + have hfilter : (chargingEntries (charging up n)).filter + (fun b => b.1 < n + 1) = chargingEntries (charging up n) := by + apply List.filter_eq_self.mpr + intro b hb + simpa using Nat.lt_succ_of_le (charging_index_le up n b hb) + have hp : chargePrefix w (charging up (n + 1)) (n + 1) = + chargeTotal w (charging up n) := by + unfold chargePrefix + rw [he] + simp only [List.filter_cons, lt_self_iff_false, decide_false, + Bool.false_eq_true, ↓reduceIte] + rw [hfilter] + rfl + rw [hp] + exact (htotal n).trans (hB (Nat.le_succ n)) + · have ht : ¬n + 1 < b.1 := by + have hi := charging_index_le up n b hb + omega + have hp : chargePrefix w (charging up (n + 1)) b.1 = + chargePrefix w (charging up n) b.1 := by + simp [chargePrefix, he, ht] + rw [hp] + exact ih b hb + | false => + have hi := charging_indices up n + have he : chargingEntries (charging up (n + 1)) = + ((charging up n).active.1, (charging up n).active.2 + 1) :: + (charging up n).past := by + simp [charging, hu, chargingEntries] + rw [he] at hb + have hle : b.1 ≤ (charging up n).active.1 := by + rcases List.mem_cons.mp hb with hb | hb + · subst b; exact le_rfl + · exact (hi.2.1 b hb).le + have hp : chargePrefix w (charging up (n + 1)) b.1 = + chargePrefix w (charging up n) b.1 := by + unfold chargePrefix + rw [he] + simp [chargingEntries, not_lt_of_ge hle] + rw [hp] + rcases List.mem_cons.mp hb with hb | hb + · subst b + exact ih (charging up n).active List.mem_cons_self + · exact ih b (List.mem_cons_of_mem _ hb) + +lemma charging_count (up : ℕ → Bool) (n : ℕ) : + (charging up n).active.2 + ((charging up n).past.map Prod.snd).sum = n := by + induction n with + | zero => rfl + | succ n ih => + cases hu : up (n + 1) <;> + simp [charging, hu, List.map_cons, List.sum_cons] <;> omega + +lemma charging_nodup (up : ℕ → Bool) (n : ℕ) : + (chargingEntries (charging up n)).Nodup := by + have h := (charging_indices up n).2.2.1 + exact h.imp (fun {a b} hab he => by subst b; exact (Nat.lt_irrefl _ hab)) + +lemma charging_unique_index (up : ℕ → Bool) (n : ℕ) : + Set.InjOn Prod.fst {b | b ∈ chargingEntries (charging up n)} := by + have h : ((chargingEntries (charging up n)).map Prod.fst).Pairwise + (fun a b => b < a) := List.pairwise_map.mpr (charging_indices up n).2.2.1 + have hn : ((chargingEntries (charging up n)).map Prod.fst).Nodup := + h.imp (fun {a b} hab => Ne.symm (Nat.ne_of_lt hab)) + exact (List.nodup_map_iff_inj_on (charging_nodup up n)).mp hn + +/-- The finite set of active and completed charging blocks. -/ +def chargingSet (up : ℕ → Bool) (n : ℕ) : Finset (ℕ × ℕ) := + (chargingEntries (charging up n)).toFinset + +lemma charging_sum (up : ℕ → Bool) (n : ℕ) (w : ℕ → ℝ) : + (∑ b ∈ chargingSet up n, chargeValue w b) = chargeTotal w (charging up n) := by + rw [chargingSet, List.sum_toFinset _ (charging_nodup up n)] + rfl + +lemma charging_sum_count (up : ℕ → Bool) (n : ℕ) : + (∑ b ∈ chargingSet up n, b.2) = n := by + rw [chargingSet, List.sum_toFinset _ (charging_nodup up n)] + exact charging_count up n + +lemma charging_sum_prefix (up : ℕ → Bool) (n : ℕ) (w : ℕ → ℝ) (t : ℕ) : + (∑ b ∈ (chargingSet up n).filter (fun b => b.1 < t), chargeValue w b) = + chargePrefix w (charging up n) t := by + have h := List.sum_toFinset (chargeValue w) + ((charging_nodup up n).filter (fun b => decide (b.1 < t))) + simpa only [List.toFinset_filter, decide_eq_true_eq, chargingSet, chargePrefix] using h + +end LongTails.OracleTemplate.GeneralizedAccelerated diff --git a/LeanPool/LongTails/Proofs/GeneralizedConvergence.lean b/LeanPool/LongTails/Proofs/GeneralizedConvergence.lean new file mode 100644 index 000000000..d225d7aa4 --- /dev/null +++ b/LeanPool/LongTails/Proofs/GeneralizedConvergence.lean @@ -0,0 +1,197 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import LeanPool.LongTails.Proofs.GeneralizedMixedRate +public import LeanPool.LongTails.Proofs.DampedGeneralizedExecution + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +open Finset Set + +namespace LongTails.OracleTemplate.GeneralizedAccelerated + +open LongTails.Setups.GeneralizedSmoothAndConvex + +lemma root_log_le {A0 A : ℝ} (hA0 : 0 < A0) (hA : A0 ≤ A) : + Real.log (2 * A ^ (1 / 3 : ℝ) / A0 ^ (1 / 3 : ℝ)) ≤ Real.log (2 * A / A0) := by + have hAp : 0 < A := hA0.trans_le hA + have hroot0 := Real.rpow_pos_of_pos hA0 (1 / 3 : ℝ) + have hroot := Real.rpow_pos_of_pos hAp (1 / 3 : ℝ) + rw [Real.log_div (mul_pos (by norm_num) hroot).ne' hroot0.ne', + Real.log_mul (by norm_num : (2 : ℝ) ≠ 0) hroot.ne', + Real.log_div (mul_pos (by norm_num) hAp).ne' hA0.ne', + Real.log_mul (by norm_num : (2 : ℝ) ≠ 0) hAp.ne', + Real.log_rpow hAp, Real.log_rpow hA0] + have h := Real.log_le_log hA0 hA + linarith + +lemma high_log_simplify {A0 A a : ℝ} (hA0 : 0 < A0) (hA : A0 ≤ A) (ha : 0 ≤ a) : + let β := 1 / (64 * (1 + a ^ (2 / 3 : ℝ))) + 2 * Real.log (2 * A ^ (1 / 3 : ℝ) / A0 ^ (1 / 3 : ℝ)) / + (β * (2 * Real.log 2 / 3)) ≤ + 384 * (1 + a ^ (2 / 3 : ℝ)) * Real.log (2 * A / A0) := by + let t := a ^ (2 / 3 : ℝ) + have ht : 0 ≤ t := Real.rpow_nonneg ha _ + have hc : 0 < 2 * Real.log 2 / 3 := lt_of_lt_of_le (by norm_num) count_exponent_lower + have hden : 0 < 1 / (64 * (1 + t)) * (2 * Real.log 2 / 3) := by positivity + have hlog : 0 ≤ Real.log (2 * A / A0) := by + apply Real.log_nonneg + apply (le_div_iff₀ hA0).mpr + linarith + have hprod : 2 ≤ (384 * (1 + t)) * + (1 / (64 * (1 + t)) * (2 * Real.log 2 / 3)) := by + have he : (384 * (1 + t)) * (1 / (64 * (1 + t)) * (2 * Real.log 2 / 3)) = + 6 * (2 * Real.log 2 / 3) := by + have hd : 1 + t ≠ 0 := ne_of_gt (by positivity) + field_simp; ring + rw [he] + linarith [count_exponent_lower] + have hm := mul_le_mul_of_nonneg_right hprod hlog + apply (div_le_iff₀ hden).mpr + have hl := root_log_le hA0 hA + change _ ≤ 384 * (1 + t) * _ * _ + nlinarith only [hm, hl] + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] + +lemma run_count_positive {f : E → ℝ} {g : E → E} {L0 L1 R : ℝ} + (hL0 : 0 < L0) (hL1 : 0 < L1) (hR : 0 ≤ R) + (hc : ConvexOn ℝ univ f) (hg : ∀ x, HasGradientAt f (g x) x) + (hgd : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) + (s : Iterate E) (u : E) (hmin : IsMinOn f univ u) + (hA : 0 < s.A) (hG : 0 < s.guess) (hE : energy f u s ≤ R ^ 2) + (hfirst : localCurvature L0 L1 (g (coupling s)) = s.guess) (n : ℕ) : + (n : ℝ) ≤ 96 * Real.sqrt (L0 * (run L0 L1 g s (n + 1)).A) + + 384 * (1 + (L1 * R) ^ (2 / 3 : ℝ)) * + Real.log (2 * (run L0 L1 g s (n + 1)).A / s.A) := by + classical + let Q := chargingSet (runUp L0 L1 g s) n + let A := fun b : ℕ × ℕ => (run L0 L1 g s (b.1 + 1)).A + let G := fun b : ℕ × ℕ => (run L0 L1 g s b.1).guess + let M := fun b : ℕ × ℕ => localCurvature L0 L1 (g (coupling (run L0 L1 g s b.1))) + let low := Q.filter (fun b => M b ≤ 8 * L0) + let high := Q.filter (fun b => ¬M b ≤ 8 * L0) + let Afinal := (run L0 L1 g s (n + 1)).A + obtain ⟨hbase, hguess, hlow, henergy, hweights, hprefix, hinj, hsplit⟩ := + run_charging_geometry hL0 hL1 hc hg hgd hH s u hmin hA hG hE hfirst n + have hAF : s.A ≤ Afinal := hbase _ + have htune := mixed_tuning (mul_nonneg hL1.le hR) + have hh := high_count_log_bound high Prod.fst A G Prod.snd hA hAF + (fun b _ => hbase _) (fun b _ => hguess b.1) (by positivity) htune.1 htune.2.1 + hinj henergy hweights hprefix htune.2.2 + have hhigh := hh.trans (high_log_simplify hA hAF (mul_nonneg hL1.le hR)) + change (n : ℝ) ≤ 96 * Real.sqrt (L0 * Afinal) + _ + linarith only [hlow, hhigh, hsplit] + +omit [CompleteSpace E] in +lemma run_count_smooth {g : E → E} {L0 : ℝ} + (hL0 : 0 < L0) (s : Iterate E) (hA : 0 ≤ s.A) (hG : 0 < s.guess) + (hfirst : localCurvature L0 0 (g (coupling s)) = s.guess) (n : ℕ) : + (n : ℝ) ≤ 96 * Real.sqrt (L0 * (run L0 0 g s (n + 1)).A) := by + let Q := chargingSet (runUp L0 0 g s) n + let G := fun b : ℕ × ℕ => (run L0 0 g s b.1).guess + have hcharge := run_charging_bound (g := g) hL0 (le_refl 0) s hA hG hfirst.le n + have hgpos (b : ℕ × ℕ) : 0 < G b := (run_valid (g := g) hL0 (le_refl 0) s hA hG b.1).2 + have hbound : ∀ b ∈ Q, G b ≤ 8 * L0 := by + intro b hb + have hh := charging_selected_curvature s hfirst n b hb + simp only [localCurvature, zero_mul, add_zero] at hh + change G b ≤ _ at hh + linarith + have hweights : (∑ b ∈ Q, (2 : ℝ) ^ b.2 / Real.sqrt (G b)) ≤ + 32 * Real.sqrt (run L0 0 g s (n + 1)).A := by + simpa only [chargeValue, mul_one_div] using hcharge.1 + have h := low_count_sqrt_bound Q G Prod.snd hL0.le (fun b _ => hgpos b) hbound hweights + have hcount : (∑ b ∈ Q, (b.2 : ℝ)) = n := by + exact_mod_cast charging_sum_count (runUp L0 0 g s) n + rwa [hcount] at h + +lemma run_accuracy {f : E → ℝ} {g : E → E} {L0 L1 R Δ ε : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hR : 0 < R) (hΔ : 0 < Δ) (hε : 0 < ε) + (hc : ConvexOn ℝ univ f) (hg : ∀ x, HasGradientAt f (g x) x) + (hgd : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) + (x0 u : E) (hmin : IsMinOn f univ u) (hdist : ‖x0 - u‖ ≤ R) + (hgap : f x0 - f u ≤ Δ) (N : ℕ) + (hN : 4096 * (1 + Real.sqrt (L0 * R ^ 2 / ε) + + (⌈(L1 * R) ^ (2 / 3 : ℝ)⌉₊ : ℝ) * Real.log (4 + 4 * Δ / ε)) ≤ N) : + f (run L0 L1 g (initialIterate L0 L1 R Δ x0 g) N).x - f u ≤ ε := by + let s := initialIterate L0 L1 R Δ x0 g + let S := Real.sqrt (L0 * R ^ 2 / ε) + let C := (⌈(L1 * R) ^ (2 / 3 : ℝ)⌉₊ : ℝ) + let D := Real.log (4 + 4 * Δ / ε) + have hS : 0 ≤ S := Real.sqrt_nonneg _ + have hC : 0 ≤ C := Nat.cast_nonneg _ + have hD : 0 ≤ D := by + apply Real.log_nonneg + have ht : 0 < 4 * Δ / ε := by positivity + linarith + have hA : 0 < s.A := by dsimp [s, initialIterate]; positivity + have hG : 0 < s.guess := localCurvature_pos hL0 hL1 _ + have hfirst : localCurvature L0 L1 (g (coupling s)) = s.guess := + initial_first_down hL0 hL1 hΔ x0 + have hE : energy f u s ≤ R ^ 2 := initial_energy hΔ x0 u hdist hgap + have hNpos : 0 < N := by + change 4096 * (1 + S + C * D) ≤ (N : ℝ) at hN + have hn : (0 : ℝ) < N := by linarith only [hS, hN, mul_nonneg hC hD] + exact_mod_cast hn + obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hNpos) + change f (run L0 L1 g s (n + 1)).x - f u ≤ ε + by_contra hfail + have hfail' : ε < f (run L0 L1 g s (n + 1)).x - f u := lt_of_not_ge hfail + let Afinal := (run L0 L1 g s (n + 1)).A + have hAF : s.A ≤ Afinal := + run_weight_mono (g := g) hL0 hL1 s hA.le hG (Nat.zero_le _) + have hAFpos : 0 < Afinal := hA.trans_le hAF + have hsmall : Afinal ≤ R ^ 2 / ε := + run_weight_le_of_inaccurate hL0 hL1 hc hg hgd hH s u hA.le hG hE hε (n + 1) hfail' + have hsqrt : Real.sqrt (L0 * Afinal) ≤ S := by + apply Real.sqrt_le_sqrt + have hm := mul_le_mul_of_nonneg_left hsmall hL0.le + simpa only [mul_div_assoc] using hm + have hlog : Real.log (2 * Afinal / s.A) ≤ D := by + apply Real.log_le_log (by positivity) + have hm := div_le_div_of_nonneg_right + (mul_le_mul_of_nonneg_left hsmall (by norm_num : (0 : ℝ) ≤ 2)) hA.le + have he : 2 * (R ^ 2 / ε) / s.A = 4 * Δ / ε := by + dsimp [s, initialIterate] + field_simp; ring + rw [he] at hm + change 2 * Afinal / s.A ≤ 4 + 4 * Δ / ε + linarith only [hm] + have hcount : (n : ℝ) ≤ 96 * S + 768 * C * D := by + by_cases hz : L1 = 0 + · subst L1 + have hb := run_count_smooth hL0 s hA.le hG hfirst n + change (n : ℝ) ≤ 96 * Real.sqrt (L0 * Afinal) at hb + linarith only [hb, hsqrt, mul_nonneg hC hD] + · have hL1p : 0 < L1 := lt_of_le_of_ne hL1 (Ne.symm hz) + have hb := run_count_positive hL0 hL1p hR.le hc hg hgd hH s u hmin hA hG hE hfirst n + have htpos : 0 < (L1 * R) ^ (2 / 3 : ℝ) := Real.rpow_pos_of_pos (mul_pos hL1p hR) _ + have hceil : (L1 * R) ^ (2 / 3 : ℝ) ≤ C := Nat.le_ceil _ + have hCone : 1 ≤ C := by + have hh : 0 < ⌈(L1 * R) ^ (2 / 3 : ℝ)⌉₊ := Nat.ceil_pos.mpr htpos + have hh' : 1 ≤ ⌈(L1 * R) ^ (2 / 3 : ℝ)⌉₊ := hh + dsimp [C] + exact_mod_cast hh' + have hm := mul_le_mul_of_nonneg_left hlog + (show 0 ≤ 384 * (1 + (L1 * R) ^ (2 / 3 : ℝ)) by positivity) + have hm' := mul_le_mul_of_nonneg_right + (show 384 * (1 + (L1 * R) ^ (2 / 3 : ℝ)) ≤ 768 * C by linarith) hD + change (n : ℝ) ≤ 96 * Real.sqrt (L0 * Afinal) + _ at hb + nlinarith only [hb, hsqrt, hm, hm'] + change 4096 * (1 + S + C * D) ≤ ((n + 1 : ℕ) : ℝ) at hN + push_cast at hN + linarith only [hS, hN, hcount, mul_nonneg hC hD] + +end LongTails.OracleTemplate.GeneralizedAccelerated diff --git a/LeanPool/LongTails/Proofs/GeneralizedGradientStep.lean b/LeanPool/LongTails/Proofs/GeneralizedGradientStep.lean new file mode 100644 index 000000000..fca271908 --- /dev/null +++ b/LeanPool/LongTails/Proofs/GeneralizedGradientStep.lean @@ -0,0 +1,169 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import LeanPool.LongTails.Algorithms.DampedGeneralizedAccelerated +public import Mathlib.Analysis.ODE.Gronwall +public import Mathlib.Tactic.Convert +public import Mathlib.Tactic.FieldSimp +public import Mathlib.Tactic.GCongr +public import Mathlib.Tactic.Linarith +public import Mathlib.Tactic.Module +public import Mathlib.Tactic.NormNum +public import Mathlib.Tactic.Positivity +public import Mathlib.Tactic.Ring + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +open Set InnerProductSpace +open scoped RealInnerProductSpace + +namespace LongTails.OracleTemplate.GeneralizedAccelerated + +open LongTails.Setups.GeneralizedSmoothAndConvex + +lemma gronwall_unit_bound {K c : ℝ} (hK : 0 ≤ K) (hc : 0 ≤ c) : + gronwallBound 0 K c 1 ≤ c * Real.exp K := by + by_cases hz : K = 0 + · simp [hz, gronwallBound_K0] + · have hpos : 0 < K := lt_of_le_of_ne hK (Ne.symm hz) + rw [gronwallBound_of_K_ne_0 hz] + simp only [zero_mul, zero_add, mul_one] + have he := mul_le_mul_of_nonneg_right (Real.one_sub_le_exp_neg K) + (Real.exp_pos K).le + rw [← Real.exp_add] at he + simp only [neg_add_cancel, Real.exp_zero] at he + have he' : Real.exp K - 1 ≤ K * Real.exp K := by nlinarith + have hm := mul_le_mul_of_nonneg_left he' (div_nonneg hc hK) + calc + c / K * (Real.exp K - 1) ≤ c / K * (K * Real.exp K) := hm + _ = c * Real.exp K := by field_simp + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] + +omit [CompleteSpace E] in +lemma gradient_growth {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 ≤ L0) (hL1 : 0 ≤ L1) (hg : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) (x y : E) : + ‖g x - g y‖ ≤ (L0 + L1 * ‖g y‖) * + Real.exp (L1 * ‖x - y‖) * ‖x - y‖ := by + let d := x - y + let F := fun t : ℝ => g (y + t • d) - g y + let F' := fun t : ℝ => (fderiv ℝ g (y + t • d)) d + have hF : ∀ t, HasDerivAt F (F' t) t := by + intro t + simpa [F, F'] using + (((hg (y + t • d)).hasFDerivAt.comp_hasDerivAt t + ((hasDerivAt_id t).smul_const d |>.const_add y)).sub_const (g y)) + have hbound : ∀ t, ‖F' t‖ ≤ (L1 * ‖d‖) * ‖F t‖ + + (L0 + L1 * ‖g y‖) * ‖d‖ := by + intro t + calc + ‖F' t‖ ≤ ‖fderiv ℝ g (y + t • d)‖ * ‖d‖ := + ContinuousLinearMap.le_opNorm _ _ + _ ≤ (L0 + L1 * ‖g (y + t • d)‖) * ‖d‖ := + mul_le_mul_of_nonneg_right (hH _) (norm_nonneg _) + _ ≤ (L0 + L1 * (‖F t‖ + ‖g y‖)) * ‖d‖ := by + gcongr + exact norm_le_norm_sub_add _ _ + _ = (L1 * ‖d‖) * ‖F t‖ + (L0 + L1 * ‖g y‖) * ‖d‖ := by ring + have h := norm_le_gronwallBound_of_norm_deriv_right_le + (show ContinuousOn F (Icc 0 1) from + (continuous_iff_continuousAt.mpr (fun t => (hF t).continuousAt)).continuousOn) + (fun t _ => (hF t).hasDerivWithinAt) + (show ‖F 0‖ ≤ (0 : ℝ) by simp [F]) (fun t _ => hbound t) + 1 (by norm_num : (1 : ℝ) ∈ Icc 0 1) + have hb := gronwall_unit_bound (K := L1 * ‖d‖) + (c := (L0 + L1 * ‖g y‖) * ‖d‖) (by positivity) (by positivity) + simp only [sub_zero] at h + have hr := h.trans hb + simpa [F, d, mul_assoc, mul_left_comm, mul_comm] using hr + +omit [InnerProductSpace ℝ E] [CompleteSpace E] in +lemma localCurvature_pos {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (g : E) : + 0 < localCurvature L0 L1 g := by + unfold localCurvature + positivity + +omit [CompleteSpace E] in +lemma local_step_norm {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (y g : E) : + ‖y - (1 / localCurvature L0 L1 g) • g - y‖ = + ‖g‖ / localCurvature L0 L1 g := by + have he : y - (1 / localCurvature L0 L1 g) • g - y = + -(1 / localCurvature L0 L1 g) • g := by module + rw [he, norm_smul, Real.norm_eq_abs, abs_neg, + abs_of_pos (one_div_pos.mpr (localCurvature_pos hL0 hL1 g))] + ring + +omit [CompleteSpace E] in +lemma local_step_gradient_error {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hg : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) (y : E) : + ‖g (y - (1 / localCurvature L0 L1 (g y)) • g y) - g y‖ ≤ ‖g y‖ / 2 := by + have hcurv := localCurvature_pos hL0 hL1 (g y) + have hdist := local_step_norm hL0 hL1 y (g y) + have hsmall : L1 * (‖g y‖ / localCurvature L0 L1 (g y)) ≤ 1 / 4 := by + rw [← mul_div_assoc] + apply (div_le_iff₀ hcurv).mpr + unfold localCurvature + nlinarith + have hexp : Real.exp (L1 * (‖g y‖ / localCurvature L0 L1 (g y))) ≤ 2 := by + apply (Real.exp_le_exp.mpr hsmall).trans + have h := Real.exp_bound_div_one_sub_of_interval (x := (1 / 4 : ℝ)) + (by norm_num) (by norm_num) + norm_num at h + linarith + have hb := gradient_growth hL0.le hL1 hg hH + (y - (1 / localCurvature L0 L1 (g y)) • g y) y + rw [hdist] at hb + calc + _ ≤ (L0 + L1 * ‖g y‖) * + Real.exp (L1 * (‖g y‖ / localCurvature L0 L1 (g y))) * + (‖g y‖ / localCurvature L0 L1 (g y)) := hb + _ ≤ (L0 + L1 * ‖g y‖) * 2 * (‖g y‖ / localCurvature L0 L1 (g y)) := by + gcongr + _ = ‖g y‖ / 2 := by + have hc : L0 + L1 * ‖g y‖ ≠ 0 := ne_of_gt (by positivity) + unfold localCurvature + field_simp; ring + +omit [CompleteSpace E] in +lemma local_step_residual {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hg : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) (y : E) : + let M := localCurvature L0 L1 (g y) + let w := y - (1 / M) • g y + ‖g w + M • (w - y)‖ ≤ M / 2 * ‖w - y‖ := by + dsimp only + have hM := localCurvature_pos hL0 hL1 (g y) + have he : localCurvature L0 L1 (g y) • + (y - (1 / localCurvature L0 L1 (g y)) • g y - y) = -g y := by + match_scalars + all_goals field_simp [hM.ne'] <;> ring + rw [he, ← sub_eq_add_neg, local_step_norm hL0 hL1 y (g y)] + convert local_step_gradient_error hL0 hL1 hg hH y using 1 + field_simp + + +omit [CompleteSpace E] in +lemma local_step_movement {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 < L1) (y g : E) : + localCurvature L0 L1 g ≤ 8 * L0 ∨ + 1 / (8 * L1) ≤ ‖y - (1 / localCurvature L0 L1 g) • g - y‖ := by + by_cases hsmall : localCurvature L0 L1 g ≤ 8 * L0 + · exact Or.inl hsmall + · right + rw [local_step_norm hL0 hL1.le y g] + apply (div_le_div_iff₀ (by positivity : (0 : ℝ) < 8 * L1) + (localCurvature_pos hL0 hL1.le g)).mpr + unfold localCurvature at hsmall ⊢ + nlinarith + +end LongTails.OracleTemplate.GeneralizedAccelerated diff --git a/LeanPool/LongTails/Proofs/GeneralizedLogCharging.lean b/LeanPool/LongTails/Proofs/GeneralizedLogCharging.lean new file mode 100644 index 000000000..3721ece98 --- /dev/null +++ b/LeanPool/LongTails/Proofs/GeneralizedLogCharging.lean @@ -0,0 +1,268 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import LeanPool.LongTails.Proofs.GeneralizedMixedRate + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +open Finset + +namespace LongTails.OracleTemplate.GeneralizedAccelerated + +open LongTails.Setups.GeneralizedSmoothAndConvex + +lemma exp_sub_one_le_mul_exp (d : ℝ) : + Real.exp d - 1 ≤ d * Real.exp d := by + have h := Real.add_one_le_exp (-d) + have h' := mul_le_mul_of_nonneg_right h (Real.exp_pos d).le + rw [← Real.exp_add] at h' + simp only [neg_add_cancel, Real.exp_zero] at h' + nlinarith + +lemma nat_cube_le_exp_two (q : ℕ) : (q : ℝ) ^ 3 ≤ 48 * (2 : ℝ) ^ q := by + have hlog : (1 / 2 : ℝ) ≤ Real.log 2 := by + have h := Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 1 / 2) + norm_num [Real.log_div] at h + linarith + have h := Real.pow_div_factorial_le_exp (Real.log 2 * (q : ℝ)) + (show 0 ≤ Real.log 2 * (q : ℝ) by positivity) 3 + norm_num [mul_comm (Real.log 2), Real.exp_nat_mul, Real.exp_log (by norm_num : (0 : ℝ) < 2)] at h + have hp := pow_le_pow_left₀ (show (0 : ℝ) ≤ 1 / 2 * (q : ℝ) by positivity) + (mul_le_mul_of_nonneg_right hlog (Nat.cast_nonneg q)) 3 + nlinarith + +lemma logarithmic_charge_cube {u d : ℝ} (hu : 0 < u) (hd : 0 < d) + (q : ℕ) (h : (2 : ℝ) ^ q ≤ 64 * Real.sqrt u * (Real.exp d - 1)) : + (max 0 ((q : ℝ) - 4 * d)) ^ 3 ≤ 262144 * u * d ^ 2 := by + by_cases hlarge : (q : ℝ) ≤ 4 * d + · rw [max_eq_left (by linarith), zero_pow (by decide : 3 ≠ 0)] + positivity + · have hsmall : 2 * d ≤ Real.log 2 * q := by + have hlog : (1 / 2 : ℝ) ≤ Real.log 2 := by + have ht := Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 1 / 2) + norm_num [Real.log_div] at ht + linarith + nlinarith [mul_le_mul_of_nonneg_right hlog (Nat.cast_nonneg q)] + have he : Real.exp (2 * d) ≤ (2 : ℝ) ^ q := by + have ht := Real.exp_le_exp.mpr hsmall + simpa [mul_comm (Real.log 2), Real.exp_nat_mul, + Real.exp_log (by norm_num : (0 : ℝ) < 2)] using ht + have ht := exp_sub_one_le_mul_exp d + have hs : (2 : ℝ) ^ q ≤ 64 * Real.sqrt u * (d * Real.exp d) := + h.trans (mul_le_mul_of_nonneg_left ht (by positivity)) + have hs2 := pow_le_pow_left₀ (show 0 ≤ (2 : ℝ) ^ q by positivity) hs 2 + have hexp : (Real.exp d) ^ 2 = Real.exp (2 * d) := by + rw [pow_two, ← Real.exp_add] + congr 1 + ring + simp only [mul_pow, Real.sq_sqrt hu.le, hexp] at hs2 + have hm := mul_le_mul_of_nonneg_left he (show 0 ≤ 4096 * u * d ^ 2 by positivity) + have hb : (2 : ℝ) ^ q ≤ 4096 * u * d ^ 2 := by + apply (mul_le_mul_iff_right₀ (show 0 < (2 : ℝ) ^ q by positivity)).mp + nlinarith only [hs2, hm] + have hc := nat_cube_le_exp_two q + have hpow := pow_le_pow_left₀ (show 0 ≤ (q : ℝ) - 4 * d by linarith) + (show (q : ℝ) - 4 * d ≤ (q : ℝ) by linarith) 3 + rw [max_eq_right (by linarith)] + nlinarith [mul_nonneg hu.le (sq_nonneg d)] + +lemma ordered_log_telescope {ι : Type*} + (s : Finset ι) (time : ι → ℕ) (w : ι → ℝ) (B : ℝ) + (hinj : Set.InjOn time (s : Set ι)) : + (∑ i ∈ s, (Real.log (B + ∑ j ∈ s.filter (fun j => time j ≤ time i), w j) - + Real.log (B + ∑ j ∈ s.filter (fun j => time j < time i), w j))) = + Real.log (B + ∑ i ∈ s, w i) - Real.log B := by + classical + induction s using Finset.induction_on_max_value time with + | empty => simp + | insert a t ha hmax ih => + have hinjt : Set.InjOn time (t : Set ι) := + hinj.mono (by exact_mod_cast (subset_insert a t)) + have hlt : ∀ i ∈ t, time i < time a := by + intro i hi + apply lt_of_le_of_ne (hmax i hi) + intro he + have heq := hinj (mem_insert_of_mem hi) (mem_insert_self a t) he + exact ha (heq ▸ hi) + have hle_a : (insert a t).filter (fun j => time j ≤ time a) = insert a t := by + apply filter_eq_self.mpr + intro i hi + rcases mem_insert.mp hi with rfl | hi + · exact le_rfl + · exact hmax i hi + have hlt_a : (insert a t).filter (fun j => time j < time a) = t := by + ext i + simp only [mem_filter, mem_insert] + constructor + · rintro ⟨rfl | hi, hh⟩ + · exact (lt_irrefl _ hh).elim + · exact hi + · intro hi + exact ⟨Or.inr hi, hlt i hi⟩ + have hle_i (i : ι) (hi : i ∈ t) : + (insert a t).filter (fun j => time j ≤ time i) = t.filter (fun j => time j ≤ time i) := by + rw [filter_insert] + simp [not_le.mpr (hlt i hi)] + have hlt_i (i : ι) (hi : i ∈ t) : + (insert a t).filter (fun j => time j < time i) = t.filter (fun j => time j < time i) := by + rw [filter_insert] + simp [not_lt.mpr (hmax i hi)] + rw [sum_insert ha, hle_a, hlt_a] + have heq : (∑ i ∈ t, (Real.log (B + ∑ j ∈ (insert a t).filter (fun j => time j ≤ time i), w j) - + Real.log (B + ∑ j ∈ (insert a t).filter (fun j => time j < time i), w j))) = + Real.log (B + ∑ i ∈ t, w i) - Real.log B := by + convert ih hinjt using 1 + apply sum_congr rfl + intro i hi + rw [hle_i i hi, hlt_i i hi] + rw [heq] + ring + +lemma ordered_log_increments {ι : Type*} + (s : Finset ι) (time : ι → ℕ) (w : ι → ℝ) {B : ℝ} + (hB : 0 < B) (hw : ∀ i ∈ s, 0 < w i) + (hinj : Set.InjOn time (s : Set ι)) : + (∑ i ∈ s, Real.log (1 + w i / + (B + ∑ j ∈ s.filter (fun j => time j < time i), w j))) = + Real.log ((B + ∑ i ∈ s, w i) / B) := by + classical + have htotal : 0 < B + ∑ i ∈ s, w i := + add_pos_of_pos_of_nonneg hB (sum_nonneg (fun i hi => (hw i hi).le)) + rw [Real.log_div htotal.ne' hB.ne', ← ordered_log_telescope s time w B hinj] + apply sum_congr rfl + intro i hi + have hWi : 0 < B + ∑ j ∈ s.filter (fun j => time j < time i), w j := + add_pos_of_pos_of_nonneg hB (sum_nonneg (fun j hj => (hw j (mem_filter.mp hj).1).le)) + have hf : s.filter (fun j => time j ≤ time i) = + insert i (s.filter (fun j => time j < time i)) := by + ext j + simp only [mem_filter, mem_insert] + constructor + · rintro ⟨hj, hji⟩ + rcases lt_or_eq_of_le hji with hlt | heq + · exact Or.inr ⟨hj, hlt⟩ + · exact Or.inl (hinj hj hi heq) + · rintro (rfl | ⟨hj, hji⟩) + · exact ⟨hi, le_rfl⟩ + · exact ⟨hj, hji.le⟩ + rw [hf, sum_insert (by simp)] + have he : 1 + w i / (B + ∑ j ∈ s.filter (fun j => time j < time i), w j) = + (B + (w i + ∑ j ∈ s.filter (fun j => time j < time i), w j)) / + (B + ∑ j ∈ s.filter (fun j => time j < time i), w j) := by + field_simp + ring + rw [he, Real.log_div (by linarith [hw i hi]) hWi.ne'] + +lemma high_count_self_normalized {ι : Type*} + (s : Finset ι) (time : ι → ℕ) (A G : ι → ℝ) (q : ι → ℕ) + {A0 Afinal H : ℝ} (hA0 : 0 < A0) (hAF : A0 ≤ Afinal) + (hA : ∀ i ∈ s, A0 ≤ A i) (hG : ∀ i ∈ s, 0 < G i) + (hH : 0 ≤ H) (hinj : Set.InjOn time (s : Set ι)) + (henergy : (∑ i ∈ s, A i * G i) ≤ H) + (hweights : (∑ i ∈ s, (2 : ℝ) ^ q i / Real.sqrt (G i)) ≤ 32 * Real.sqrt Afinal) + (hprefix : ∀ i ∈ s, + (∑ j ∈ s.filter (fun j => time j < time i), (2 : ℝ) ^ q j / Real.sqrt (G j)) ≤ + 32 * Real.sqrt (A i)) : + let D := Real.log (2 * Afinal / A0) + (∑ i ∈ s, (q i : ℝ)) ≤ 4 * D + 64 * (H * D ^ 2) ^ (1 / 3 : ℝ) := by + classical + let w := fun i => (2 : ℝ) ^ q i / Real.sqrt (G i) + let B := 32 * Real.sqrt A0 + let W := fun i => B + ∑ j ∈ s.filter (fun j => time j < time i), w j + let d := fun i => Real.log (1 + w i / W i) + let z := fun i => max 0 ((q i : ℝ) - 4 * d i) + let D := Real.log (2 * Afinal / A0) + have hB : 0 < B := by dsimp [B]; positivity + have hw : ∀ i ∈ s, 0 < w i := by + intro i hi + exact div_pos (by positivity) (Real.sqrt_pos.mpr (hG i hi)) + have hW : ∀ i ∈ s, 0 < W i := by + intro i hi + exact add_pos_of_pos_of_nonneg hB + (sum_nonneg (fun j hj => (hw j (mem_filter.mp hj).1).le)) + have hd : ∀ i ∈ s, 0 < d i := by + intro i hi + apply Real.log_pos + have hh := div_pos (hw i hi) (hW i hi) + change 1 < 1 + w i / W i + linarith + have hz : ∀ i ∈ s, 0 ≤ z i := fun _ _ => le_max_left _ _ + have hAi : ∀ i ∈ s, 0 < A i := fun i hi => hA0.trans_le (hA i hi) + have hWi : ∀ i ∈ s, W i ≤ 64 * Real.sqrt (A i) := by + intro i hi + have hh := Real.sqrt_le_sqrt (hA i hi) + have hp := hprefix i hi + change (∑ j ∈ s.filter (fun j => time j < time i), w j) ≤ _ at hp + dsimp only [W, B] + linarith + have hcube : ∀ i ∈ s, z i ^ 3 ≤ (262144 * (A i * G i)) * d i ^ 2 := by + intro i hi + have he : Real.exp (d i) - 1 = w i / W i := by + dsimp only [d] + rw [Real.exp_log (by linarith [div_pos (hw i hi) (hW i hi)])] + ring + have ht : (2 : ℝ) ^ q i ≤ 64 * Real.sqrt (A i * G i) * (Real.exp (d i) - 1) := by + rw [he, Real.sqrt_mul (hAi i hi).le] + dsimp only [w] + have hGi := (Real.sqrt_pos.mpr (hG i hi)).ne' + have hWi0 := (hW i hi).ne' + have hid : 64 * (Real.sqrt (A i) * Real.sqrt (G i)) * + ((2 : ℝ) ^ q i / Real.sqrt (G i) / W i) = + (64 * Real.sqrt (A i) * (2 : ℝ) ^ q i) / W i := by + field_simp + rw [hid] + apply (le_div_iff₀ (hW i hi)).mpr + have hh := mul_le_mul_of_nonneg_left (hWi i hi) (show 0 ≤ (2 : ℝ) ^ q i by positivity) + nlinarith only [hh] + exact logarithmic_charge_cube (mul_pos (hAi i hi) (hG i hi)) (hd i hi) (q i) ht + have hholder := weighted_holder_cube s (fun i => 262144 * (A i * G i)) d z + (fun i hi => mul_nonneg (by norm_num) (mul_nonneg (hAi i hi).le (hG i hi).le)) hd hz hcube + have hsumd : (∑ i ∈ s, d i) ≤ D := by + rw [show (∑ i ∈ s, d i) = Real.log ((B + ∑ i ∈ s, w i) / B) from + ordered_log_increments s time w hB hw hinj] + have hsumw := sum_nonneg (fun i hi => (hw i hi).le) + apply Real.log_le_log (by positivity) + apply (div_le_div_iff₀ hB hA0).mpr + have hp := hweights + change (∑ i ∈ s, w i) ≤ 32 * Real.sqrt Afinal at hp + have hs0 := Real.sq_sqrt hA0.le + have hsF := Real.sq_sqrt (hA0.le.trans hAF) + have hs := Real.sqrt_le_sqrt hAF + have hm := mul_le_mul_of_nonneg_right hs (Real.sqrt_nonneg Afinal) + have ht := mul_le_mul_of_nonneg_right hp hA0.le + dsimp only [B] + nlinarith [Real.sqrt_nonneg A0, Real.sqrt_nonneg Afinal] + have hD : 0 ≤ D := (sum_nonneg (fun i hi => (hd i hi).le)).trans hsumd + have hdsq := pow_le_pow_left₀ (sum_nonneg (fun i hi => (hd i hi).le)) hsumd 2 + have hbound : (∑ i ∈ s, z i) ^ 3 ≤ 262144 * (H * D ^ 2) := by + rw [← mul_sum] at hholder + have hm := mul_le_mul henergy hdsq (sq_nonneg _) hH + nlinarith only [hholder, hm] + have hroot : ((H * D ^ 2) ^ (1 / 3 : ℝ)) ^ 3 = H * D ^ 2 := by + rw [← Real.rpow_natCast, ← Real.rpow_mul (by positivity : 0 ≤ H * D ^ 2)] + norm_num + have hzbound : (∑ i ∈ s, z i) ≤ 64 * (H * D ^ 2) ^ (1 / 3 : ℝ) := by + apply (pow_le_pow_iff_left₀ (sum_nonneg hz) (by positivity) (by decide : 3 ≠ 0)).mp + rw [mul_pow, hroot] + norm_num + exact hbound + have hcount : (∑ i ∈ s, (q i : ℝ)) ≤ 4 * (∑ i ∈ s, d i) + ∑ i ∈ s, z i := by + rw [mul_sum, ← sum_add_distrib] + apply sum_le_sum + intro i hi + have hh := le_max_right 0 ((q i : ℝ) - 4 * d i) + dsimp only [z] + linarith + change (∑ i ∈ s, (q i : ℝ)) ≤ 4 * D + _ + linarith + +end LongTails.OracleTemplate.GeneralizedAccelerated diff --git a/LeanPool/LongTails/Proofs/GeneralizedMixedRate.lean b/LeanPool/LongTails/Proofs/GeneralizedMixedRate.lean new file mode 100644 index 000000000..c5b726aa8 --- /dev/null +++ b/LeanPool/LongTails/Proofs/GeneralizedMixedRate.lean @@ -0,0 +1,472 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import Mathlib.Analysis.Convex.SpecificFunctions.Basic +public import Mathlib.Data.Finset.Max +public import LeanPool.LongTails.Proofs.DampedGeneralizedDynamics +public import LeanPool.LongTails.Proofs.GeneralizedCharging + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +open Finset + +namespace LongTails.OracleTemplate.GeneralizedAccelerated + +open LongTails.Setups.GeneralizedSmoothAndConvex + +lemma weighted_holder_cube {ι : Type*} (s : Finset ι) (x y z : ι → ℝ) + (hx : ∀ i ∈ s, 0 ≤ x i) (hy : ∀ i ∈ s, 0 < y i) + (hz : ∀ i ∈ s, 0 ≤ z i) (hxyz : ∀ i ∈ s, z i ^ 3 ≤ x i * y i ^ 2) : + (∑ i ∈ s, z i) ^ 3 ≤ (∑ i ∈ s, x i) * (∑ i ∈ s, y i) ^ 2 := by + let v := fun i => z i ^ 2 / y i + have hv : ∀ i ∈ s, 0 ≤ v i := fun i hi => div_nonneg (sq_nonneg _) (hy i hi).le + have hfirst : (∑ i ∈ s, z i) ^ 2 ≤ (∑ i ∈ s, v i) * (∑ i ∈ s, y i) := by + apply sum_sq_le_sum_mul_sum_of_sq_le_mul s hv (fun i hi => (hy i hi).le) + intro i hi + simp [v, (hy i hi).ne'] + have hsecond : (∑ i ∈ s, v i) ^ 2 ≤ (∑ i ∈ s, x i) * (∑ i ∈ s, z i) := by + apply sum_sq_le_sum_mul_sum_of_sq_le_mul s hx hz + intro i hi + dsimp [v] + rw [div_pow] + apply (div_le_iff₀ (sq_pos_of_pos (hy i hi))).mpr + have h := mul_le_mul_of_nonneg_right (hxyz i hi) (hz i hi) + nlinarith only [h] + have hsum : 0 ≤ ∑ i ∈ s, z i := sum_nonneg hz + have hsquare := mul_self_le_mul_self (sq_nonneg (∑ i ∈ s, z i)) hfirst + have hmul := mul_le_mul_of_nonneg_right hsecond (sq_nonneg (∑ i ∈ s, y i)) + by_cases hzero : ∑ i ∈ s, z i = 0 + · rw [hzero] + simpa only [zero_pow (by decide : 3 ≠ 0)] using + mul_nonneg (sum_nonneg hx) (sq_nonneg (∑ i ∈ s, y i)) + · have hpos : 0 < ∑ i ∈ s, z i := lt_of_le_of_ne hsum (Ne.symm hzero) + apply (mul_le_mul_iff_left₀ hpos).mp + nlinarith only [hsquare, hmul] + +lemma weighted_exp_cube (A : ℝ) (hA : 0 ≤ A) (q : ℕ) : + (A ^ (1 / 3 : ℝ) * Real.exp ((2 * Real.log 2 / 3) * q)) ^ 3 = + A * ((2 : ℝ) ^ q) ^ 2 := by + have hroot : (A ^ (1 / 3 : ℝ)) ^ 3 = A := by + rw [← Real.rpow_natCast, ← Real.rpow_mul hA] + norm_num + have ht : (2 : ℝ) ^ q = Real.exp ((q : ℝ) * Real.log 2) := by + rw [Real.exp_nat_mul, Real.exp_log (by norm_num : (0 : ℝ) < 2)] + rw [mul_pow, hroot, ht, ← Real.exp_nat_mul, ← Real.exp_nat_mul] + congr 2 + ring + +lemma weighted_curvature_holder {ι : Type*} (s : Finset ι) (A G : ι → ℝ) (q : ι → ℕ) + (hA : ∀ i ∈ s, 0 ≤ A i) (hG : ∀ i ∈ s, 0 < G i) : + (∑ i ∈ s, A i ^ (1 / 3 : ℝ) * Real.exp ((2 * Real.log 2 / 3) * q i)) ^ 3 ≤ + (∑ i ∈ s, A i * G i) * (∑ i ∈ s, (2 : ℝ) ^ q i / Real.sqrt (G i)) ^ 2 := by + apply weighted_holder_cube s (fun i => A i * G i) + (fun i => (2 : ℝ) ^ q i / Real.sqrt (G i)) + (fun i => A i ^ (1 / 3 : ℝ) * Real.exp ((2 * Real.log 2 / 3) * q i)) + (fun i hi => mul_nonneg (hA i hi) (hG i hi).le) + (fun i hi => div_pos (by positivity) (Real.sqrt_pos.mpr (hG i hi))) + (fun i hi => mul_nonneg (Real.rpow_nonneg (hA i hi) _) (Real.exp_pos _).le) + intro i hi + rw [weighted_exp_cube _ (hA i hi), div_pow, Real.sq_sqrt (hG i hi).le] + have he : A i * G i * ((2 ^ q i) ^ 2 / G i) = A i * (2 ^ q i) ^ 2 := by + field_simp [(hG i hi).ne'] + rw [he] + +lemma weighted_curvature_growth {ι : Type*} (s : Finset ι) (A G : ι → ℝ) (q : ι → ℕ) + {H C β Afinal : ℝ} (hA : ∀ i ∈ s, 0 ≤ A i) (hG : ∀ i ∈ s, 0 < G i) + (hH : 0 ≤ H) (hβ : 0 ≤ β) (hAf : 0 ≤ Afinal) + (henergy : (∑ i ∈ s, A i * G i) ≤ H) + (hweights : (∑ i ∈ s, (2 : ℝ) ^ q i / Real.sqrt (G i)) ≤ C * Real.sqrt Afinal) + (htuning : β ^ 3 * H * C ^ 2 ≤ 1) : + β * (∑ i ∈ s, A i ^ (1 / 3 : ℝ) * Real.exp ((2 * Real.log 2 / 3) * q i)) ≤ + Afinal ^ (1 / 3 : ℝ) := by + have hw : 0 ≤ ∑ i ∈ s, (2 : ℝ) ^ q i / Real.sqrt (G i) := by + apply sum_nonneg + intro i hi + positivity + have hz : 0 ≤ ∑ i ∈ s, A i ^ (1 / 3 : ℝ) * Real.exp ((2 * Real.log 2 / 3) * q i) := by + apply sum_nonneg + intro i hi + exact mul_nonneg (Real.rpow_nonneg (hA i hi) _) (Real.exp_pos _).le + have hw2 := pow_le_pow_left₀ hw hweights 2 + have hb := mul_le_mul henergy hw2 (sq_nonneg _) hH + rw [mul_pow, Real.sq_sqrt hAf] at hb + have hh := (weighted_curvature_holder s A G q hA hG).trans hb + have hh' := mul_le_mul_of_nonneg_left hh (pow_nonneg hβ 3) + have ht := mul_le_mul_of_nonneg_right htuning hAf + have hroot : (Afinal ^ (1 / 3 : ℝ)) ^ 3 = Afinal := by + rw [← Real.rpow_natCast, ← Real.rpow_mul hAf] + norm_num + apply (pow_le_pow_iff_left₀ (mul_nonneg hβ hz) (Real.rpow_nonneg hAf _) (by decide : 3 ≠ 0)).mp + nlinarith only [hh', ht, hroot] + +lemma exp_growth_log_bound {B0 β c S Bfinal : ℝ} + (hB0 : 0 < B0) (hβ : 0 < β) (hc : 0 < c) (hBf : 0 < Bfinal) + (h : B0 / 2 * Real.exp (β * c / 2 * S) ≤ Bfinal) : + S ≤ 2 * Real.log (2 * Bfinal / B0) / (β * c) := by + have he : Real.exp (β * c / 2 * S) ≤ 2 * Bfinal / B0 := by + apply (le_div_iff₀ hB0).mpr + nlinarith only [h] + have hl := (Real.le_log_iff_exp_le (show 0 < 2 * Bfinal / B0 by positivity)).mpr he + apply (le_div_iff₀ (mul_pos hβ hc)).mpr + nlinarith only [hl] + +lemma exp_scaled_le {θ : ℝ} (hθ : 0 ≤ θ) (hθ1 : θ ≤ 1) (x : ℝ) : + Real.exp (θ * x) ≤ 1 + θ * Real.exp x := by + have h := convexOn_exp.2 (Set.mem_univ (0 : ℝ)) (Set.mem_univ x) + (show 0 ≤ 1 - θ by linarith) hθ (show 1 - θ + θ = 1 by ring) + simp only [smul_eq_mul, mul_zero, zero_add, Real.exp_zero, mul_one] at h + linarith + +lemma finite_prefix_exponential_growth {ι : Type*} + (s : Finset ι) (time : ι → ℕ) (B r : ι → ℝ) {B0 β c Bfinal : ℝ} + (hB0 : 0 < B0) (hβ : 0 < β) (hβ1 : β ≤ 1) + (hinj : Set.InjOn time (s : Set ι)) + (hbase : ∀ i ∈ s, B0 ≤ B i) + (hprefix : ∀ i ∈ s, + β * (∑ j ∈ s.filter (fun j => time j < time i), B j * Real.exp (c * r j)) ≤ B i) + (hfinalbase : B0 ≤ Bfinal) + (hfinal : β * (∑ i ∈ s, B i * Real.exp (c * r i)) ≤ Bfinal) : + B0 / 2 * Real.exp (β * c / 2 * ∑ i ∈ s, r i) ≤ Bfinal := by + classical + have hgrowth : ∀ t : Finset ι, t ⊆ s → + B0 / β * Real.exp (β * c / 2 * ∑ i ∈ t, r i) ≤ + B0 / β + ∑ i ∈ t, B i * Real.exp (c * r i) := by + intro t + induction t using Finset.induction_on_max_value time with + | empty => intro _; simp + | insert a t ha hmax ih => + intro hsub + have haS : a ∈ s := hsub (mem_insert_self _ _) + have htS : t ⊆ s := fun i hi => hsub (mem_insert_of_mem hi) + have hlt : ∀ i ∈ t, time i < time a := by + intro i hi + apply lt_of_le_of_ne (hmax i hi) + intro he + have heq := hinj (htS hi) haS he + exact ha (heq ▸ hi) + have hsubset : t ⊆ s.filter (fun i => time i < time a) := + fun i hi => mem_filter.mpr ⟨htS hi, hlt i hi⟩ + have hsum := sum_le_sum_of_subset_of_nonneg (f := fun i => B i * Real.exp (c * r i)) hsubset + (fun i hi _ => mul_nonneg (hB0.le.trans (hbase i (mem_filter.mp hi).1)) + (Real.exp_pos _).le) + have hp := mul_le_mul_of_nonneg_left hsum hβ.le + have hsmall : β * (∑ i ∈ t, B i * Real.exp (c * r i)) ≤ B a := + hp.trans (hprefix a haS) + let Q := B0 / β + ∑ i ∈ t, B i * Real.exp (c * r i) + have hQ : β * Q ≤ 2 * B a := by + have he : β * Q = B0 + β * (∑ i ∈ t, B i * Real.exp (c * r i)) := by + dsimp [Q] + field_simp + rw [he] + linarith [hbase a haS] + have hQnonneg : 0 ≤ Q := by + apply add_nonneg (div_pos hB0 hβ).le + exact sum_nonneg (fun i hi => mul_nonneg (hB0.le.trans (hbase i (htS hi))) + (Real.exp_pos _).le) + have hexp := exp_scaled_le (θ := β / 2) (by positivity) (by linarith) (c * r a) + have he : β / 2 * (c * r a) = β * c / 2 * r a := by ring + rw [he] at hexp + have hm := mul_le_mul_of_nonneg_left hexp hQnonneg + have hbound := mul_le_mul_of_nonneg_right hQ (Real.exp_pos (c * r a)).le + have hrec : Q * Real.exp (β * c / 2 * r a) ≤ Q + B a * Real.exp (c * r a) := by + nlinarith only [hm, hbound] + have hi := mul_le_mul_of_nonneg_right (ih htS) (Real.exp_pos (β * c / 2 * r a)).le + rw [sum_insert ha, sum_insert ha, mul_add, Real.exp_add] + dsimp [Q] at hrec + nlinarith only [hi, hrec] + have hg := mul_le_mul_of_nonneg_left (hgrowth s (Subset.refl _)) hβ.le + have he (X : ℝ) : β * (B0 / β * X) = B0 * X := by field_simp + have he' (X : ℝ) : β * (B0 / β + X) = B0 + β * X := by field_simp + rw [he, he'] at hg + linarith + +lemma high_count_log_bound {ι : Type*} + (s : Finset ι) (time : ι → ℕ) (A G : ι → ℝ) (q : ι → ℕ) + {A0 Afinal H β : ℝ} (hA0 : 0 < A0) (hAF : A0 ≤ Afinal) + (hA : ∀ i ∈ s, A0 ≤ A i) (hG : ∀ i ∈ s, 0 < G i) + (hH : 0 ≤ H) (hβ : 0 < β) (hβ1 : β ≤ 1) + (hinj : Set.InjOn time (s : Set ι)) + (henergy : (∑ i ∈ s, A i * G i) ≤ H) + (hweights : (∑ i ∈ s, (2 : ℝ) ^ q i / Real.sqrt (G i)) ≤ 32 * Real.sqrt Afinal) + (hprefix : ∀ i ∈ s, + (∑ j ∈ s.filter (fun j => time j < time i), (2 : ℝ) ^ q j / Real.sqrt (G j)) ≤ + 32 * Real.sqrt (A i)) + (htuning : β ^ 3 * H * 32 ^ 2 ≤ 1) : + (∑ i ∈ s, (q i : ℝ)) ≤ + 2 * Real.log (2 * Afinal ^ (1 / 3 : ℝ) / A0 ^ (1 / 3 : ℝ)) / + (β * (2 * Real.log 2 / 3)) := by + classical + have hAnonneg : ∀ i ∈ s, 0 ≤ A i := fun i hi => hA0.le.trans (hA i hi) + have hAFpos : 0 < Afinal := hA0.trans_le hAF + have hB0 : 0 < A0 ^ (1 / 3 : ℝ) := Real.rpow_pos_of_pos hA0 _ + have hBf : 0 < Afinal ^ (1 / 3 : ℝ) := Real.rpow_pos_of_pos hAFpos _ + have hc : 0 < 2 * Real.log 2 / 3 := by + have hh := Real.log_pos (by norm_num : (1 : ℝ) < 2) + positivity + have hfinal := weighted_curvature_growth s A G q hAnonneg hG hH hβ.le hAFpos.le + henergy hweights htuning + have hprefix' : ∀ i ∈ s, + β * (∑ j ∈ s.filter (fun j => time j < time i), + A j ^ (1 / 3 : ℝ) * Real.exp ((2 * Real.log 2 / 3) * q j)) ≤ A i ^ (1 / 3 : ℝ) := by + intro i hi + have hsub : s.filter (fun j => time j < time i) ⊆ s := filter_subset _ _ + have hsum := sum_le_sum_of_subset_of_nonneg (f := fun j => A j * G j) hsub + (fun j hj _ => mul_nonneg (hAnonneg j hj) (hG j hj).le) + exact weighted_curvature_growth _ A G q (fun j hj => hAnonneg j (hsub hj)) + (fun j hj => hG j (hsub hj)) hH hβ.le (hAnonneg i hi) + (hsum.trans henergy) (hprefix i hi) htuning + have hexp := finite_prefix_exponential_growth s time (fun i => A i ^ (1 / 3 : ℝ)) + (fun i => (q i : ℝ)) hB0 hβ hβ1 hinj + (fun i hi => Real.rpow_le_rpow hA0.le (hA i hi) (by norm_num)) hprefix' + (Real.rpow_le_rpow hA0.le hAF (by norm_num)) hfinal + exact exp_growth_log_bound hB0 hβ hc hBf hexp + +lemma low_count_bound {ι : Type*} (s : Finset ι) (G : ι → ℝ) (q : ι → ℕ) + {K W : ℝ} (hG : ∀ i ∈ s, 0 < G i) (hK : ∀ i ∈ s, G i ≤ K) + (hweights : (∑ i ∈ s, (2 : ℝ) ^ q i / Real.sqrt (G i)) ≤ W) : + (∑ i ∈ s, (q i : ℝ)) ≤ Real.sqrt K * W := by + calc + _ ≤ ∑ i ∈ s, Real.sqrt K * ((2 : ℝ) ^ q i / Real.sqrt (G i)) := by + apply sum_le_sum + intro i hi + have hq : (q i : ℝ) ≤ (2 : ℝ) ^ q i := by + exact_mod_cast (Nat.lt_two_pow_self (n := q i)).le + have hs := Real.sqrt_le_sqrt (hK i hi) + have hm := mul_le_mul_of_nonneg_right hs + (show 0 ≤ (2 : ℝ) ^ q i / Real.sqrt (G i) by positivity) + have he : Real.sqrt (G i) * ((2 : ℝ) ^ q i / Real.sqrt (G i)) = (2 : ℝ) ^ q i := by + field_simp [(Real.sqrt_pos.mpr (hG i hi)).ne'] + rw [he] at hm + exact hq.trans hm + _ = Real.sqrt K * (∑ i ∈ s, (2 : ℝ) ^ q i / Real.sqrt (G i)) := (mul_sum _ _ _).symm + _ ≤ Real.sqrt K * W := mul_le_mul_of_nonneg_left hweights (Real.sqrt_nonneg K) + +lemma low_count_sqrt_bound {ι : Type*} (s : Finset ι) (G : ι → ℝ) (q : ι → ℕ) + {L0 Afinal : ℝ} (hL0 : 0 ≤ L0) (hG : ∀ i ∈ s, 0 < G i) + (hK : ∀ i ∈ s, G i ≤ 8 * L0) + (hweights : (∑ i ∈ s, (2 : ℝ) ^ q i / Real.sqrt (G i)) ≤ 32 * Real.sqrt Afinal) : + (∑ i ∈ s, (q i : ℝ)) ≤ 96 * Real.sqrt (L0 * Afinal) := by + have h := low_count_bound s G q hG hK hweights + have h8 : Real.sqrt (8 : ℝ) ≤ 3 := (Real.sqrt_le_iff).mpr ⟨by norm_num, by norm_num⟩ + have hs := mul_le_mul_of_nonneg_right h8 (Real.sqrt_nonneg L0) + rw [← Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 8)] at hs + have hm := mul_le_mul_of_nonneg_right hs (show 0 ≤ 32 * Real.sqrt Afinal by positivity) + rw [Real.sqrt_mul hL0] + nlinarith only [h, hm] + +lemma mixed_tuning {a : ℝ} (ha : 0 ≤ a) : + let β := 1 / (64 * (1 + a ^ (2 / 3 : ℝ))) + 0 < β ∧ β ≤ 1 ∧ β ^ 3 * ((512 / 3) * a ^ 2) * 32 ^ 2 ≤ 1 := by + let t := a ^ (2 / 3 : ℝ) + have ht : 0 ≤ t := Real.rpow_nonneg ha _ + have ht3 : t ^ 3 = a ^ 2 := by + dsimp [t] + rw [← Real.rpow_natCast, ← Real.rpow_mul ha] + norm_num + have hd : 0 < 64 * (1 + t) := by positivity + change 0 < 1 / (64 * (1 + t)) ∧ _ ≤ 1 ∧ _ ≤ 1 + refine ⟨one_div_pos.mpr hd, (div_le_one hd).mpr (by linarith), ?_⟩ + change (1 / (64 * (1 + t))) ^ 3 * ((512 / 3) * a ^ 2) * 32 ^ 2 ≤ 1 + rw [div_pow] + have hpow : 0 < (64 * (1 + t)) ^ 3 := pow_pos hd 3 + field_simp + nlinarith [sq_nonneg t, pow_nonneg ht 3] + +lemma count_exponent_lower : (1 / 3 : ℝ) ≤ 2 * Real.log 2 / 3 := by + have h := Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 1 / 2) + norm_num [Real.log_div] at h + linarith + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] + +/-- Whether the current local curvature exceeds the algorithm curvature guess. -/ +noncomputable def runUp (L0 L1 : ℝ) (g : E → E) (s : Iterate E) (n : ℕ) : Bool := by + classical + exact decide ((run L0 L1 g s n).guess < + localCurvature L0 L1 (g (coupling (run L0 L1 g s n)))) + +omit [CompleteSpace E] in +lemma run_charging_bound {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (s : Iterate E) + (hA : 0 ≤ s.A) (hG : 0 < s.guess) + (hfirst : localCurvature L0 L1 (g (coupling s)) ≤ s.guess) (n : ℕ) : + let w := fun i => 1 / Real.sqrt (run L0 L1 g s i).guess + let up := runUp L0 L1 g s + (∑ b ∈ chargingSet up n, chargeValue w b) ≤ 32 * Real.sqrt (run L0 L1 g s (n + 1)).A ∧ + ∀ b ∈ chargingSet up n, + (∑ a ∈ (chargingSet up n).filter (fun a => a.1 < b.1), chargeValue w a) ≤ + 32 * Real.sqrt (run L0 L1 g s (b.1 + 1)).A := by + let w := fun i => 1 / Real.sqrt (run L0 L1 g s i).guess + let up := runUp L0 L1 g s + have hzero : up 0 = false := by simp [up, runUp, run, not_lt_of_ge hfirst] + have hw : ∀ i, 0 ≤ w i := fun i => one_div_nonneg.mpr (Real.sqrt_nonneg _) + have hnext : ∀ i, w (i + 1) = if up i then w i / 4 else 4 * w i := by + intro i + have hv := run_valid (g := g) hL0 hL1 s hA hG i + have hs := step_inverse_sqrt_guess (g := g) (L0 := L0) (L1 := L1) + (run L0 L1 g s i) hv.2 + dsimp [w, up, runUp] + simp only [decide_eq_true_eq, ← not_le, ite_not] + exact hs + have hmass (i : ℕ) : downMass up w i ≤ 2 * Real.sqrt (run L0 L1 g s (i + 1)).A := by + have hs := down_sum_le_sqrt (g := g) hL0 hL1 s hA hG (i + 1) + simpa only [downMass, up, runUp, w, decide_eq_true_eq, ← not_le, ite_not] using hs + have htotal (i : ℕ) : chargeTotal w (charging up i) ≤ + 32 * Real.sqrt (run L0 L1 g s (i + 1)).A := by + have hs := charging_total_le hzero hw hnext i + linarith [hmass i] + have hmono : Monotone (fun i => 32 * Real.sqrt (run L0 L1 g s (i + 1)).A) := by + intro i j hij + have h := Real.sqrt_le_sqrt + (run_weight_mono (g := g) hL0 hL1 s hA hG (Nat.add_le_add_right hij 1)) + linarith + have hprefix := charging_prefix_bound + (show 0 ≤ 32 * Real.sqrt (run L0 L1 g s (0 + 1)).A by positivity) + hmono htotal n + dsimp only + constructor + · rw [charging_sum] + exact htotal n + · intro b hb + rw [charging_sum_prefix] + exact hprefix b (List.mem_toFinset.mp hb) + +omit [CompleteSpace E] in +lemma charging_selected_curvature {g : E → E} {L0 L1 : ℝ} (s : Iterate E) + (hfirst : localCurvature L0 L1 (g (coupling s)) = s.guess) + (n : ℕ) (b : ℕ × ℕ) (hb : b ∈ chargingSet (runUp L0 L1 g s) n) : + (run L0 L1 g s b.1).guess ≤ localCurvature L0 L1 (g (coupling (run L0 L1 g s b.1))) := by + have h := (charging_indices (runUp L0 L1 g s) n).2.2.2 b (List.mem_toFinset.mp hb) + rcases h with h | h + · rw [h] + simpa only [run] using hfirst.ge + · have ht : (run L0 L1 g s b.1).guess < + localCurvature L0 L1 (g (coupling (run L0 L1 g s b.1))) := of_decide_eq_true h + exact ht.le + +lemma charged_high_energy {f : E → ℝ} {g : E → E} {L0 L1 : ℝ} + (hL0 : 0 < L0) (hL1 : 0 < L1) + (hc : ConvexOn ℝ Set.univ f) (hg : ∀ x, HasGradientAt f (g x) x) + (hgd : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) + (s : Iterate E) (u : E) (hmin : IsMinOn f Set.univ u) + (hA : 0 ≤ s.A) (hG : 0 < s.guess) + (hfirst : localCurvature L0 L1 (g (coupling s)) = s.guess) + (n : ℕ) (Q : Finset (ℕ × ℕ)) (hQ : Q ⊆ chargingSet (runUp L0 L1 g s) n) + (hhigh : ∀ b ∈ Q, 8 * L0 < localCurvature L0 L1 (g (coupling (run L0 L1 g s b.1)))) : + (∑ b ∈ Q, (run L0 L1 g s (b.1 + 1)).A * (run L0 L1 g s b.1).guess) ≤ + (512 / 3) * L1 ^ 2 * energy f u s := by + have hindex : Q.image Prod.fst ⊆ range (n + 1) := by + intro i hi + obtain ⟨b, hb, rfl⟩ := mem_image.mp hi + exact mem_range.mpr (Nat.lt_succ_of_le + (charging_index_le _ n b (List.mem_toFinset.mp (hQ hb)))) + have hup : ∀ i ∈ Q.image Prod.fst, (run L0 L1 g s i).guess ≤ + localCurvature L0 L1 (g (coupling (run L0 L1 g s i))) := by + intro i hi + obtain ⟨b, hb, rfl⟩ := mem_image.mp hi + exact charging_selected_curvature s hfirst n b (hQ hb) + have hhigh' : ∀ i ∈ Q.image Prod.fst, + 8 * L0 < localCurvature L0 L1 (g (coupling (run L0 L1 g s i))) := by + intro i hi + obtain ⟨b, hb, rfl⟩ := mem_image.mp hi + exact hhigh b hb + have he := run_high_sum_le hL0 hL1 hc hg hgd hH s u hmin hA hG (n + 1) + (Q.image Prod.fst) hindex hup hhigh' + have hinj : ∀ a ∈ Q, ∀ b ∈ Q, a.1 = b.1 → a = b := by + intro a ha b hb hab + exact charging_unique_index _ n (List.mem_toFinset.mp (hQ ha)) + (List.mem_toFinset.mp (hQ hb)) hab + rw [sum_image hinj] at he + exact he + +/-- Shared low/high-curvature charging facts for both accelerated iteration-count bounds. -/ +lemma run_charging_geometry {f : E → ℝ} {g : E → E} {L0 L1 R : ℝ} + (hL0 : 0 < L0) (hL1 : 0 < L1) + (hc : ConvexOn ℝ Set.univ f) (hg : ∀ x, HasGradientAt f (g x) x) + (hgd : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) + (s : Iterate E) (u : E) (hmin : IsMinOn f Set.univ u) + (hA : 0 < s.A) (hG : 0 < s.guess) (hE : energy f u s ≤ R ^ 2) + (hfirst : localCurvature L0 L1 (g (coupling s)) = s.guess) (n : ℕ) : + let Q := chargingSet (runUp L0 L1 g s) n + let A := fun b : ℕ × ℕ => (run L0 L1 g s (b.1 + 1)).A + let G := fun b : ℕ × ℕ => (run L0 L1 g s b.1).guess + let M := fun b : ℕ × ℕ => localCurvature L0 L1 (g (coupling (run L0 L1 g s b.1))) + let low := Q.filter (fun b => M b ≤ 8 * L0) + let high := Q.filter (fun b => ¬M b ≤ 8 * L0) + let Afinal := (run L0 L1 g s (n + 1)).A + (∀ i, s.A ≤ (run L0 L1 g s i).A) ∧ + (∀ i, 0 < (run L0 L1 g s i).guess) ∧ + (∑ b ∈ low, (b.2 : ℝ)) ≤ 96 * Real.sqrt (L0 * Afinal) ∧ + (∑ b ∈ high, A b * G b) ≤ (512 / 3) * (L1 * R) ^ 2 ∧ + (∑ b ∈ high, (2 : ℝ) ^ b.2 / Real.sqrt (G b)) ≤ 32 * Real.sqrt Afinal ∧ + (∀ b ∈ high, + (∑ a ∈ high.filter (fun a => a.1 < b.1), (2 : ℝ) ^ a.2 / Real.sqrt (G a)) ≤ + 32 * Real.sqrt (A b)) ∧ + Set.InjOn Prod.fst (high : Set (ℕ × ℕ)) ∧ + (∑ b ∈ low, (b.2 : ℝ)) + (∑ b ∈ high, (b.2 : ℝ)) = n := by + classical + let Q := chargingSet (runUp L0 L1 g s) n + let A := fun b : ℕ × ℕ => (run L0 L1 g s (b.1 + 1)).A + let G := fun b : ℕ × ℕ => (run L0 L1 g s b.1).guess + let M := fun b : ℕ × ℕ => localCurvature L0 L1 (g (coupling (run L0 L1 g s b.1))) + let low := Q.filter (fun b => M b ≤ 8 * L0) + let high := Q.filter (fun b => ¬M b ≤ 8 * L0) + let Afinal := (run L0 L1 g s (n + 1)).A + have hv (i : ℕ) := run_valid (g := g) hL0 hL1.le s hA.le hG i + have hbase (i : ℕ) : s.A ≤ (run L0 L1 g s i).A := + run_weight_mono (g := g) hL0 hL1.le s hA.le hG (Nat.zero_le i) + have hcharge := run_charging_bound (g := g) hL0 hL1.le s hA.le hG hfirst.le n + have hweights : (∑ b ∈ Q, (2 : ℝ) ^ b.2 / Real.sqrt (G b)) ≤ 32 * Real.sqrt Afinal := by + simpa only [chargeValue, mul_one_div] using hcharge.1 + have hsubset (T : Finset (ℕ × ℕ)) (hT : T ⊆ Q) : + (∑ b ∈ T, (2 : ℝ) ^ b.2 / Real.sqrt (G b)) ≤ 32 * Real.sqrt Afinal := by + apply le_trans (sum_le_sum_of_subset_of_nonneg hT ?_) hweights + intro b _ _ + positivity + have hlow := low_count_sqrt_bound low G Prod.snd hL0.le + (fun b _ => (hv b.1).2) + (fun b hb => (charging_selected_curvature s hfirst n b (mem_filter.mp hb).1).trans + (mem_filter.mp hb).2) + (hsubset low (filter_subset _ _)) + have henergy : (∑ b ∈ high, A b * G b) ≤ (512 / 3) * (L1 * R) ^ 2 := by + have he := charged_high_energy hL0 hL1 hc hg hgd hH s u hmin hA.le hG hfirst n high + (filter_subset _ _) (fun b hb => lt_of_not_ge (mem_filter.mp hb).2) + have hm := mul_le_mul_of_nonneg_left hE (show 0 ≤ (512 / 3) * L1 ^ 2 by positivity) + change (∑ b ∈ high, A b * G b) ≤ _ at he + nlinarith only [he, hm] + have hprefix : ∀ b ∈ high, + (∑ a ∈ high.filter (fun a => a.1 < b.1), (2 : ℝ) ^ a.2 / Real.sqrt (G a)) ≤ + 32 * Real.sqrt (A b) := by + intro b hb + have hsub : high.filter (fun a => a.1 < b.1) ⊆ Q.filter (fun a => a.1 < b.1) := by + intro a ha + exact mem_filter.mpr ⟨(mem_filter.mp (mem_filter.mp ha).1).1, (mem_filter.mp ha).2⟩ + have hs := sum_le_sum_of_subset_of_nonneg + (f := fun a => (2 : ℝ) ^ a.2 / Real.sqrt (G a)) hsub (fun a _ _ => by positivity) + have hp := hcharge.2 b (mem_filter.mp hb).1 + simp only [chargeValue, mul_one_div] at hp + exact hs.trans hp + have hinj : Set.InjOn Prod.fst (high : Set (ℕ × ℕ)) := by + intro a ha b hb hab + exact charging_unique_index _ n (List.mem_toFinset.mp (mem_filter.mp ha).1) + (List.mem_toFinset.mp (mem_filter.mp hb).1) hab + have hcount : (∑ b ∈ Q, (b.2 : ℝ)) = n := by + exact_mod_cast charging_sum_count (runUp L0 L1 g s) n + have hsplit : (∑ b ∈ low, (b.2 : ℝ)) + (∑ b ∈ high, (b.2 : ℝ)) = n := by + rw [← hcount] + exact sum_filter_add_sum_filter_not Q _ _ + exact ⟨hbase, fun i => (hv i).2, hlow, henergy, + hsubset high (filter_subset _ _), hprefix, hinj, hsplit⟩ + +end LongTails.OracleTemplate.GeneralizedAccelerated diff --git a/LeanPool/LongTails/Proofs/GeneralizedSelfNormalizedConvergence.lean b/LeanPool/LongTails/Proofs/GeneralizedSelfNormalizedConvergence.lean new file mode 100644 index 000000000..6b10e4a7a --- /dev/null +++ b/LeanPool/LongTails/Proofs/GeneralizedSelfNormalizedConvergence.lean @@ -0,0 +1,174 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import LeanPool.LongTails.Proofs.GeneralizedLogCharging +public import LeanPool.LongTails.Proofs.GeneralizedConvergence + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +open Finset Set + +namespace LongTails.OracleTemplate.GeneralizedAccelerated + +open LongTails.Setups.GeneralizedSmoothAndConvex + +lemma high_root_simplify {a D : ℝ} (ha : 0 ≤ a) (hD : 0 ≤ D) : + 64 * ((512 / 3 * a ^ 2) * D ^ 2) ^ (1 / 3 : ℝ) ≤ + 512 * (a * D) ^ (2 / 3 : ℝ) := by + have hroot : (((512 / 3 * a ^ 2) * D ^ 2) ^ (1 / 3 : ℝ)) ^ 3 = + (512 / 3 * a ^ 2) * D ^ 2 := by + rw [← Real.rpow_natCast, ← Real.rpow_mul (by positivity : 0 ≤ (512 / 3 * a ^ 2) * D ^ 2)] + norm_num + have hpow : ((a * D) ^ (2 / 3 : ℝ)) ^ 3 = (a * D) ^ 2 := by + rw [← Real.rpow_natCast, ← Real.rpow_mul (mul_nonneg ha hD)] + norm_num + apply (pow_le_pow_iff_left₀ (by positivity) (by positivity) (by decide : 3 ≠ 0)).mp + rw [mul_pow, mul_pow, hroot, hpow] + nlinarith [mul_nonneg (sq_nonneg a) (sq_nonneg D)] + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] + +lemma run_count_self_normalized {f : E → ℝ} {g : E → E} {L0 L1 R : ℝ} + (hL0 : 0 < L0) (hL1 : 0 < L1) (hR : 0 ≤ R) + (hc : ConvexOn ℝ univ f) (hg : ∀ x, HasGradientAt f (g x) x) + (hgd : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) + (s : Iterate E) (u : E) (hmin : IsMinOn f univ u) + (hA : 0 < s.A) (hG : 0 < s.guess) (hE : energy f u s ≤ R ^ 2) + (hfirst : localCurvature L0 L1 (g (coupling s)) = s.guess) (n : ℕ) : + (n : ℝ) ≤ 96 * Real.sqrt (L0 * (run L0 L1 g s (n + 1)).A) + + 4 * Real.log (2 * (run L0 L1 g s (n + 1)).A / s.A) + + 512 * (L1 * R * Real.log (2 * (run L0 L1 g s (n + 1)).A / s.A)) ^ (2 / 3 : ℝ) := by + classical + let Q := chargingSet (runUp L0 L1 g s) n + let A := fun b : ℕ × ℕ => (run L0 L1 g s (b.1 + 1)).A + let G := fun b : ℕ × ℕ => (run L0 L1 g s b.1).guess + let M := fun b : ℕ × ℕ => localCurvature L0 L1 (g (coupling (run L0 L1 g s b.1))) + let low := Q.filter (fun b => M b ≤ 8 * L0) + let high := Q.filter (fun b => ¬M b ≤ 8 * L0) + let Afinal := (run L0 L1 g s (n + 1)).A + obtain ⟨hbase, hguess, hlow, henergy, hweights, hprefix, hinj, hsplit⟩ := + run_charging_geometry hL0 hL1 hc hg hgd hH s u hmin hA hG hE hfirst n + have hAF : s.A ≤ Afinal := hbase _ + let D := Real.log (2 * Afinal / s.A) + have hD : 0 ≤ D := by + apply Real.log_nonneg + apply (le_div_iff₀ hA).mpr + linarith + have hh := high_count_self_normalized high Prod.fst A G Prod.snd hA hAF + (fun b _ => hbase _) (fun b _ => hguess b.1) (by positivity) + hinj henergy hweights hprefix + have hr := high_root_simplify (mul_nonneg hL1.le hR) hD + change (∑ b ∈ high, (b.2 : ℝ)) ≤ 4 * D + + 64 * ((512 / 3 * (L1 * R) ^ 2) * D ^ 2) ^ (1 / 3 : ℝ) at hh + have hhigh : (∑ b ∈ high, (b.2 : ℝ)) ≤ 4 * D + 512 * (L1 * R * D) ^ (2 / 3 : ℝ) := by + linarith only [hh, hr] + change (n : ℝ) ≤ 96 * Real.sqrt (L0 * Afinal) + 4 * D + _ + linarith only [hlow, hhigh, hsplit] + +lemma run_accuracy_self_normalized {f : E → ℝ} {g : E → E} {L0 L1 R Δ ε : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hR : 0 < R) (hΔ : 0 < Δ) (hε : 0 < ε) + (hc : ConvexOn ℝ univ f) (hg : ∀ x, HasGradientAt f (g x) x) + (hgd : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) + (x0 u : E) (hmin : IsMinOn f univ u) (hdist : ‖x0 - u‖ ≤ R) + (hgap : f x0 - f u ≤ Δ) (N : ℕ) + (hN : 4096 * (1 + Real.sqrt (L0 * R ^ 2 / ε) + + Real.log (4 + 4 * Δ / ε) + (L1 * R * Real.log (4 + 4 * Δ / ε)) ^ (2 / 3 : ℝ)) ≤ N) : + f (run L0 L1 g (initialIterate L0 L1 R Δ x0 g) N).x - f u ≤ ε := by + let s := initialIterate L0 L1 R Δ x0 g + let S := Real.sqrt (L0 * R ^ 2 / ε) + let D := Real.log (4 + 4 * Δ / ε) + have hS : 0 ≤ S := Real.sqrt_nonneg _ + have hD : 0 ≤ D := by + apply Real.log_nonneg + have ht : 0 < 4 * Δ / ε := by positivity + linarith + let T := (L1 * R * D) ^ (2 / 3 : ℝ) + have hT : 0 ≤ T := Real.rpow_nonneg (mul_nonneg (mul_nonneg hL1 hR.le) hD) _ + have hA : 0 < s.A := by dsimp [s, initialIterate]; positivity + have hG : 0 < s.guess := localCurvature_pos hL0 hL1 _ + have hfirst : localCurvature L0 L1 (g (coupling s)) = s.guess := + initial_first_down hL0 hL1 hΔ x0 + have hE : energy f u s ≤ R ^ 2 := initial_energy hΔ x0 u hdist hgap + have hNpos : 0 < N := by + change 4096 * (1 + S + D + T) ≤ (N : ℝ) at hN + have hn : (0 : ℝ) < N := by linarith only [hS, hD, hT, hN] + exact_mod_cast hn + obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hNpos) + change f (run L0 L1 g s (n + 1)).x - f u ≤ ε + by_contra hfail + have hfail' : ε < f (run L0 L1 g s (n + 1)).x - f u := lt_of_not_ge hfail + let Afinal := (run L0 L1 g s (n + 1)).A + have hAF : s.A ≤ Afinal := + run_weight_mono (g := g) hL0 hL1 s hA.le hG (Nat.zero_le _) + have hAFpos : 0 < Afinal := hA.trans_le hAF + have hsmall : Afinal ≤ R ^ 2 / ε := + run_weight_le_of_inaccurate hL0 hL1 hc hg hgd hH s u hA.le hG hE hε (n + 1) hfail' + have hsqrt : Real.sqrt (L0 * Afinal) ≤ S := by + apply Real.sqrt_le_sqrt + have hm := mul_le_mul_of_nonneg_left hsmall hL0.le + simpa only [mul_div_assoc] using hm + have hlog : Real.log (2 * Afinal / s.A) ≤ D := by + apply Real.log_le_log (by positivity) + have hm := div_le_div_of_nonneg_right + (mul_le_mul_of_nonneg_left hsmall (by norm_num : (0 : ℝ) ≤ 2)) hA.le + have he : 2 * (R ^ 2 / ε) / s.A = 4 * Δ / ε := by + dsimp [s, initialIterate] + field_simp + ring + rw [he] at hm + change 2 * Afinal / s.A ≤ 4 + 4 * Δ / ε + linarith only [hm] + have hcount : (n : ℝ) ≤ 96 * S + 4 * D + 512 * T := by + by_cases hz : L1 = 0 + · subst L1 + have hb := run_count_smooth hL0 s hA.le hG hfirst n + change (n : ℝ) ≤ 96 * Real.sqrt (L0 * Afinal) at hb + linarith only [hb, hsqrt, hD, hT] + · have hL1p : 0 < L1 := lt_of_le_of_ne hL1 (Ne.symm hz) + have hb := run_count_self_normalized hL0 hL1p hR.le hc hg hgd hH s u hmin hA hG hE hfirst n + have hlogpos : 0 ≤ Real.log (2 * Afinal / s.A) := by + apply Real.log_nonneg + apply (le_div_iff₀ hA).mpr + linarith + have hp := Real.rpow_le_rpow + (mul_nonneg (mul_nonneg hL1 hR.le) hlogpos) + (mul_le_mul_of_nonneg_left hlog (mul_nonneg hL1 hR.le)) (by norm_num : (0 : ℝ) ≤ 2 / 3) + change (n : ℝ) ≤ 96 * Real.sqrt (L0 * Afinal) + 4 * Real.log (2 * Afinal / s.A) + + 512 * (L1 * R * Real.log (2 * Afinal / s.A)) ^ (2 / 3 : ℝ) at hb + change (L1 * R * Real.log (2 * Afinal / s.A)) ^ (2 / 3 : ℝ) ≤ T at hp + nlinarith only [hb, hsqrt, hlog, hp] + change 4096 * (1 + S + D + T) ≤ ((n + 1 : ℕ) : ℝ) at hN + push_cast at hN + linarith only [hS, hD, hT, hN, hcount] + +lemma run_accuracy_min {f : E → ℝ} {g : E → E} {L0 L1 R Δ ε : ℝ} + (hL0 : 0 < L0) (hL1 : 0 ≤ L1) (hR : 0 < R) (hΔ : 0 < Δ) (hε : 0 < ε) + (hc : ConvexOn ℝ univ f) (hg : ∀ x, HasGradientAt f (g x) x) + (hgd : Differentiable ℝ g) + (hH : ∀ x, ‖fderiv ℝ g x‖ ≤ L0 + L1 * ‖g x‖) + (x0 u : E) (hmin : IsMinOn f univ u) (hdist : ‖x0 - u‖ ≤ R) + (hgap : f x0 - f u ≤ Δ) (N : ℕ) + (hN : 4096 * (1 + Real.sqrt (L0 * R ^ 2 / ε) + + min ((⌈(L1 * R) ^ (2 / 3 : ℝ)⌉₊ : ℝ) * Real.log (4 + 4 * Δ / ε)) + (Real.log (4 + 4 * Δ / ε) + (L1 * R * Real.log (4 + 4 * Δ / ε)) ^ (2 / 3 : ℝ))) ≤ N) : + f (run L0 L1 g (initialIterate L0 L1 R Δ x0 g) N).x - f u ≤ ε := by + rcases le_total ((⌈(L1 * R) ^ (2 / 3 : ℝ)⌉₊ : ℝ) * Real.log (4 + 4 * Δ / ε)) + (Real.log (4 + 4 * Δ / ε) + (L1 * R * Real.log (4 + 4 * Δ / ε)) ^ (2 / 3 : ℝ)) with h | h + · rw [min_eq_left h] at hN + exact run_accuracy hL0 hL1 hR hΔ hε hc hg hgd hH x0 u hmin hdist hgap N hN + · rw [min_eq_right h] at hN + apply run_accuracy_self_normalized hL0 hL1 hR hΔ hε hc hg hgd hH x0 u hmin hdist hgap N + linarith + +end LongTails.OracleTemplate.GeneralizedAccelerated diff --git a/LeanPool/LongTails/Setups/GeneralizedSmoothAndConvex.lean b/LeanPool/LongTails/Setups/GeneralizedSmoothAndConvex.lean new file mode 100644 index 000000000..ff7e61492 --- /dev/null +++ b/LeanPool/LongTails/Setups/GeneralizedSmoothAndConvex.lean @@ -0,0 +1,75 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import Mathlib.Analysis.Calculus.Gradient.Basic +public import Mathlib.Analysis.Convex.Function +public import LeanPool.LongTails.Template + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +namespace LongTails.Setups.GeneralizedSmoothAndConvex + +universe u + +open LongTails.OracleTemplate + +/-- Problem information available to the method, excluding its target accuracy. -/ +structure Public where + /-- Real Hilbert space in which optimization takes place. -/ + E : Type u + /-- Normed additive structure of the optimization space. -/ + [normedE : NormedAddCommGroup E] + /-- Real inner product defining gradients. -/ + [linearE : InnerProductSpace ℝ E] + /-- Completeness of the optimization space. -/ + [completeE : CompleteSpace E] + /-- Constant part of the Hessian-growth bound. -/ + L0 : ℝ + /-- Coefficient of gradient norm in the Hessian-growth bound. -/ + L1 : ℝ + /-- Bound on initial distance to an attained minimizer. -/ + R : ℝ + /-- Bound on the initial objective gap. -/ + Δ : ℝ + /-- Initial point of the algorithm. -/ + x0 : E + +attribute [instance] Public.normedE Public.linearE Public.completeE + +/-- Public problem information together with the parameters of the accuracy guarantee. -/ +structure Params extends Public where + /-- Positive target objective-gap accuracy. -/ + ε : ℝ + +/-- Convex optimization with exact gradients and the displayed regularity assumptions. -/ +abbrev spec : Setup where + Params := Params + Public := Public + Instance p := p.E → ℝ + Query p := p.E + Reply p := p.E + Output p := p.E + publicInput := Params.toPublic + valid q := 0 < q.L0 ∧ 0 ≤ q.L1 ∧ 0 < q.R ∧ 0 < q.Δ ∧ 0 < q.ε + admissible q f oracle := + ConvexOn ℝ Set.univ f ∧ + (∀ k seed x, HasGradientAt f (oracle.answer k (0, x) seed) x) ∧ + (∀ k seed, Differentiable ℝ (fun x => oracle.answer k (0, x) seed)) ∧ + (∀ k seed x, ‖fderiv ℝ (fun y => oracle.answer k (0, y) seed) x‖ ≤ + q.L0 + q.L1 * ‖oracle.answer k (0, x) seed‖) ∧ + (∃ xstar, IsMinOn f Set.univ xstar ∧ ‖q.x0 - xstar‖ ≤ q.R ∧ + f q.x0 - f xstar ≤ q.Δ) + successful q f output P := + ∃ xstar, IsMinOn f Set.univ xstar ∧ + ∀ᵐ ω ∂(P : MeasureTheory.Measure _), f (output ω) - f xstar ≤ q.ε + +end LongTails.Setups.GeneralizedSmoothAndConvex diff --git a/LeanPool/LongTails/Setups/SmoothAndConvex.lean b/LeanPool/LongTails/Setups/SmoothAndConvex.lean new file mode 100644 index 000000000..2ab168713 --- /dev/null +++ b/LeanPool/LongTails/Setups/SmoothAndConvex.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import Mathlib.Analysis.Calculus.Gradient.Basic +public import Mathlib.Analysis.Convex.Function +public import Mathlib.Algebra.Order.Floor.Ring +public import LeanPool.LongTails.Template + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +namespace LongTails.Setups.SmoothAndConvex + +universe u + +open LongTails.OracleTemplate + +/-- Problem information available to the method, excluding its target accuracy. -/ +structure Public where + /-- Real Hilbert space in which optimization takes place. -/ + E : Type u + /-- Normed additive structure of the optimization space. -/ + [normedE : NormedAddCommGroup E] + /-- Real inner product defining gradients. -/ + [linearE : InnerProductSpace ℝ E] + /-- Completeness of the optimization space. -/ + [completeE : CompleteSpace E] + /-- Global Lipschitz bound for the gradient. -/ + L : ℝ + /-- Initial point of the algorithm. -/ + x0 : E + +attribute [instance] Public.normedE Public.linearE Public.completeE + +/-- Public problem information together with the parameters of the accuracy guarantee. -/ +structure Params extends Public where + /-- Bound on the initial distance to a minimizer. -/ + R : ℝ + /-- Positive target objective-gap accuracy. -/ + ε : ℝ + +/-- Convex optimization with exact gradients and the displayed regularity assumptions. -/ +abbrev spec : Setup where + Params := Params + Public := Public + Instance p := p.E → ℝ + Query p := p.E + Reply p := p.E + Output p := p.E + publicInput := Params.toPublic + valid q := 0 < q.L ∧ 0 ≤ q.R ∧ 0 < q.ε + admissible q f oracle := + ConvexOn ℝ Set.univ f ∧ + (∀ k seed x, HasGradientAt f (oracle.answer k (0, x) seed) x) ∧ + (∀ k seed x y, ‖oracle.answer k (0, x) seed - oracle.answer k (0, y) seed‖ ≤ q.L * ‖x - y‖) ∧ + (∃ xstar, IsMinOn f Set.univ xstar ∧ ‖q.x0 - xstar‖ ≤ q.R) + successful q f output P := + ∃ xstar, IsMinOn f Set.univ xstar ∧ + ∀ᵐ ω ∂(P : MeasureTheory.Measure _), f (output ω) - f xstar ≤ q.ε + +end LongTails.Setups.SmoothAndConvex diff --git a/LeanPool/LongTails/Template.lean b/LeanPool/LongTails/Template.lean new file mode 100644 index 000000000..7efd98646 --- /dev/null +++ b/LeanPool/LongTails/Template.lean @@ -0,0 +1,132 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure +public import Mathlib.MeasureTheory.Measure.Prod + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +open MeasureTheory + +namespace LongTails.OracleTemplate + +universe uP uD uI uQ uR uO + +/-- An oracle algorithm with an internal state and its own random seed. -/ +structure Algorithm (Query : Type uQ) (Reply : Type uR) (Output : Type uO) + (numOracles : ℕ := 1) where + /-- Random seed used to initialize the algorithm. -/ + Seed : Type := Unit + /-- Measurable structure on algorithm seeds. -/ + [seedSpace : MeasurableSpace Seed] + /-- Probability law of the algorithm seed. -/ + law : ProbabilityMeasure Seed := by exact ⟨MeasureTheory.Measure.dirac (), inferInstance⟩ + /-- Internal state retained between oracle calls. -/ + State : Type (max uQ uR uO) + /-- Initial state chosen from the algorithm seed. -/ + initial : Seed → State + /-- Oracle index and query selected by the current state. -/ + query : State → Fin numOracles × Query + /-- State after receiving the reply to the selected query. -/ + update : State → Reply → State + /-- Point reported when the query budget is exhausted. -/ + output : State → Output + +attribute [instance] Algorithm.seedSpace + +/-- A sequence of oracle replies, with an arbitrary joint law for the query samples. -/ +structure Oracle (Query : Type uQ) (Reply : Type uR) (numOracles : ℕ := 1) where + /-- Sample type at each query index. -/ + Seed : ℕ → Type := fun _ => Unit + /-- Measurable structure on each query sample. -/ + [seedSpace : ∀ k, MeasurableSpace (Seed k)] + /-- Joint probability law of all samples; independence is not assumed. -/ + law : ProbabilityMeasure ((k : ℕ) → Seed k) := by + exact ⟨MeasureTheory.Measure.dirac (fun _ => ()), inferInstance⟩ + /-- Reply at a query index, oracle index, query and sample. -/ + answer : (k : ℕ) → (Fin numOracles × Query) → Seed k → Reply + +attribute [instance] Oracle.seedSpace + +/-- Run at most the supplied fuel, decrementing the budget of each queried oracle. -/ +def executeLoop + {Query : Type uQ} {Reply : Type uR} {Output : Type uO} + {numOracles : ℕ} + (oracle : ℕ → (Fin numOracles × Query) → Reply) + (A : Algorithm Query Reply Output numOracles) : + Nat → Nat → (Fin numOracles → ℕ) → A.State → Output + | 0, _, _, state => A.output state + | k + 1, call, remaining, state => + let query := A.query state + if remaining query.1 = 0 then A.output state + else + let reply := oracle call query + let remaining := Function.update remaining query.1 (remaining query.1 - 1) + executeLoop oracle A k (call + 1) remaining (A.update state reply) + +/-- Execute an algorithm using explicit per-oracle call budgets and fixed random seeds. -/ +def execute + {Query : Type uQ} {Reply : Type uR} {Output : Type uO} + {numOracles : ℕ} + (oracle : Oracle Query Reply numOracles) (A : Algorithm Query Reply Output numOracles) + (budget : Fin numOracles → ℕ) (seed : A.Seed := by exact ()) + (oracleSeed : (k : ℕ) → oracle.Seed k := by exact fun _ => ()) : Output := + executeLoop (fun k query => oracle.answer k query (oracleSeed k)) + A (∑ i, budget i) 0 budget (A.initial seed) + +/-- The public information, admissible instances and success criterion of an oracle problem. -/ +structure Setup where + /-- Number of available oracle interfaces. -/ + numOracles : ℕ := 1 + /-- Parameters of a guarantee, including hidden accuracy targets. -/ + Params : Type uP + /-- Information available to the algorithm. -/ + Public : Type uD + /-- Mathematical instance hidden behind the oracle. -/ + Instance : Public → Type uI + /-- Type of query accepted by each oracle. -/ + Query : Public → Type uQ + /-- Type of oracle reply. -/ + Reply : Public → Type uR + /-- Type of result returned by the algorithm. -/ + Output : Public → Type uO + /-- Public information extracted from guarantee parameters. -/ + publicInput : Params → Public + /-- Admissible numerical regimes for the guarantee parameters. -/ + valid : Params → Prop + /-- Mathematical assumptions on the instance and its oracle. -/ + admissible : (p : Params) → Instance (publicInput p) → + Oracle (Query (publicInput p)) (Reply (publicInput p)) numOracles → Prop + /-- Accuracy criterion evaluated under the supplied law of seeds. -/ + successful : {Ω : Type} → [MeasurableSpace Ω] → + (p : Params) → Instance (publicInput p) → + (Ω → Output (publicInput p)) → ProbabilityMeasure Ω → Prop + /-- Optional restrictions on the algorithm family. -/ + allowedAlgorithm : (p : Public) → Algorithm (Query p) (Reply p) (Output p) numOracles → Prop := + fun _ _ => True + +/-- One algorithm family meets the setup criterion within the stated query budgets. -/ +def Convergence (S : Setup) + (budget : S.Params → Fin S.numOracles → ℕ) : Prop := + ∃ makeAlgorithm : (p : S.Public) → Algorithm (S.Query p) (S.Reply p) (S.Output p) S.numOracles, + (∀ p, S.valid p → + ∀ (I : S.Instance (S.publicInput p)) + (oracle : Oracle (S.Query (S.publicInput p)) (S.Reply (S.publicInput p)) S.numOracles), + S.admissible p I oracle → + let A := makeAlgorithm (S.publicInput p) + let result := fun seed : A.Seed × ((k : ℕ) → oracle.Seed k) => + execute oracle A (budget p) seed.1 seed.2 + S.successful p I result + ⟨(A.law : Measure _).prod (oracle.law : Measure _), inferInstance⟩) ∧ + ∀ p, S.valid p → S.allowedAlgorithm (S.publicInput p) (makeAlgorithm (S.publicInput p)) + +end LongTails.OracleTemplate diff --git a/LeanPool/LongTails/Theorems/GeneralizedSelfNormalizedConvex.lean b/LeanPool/LongTails/Theorems/GeneralizedSelfNormalizedConvex.lean new file mode 100644 index 000000000..4b59c3bf3 --- /dev/null +++ b/LeanPool/LongTails/Theorems/GeneralizedSelfNormalizedConvex.lean @@ -0,0 +1,67 @@ +/- +Copyright (c) 2026 LongTails contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, Ivan Oseledets +-/ +module + +public import LeanPool.LongTails.Setups.GeneralizedSmoothAndConvex +public import LeanPool.LongTails.Proofs.Execution +public import LeanPool.LongTails.Proofs.GeneralizedSelfNormalizedConvergence + +/-! +Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. +Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib. +-/ + +@[expose] public section + +namespace LongTails.OracleTemplate.GeneralizedAccelerated.SelfNormalized + +open LongTails.Setups.GeneralizedSmoothAndConvex + +/-- Exact gradient-query budget, including both queries in every accelerated step. -/ +noncomputable def budget : (let S := spec; S.Params → Fin S.numOracles → ℕ) := fun q _ => + if q.Δ ≤ q.ε then 0 else + 2 * ⌈4096 * (1 + Real.sqrt (q.L0 * q.R ^ 2 / q.ε) + + min ((⌈(q.L1 * q.R) ^ (2 / 3 : ℝ)⌉₊ : ℝ) * Real.log (4 + 4 * q.Δ / q.ε)) + (Real.log (4 + 4 * q.Δ / q.ε) + + (q.L1 * q.R * Real.log (4 + 4 * q.Δ / q.ε)) ^ (2 / 3 : ℝ)))⌉₊ + +/-- Gradient-only acceleration under a Hessian-growth bound, uniformly in the target accuracy. -/ +theorem result : Convergence LongTails.Setups.GeneralizedSmoothAndConvex.spec budget := by + let trials (q : Public) (ε : ℝ) : ℕ := + ⌈4096 * (1 + Real.sqrt (q.L0 * q.R ^ 2 / ε) + + min ((⌈(q.L1 * q.R) ^ (2 / 3 : ℝ)⌉₊ : ℝ) * Real.log (4 + 4 * q.Δ / ε)) + (Real.log (4 + 4 * q.Δ / ε) + + (q.L1 * q.R * Real.log (4 + 4 * q.Δ / ε)) ^ (2 / 3 : ℝ)))⌉₊ + refine ⟨algorithm, ?_, fun _ _ => trivial⟩ + rintro q ⟨hL0, hL1, hR, hΔ, hε⟩ + rintro f oracle ⟨hc, hg, hgd, hH, u, hmin, hdist, hgap⟩ + let seed0 := (Classical.choice oracle.law.nonempty) 0 + let g := fun x => oracle.answer 0 (0, x) seed0 + by_cases he : q.Δ ≤ q.ε + · refine ⟨u, hmin, Filter.Eventually.of_forall ?_⟩ + intro seed + change f (execute oracle (algorithm q.toPublic) (budget q) seed.1 seed.2) - f u ≤ q.ε + have hb : budget q = fun _ => 0 := by funext i; simp [budget, he] + rw [hb] + exact hgap.trans he + · let K := trials q.toPublic q.ε + have hacc := run_accuracy_min hL0 hL1 hR hΔ hε hc (hg 0 seed0) (hgd 0 seed0) + (hH 0 seed0) q.x0 u hmin hdist hgap K (Nat.le_ceil _) + refine ⟨u, hmin, Filter.Eventually.of_forall ?_⟩ + intro seed + have hexec := execute_gradient_oracle q.toPublic f g oracle (hg 0 seed0) hg hL0 hL1 hΔ K + seed.1 seed.2 + change f (execute oracle (algorithm q.toPublic) (budget q) seed.1 seed.2) - f u ≤ q.ε + have hb : budget q = fun _ => 2 * K := by + funext i + simp only [budget, ite_eq_right he] + rfl + rw [hb] + change f (execute oracle (algorithm q.toPublic) (fun _ => 2 * K) seed.1 seed.2) - f u ≤ q.ε + rw [hexec] + exact hacc + +end LongTails.OracleTemplate.GeneralizedAccelerated.SelfNormalized diff --git a/LeanPool/projects/longtails-generalized-convex.yaml b/LeanPool/projects/longtails-generalized-convex.yaml new file mode 100644 index 000000000..40e9490e7 --- /dev/null +++ b/LeanPool/projects/longtails-generalized-convex.yaml @@ -0,0 +1,63 @@ +slug: longtails-generalized-convex +title: Gradient-only acceleration for generalized-smooth convex optimization +summary: >- + A damped accelerated method minimizes convex functions on real Hilbert spaces + whose differentiable gradients satisfy the Hessian-growth bound + norm(D gradient f x) <= L0 + L1 * norm(gradient f x). The development proves an + explicit gradient-query budget for any positive accuracy, initial distance + bound and initial objective-gap bound, with an attained minimum. It retains + the oracle execution model, ordinary gradient descent, energy dissipation, + charging arguments and two complementary convergence bounds. No objective + value or line-search oracle is assumed. +branch: optimization +entry_module: LeanPool.LongTails +authors: +- Alexander Tyurin +- QuocViet Pham +- Valentin Khrulkov +- Ivan Oseledets +source: + url: https://github.com/k3nfalt/longtails/tree/269cbc764dd36851fd0b64f2f950f329ee127de4 + github_repo: k3nfalt/longtails + commit: 269cbc764dd36851fd0b64f2f950f329ee127de4 + completion_url: https://github.com/k3nfalt/longtails/commit/32aa9399511f9a11ecffb74ca284d8229bfd80c0 + completion_date: '2026-10-14T11:59:40Z' +license: Apache-2.0 +status: verified +provenance: AI +main_declarations: +- LongTails.OracleTemplate.GeneralizedAccelerated.SelfNormalized.result +main_results: +- declaration: LongTails.OracleTemplate.GeneralizedAccelerated.SelfNormalized.result + informal: >- + For positive L0, R, Delta and epsilon and nonnegative L1, a single damped + accelerated algorithm returns a point of objective gap at most epsilon for + every admissible convex objective with an attained minimum within distance + R and initial objective gap at most Delta. Its exact gradient-query budget + is zero when Delta <= epsilon; otherwise it is twice the natural ceiling + of 4096 times (1 + sqrt(L0*R^2/epsilon) + min(ceil((L1*R)^(2/3))*D, + D + (L1*R*D)^(2/3))), where D = log(4 + 4*Delta/epsilon). +- declaration: LongTails.OracleTemplate.GeneralizedAccelerated.run_accuracy_self_normalized + informal: >- + Under the same convexity, gradient, Hessian-growth and initialization + hypotheses, N accelerated steps reach objective gap epsilon whenever + N >= 4096*(1 + sqrt(L0*R^2/epsilon) + D + (L1*R*D)^(2/3)). +- declaration: LongTails.OracleTemplate.GeneralizedAccelerated.execute_gradient_oracle + informal: >- + Execution with any admissible exact-gradient oracle and a budget of 2*N + gradient queries equals the N-step accelerated iterate, for every seed. +- declaration: LongTails.OracleTemplate.Gradient.gd_accuracy + informal: >- + For L > 0, R >= 0 and epsilon > 0, a convex function with an exact + L-Lipschitz gradient and initial distance at most R from a comparison point, + ordinary gradient descent reaches objective gap epsilon after + max(1, ceil(L*R^2/(2*epsilon))) queries. +tags: +- convex-optimization +- gradient-methods +- oracle-complexity +- hilbert-spaces +msc: +- 90C25 +- 90C30 +- 68Q25