production module

`AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveCondition`

Read the mathematical statements and proofs in order

1 named declarations scanned from AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/RecursiveCondition.lean.

Imports

Mathlib.Data.Real.Basic externalMathlib.Tactic.Linarith external

Imported by

AutoSamplingTheory.ExampleCasesAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveDepthTests.SmoothedPicardRGOCalculusTests.SmoothedPicardRecursiveCondition

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveCondition.contraction_bounds Partial Not mapped

Read the complete mathematical statement and proof, with Lean below each

- The ill-conditioned recursive update lies between half and four fifths of its previous condition number. The denominator is proved positive from the hypotheses, so no totalized-division exceptional case is used.

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

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/RecursiveCondition.lean:23published source at 0e31a3cda412