Why an ill-conditioned recursive stage makes geometric progress

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveCondition.contraction_bounds · theorem · Teaching coverage

Statement

For any real numbers k and h with k at least 2 and h strictly between 0 and 1/4, the displayed rational update lies between k/2 and four fifths of k.

All objects and hypotheses

• k,h are real scalars; 2 ≤ k and 0 < h < 1/4.
• In the paper application k is the ratio of the specified curvature bounds, h is the smoothing parameter, and tau=k. It is not necessarily the optimal condition number of the target.
• The source assumes 0<h≤c0<1/4. For this uniform single-stage calculation, eliminating the unused cutoff gives exactly 0<h<1/4; conversely any such h admits c0=h. No zero-smoothing or closed-endpoint extension is asserted.
• This calculation does not involve a measure, derivative or random variable. The recurrence-to-RGO identification is a separate obligation.

Mathematical proof

theorem contraction_bounds {k h : ℝ} (hk : 2 ≤ k) (hh : 0 < h)
    (hh_upper : h < 1 / 4) :
    k / 2 ≤ k * (k + h + 1) / (2 * k + h) ∧
      k * (k + h + 1) / (2 * k + h) ≤ (4 / 5) * k

theorem contraction_bounds {k h : ℝ} (hk : 2 ≤ k) (hh : 0 < h)
    (hh_upper : h < 1 / 4) :
    k / 2 ≤ k * (k + h + 1) / (2 * k + h) ∧
      k * (k + h + 1) / (2 * k + h) ≤ (4 / 5) * k := by
  have hk_nonneg : 0 ≤ k := by linarith
  have hden : 0 < 2 * k + h := by linarith
  constructor
  · apply (le_div_iff₀ hden).2
    nlinarith [mul_nonneg hk_nonneg hh.le]
  · apply (div_le_iff₀ hden).2
    have hmargin : 0 ≤ 3 * k - h - 5 := by linarith
    nlinarith [mul_nonneg hk_nonneg hmargin]

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveCondition

Scope and omitted-condition boundaries

• Only Lemma 6.6(i)'s scalar calculation is covered. Lemma 6.4's normalized RGO closure and curvature formulas remain separate.
• The well-conditioned phase, finite termination, sampling-error propagation and actual expected query count are not conclusions.
• The first test checks k=2,h=1/8; the second derives this interface from the paper's strict c0 range. An earlier unneeded endpoint generalization was removed after independent source review; its artifacts are retained.