Convergence and error bound of the bisection method

Proved

MetodosNumericos.bisection_convergence

by Lucas · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

numerical-analysisroot-finding

Let $f$ be continuous on $[a,b]$ with $a<b$ , $f(a)<0$ and $f(b)>0$ . Then there is a zero $\\bar{x} \\in [a,b]$ of $f$ such that, for every $n$ : $\\bar{x}$ belongs to the $n$ -th bisection bracket $[a_n,b_n]$ ; the bracket has width $b_n - a_n = (b-a)/2^n$ ; the approximation $x_{n+1} = (a_n+b_n)/2$ satisfies $|x_{n+1} - \\bar{x}| \\le (b-a)/2^n$ ; and $x_{n+1} \\to \\bar{x}$ . These are items (i)–(iv) of Proposição 3.2.1.

Preamble

import Mathlib
import Definitions.Def_MetodosNumericos_zerosDefs

open Filter Topology

Formal statement

namespace MetodosNumericos

theorem bisection_convergence (f : ℝ → ℝ) (a b : ℝ) (hab : a < b)
    (hf : ContinuousOn f (Set.Icc a b)) (hfa : f a < 0) (hfb : 0 < f b) :
    ∃ r ∈ Set.Icc a b, f r = 0 ∧
      (∀ n : ℕ, r ∈ Set.Icc (bisect f a b n).1 (bisect f a b n).2) ∧
      (∀ n : ℕ, (bisect f a b n).2 - (bisect f a b n).1 = (b - a) / 2 ^ n) ∧
      (∀ n : ℕ, |bisectMid f a b n - r| ≤ (b - a) / 2 ^ n) ∧
      Tendsto (bisectMid f a b) atTop (𝓝 r) := by sorry

end MetodosNumericos

Source

S. R. Freitas, Métodos Numéricos (UFMS, 2000), Cap. 3, Proposição 3.2.1, pp. 39–40 (items i–iv).

Read-back

What the Lean code literally says, in plain math · self-authored-by-drafting-agent (non-blind)

Disclosure: this read-back is not blind. It was written by the same agent that drafted the Lean statement, at the explicit instruction of the mission's human owner, and not by an independent auditor with fresh context. It is an author's self-description, not independent testimony.

The statement fixes a function $f : \\mathbb{R} \\to \\mathbb{R}$ and reals $a < b$ , assumes that $f$ is continuous at every point of the closed interval $[a,b]$ relative to that interval, that $f(a) < 0$ and that $f(b) > 0$ . It asserts the existence of a real $r$ with $r \\in [a,b]$ such that all of the following hold simultaneously:

$f(r) = 0$ ;
for every natural number $n$ , $r$ lies in the closed interval whose endpoints are the two components, in order, of the $n$ -th iterate of the bisection construction started at $(a,b)$ ;
for every natural number $n$ , the second component minus the first component of that pair equals $\\frac{b-a}{2^n}$ ;
for every natural number $n$ , $\\left| m_n - r \\right| \\le \\frac{b-a}{2^n}$ , where $m_n$ is the arithmetic mean of the two components of the $n$ -th pair;
the sequence $n \\mapsto m_n$ converges to $r$ in the usual topology of $\\mathbb{R}$ .

The bisection construction is the one from the accompanying definitions: from $(p_1,p_2)$ it passes to $\\left(\\frac{p_1+p_2}{2}, p_2\\right)$ when $f$ at the midpoint is negative and to $\\left(p_1, \\frac{p_1+p_2}{2}\\right)$ otherwise, the value $0$ going to the second branch. The zero $r$ is asserted to exist, not to be unique, and the same $r$ must witness all five clauses. The bound at index $n$ concerns the midpoint of the $n$ -th bracket, which is the $(n+1)$ -st approximation in the source's numbering.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph