AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveDepth

- Actual scheduled precision recursion has persistent well-conditioning and an explicit geometric terminal-parameter bound. This is not an error or cost bound for a random sampler. All finite variance readings occur at positive successor precision, including when the initial precision is zero.

theorem parameter_control {κ c r₀ : ℝ} {η : ℕ → ℝ}
    (hκ : 1 ≤ κ) (hc : 0 < c) (hc_upper : c < 1 / 4) (hr₀ : 0 ≤ r₀)
    (hη : ∀ n, 0 < η n ∧ η n ≤ 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))
    (∀ n, 0 ≤ r n ∧ 0 < r (n + 1)) ∧
      Antitone (fun n => K (r n)) ∧
      (∀ m n, m ≤ n → K (r m) < 2 → K (r n) < 2) ∧
      (∀ M N, (4 / 5 : ℝ)^M * K r₀ < 2 →
        0 < (r (M + 1 + N))⁻¹ ∧
        (r (M + 1 + N))⁻¹ ≤ 2 * c * (2 * c / (1 + 2 * c))^N) ∧
      (∀ B : ℝ, 0 < B → ∃ J : ℕ,
        0 < J ∧ 0 < (r J)⁻¹ ∧ (r J)⁻¹ ≤ B) := by
  let condition (κ r : ℝ) : ℝ := (1 + r) / (κ⁻¹ + r)
  let heat (κ c r : ℝ) : ℝ := if 2 ≤ condition κ r then condition κ r else c
  let stepVariance (κ c r h : ℝ) : ℝ := (h + heat κ c r) / (1 + r)
  let nextPrecision (κ c r h : ℝ) : ℝ := r + (stepVariance κ c r h)⁻¹
  let precision (κ c r₀ : ℝ) (η : ℕ → ℝ) : ℕ → ℝ :=
    Nat.rec r₀ (fun j r => nextPrecision κ c r (η j))
  have condition_bounds {κ r : ℝ} (hκ : 1 ≤ κ) (hr : 0 ≤ r) :
      1 ≤ condition κ r := by
    have hkpos : 0 < κ := lt_of_lt_of_le zero_lt_one hκ
    have hbpos : 0 < κ⁻¹ := inv_pos.mpr hkpos
    have hble : κ⁻¹ ≤ 1 := (inv_le_one₀ hkpos).2 hκ
    unfold condition
    apply (one_le_div (add_pos_of_pos_of_nonneg hbpos hr)).2
    linarith

  have condition_antitone {κ r s : ℝ} (hκ : 1 ≤ κ)
      (hr : 0 ≤ r) (hrs : r ≤ s) : condition κ s ≤ condition κ r := by
    have hkpos : 0 < κ := lt_of_lt_of_le zero_lt_one hκ
    have hbpos : 0 < κ⁻¹ := inv_pos.mpr hkpos
    have hble : κ⁻¹ ≤ 1 := (inv_le_one₀ hkpos).2 hκ
    unfold condition
    apply (div_le_div_iff₀ (add_pos_of_pos_of_nonneg hbpos (hr.trans hrs))
      (add_pos_of_pos_of_nonneg hbpos hr)).2
    nlinarith [mul_nonneg (sub_nonneg.mpr hrs) (sub_nonneg.mpr hble)]

  have stepVariance_pos {κ c r h : ℝ} (_hκ : 1 ≤ κ)
      (hc : 0 < c) (hr : 0 ≤ r) (hh : 0 < h) :
      0 < stepVariance κ c r h := by
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/RecursiveDepth.lean:20published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.