Steffensen’s derivative-free step

Paper

Remarks on iteration, 1933. Skandinavisk Aktuarietidskrift 1933(1), pp. 64–72. Read a later research treatment of the method.

The result

For f(x) = x² − r², the finite-difference update simplifies to a rational step. Starting above a positive root keeps the denominator positive and the next estimate between the root and the old estimate.

S(x) = x − f(x)/(2x + f(x)) S(x) − r = (x − r)²(1 + x + r)/(2x + x² − r²)

Scope & assumptions

7 checked theorems. Finite-difference factorization, equivalence of raw and simplified updates, fixed roots, exact error, safe denominator, bracket preservation, and a quadratic error bound on r ≤ x ≤ R. No general convergence theorem.

Exact real arithmetic. For the safe region, r > 0 and x ≥ r. The quadratic constant is (1 + R + r)/(2r). Lean defines division by zero as zero; the simplified formula is regular at the root. A numerical implementation of the raw quotient must stop when f(x) = 0 instead of evaluating 0/0.

Prior work

No matching named formalization was located in the bounded search of two Mathlib revisions and indexed web results on 2026-09-10. Related library ingredients already exist. First-formalization status is unconfirmed; this does not establish priority.

Lean proof

Lean + Mathlib 4.33.1 · 7 checked theorems

import Mathlib.Algebra.Field.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity

/-! Steffensen (1933): a derivative-free root step for quadratic functions.
We prove its exact error, denominator safety on a positive branch, and
interval preservation. This is a specialization, not general convergence. -/
namespace PaperToLean.Steffensen
noncomputable section
def f (a x : ℝ) : ℝ := x ^ 2 - a
def slope (a x : ℝ) : ℝ := 2 * x + f a x
def step (a x : ℝ) : ℝ := x - f a x / slope a x
def rawStep (a x : ℝ) : ℝ := x - (f a x) ^ 2 / (f a (x + f a x) - f a x)

theorem divided_difference (a x : ℝ) :
    f a (x + f a x) - f a x = f a x * slope a x := by
  simp only [slope, f]
  ring

theorem raw_equivalence (a x : ℝ) (hd : slope a x ≠ 0) :
    rawStep a x = step a x := by
  unfold rawStep step
  rw [divided_difference]
  field_simp

theorem fixed_root (r : ℝ) : step (r ^ 2) r = r := by
  simp [step, f]

theorem exact_error (r x : ℝ) (hd : slope (r ^ 2) x ≠ 0) :
    step (r ^ 2) x - r = (x - r) ^ 2 * (1 + x + r) / slope (r ^ 2) x := by
  unfold step
  apply (eq_div_iff hd).mpr
  field_simp
  unfold slope f
  ring

theorem safe_denominator (r x : ℝ) (hr : 0 < r) (hx : r ≤ x) :
    0 < slope (r ^ 2) x := by
  unfold slope f
  nlinarith

theorem bracket (r x : ℝ) (hr : 0 < r) (hx : r ≤ x) :
    r ≤ step (r ^ 2) x ∧ step (r ^ 2) x ≤ x := by
  have hd := safe_denominator r x hr hx
  constructor
  · rw [← sub_nonneg, exact_error r x (ne_of_gt hd)]
    have hx0 : 0 < x := lt_of_lt_of_le hr hx
    positivity
  · unfold step
    have hf : 0 ≤ f (r ^ 2) x := by unfold f; nlinarith
    exact sub_le_self _ (div_nonneg hf (le_of_lt hd))

theorem quadratic_bound (r x R : ℝ) (hr : 0 < r) (hx : r ≤ x) (hR : x ≤ R) :
    step (r ^ 2) x - r ≤ (1 + R + r) / (2 * r) * (x - r) ^ 2 := by
  have hd := safe_denominator r x hr hx
  rw [exact_error r x (ne_of_gt hd)]
  have hden : 2 * r ≤ slope (r ^ 2) x := by unfold slope f; nlinarith
  have hx0 : 0 < x := lt_of_lt_of_le hr hx
  calc
    _ ≤ (x - r) ^ 2 * (1 + x + r) / (2 * r) :=
      div_le_div_of_nonneg_left (by positivity) (by positivity) hden
    _ ≤ (x - r) ^ 2 * (1 + R + r) / (2 * r) := by
      apply (div_le_div_iff_of_pos_right (by positivity : 0 < 2 * r)).mpr
      exact mul_le_mul_of_nonneg_left (by linarith) (sq_nonneg _)
    _ = _ := by ring

#print axioms divided_difference
#print axioms raw_equivalence
#print axioms fixed_root
#print axioms exact_error
#print axioms safe_denominator
#print axioms bracket
#print axioms quadratic_bound
end
end PaperToLean.Steffensen

Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Steffensen.lean
SHA-256: 6324c6872f255d1db618724598b0301e51d10482f516f8a97853caf34aaafc25
Result: passed

'PaperToLean.Steffensen.divided_difference' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Steffensen.raw_equivalence' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Steffensen.fixed_root' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Steffensen.exact_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Steffensen.safe_denominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Steffensen.bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Steffensen.quadratic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]

Run it

Install Lean with elan and Git. Download the project ZIP, extract it, and run these commands in that folder. The first command downloads the pinned Mathlib dependencies.

python3 prepare.py
lake env lean -DwarningAsError=true Steffensen.lean

A successful check prints the axiom dependencies and exits without errors.