Root Finding: MVT-based bounds for Newton contraction proofs #
This file contains Mean Value Theorem-based lemmas used to prove Newton method correctness, particularly for showing that Newton contraction implies root existence.
Main lemmas #
mvt_lower_bound- Lower bound from MVTmvt_upper_bound- Upper bound from MVTnewton_positive_increasing_contradicts_contraction- MVT contradiction lemmanewton_negative_increasing_contradicts_contraction- MVT contradiction lemmaquotient_hi_lower_bound- Quotient bound for positive derivativequotient_lo_upper_bound- Quotient bound for positive derivativenewtonStepSimple_contraction_absurd_hi- Contraction contradictionnewtonStepSimple_contraction_absurd_lo- Contraction contradiction
MVT wrapper lemmas #
MVT lower bound: if f' ≥ C on interval I, then f(y) - f(x) ≥ C * (y - x) for x ≤ y in I. This wraps Mathlib's Convex.mul_sub_le_image_sub_of_le_deriv for our use case.
MVT upper bound: if f' ≤ C on interval I, then f(y) - f(x) ≤ C * (y - x) for x ≤ y in I. This wraps Mathlib's Convex.image_sub_le_mul_sub_of_deriv_le for our use case.
Contradiction lemmas for increasing functions #
Contradiction lemma: If f > 0 at I.lo with f' ≥ dI.lo > 0 (increasing), then the Newton quotient Q.hi > hw, contradicting strict contraction Q.hi < hw.
Key argument:
- By MVT: f(c) - f(I.lo) ≥ dI.lo * hw, so f(c) ≥ f(I.lo) + dI.lo * hw > dI.lo * hw
- fc.hi ≥ f(c) > dI.lo * hw
- Q.hi = fc.hi / dI.lo > hw
- But contraction requires Q.hi < hw (from N.lo > I.lo)
- Contradiction
Contradiction lemma: If f < 0 at I.hi with f' ≥ dI.lo > 0 (increasing), then the Newton quotient Q.lo < -hw, contradicting strict contraction Q.lo > -hw.
Key argument:
- By MVT: f(I.hi) - f(c) ≥ dI.lo * hw, so f(c) ≤ f(I.hi) - dI.lo * hw < -dI.lo * hw
- fc.lo ≤ f(c) < -dI.lo * hw
- Q.lo = fc.lo / dI.lo < -hw
- But contraction requires Q.lo > -hw (from N.hi < I.hi)
- Contradiction
Quotient bound lemmas #
When dI.lo > 0, the quotient Q has Q.hi ≥ fc.hi / dI.lo (regardless of fc signs). This is because the invNonzero of positive dI is [1/dI.hi, 1/dI.lo], and the max includes fc.hi * dI.lo⁻¹ as one of its corners.
When dI.lo > 0, the quotient Q has Q.lo ≤ fc.lo / dI.lo.
For negative dI, the quotient Q has Q.hi ≥ fc.lo / dI.hi. This is because fc.lo * dI.hi⁻¹ is one of the four corners in Q = fc * inv(dI), and Q.hi = max of all corners. This bound is used for Newton contraction contradiction when f < 0 at both endpoints.
For negative dI, the quotient Q has Q.lo ≤ fc.hi / dI.hi. This is because fc.hi * dI.hi⁻¹ is one of the four corners in Q = fc * inv(dI), and Q.lo = min of all corners. This bound is used for Newton contraction contradiction when f > 0 at both endpoints.
Generic contraction contradiction lemmas #
These lemmas abstract the Newton step structure to work with any interval fc
that contains f(c). This allows them to be used with both newtonStepSimple
(where fc = evalInterval1 e (singleton c)) and newtonStepTM
(where fc = TaylorModel.valueAtCenterInterval tm).
Generic contradiction: if Q is computed from fc/dI with dI.lo > 0, contraction holds, and f(c) > dI.lo * hw, then False.
This abstracts the key Newton contraction argument:
- Contraction implies Q.hi < hw (since N.lo > I.lo means c - Q.hi > I.lo)
- f(c) > dI.lo * hw implies fc.hi > dI.lo * hw (since fc.hi ≥ f(c))
- quotient_hi_lower_bound says Q.hi ≥ fc.hi / dI.lo > hw
- Contradiction: Q.hi < hw and Q.hi > hw
Generic contradiction for Q.lo case with dI.lo > 0.
Generic contradiction for Q.hi case with dI.hi < 0 (decreasing function).
Generic contradiction for Q.lo case with dI.hi < 0 (decreasing function).
Simple step contradiction lemmas (using generic lemmas) #
Key contradiction: if newtonStepSimple contracts AND fc.hi/dI.lo ≥ hw (with dI.lo > 0), then False.
Key contradiction: if newtonStepSimple contracts AND fc.lo/dI.lo ≤ -hw (with dI.lo > 0), then False.
Contradiction lemmas for decreasing functions #
Contradiction lemma for decreasing function: If f > 0 at I.hi with f' ≤ dI.hi < 0 (decreasing), then the Newton quotient Q.lo = fc.hi/dI.hi ≤ -hw, contradicting strict contraction Q.lo > -hw.
Contradiction lemma for decreasing function: If f < 0 at I.lo with f' ≤ dI.hi < 0 (decreasing), then the Newton quotient violates contraction bounds.
Generic MVT bounds on f(c) #
These lemmas give bounds on evalFunc1 e c (the true function value at the midpoint)
rather than on interval enclosures. This allows them to be used with any interval
that contains f(c), whether from evalInterval1 or TaylorModel.valueAtCenterInterval.
Generic MVT bound: If f' ≥ dI.lo > 0 (increasing) and f(I.lo) > 0, then f(c) > dI.lo * hw where c = midpoint and hw = half-width. This is the core analytic fact used for Newton contraction contradictions.
Generic MVT bound: If f' ≥ dI.lo > 0 (increasing) and f(I.hi) < 0, then f(c) < -dI.lo * hw where c = midpoint and hw = half-width.
Generic MVT bound: If f' ≤ dI.hi < 0 (decreasing) and f(I.lo) < 0, then f(c) < dI.hi * hw where c = midpoint and hw = half-width. Since dI.hi < 0 and hw > 0, we have dI.hi * hw < 0, so f(c) < 0.
Generic MVT bound: If f' ≤ dI.hi < 0 (decreasing) and f(I.hi) > 0, then f(c) > -dI.hi * hw where c = midpoint and hw = half-width.