AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.LogarithmicDepth

- The actual schedule reaches the source terminal variance threshold at the prescribed logarithmic stage. The upper-depth coefficient is explicit and is distinct from the coefficient defining that stage.

theorem terminal_depth {κ c r₀ q Δ γ C : ℝ} {d : ℕ} {η : ℕ → ℝ}
    (hκ : 1 ≤ κ) (hc : 0 < c) (hc1 : c < 1/4) (hr₀ : 0 ≤ r₀)
    (hη : ∀ n, 0 < η n ∧ η n ≤ c) (hd : 0 < d) (hq : 2 ≤ q)
    (hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1/2) (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hC : 8 ≤ C) :
    let K := fun r : ℝ => (1+r)/(κ⁻¹+r)
    let τ := fun r : ℝ => if 2 ≤ K r then K r else c
    let a := fun r h : ℝ => (h+τ r)/(1+r)
    let step := fun r h : ℝ => r+(a r h)⁻¹
    let r : ℕ → ℝ := Nat.rec r₀ (fun j r => step r (η j))
    let L := q+Real.log (K r₀*d*q/Δ)
    let B := γ/(Real.sqrt (d*L)+L)
    let J := Nat.ceil (C*Real.log (Real.exp 1*K r₀/B))
    2 ≤ L ∧ (0 < B ∧ B ≤ 1) ∧ 0 < J ∧ 0 < (r J)⁻¹ ∧ (r J)⁻¹ ≤ B ∧
      (J:ℝ) ≤ (3*C+(C/2)*Real.log (1/γ))*L := by
  have depth_indices {K B C : ℝ} (hK : 1 ≤ K) (hB : 0 < B) (hB1 : B ≤ 1)
      (hC : 8 ≤ C) :
      let M := Nat.ceil (5 * Real.log K)
      let P := Nat.ceil (2 * Real.log (1 / B))
      let J := Nat.ceil (C * Real.log (Real.exp 1 * K / B))
      (4 / 5 : ℝ)^M * K < 2 ∧ M + 1 + P ≤ J ∧
        (1 / 2 : ℝ)^P ≤ B := by
    dsimp only
    have hKpos : 0 < K := by linarith
    have hL : 0 ≤ Real.log K := Real.log_nonneg hK
    have hH : 0 ≤ Real.log (1 / B) := Real.log_nonneg ((one_le_div hB).2 hB1)
    have hlog : Real.log (Real.exp 1 * K / B) =
        1 + Real.log K + Real.log (1 / B) := by
      rw [Real.log_div (mul_pos (Real.exp_pos _) hKpos).ne' hB.ne',
        Real.log_mul (Real.exp_pos _).ne' hKpos.ne', Real.log_exp]
      simp [sub_eq_add_neg]
    have hM := Nat.le_ceil (5 * Real.log K)
    have hP := Nat.le_ceil (2 * Real.log (1 / B))
    have hMupper := Nat.ceil_lt_add_one (mul_nonneg (by norm_num : (0:ℝ) ≤ 5) hL)
    have hPupper := Nat.ceil_lt_add_one (mul_nonneg (by norm_num : (0:ℝ) ≤ 2) hH)
    have hfour : Real.log (4 / 5 : ℝ) ≤ -(1 / 5) := by
      have := Real.log_le_sub_one_of_pos (by norm_num : (0:ℝ) < 4/5)
      linarith
    have hhalf : Real.log (1 / 2 : ℝ) ≤ -(1 / 2) := by
      have := Real.log_le_sub_one_of_pos (by norm_num : (0:ℝ) < 1/2)
      linarith
    have hentry : (4 / 5 : ℝ)^⌈5 * Real.log K⌉₊ * K ≤ 1 := by
      apply (Real.log_le_log_iff (mul_pos (pow_pos (by norm_num) _) hKpos) zero_lt_one).1
      rw [Real.log_mul (pow_pos (by norm_num : (0:ℝ)<4/5) _).ne' hKpos.ne',
        Real.log_pow, Real.log_one]
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/LogarithmicDepth.lean:19published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.