Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib.

theorem LongTails.OracleTemplate.GeneralizedAccelerated.weighted_holder_cube {ι : Type u_1} (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

theorem LongTails.OracleTemplate.GeneralizedAccelerated.weighted_exp_cube (A : ℝ) (hA : 0 ≤ A) (q : ℕ) : (A ^ (1 / 3) * Real.exp (2 * Real.log 2 / 3 * ↑q)) ^ 3 = A * (2 ^ q) ^ 2

theorem LongTails.OracleTemplate.GeneralizedAccelerated.weighted_curvature_holder {ι : Type u_1} (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 / √(G i)) ^ 2

theorem LongTails.OracleTemplate.GeneralizedAccelerated.weighted_curvature_growth {ι : Type u_1} (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 / √(G i) ≤ C * √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)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.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)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.exp_scaled_le {θ : ℝ} (hθ : 0 ≤ θ) (hθ1 : θ ≤ 1) (x : ℝ) : Real.exp (θ * x) ≤ 1 + θ * Real.exp x

theorem LongTails.OracleTemplate.GeneralizedAccelerated.finite_prefix_exponential_growth {ι : Type u_1} (s : Finset ι) (time : ι → ℕ) (B r : ι → ℝ) {B0 β c Bfinal : ℝ} (hB0 : 0 < B0) (hβ : 0 < β) (hβ1 : β ≤ 1) (hinj : Set.InjOn time ↑s) (hbase : ∀ i ∈ s, B0 ≤ B i) (hprefix : ∀ i ∈ s, β * ∑ j ∈ s with 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

theorem LongTails.OracleTemplate.GeneralizedAccelerated.high_count_log_bound {ι : Type u_1} (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) (henergy : ∑ i ∈ s, A i * G i ≤ H) (hweights : ∑ i ∈ s, 2 ^ q i / √(G i) ≤ 32 * √Afinal) (hprefix : ∀ i ∈ s, ∑ j ∈ s with time j < time i, 2 ^ q j / √(G j) ≤ 32 * √(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))

theorem LongTails.OracleTemplate.GeneralizedAccelerated.low_count_bound {ι : Type u_1} (s : Finset ι) (G : ι → ℝ) (q : ι → ℕ) {K W : ℝ} (hG : ∀ i ∈ s, 0 < G i) (hK : ∀ i ∈ s, G i ≤ K) (hweights : ∑ i ∈ s, 2 ^ q i / √(G i) ≤ W) : ∑ i ∈ s, ↑(q i) ≤ √K * W

theorem LongTails.OracleTemplate.GeneralizedAccelerated.low_count_sqrt_bound {ι : Type u_1} (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 / √(G i) ≤ 32 * √Afinal) : ∑ i ∈ s, ↑(q i) ≤ 96 * √(L0 * Afinal)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.mixed_tuning {a : ℝ} (ha : 0 ≤ a) : have β := 1 / (64 * (1 + a ^ (2 / 3))); 0 < β ∧ β ≤ 1 ∧ β ^ 3 * (512 / 3 * a ^ 2) * 32 ^ 2 ≤ 1

theorem LongTails.OracleTemplate.GeneralizedAccelerated.count_exponent_lower : 1 / 3 ≤ 2 * Real.log 2 / 3

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.runUp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L0 L1 : ℝ) (g : E → E) (s : Iterate E) (n : ℕ) : Bool

Whether the current local curvature exceeds the algorithm curvature guess.

Equations

• One or more equations did not get rendered due to their size.

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_charging_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {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 : ℕ) : have w := fun (i : ℕ) => 1 / √(run L0 L1 g s i).guess; have up := runUp L0 L1 g s; ∑ b ∈ chargingSet up n, chargeValue w b ≤ 32 * √(run L0 L1 g s (n + 1)).A ∧ ∀ b ∈ chargingSet up n, ∑ a ∈ chargingSet up n with a.1 < b.1, chargeValue w a ≤ 32 * √(run L0 L1 g s (b.1 + 1)).A

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_selected_curvature {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {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)))

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charged_high_energy {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → E} {L0 L1 : ℝ} (hL0 : 0 < L0) (hL1 : 0 < L1) (hc : ConvexOn ℝ Set.univ f) (hg : ∀ (x : E), HasGradientAt f (g x) x) (hgd : Differentiable ℝ g) (hH : ∀ (x : E), ‖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

theorem LongTails.OracleTemplate.GeneralizedAccelerated.run_charging_geometry {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E → E} {L0 L1 R : ℝ} (hL0 : 0 < L0) (hL1 : 0 < L1) (hc : ConvexOn ℝ Set.univ f) (hg : ∀ (x : E), HasGradientAt f (g x) x) (hgd : Differentiable ℝ g) (hH : ∀ (x : E), ‖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 : ℕ) : have Q := chargingSet (runUp L0 L1 g s) n; have A := fun (b : ℕ × ℕ) => (run L0 L1 g s (b.1 + 1)).A; have G := fun (b : ℕ × ℕ) => (run L0 L1 g s b.1).guess; have M := fun (b : ℕ × ℕ) => localCurvature L0 L1 (g (coupling (run L0 L1 g s b.1))); have low := {b ∈ Q | M b ≤ 8 * L0}; have high := {b ∈ Q | ¬M b ≤ 8 * L0}; have 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 * √(L0 * Afinal) ∧ ∑ b ∈ high, A b * G b ≤ 512 / 3 * (L1 * R) ^ 2 ∧ ∑ b ∈ high, 2 ^ b.2 / √(G b) ≤ 32 * √Afinal ∧ (∀ b ∈ high, ∑ a ∈ high with a.1 < b.1, 2 ^ a.2 / √(G a) ≤ 32 * √(A b)) ∧ Set.InjOn Prod.fst ↑high ∧ ∑ b ∈ low, ↑b.2 + ∑ b ∈ high, ↑b.2 = ↑n

Shared low/high-curvature charging facts for both accelerated iteration-count bounds.