Grace/Cumulus/Real/Analysis/IntermediateValue.g17

Open in Workbench Download source

Imports

Intervals

Declarations

Source

1-- The intermediate value theorem for continuous functions on a closed interval2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Real.Analysis.IntermediateValue8import Intervals910-- The points of the interval where f stays below the target value.11def belowPoints (f : Set) (A B V : Real) : Set :=12  { X ∈ closedInterval(A, B) | (f(X):R) < V }1314-- A continuous function on [A, B] that starts below V and ends above it takes15-- the value V. The point is the supremum C of the set where f < V: if f(C)16-- were below V, continuity would put a point to the right of C into that set;17-- if f(C) were above V, every point of the set would sit below C minus some18-- positive margin, so C would not be the least upper bound.19theorem closedInterval.intermediate_value (f : Set) (A B V : Real)20  requires ordered : A ≤ B21  requires continuous : ContinuousOn(f, closedInterval(A, B))22  requires below : (f(A):R) < V23  requires above : V < (f(B):R)24  shows ∃ C ∈ closedInterval(A, B), f(C) = V25proof26  rcases continuous with ⟨function, subset, pointwise⟩27  have leftMember := closedInterval.left_mem with *28  have rightMember := closedInterval.right_mem with *29  have aData : A ∈ closedInterval(A, B) ∧ (f(A):R) < V30    constructor31    . exact leftMember32    . exact below33  have aIn : A ∈ belowPoints(f, A, B, V)34    exact belowPoints.membership.backward with aData35  have inhabited : Nonempty(belowPoints(f, A, B, V)) := ⟨A, aIn⟩36  have pointsReal : belowPoints(f, A, B, V) ⊆ ℝ37    intros X member38    obtain ⟨inInterval, negative⟩ := belowPoints.membership.forward with member39    obtain ⟨realX, lowerX, upperX⟩ := closedInterval.membership.forward with inInterval40    exact realX41  have upper : RealUpperBound(belowPoints(f, A, B, V), B)42    unfold RealUpperBound43    have typedB : Real(B) by assumption44    refine ⟨typedB, pointsReal, _⟩45    intros X member46    obtain ⟨inInterval, negative⟩ := belowPoints.membership.forward with member47    obtain ⟨realX, lowerX, upperX⟩ := closedInterval.membership.forward with inInterval48    exact realLe.subset with *49  have bounded : ∃ D, RealUpperBound(belowPoints(f, A, B, V), D) := ⟨B, upper⟩50  obtain ⟨C, lubC⟩ := Real.least_upper_bound_property at belowPoints(f, A, B, V) with *51  rcases lubC with ⟨⟨typedC, pointsSubset, boundsC⟩, leastC⟩52  have realC : C ∈ ℝ by exact typedC53  have aSubset := boundsC with A, aIn54  have aLe := realLe.of_subset at A, C with *55  have cSubset := leastC with B, upper56  have cLe := realLe.of_subset at C, B with *57  have cData : C ∈ ℝ ∧ A ≤ C ∧ C ≤ B by refine ⟨realC, aLe, cLe⟩58  have cIn : C ∈ closedInterval(A, B)59    exact closedInterval.membership.backward with cData60  have within := pointwise with C, cIn61  witness C62  constructor63  . exact cIn64  . have split : (f(C):R) < V ∨ ¬((f(C):R) < V)65      tauto66    cases split with lowC | notLow67    . exfalso68      have gap : 0 < V - (f(C):R) by linarith69      obtain ⟨D, realD, positiveD, maps⟩ :=70        ContinuousWithinAt.maps_ball with *71      have halfPositive := half.positive at D with *72      have halfLess := half.lt_self at D with *73      have reach : C + half(D) ≤ B ∨ ¬(C + half(D) ≤ B) by tauto74      cases reach with inside | outside75      . have xReal := realAddValue.real at C, half(D) with *76        have xMember : C + half(D) ∈ ℝ by exact xReal77        have xData : C + half(D) ∈ ℝ ∧ A ≤ C + half(D) ∧ C + half(D) ≤ B78          refine ⟨xMember, _, inside⟩79          linarith80        have xIn : C + half(D) ∈ closedInterval(A, B)81          exact closedInterval.membership.backward with xData82        have nearData : C - D < C + half(D) ∧ C + half(D) < C + D83          constructor84          . linarith85          . linarith86        have near : C + half(D) ∈ openBall(C, D)87          exact openBall.order_characterization.backward with *88        have mapped := maps with C + half(D), xIn, near89        obtain ⟨lowerBound, upperBound⟩ := openBall.order_characterization.forward with mapped90        have xLow : (f(C + half(D)):R) < V by linarith91        have xPointData : C + half(D) ∈ closedInterval(A, B) ∧ (f(C + half(D)):R) < V92          constructor93          . exact xIn94          . exact xLow95        have xInPoints : C + half(D) ∈ belowPoints(f, A, B, V)96          exact belowPoints.membership.backward with xPointData97        have xSubset := boundsC with C + half(D), xInPoints98        have xLe := realLe.of_subset at C + half(D), C with *99        linarith100      . have bLess := realLess.of_not_le with *101        have nearData : C - D < B ∧ B < C + D102          constructor103          . linarith104          . linarith105        have near : B ∈ openBall(C, D)106          exact openBall.order_characterization.backward with *107        have mapped := maps with B, rightMember, near108        obtain ⟨lowerBound, upperBound⟩ := openBall.order_characterization.forward with mapped109        linarith110    . have notBelow := realLe.of_not_less with *111      have split2 : V < (f(C):R) ∨ ¬(V < (f(C):R)) by tauto112      cases split2 with highC | notHigh113      . exfalso114        have gap : 0 < (f(C):R) - V by linarith115        obtain ⟨D, realD, positiveD, maps⟩ :=116          ContinuousWithinAt.maps_ball with *117        have halfPositive := half.positive at D with *118        have halfLess := half.lt_self at D with *119        have marginReal := realSubValue.real at C, half(D) with *120        have smallerUpper : RealUpperBound(belowPoints(f, A, B, V), C - half(D))121          unfold RealUpperBound122          refine ⟨marginReal, pointsReal, _⟩123          intros X member124          obtain ⟨xIn, xLow⟩ := belowPoints.membership.forward with member125          obtain ⟨xMember, lowerX, upperX⟩ := closedInterval.membership.forward with xIn126          have xSubsetC := boundsC with X, member127          have xLeC := realLe.of_subset at X, C with *128          have xLe : X ≤ C - half(D)129            by_contra notLe130            have far := realLess.of_not_le with *131            have nearData : C - D < X ∧ X < C + D132              constructor133              . linarith134              . linarith135            have near : X ∈ openBall(C, D)136              exact openBall.order_characterization.backward with *137            have mapped := maps with X, xIn, near138            obtain ⟨lowerBound, upperBound⟩ := openBall.order_characterization.forward with mapped139            linarith140          exact realLe.subset with *141        have cSubsetSmaller := leastC with C - half(D), smallerUpper142        have cLeSmaller := realLe.of_subset at C, C - half(D) with *143        linarith144      . have notAbove := realLe.of_not_less at f(C), V with *145        exact realLe.antisymmetric with *146147-- The usual statement with weak inequalities at the endpoints.148theorem closedInterval.intermediate_value_le (f : Set) (A B V : Real)149  requires ordered : A ≤ B150  requires continuous : ContinuousOn(f, closedInterval(A, B))151  requires below : (f(A):R) ≤ V152  requires above : V ≤ (f(B):R)153  shows ∃ C ∈ closedInterval(A, B), f(C) = V154proof155  have leftMember := closedInterval.left_mem at A, B with *156  have rightMember := closedInterval.right_mem at A, B with *157  have function : f : ℝ → ℝ158    rcases continuous with ⟨function, subset, pointwise⟩159    exact function160  have leftCase : (f(A):R) = V ∨ ¬((f(A):R) = V) by tauto161  cases leftCase with leftEqual | leftDifferent162  . refine ⟨A, leftMember, leftEqual⟩163  . have rightCase : (f(B):R) = V ∨ ¬((f(B):R) = V)164      tauto165    cases rightCase with rightEqual | rightDifferent166    . refine ⟨B, rightMember, rightEqual⟩167    . have strictBelow : (f(A):R) < V168        have notLe : ¬(V ≤ (f(A):R))169          intro le170          have equal := realLe.antisymmetric at f(A), V with *171          exact leftDifferent with equal172        exact realLess.of_not_le with *173      have strictAbove : V < (f(B):R)174        have notLe : ¬((f(B):R) ≤ V)175          intro le176          have equal := realLe.antisymmetric at f(B), V with *177          exact rightDifferent with equal178        exact realLess.of_not_le with *179      exact closedInterval.intermediate_value with *180181-- A continuous function that changes sign on [A, B] has a zero there.182theorem closedInterval.zero_of_sign_change (f : Set) (A B : Real)183  requires ordered : A ≤ B184  requires continuous : ContinuousOn(f, closedInterval(A, B))185  requires negative : (f(A):R) < 0186  requires positive : 0 < (f(B):R)187  shows ∃ C ∈ closedInterval(A, B), f(C) = (0:R)188proof189  exact closedInterval.intermediate_value with *190