AutoSamplingTheory.TechnicalLemmas.Analysis.RestartLogComplexity

- A rounded logarithmic horizon gives actual restart accuracy and explicit cost, including zero rounds; budget absorption and small-error order are conditional.

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
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Analysis/RestartLogComplexity.lean:22published source at 0e31a3cda412Open detailed card

Excerpt truncated; the exact source link is authoritative.