/-- A positive **binary64 number** (an IEEE 754 "double"), ignoring the limits on the exponent:`m · 2ᵉ` with an integer *significand* `m` of exactly 53 bits, `2⁵² ≤ m < 2⁵³`, and an integerexponent `e`. -/def IsBinary64 (x : ℝ) : Prop := ∃ m e : ℤ, 2 ^ 52 ≤ m ∧ m < 2 ^ 53 ∧ x = m * (2 : ℝ) ^ e
/-- The **standard model of floating-point arithmetic**: `x̂` is `x` with a relative error of atmost `u`, i.e. `x̂ = x (1 + δ)` for some `|δ| ≤ u`. For binary64 with rounding to nearest,`u = 2⁻⁵³`, half of machine epsilon. -/def RoundsTo (u x xhat : ℝ) : Prop := ∃ δ : ℝ, |δ| ≤ u ∧ xhat = x * (1 + δ)
/-- One step of **bisection** on an interval `[a, b]` (stored as a pair): look at the midpoint`m`; keep `[m, b]` if `f m ≤ 0` and `[a, m]` otherwise, so a sign change is kept. -/noncomputable def bisectStep (f : ℝ → ℝ) (p : ℝ × ℝ) : ℝ × ℝ := if f ((p.1 + p.2) / 2) ≤ 0 then ((p.1 + p.2) / 2, p.2) else (p.1, (p.1 + p.2) / 2)
/-- The interval after `n` steps of bisection, starting from `[a, b]`. -/noncomputable def bisect (f : ℝ → ℝ) (a b : ℝ) : ℕ → ℝ × ℝ | 0 => (a, b) | n + 1 => bisectStep f (bisect f a b n)
bisect_widththeoremProved here from basic factspropext, Classical.choice, Quot.sound
bisect_widthLean 4Proved here from basic factsFormally verified
/-- **Bisection halves the interval**: after `n` steps its width is `(b − a)/2ⁿ`. -/theorem bisect_width (f : ℝ → ℝ) (a b : ℝ) (n : ℕ) : (bisect f a b n).2 - (bisect f a b n).1 = (b - a) / 2 ^ n := by induction n with | zero => simp [bisect] | succ k ih => simp only [bisect, bisectStep] split_ifs <;> simp only [pow_succ] <;> linear_combination ih / 2
bisect_signtheoremProved here from basic factspropext, Classical.choice, Quot.sound
bisect_signLean 4Proved here from basic factsFormally verified
/-- **The loop invariant of bisection**: if `f a ≤ 0 ≤ f b`, then after every step the left endstill has `f ≤ 0` and the right end `f ≥ 0`. -/theorem bisect_sign (f : ℝ → ℝ) (a b : ℝ) (ha : f a ≤ 0) (hb : 0 ≤ f b) (n : ℕ) : f (bisect f a b n).1 ≤ 0 ∧ 0 ≤ f (bisect f a b n).2 := by induction n with | zero => exact ⟨ha, hb⟩ | succ k ih => simp only [bisect, bisectStep] split_ifs with h · exact ⟨h, ih.2⟩ · exact ⟨ih.1, (lt_of_not_ge h).le⟩
bisection_convergestheoremProved here from basic factspropext, Classical.choice, Quot.sound
bisection_convergesLean 4Proved here from basic factsFormally verified
/-- **Bisection always works for a continuous function with a sign change.** If `f` iscontinuous, `a ≤ b` and `f a ≤ 0 ≤ f b`, then for every `n` there is a root `c` of `f` within`(b − a)/2ⁿ⁺¹` of the `n`-th midpoint. The root comes from the intermediate value theorem(Mathlib's `intermediate_value_Icc`) applied to the current interval. -/theorem bisection_converges (f : ℝ → ℝ) (hf : Continuous f) (a b : ℝ) (hab : a ≤ b) (ha : f a ≤ 0) (hb : 0 ≤ f b) (n : ℕ) : ∃ c, f c = 0 ∧ |((bisect f a b n).1 + (bisect f a b n).2) / 2 - c| ≤ (b - a) / 2 ^ (n + 1) := by set p := bisect f a b n with hp have hw : p.2 - p.1 = (b - a) / 2 ^ n := bisect_width f a b n have hs := bisect_sign f a b ha hb n have hle : p.1 ≤ p.2 := by have : 0 ≤ (b - a) / 2 ^ n := div_nonneg (by linarith) (by positivity) linarith obtain ⟨c, ⟨hc1, hc2⟩, hfc⟩ := intermediate_value_Icc hle hf.continuousOn ⟨hs.1, hs.2⟩ refine ⟨c, hfc, ?_⟩ rw [abs_le, pow_succ] constructor <;> · rw [div_mul_eq_div_div] at * linarith
heron_ge_sqrttheoremProved here from basic factspropext, Classical.choice, Quot.sound
heron_ge_sqrtLean 4Proved here from basic factsFormally verified
/-- From any positive start, every Heron iterate is at least `√a` (an instance of the AM–GMinequality, read off from `heron_error`: the right-hand side is a square over a positivenumber). -/theorem heron_ge_sqrt {a x : ℝ} (ha : 0 ≤ a) (hx : 0 < x) : √a ≤ (x + a / x) / 2 := by have h := heron_error ha hx have : 0 ≤ (x - √a) ^ 2 / (2 * x) := by positivity linarith
heron_quadratictheoremProved here from basic factspropext, Classical.choice, Quot.sound
heron_quadraticLean 4Proved here from basic factsFormally verified
/-- **Quadratic convergence of Heron's method.** If `x ≥ √a > 0`, the new error is at most theold error squared, divided by `2√a`. So once the error is below `√a`, the number of correctdigits roughly doubles at every step. -/theorem heron_quadratic {a x : ℝ} (ha : 0 < a) (hx : √a ≤ x) : |(x + a / x) / 2 - √a| ≤ (x - √a) ^ 2 / (2 * √a) := by have hs : 0 < √a := sqrt_pos.mpr ha have hx0 : 0 < x := lt_of_lt_of_le hs hx rw [heron_error ha.le hx0, abs_of_nonneg (by positivity)] apply div_le_div_of_nonneg_left (by positivity) (by positivity) linarith
newton_algebraictheoremApplies a library theorempropext, Classical.choice, Quot.sound
newton_algebraicLean 4Applies a library theoremFormally verified
/-- **Quadratic convergence, algebraically.** For a polynomial `P` over a commutative ring, if`P(x)` is nilpotent and `P'(x)` is invertible, then after `n` Newton steps `P(x)^(2ⁿ)` dividesthe new value of `P`: the "error" is raised to the power `2ⁿ`. This is Mathlib's`Polynomial.aeval_pow_two_pow_dvd_aeval_iterate_newtonMap`, the engine of Hensel's lemma. -/theorem newton_algebraic {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] {P : R[X]} {x : S} (h : IsNilpotent (aeval x P)) (h' : IsUnit (aeval x (derivative P))) (n : ℕ) : (aeval x P) ^ (2 ^ n) ∣ aeval (P.newtonMap^[n] x) P := aeval_pow_two_pow_dvd_aeval_iterate_newtonMap h h' n
trapezoid_errortheoremApplies a library theorempropext, Classical.choice, Quot.sound
trapezoid_errorLean 4Applies a library theoremFormally verified
/-- **The error of the composite trapezoidal rule** with `N` strips is at most`|b − a|³ ζ / (12 N²)` when `|f''| ≤ ζ` on the interval — that is, `(b − a) h² ζ / 12` with`h = (b − a)/N`: the `O(h²)` of the lesson. This applies Mathlib's`trapezoidal_error_le_of_c2`, whose proof is the lesson's proof (differentiate the error of onestrip twice). -/theorem trapezoid_error {f : ℝ → ℝ} {a b : ℝ} (hf : ContDiffOn ℝ 2 f (uIcc a b)) {ζ : ℝ} (hζ : ∀ x, |iteratedDerivWithin 2 f (uIcc a b) x| ≤ ζ) {N : ℕ} (hN : 0 < N) : |trapezoidal_error f N a b| ≤ |b - a| ^ 3 * ζ / (12 * N ^ 2) := trapezoidal_error_le_of_c2 hf hζ hN
/-- Show that every Heron iterate from a positive start is at least `√a`.Hint: use `heron_error` and the fact that `(x - √a) ^ 2 / (2 * x)` is non-negative(`positivity`), then `linarith`. -/theorem heron_ge_sqrt {a x : ℝ} (ha : 0 ≤ a) (hx : 0 < x) : √a ≤ (x + a / x) / 2 := by sorry
Show the compiled solution
heron_ge_sqrtLean 4Proved here from basic factsFormally verified
/-- From any positive start, every Heron iterate is at least `√a` (an instance of the AM–GMinequality, read off from `heron_error`: the right-hand side is a square over a positivenumber). -/theorem heron_ge_sqrt {a x : ℝ} (ha : 0 ≤ a) (hx : 0 < x) : √a ≤ (x + a / x) / 2 := by have h := heron_error ha hx have : 0 ≤ (x - √a) ^ 2 / (2 * x) := by positivity linarith
/-- Prove the loop invariant of bisection.Hint: induction on `n`; in the step, unfold `bisect` and `bisectStep` and split on the `if`(`split_ifs with h`). In the `else` branch, `h : ¬ f m ≤ 0` gives `0 < f m`. -/theorem bisect_sign (f : ℝ → ℝ) (a b : ℝ) (ha : f a ≤ 0) (hb : 0 ≤ f b) (n : ℕ) : f (bisect f a b n).1 ≤ 0 ∧ 0 ≤ f (bisect f a b n).2 := by sorry
Show the compiled solution
bisect_signLean 4Proved here from basic factsFormally verified
/-- **The loop invariant of bisection**: if `f a ≤ 0 ≤ f b`, then after every step the left endstill has `f ≤ 0` and the right end `f ≥ 0`. -/theorem bisect_sign (f : ℝ → ℝ) (a b : ℝ) (ha : f a ≤ 0) (hb : 0 ≤ f b) (n : ℕ) : f (bisect f a b n).1 ≤ 0 ∧ 0 ≤ f (bisect f a b n).2 := by induction n with | zero => exact ⟨ha, hb⟩ | succ k ih => simp only [bisect, bisectStep] split_ifs with h · exact ⟨h, ih.2⟩ · exact ⟨ih.1, (lt_of_not_ge h).le⟩