Bisection method

9 fully proved

Bisection sequences

DefinitionBisection sequence#✓fully proved

For a function \(f : \mathbb{R} \to \mathbb{R}\) and reals \(a\), \(b\), two sequences \(u, v : \mathbb{N} \to \mathbb{R}\) form a bisection sequence for \(f\) from \(a\) to \(b\) when \(u_0 = a\), \(v_0 = b\), and for every \(n\), writing \(m_n = (u_n + v_n)/2\) for the midpoint, either \(f(m_n) \le 0\), \(u_{n+1} = m_n\) and \(v_{n+1} = v_n\), or \(f(m_n) \ge 0\), \(u_{n+1} = u_n\) and \(v_{n+1} = m_n\).

These are the bracketing endpoints produced by the bisection algorithm; when \(f(m_n) = 0\) either step is allowed.

def IsBisectionSequence (f : ℝ → ℝ) (a b : ℝ) (u v : ℕ → ℝ) : Prop :=
  u 0 = a ∧ v 0 = b ∧ ∀ n,
    let m := (u n + v n) / 2
    (f m ≤ 0 ∧ u (n + 1) = m ∧ v (n + 1) = v n) ∨
      (0 ≤ f m ∧ u (n + 1) = u n ∧ v (n + 1) = m)

Used by 8

Used byBisection method converges at a linear rate · Bisection method: nested intervals · Existence of bisection sequences · Nested bisection intervals from a sign bracket · Bisection invariants · Bisection intervals stay inside the initial interval · Bisection intervals are nested · Length of the bisection intervals

Is Bisection Sequence

TheoremBisection intervals stay inside the initial interval#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\), let \(a \le b\), and let \(u, v\) be a bisection sequence for \(f\) from \(a\) to \(b\). Then \(a \le u_n \le v_n \le b\) for every \(n \in \mathbb{N}\).

theorem le_and_le
    {f : ℝ → ℝ} {a b : ℝ} {u v : ℕ → ℝ}
    (huv : IsBisectionSequence f a b u v) (hab : a ≤ b) (n : ℕ) :
    a ≤ u n ∧ u n ≤ v n ∧ v n ≤ b

Uses 1

Statement usesBisection sequence

TheoremBisection invariants#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) and \(a \le b\) with \(f(a) \le 0 \le f(b)\), and let \(u, v\) be a bisection sequence for \(f\) from \(a\) to \(b\). Then for every \(n \in \mathbb{N}\) we have \(a \le u_n \le v_n \le b\) and \(f(u_n) \le 0 \le f(v_n)\).

theorem invariants
    {f : ℝ → ℝ} {a b : ℝ} {u v : ℕ → ℝ}
    (huv : IsBisectionSequence f a b u v) (hab : a ≤ b)
    (ha : f a ≤ 0) (hb : 0 ≤ f b) (n : ℕ) :
    a ≤ u n ∧ u n ≤ v n ∧ v n ≤ b ∧ f (u n) ≤ 0 ∧ 0 ≤ f (v n)

Uses 1 · Used by 1

Statement usesBisection sequence

Used byNested bisection intervals from a sign bracket

TheoremBisection intervals are nested#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\), let \(a \le b\), and let \(u, v\) be a bisection sequence for \(f\) from \(a\) to \(b\). Then for every \(n \in \mathbb{N}\), \(u_n \le u_{n+1} \le v_{n+1} \le v_n\).

theorem nested
    {f : ℝ → ℝ} {a b : ℝ} {u v : ℕ → ℝ}
    (huv : IsBisectionSequence f a b u v) (hab : a ≤ b) (n : ℕ) :
    u n ≤ u (n + 1) ∧ u (n + 1) ≤ v (n + 1) ∧ v (n + 1) ≤ v n

Uses 1 · Used by 1

Statement usesBisection sequence

Used byNested bisection intervals from a sign bracket

TheoremLength of the bisection intervals#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\), let \(a, b\) be real, and let \(u, v\) be a bisection sequence for \(f\) from \(a\) to \(b\). Then \(v_n - u_n = (b - a)/2^n\) for every \(n \in \mathbb{N}\).

theorem sub_eq
    {f : ℝ → ℝ} {a b : ℝ} {u v : ℕ → ℝ}
    (huv : IsBisectionSequence f a b u v) (n : ℕ) :
    v n - u n = (b - a) / (2 : ℝ) ^ n

Uses 1 · Used by 1

Statement usesBisection sequence

Used byNested bisection intervals from a sign bracket

Existence and convergence of bisection sequences

TheoremExistence of bisection sequences#✓fully proved

For every function \(f : \mathbb{R} \to \mathbb{R}\) and all reals \(a\), \(b\), there are sequences \(u, v\) forming a bisection sequence for \(f\) from \(a\) to \(b\).

theorem exists_isBisectionSequence (f : ℝ → ℝ) (a b : ℝ) :
    ∃ u v, IsBisectionSequence f a b u v

Uses 1 · Used by 1

Statement usesBisection sequence

Used byNested bisection intervals from a sign bracket

TheoremNested bisection intervals from a sign bracket#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) and \(a \le b\) with \(f(a) \le 0 \le f(b)\). Then there is a bisection sequence \(u, v\) for \(f\) from \(a\) to \(b\) such that for every \(n \in \mathbb{N}\): \(u_n \le u_{n+1} \le v_{n+1} \le v_n\), \(v_n - u_n = (b - a)/2^n\), and \(f(u_n)\,f(v_n) \le 0\).

No continuity of \(f\) is needed.

theorem exists_isBisectionSequence_nested
    {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (ha : f a ≤ 0) (hb : 0 ≤ f b) :
    ∃ u v : ℕ → ℝ, IsBisectionSequence f a b u v ∧
      (∀ n, u n ≤ u (n + 1) ∧ u (n + 1) ≤ v (n + 1) ∧ v (n + 1) ≤ v n) ∧
      (∀ n, v n - u n = (b - a) / (2 : ℝ) ^ n) ∧
      ∀ n, f (u n) * f (v n) ≤ 0

Uses 5 · Used by 1

Statement usesBisection sequence

Proof usesBisection invariants · Bisection intervals are nested · Length of the bisection intervals · Existence of bisection sequences

Used byBisection method: nested intervals

TheoremBisection method: nested intervals#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) be continuous on \([a, b]\), where \(a \le b\) and \(f(a) \le 0 \le f(b)\). Then there is a bisection sequence \(u, v\) for \(f\) from \(a\) to \(b\) such that for every \(n \in \mathbb{N}\): \(u_n \le u_{n+1} \le v_{n+1} \le v_n\), \(v_n - u_n = (b - a)/2^n\), and \(f(u_n)\,f(v_n) \le 0\).

Proof: The endpoint pairs are defined recursively by the sign of each midpoint, and induction proves the nesting, sign, and exact halving invariants from Burden and Faires, Section 2.1.

theorem bisection_nested_intervals
    {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b)
    (hf : ContinuousOn f (Set.Icc a b)) (ha : f a ≤ 0) (hb : 0 ≤ f b) :
    ∃ u v : ℕ → ℝ, IsBisectionSequence f a b u v ∧
      (∀ n, u n ≤ u (n + 1) ∧ u (n + 1) ≤ v (n + 1) ∧ v (n + 1) ≤ v n) ∧
      (∀ n, v n - u n = (b - a) / (2 : ℝ) ^ n) ∧
      ∀ n, f (u n) * f (v n) ≤ 0

Sources

• R. L. Burden and J. D. Faires, Numerical Analysis, 10th ed., Section 2.1; stable ref https://en.wikipedia.org/wiki/Bisection_method.

Uses 2

Statement usesBisection sequence

Proof usesNested bisection intervals from a sign bracket

TheoremBisection method converges at a linear rate#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) be continuous on \([a, b]\), where \(a \le b\) and \(f(a) \le 0 \le f(b)\), and let \(u, v\) be a bisection sequence for \(f\) from \(a\) to \(b\). Then there is \(c \in [a, b]\) with \(f(c) = 0\) such that the midpoints \((u_n + v_n)/2\) converge to \(c\) and \(|(u_n + v_n)/2 - c| \le (b - a)/2^{n+1}\) for every \(n \in \mathbb{N}\).

Proof: Monotone convergence gives the common endpoint limit, continuity makes it a root, and the halved interval length gives the midpoint error bound, following Burden and Faires, Theorem 2.1.

theorem bisection_approximate_root_with_rate
    {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b)
    (hf : ContinuousOn f (Set.Icc a b)) (ha : f a ≤ 0) (hb : 0 ≤ f b)
    (u v : ℕ → ℝ) (huv : IsBisectionSequence f a b u v) :
    ∃ c ∈ Set.Icc a b, f c = 0 ∧
      Filter.Tendsto (fun n => (u n + v n) / 2) Filter.atTop (nhds c) ∧
      ∀ n, |(u n + v n) / 2 - c| ≤ (b - a) / (2 : ℝ) ^ (n + 1)

Sources

• R. L. Burden and J. D. Faires, Numerical Analysis, 10th ed., Theorem 2.1.

Uses 1

Statement usesBisection sequence

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.