ApproximateBisection.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Approximate rational bisection for a Lipschitz residual. A numerically ambiguous sign terminates with a certified residual bound; otherwise the true endpoint signs are preserved. No monotonicity or derivative lower bound is required.

structure OAI.ContinuumCoulomb.ApproximateBisection.Interval line 14
def OAI.ContinuumCoulomb.ApproximateBisection.midpoint line 20
def OAI.ContinuumCoulomb.ApproximateBisection.width line 22
def OAI.ContinuumCoulomb.ApproximateBisection.step line 24
def OAI.ContinuumCoulomb.ApproximateBisection.initial line 30
def OAI.ContinuumCoulomb.ApproximateBisection.run line 32
theorem OAI.ContinuumCoulomb.ApproximateBisection.midpoint_cast line 35
theorem OAI.ContinuumCoulomb.ApproximateBisection.midpoint_mem line 39
structure OAI.ContinuumCoulomb.ApproximateBisection.Invariant line 45
Source documentation
The invariant concerns actual residual values, not numerical signs.
```
structure Invariant (a b : ℚ) (f : ℝ → ℝ) (δ : ℚ) (s : Interval) : Prop where
…
```
Mentions: OAI.ContinuumCoulomb.ApproximateBisection.Interval
theorem OAI.ContinuumCoulomb.ApproximateBisection.initial_invariant line 52
theorem OAI.ContinuumCoulomb.ApproximateBisection.step_invariant line 60
theorem OAI.ContinuumCoulomb.ApproximateBisection.step_width line 88
theorem OAI.ContinuumCoulomb.ApproximateBisection.run_invariant line 103
theorem OAI.ContinuumCoulomb.ApproximateBisection.run_width line 114
theorem OAI.ContinuumCoulomb.ApproximateBisection.invariant_residual line 131

theorem OAI.ContinuumCoulomb.ApproximateBisection.run_residual line 169

Source documentation

After n steps the returned rational has residual at most numerical ambiguity plus the Lipschitz constant times the halved interval width.

theorem run_residual {a b δ : ℚ} {f : ℝ → ℝ} {evaluate : ℚ → ℚ} {L : ℝ}
    (hδ : 0 ≤ δ) (hab : a ≤ b) (ha : 0 ≤ f a) (hb : f b ≤ 0) (hL : 0 ≤ L)
    (heval : ∀ q ∈ Set.Icc a b, |(evaluate q : ℝ) - f q| ≤ (δ : ℝ))
    (hLip : ∀ x ∈ Set.Icc (a : ℝ) b, ∀ y ∈ Set.Icc (a : ℝ) b,
      |f x - f y| ≤ L * |x - y|) (n : ℕ) :
    |f (midpoint (run δ evaluate a b n))| ≤
      2 * (δ : ℝ) + L * (((b : ℝ) - a) / 2 ^ n) := by
…

Mentions: OAI.ContinuumCoulomb.ApproximateBisection.midpoint, OAI.ContinuumCoulomb.ApproximateBisection.run

theorem OAI.ContinuumCoulomb.ApproximateBisection.run_mem line 179

theorem OAI.ContinuumCoulomb.ApproximateBisection.run_binary_precision line 189

Source documentation

Binary magnitude bounds give a number of bisection steps linear in the requested precision and the magnitude exponent.

theorem run_binary_precision {a b δ : ℚ} {f : ℝ → ℝ} {evaluate : ℚ → ℚ} {L : ℝ}
    (hδ : 0 ≤ δ) (hab : a ≤ b) (ha : 0 ≤ f a) (hb : f b ≤ 0) (hL : 0 ≤ L)
    (heval : ∀ q ∈ Set.Icc a b, |(evaluate q : ℝ) - f q| ≤ (δ : ℝ))
    (hLip : ∀ x ∈ Set.Icc (a : ℝ) b, ∀ y ∈ Set.Icc (a : ℝ) b,
      |f x - f y| ≤ L * |x - y|) (B p : ℕ)
    (hδp : (δ : ℝ) ≤ (2 ^ (p + 2))⁻¹)
    (hLB : L ≤ 2 ^ B) (hwidth : (b : ℝ) - a ≤ 2 ^ B) :
    |f (midpoint (run δ evaluate a b (2 * B + p + 1)))| ≤ (2 ^ p : ℝ)⁻¹ := by
…

Mentions: OAI.ContinuumCoulomb.ApproximateBisection.midpoint, OAI.ContinuumCoulomb.ApproximateBisection.run