An explicit logarithmic horizon for restarted optimization

All logarithm arguments are positive. Natural ceiling gives L<=N. Multiply by the positive log4 and use monotonicity of log together with log(4^N)=N log4 to obtain q<=4^N. Since (2^N)²=4^N, this is exactly the horizon condition required by the finite restart theorem. For L>=0, the natural ceiling is less than L+1. For L<0, it equals zero. Thus N<=max(0,L)+1 globally. More precisely, N=0 iff L<=0 iff q<=1 iff alpha R²<=epsilon. This certifies only that no halving stage is needed; the final solver call remains. Apply the existing radius_accuracy_and_cost theorem at this N using the horizon just proved. Its Nat.rec is exactly the recursion below. It supplies the actual state radius, final output error, and the natural sum of all certified call costs. The new theorem does not assume a radius invariant or an adequate iteration count. Cast the natural cost inequality to real numbers. Both phi values are nonnegative, so replacing N by its upper bound preserves the inequality. This global logarithmic bound uses no comparison between the two phi values. Under the additional condition phi(kappa)<=phi(8kappa), the final cost can be absorbed with the displayed universal factor. The result is (max(0,L)+2)phi(8kappa). If additionally q>=4, then L>=1, so L+2<=3L. This gives the explicit constant3/log4 in front of phi(8kappa)logq. These are conditional consequences; no monotonicity of phi or all-accuracy logarithmic bound is silently asserted.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem logarithmic_accuracy_and_cost {f : E → ℝ} {α β R ε : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 < α) (hβ : 0 < β) (hR : 0 < R) (hε : 0 < ε)
    {z x₀ : E} (hmin : IsMinOn f univ z) (hx₀ : ‖x₀-z‖ ≤ R)
    (A : E → ℝ → ℝ → E × ℕ) (φ : ℝ → ℕ)
    (hA : ∀ y r δ, 0 < r → 0 < δ → ‖y-z‖ ≤ r →
      f (A y r δ).1 - f z ≤ δ ∧ (A y r δ).2 ≤ φ (β*r^2/δ)) :
    let L := Real.log (α*R^2/ε) / Real.log 4
    let N := ⌈L⌉₊
    let r := fun k : ℕ => R / (2:ℝ)^k
    let run : ℕ → E × ℕ := Nat.rec (x₀, 0) (fun k p =>
      let w := A p.1 (r k) (α*(r k)^2/8)
      (w.1, p.2 + w.2))
    let last := A (run N).1 (Real.sqrt (ε/α)) ε
    let C := (run N).2 + last.2
    (N : ℝ) ≤ max 0 L + 1 ∧ (N = 0 ↔ α*R^2 ≤ ε) ∧
      ‖(run N).1-z‖ ≤ r N ∧ f last.1 - f z ≤ ε ∧
      C ≤ N * φ (8*(β/α)) + φ (β/α) ∧
      (C : ℝ) ≤ (max 0 L + 1) * φ (8*(β/α)) + φ (β/α) ∧
      (φ (β/α) ≤ φ (8*(β/α)) →
        (C : ℝ) ≤ (max 0 L + 2) * φ (8*(β/α)) ∧
        (4 ≤ α*R^2/ε → (C : ℝ) ≤ 3*L*φ (8*(β/α)))) := by
  let L := Real.log (α*R^2/ε) / Real.log 4
  let N := ⌈L⌉₊
  have hlog : 0 < Real.log 4 := Real.log_pos (by norm_num)
  have hq : 0 < α*R^2/ε := by positivity
  have hround : (N : ℝ) ≤ max 0 L + 1 := by
    by_cases hL : 0 ≤ L
    · exact (Nat.ceil_lt_add_one hL).le.trans (by rw [max_eq_right hL])
    · have hz : N = 0 := Nat.ceil_eq_zero.mpr (le_of_not_ge hL)
      rw [hz, Nat.cast_zero, max_eq_left (le_of_not_ge hL)]
      norm_num
  have hzero : N = 0 ↔ α*R^2 ≤ ε := by
    change ⌈Real.log (α*R^2/ε) / Real.log 4⌉₊ = 0 ↔ _
    rw [Nat.ceil_eq_zero, div_le_iff₀ hlog, zero_mul]
    rw [← Real.log_one, Real.log_le_log_iff hq (by norm_num)]
    exact (div_le_iff₀ hε).trans (by simp)
  have hpow : α*R^2/ε ≤ (4:ℝ)^N := by
    apply (Real.log_le_log_iff hq (by positivity)).mp
    rw [Real.log_pow]
    exact (div_le_iff₀ hlog).mp (Nat.le_ceil L)
  have hid : ((2:ℝ)^N)^2 = (4:ℝ)^N := by
    rw [← pow_mul, Nat.mul_comm N 2, pow_mul]
    norm_num
  have hN : α*(R/(2:ℝ)^N)^2 ≤ ε := by
    rw [div_pow, ← mul_div_assoc, hid]
    apply (div_le_iff₀ (by positivity : 0 < (4:ℝ)^N)).mpr
    have h := (div_le_iff₀ hε).mp hpow
    nlinarith
  have hb := RestartReduction.radius_accuracy_and_cost hf hsc hα hβ hR hε
    hmin hx₀ A φ hA N hN
  let r := fun k : ℕ => R / (2:ℝ)^k
  let run : ℕ → E × ℕ := Nat.rec (x₀, 0) (fun k p =>
    let w := A p.1 (r k) (α*(r k)^2/8)
    (w.1, p.2 + w.2))
  let last := A (run N).1 (Real.sqrt (ε/α)) ε
  let C := (run N).2 + last.2
  have hcast : (C : ℝ) ≤ (N : ℝ) * φ (8*(β/α)) + φ (β/α) := by
    have hc : C ≤ N * φ (8*(β/α)) + φ (β/α) := hb.2.2.2
    simpa only [Nat.cast_add, Nat.cast_mul] using ((Nat.cast_le (α := ℝ)).mpr hc)
  have hm : (N : ℝ) * φ (8*(β/α)) ≤
      (max 0 L + 1) * φ (8*(β/α)) :=
    mul_le_mul_of_nonneg_right hround (Nat.cast_nonneg _)
  have hreal : (C : ℝ) ≤ (max 0 L + 1) * φ (8*(β/α)) + φ (β/α) := by
    linarith
  refine ⟨hround, hzero, hb.1, hb.2.2.1, hb.2.2.2, hreal, ?_⟩
  intro hφ
  have hp : (φ (β/α) : ℝ) ≤ φ (8*(β/α)) := by exact_mod_cast hφ
  have ha : (C : ℝ) ≤ (max 0 L + 2) * φ (8*(β/α)) := by nlinarith
  refine ⟨ha, ?_⟩
  intro hsmall
  have hL : 1 ≤ L := by
    apply (le_div_iff₀ hlog).mpr
    simpa using (Real.log_le_log (by norm_num : (0:ℝ)<4) hsmall)
  rw [max_eq_right (by linarith : 0 ≤ L)] at ha
  have hfactor : L+2 ≤ 3*L := by linarith
  exact ha.trans (mul_le_mul_of_nonneg_right hfactor (Nat.cast_nonneg _))

end AutoSamplingTheory.TechnicalLemmas.Analysis.RestartLogComplexity

Exact module and namespace context