Grace/Cumulus/Real/Analysis/Intervals.g17

Open in Workbench Download source

Imports

Continuity

Declarations

Source

1-- Real analysis: Intervals2-- 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.Intervals8import Continuity910-- Section: Intervals11def closedInterval (A B : Real) : Set :=12  { X ∈ ℝ | A ≤ X ∧ X ≤ B }1314theorem closedInterval.subset_reals (A B : Real)15  shows closedInterval(A, B) ⊆ ℝ16proof17  intros X member18  obtain ⟨realX, lower, upper⟩ := closedInterval.membership.forward with member19  exact realX2021theorem closedInterval.left_mem (A B : Real)22  requires ordered : A ≤ B23  shows A ∈ closedInterval(A, B)24proof25  have realA : A ∈ ℝ by simp [Real]26  have reflexive := realLe.reflexive at A27  have data : A ∈ ℝ ∧ A ≤ A ∧ A ≤ B28    constructor29    . exact realA30    . constructor31      . exact reflexive32      . exact ordered33  exact closedInterval.membership.backward with data3435theorem closedInterval.right_mem (A B : Real)36  requires ordered : A ≤ B37  shows B ∈ closedInterval(A, B)38proof39  have realB : B ∈ ℝ by simp [Real]40  have reflexive := realLe.reflexive at B41  have data : B ∈ ℝ ∧ A ≤ B ∧ B ≤ B42    constructor43    . exact realB44    . constructor45      . exact ordered46      . exact reflexive47  exact closedInterval.membership.backward with data4849theorem closedInterval.nonempty_iff (A B : Real)50  shows (∃ X, X ∈ closedInterval(A, B)) ↔ A ≤ B51proof52  constructor53  . intro inhabited54    obtain ⟨X, member⟩ := inhabited55    obtain ⟨realX, lower, upper⟩ := closedInterval.membership.forward with member56    exact realLe.transitive with lower, upper57  . intro ordered58    witness A59    exact closedInterval.left_mem with ordered6061theorem closedInterval.nested (A B C D : Real)62  requires left : C ≤ A63  requires right : B ≤ D64  shows closedInterval(A, B) ⊆ closedInterval(C, D)65proof66  intros X member67  obtain ⟨realX, lower, upper⟩ := closedInterval.membership.forward with member68  have typedX : Real(X) by exact realX69  have lowerBound := realLe.transitive at C, A, X with70    *{2}, typedX, left, lower71  have upperBound := realLe.transitive with upper, right72  have result : X ∈ ℝ ∧ C ≤ X ∧ X ≤ D73    constructor74    . exact realX75    . constructor76      . exact lowerBound77      . exact upperBound78  exact closedInterval.membership.backward with result7980-- Continuity within S only asks about arguments of S near A. This is the81-- natural endpoint notion for functions on a closed interval.82predicate ContinuousWithinAt (f S : Set) (A : Real) :=83  FunctionBetween(f, ℝ, ℝ) ∧ S ⊆ ℝ ∧84  (∀ E ∈ ℝ, 0 < E →85    ∃ D ∈ ℝ, 0 < D ∧86      ∀ X ∈ ℝ, (X ∈ S → (X ∈ openBall(A, D) →87        f(X) ∈ openBall(f(A), E))))8889predicate ContinuousOn (f S : Set) :=90  FunctionBetween(f, ℝ, ℝ) ∧ S ⊆ ℝ ∧91  (∀ A ∈ S, ContinuousWithinAt(f, S, A))9293-- Uniform continuity chooses one input radius for every pair of points of S.94predicate UniformContinuousOn (f S : Set) :=95  FunctionBetween(f, ℝ, ℝ) ∧ S ⊆ ℝ ∧96  (∀ E ∈ ℝ, 0 < E →97    ∃ D ∈ ℝ, 0 < D ∧98      ∀ X ∈ ℝ, (X ∈ S →99        ∀ Y ∈ ℝ, (Y ∈ S → (X ∈ openBall(Y, D) →100          f(X) ∈ openBall(f(Y), E)))))101102theorem ContinuousAt.continuous_within_at (f S : Set) (A : Real)103  requires continuous : ContinuousAt(f, A)104  requires subset : S ⊆ ℝ105  shows ContinuousWithinAt(f, S, A)106proof107  constructor108  . exact ContinuousAt.function with continuous109  . constructor110    . exact subset111    . intros E realE positive112      obtain ⟨D, realD, positiveD, maps⟩ := ContinuousAt.maps_ball with continuous, positive113      witness D114      constructor115      . exact realD116      . constructor117        . exact positiveD118        . intros X realX member near119          exact maps with X, realX, near120121theorem Continuous.continuous_on (f S : Set)122  requires continuous : Continuous(f)123  requires subset : S ⊆ ℝ124  shows ContinuousOn(f, S)125proof126  constructor127  . exact Continuous.function with continuous128  . constructor129    . exact subset130    . intros A member131      have subsetLaw := subset132      have realA := subsetLaw with A, member133      have typedA : Real(A)134        unfold Real135        exact realA136      have atA := Continuous.at with continuous137      exact ContinuousAt.continuous_within_at with atA, subset138139theorem UniformContinuousOn.continuous_on (f S : Set)140  requires uniform : UniformContinuousOn(f, S)141  shows ContinuousOn(f, S)142proof143  rcases uniform with ⟨function, subset, control⟩144  constructor145  . exact function146  . constructor147    . exact subset148    . intros A member149      have subsetLaw := subset150      have realA := subsetLaw with A, member151      constructor152      . exact function153      . constructor154        . exact subset155        . intros E realE positive156          obtain ⟨D, realD, positiveD, maps⟩ :=157            control with E, realE, positive158          witness D159          constructor160          . exact realD161          . constructor162            . exact positiveD163            . intros X realX xMember near164              exact maps with X, realX, xMember, A, realA, member, near165166theorem identity.uniform_continuous_on (S : Set)167  requires subset : S ⊆ ℝ168  shows UniformContinuousOn(identity(ℝ), S)169proof170  have function := identity.function at ℝ171  constructor172  . exact function173  . constructor174    . exact subset175    . intros E realE positive176      witness E177      constructor178      . exact realE179      . constructor180        . exact positive181        . intros X realX xMember Y realY yMember near182          have mappedX := identity.relates with realX183          have valueX := FunctionBetween.apply_value with function, realX, mappedX184          have mappedY := identity.relates with realY185          have valueY := FunctionBetween.apply_value with function, realY, mappedY186          rwa [valueX, valueY]187188theorem constantFunction.uniform_continuous_on (S : Set) (L : Real)189  requires subset : S ⊆ ℝ190  shows UniformContinuousOn(constantFunction(ℝ, ℝ, L), S)191proof192  have realL : L ∈ ℝ by simp [Real]193  have function := constantFunction.function at ℝ, ℝ, L with realL194  constructor195  . exact function196  . constructor197    . exact subset198    . intros E realE positive199      witness E200      constructor201      . exact realE202      . constructor203        . exact positive204        . intros X realX xMember Y realY yMember near205          have valueX := constantFunction.apply with realX, realL206          have valueY := constantFunction.apply with realY, realL207          rw [valueX, valueY]208          exact openBall.center with positive209210-- On a closed interval the identity is continuous at both endpoints in the211-- relative sense used by integration.212theorem closedInterval.identity_continuous (A B : Real)213  shows ContinuousOn(identity(ℝ), closedInterval(A, B))214proof215  have subset := closedInterval.subset_reals at A, B with216    *{2}217  have uniform := identity.uniform_continuous_on with subset218  exact UniformContinuousOn.continuous_on with uniform219220-- Relative continuity has the same arithmetic closure as global continuity.221-- Keeping the set membership guard inside the epsilon-delta argument makes222-- these rules valid at interval endpoints.223theorem ContinuousWithinAt.maps_ball (f S : Set) (A E : Real)224  requires continuous : ContinuousWithinAt(f, S, A)225  requires positive : 0 < E226  shows ∃ D ∈ ℝ, 0 < D ∧ (∀ X ∈ ℝ, X ∈ S → X ∈ openBall(A, D) → f(X) ∈ openBall(f(A), E))227proof228  rcases continuous with ⟨function, subset, maps⟩229  exact maps with E, positive230231theorem ContinuousWithinAt.function (f S : Set) (A : Real)232  requires continuous : ContinuousWithinAt(f, S, A)233  shows f : ℝ → ℝ234proof235  rcases continuous with ⟨function, subset, maps⟩236  exact function237238theorem ContinuousWithinAt.add (f g S : Set) (A : Real)239  requires continuousF : ContinuousWithinAt(f, S, A)240  requires continuousG : ContinuousWithinAt(g, S, A)241  shows ContinuousWithinAt(pointwiseAdd(f, g), S, A)242proof243  have fFunction := ContinuousWithinAt.function with continuousF244  have gFunction := ContinuousWithinAt.function with continuousG245  have realA : A ∈ ℝ by simp [Real]246  have subset : S ⊆ ℝ247    rcases continuousF with ⟨graph, subsetF, maps⟩248    exact subsetF249  constructor250  . exact pointwiseAdd.function with fFunction, gFunction251  . constructor252    . exact subset253    . intros E realE positive254      have typedE : Real(E) by exact realE255      have radiusPositive := half.positive with positive256      obtain ⟨D, realD, positiveD, mapsF⟩ := ContinuousWithinAt.maps_ball with continuousF, radiusPositive257      obtain ⟨R, realR, positiveR, mapsG⟩ := ContinuousWithinAt.maps_ball with continuousG, radiusPositive258      have typedD : Real(D) by exact realD259      have typedR : Real(R) by exact realR260      obtain ⟨Q, realS, positiveS, sLeD, sLeR⟩ := positiveRadius.common with261        typedD, typedR, positiveD, positiveR262      have typedS : Real(Q) by exact realS263      witness Q264      constructor265      . exact realS266      . constructor267        . exact positiveS268        . intros X realX member near269          have typedX : Real(X) by exact realX270          have nearF := openBall.mono at X, A, Q, D with271            typedX, assumption, typedS, typedD, near, sLeD272          have nearG := openBall.mono at X, A, Q, R with273            typedX, assumption, typedS, typedR, near, sLeR274          have mappedF := mapsF with X, realX, member, nearF275          have mappedG := mapsG with X, realX, member, nearG276          have fXReal := FunctionBetween.apply_closed with fFunction, realX277          have gXReal := FunctionBetween.apply_closed with gFunction, realX278          have fAReal := FunctionBetween.apply_closed with fFunction, realA279          have gAReal := FunctionBetween.apply_closed with gFunction, realA280          have typedFX : Real(f(X)) by exact fXReal281          have typedGX : Real(g(X)) by exact gXReal282          have typedFA : Real(f(A)) by exact fAReal283          have typedGA : Real(g(A)) by exact gAReal284          have sumNear := openBall.add with mappedF, mappedG285          have doubled := half.add_self with typedE286          rw doubled at sumNear287          have valueX := pointwiseAdd.value with typedX, fFunction, gFunction, typedFX, typedGX288          have valueA := pointwiseAdd.value at f, g, A with289            assumption, fFunction, gFunction, typedFA, typedGA290          rwa [valueX, valueA]291292theorem ContinuousWithinAt.mul (f g S : Set) (A : Real)293  requires continuousF : ContinuousWithinAt(f, S, A)294  requires continuousG : ContinuousWithinAt(g, S, A)295  shows ContinuousWithinAt(pointwiseMul(f, g), S, A)296proof297  have fFunction := ContinuousWithinAt.function with continuousF298  have gFunction := ContinuousWithinAt.function with continuousG299  have realA : A ∈ ℝ by simp [Real]300  have fAReal := FunctionBetween.apply_closed with fFunction, realA301  have gAReal := FunctionBetween.apply_closed with gFunction, realA302  have typedFA : Real(f(A)) by exact fAReal303  have typedGA : Real(g(A)) by exact gAReal304  have subset : S ⊆ ℝ305    rcases continuousF with ⟨graph, subsetF, maps⟩306    exact subsetF307  constructor308  . exact pointwiseMul.function at f, g with fFunction, gFunction309  . constructor310    . exact subset311    . intros E realE positiveE312      have typedE : Real(E) by exact realE313      have scaleGReal := limitScale.real with typedGA314      have scaleGPositive := limitScale.positive with typedGA315      have radiusFReal := scaledRadius.real with typedE, scaleGReal316      have radiusFPositive := scaledRadius.positive with positiveE, scaleGPositive317      have absFAReal := abs.real with typedFA318      have boundReal := realAddValue.real with radiusFReal, absFAReal319      have radiusAboveAbs := realLess.add_right with realZero.real, radiusFReal, absFAReal, radiusFPositive320      have zeroPlusAbs := realAddValue.zero_left with absFAReal321      rw zeroPlusAbs at radiusAboveAbs322      have boundPositive := realLe.transitive_less at323        realZero, abs(f(A)),324        scaledRadius(E, limitScale(g(A))) + abs(f(A)) with325          realZero.real, absFAReal, boundReal,326          abs.nonnegative at f(A) with typedFA, radiusAboveAbs327      have radiusGPositive := scaledRadius.positive with positiveE, boundPositive328      obtain ⟨D, realD, positiveD, mapsF⟩ := ContinuousWithinAt.maps_ball with continuousF, radiusFPositive329      obtain ⟨R, realR, positiveR, mapsG⟩ := ContinuousWithinAt.maps_ball with continuousG, radiusGPositive330      have typedD : Real(D) by exact realD331      have typedR : Real(R) by exact realR332      obtain ⟨Q, realS, positiveS, sLeD, sLeR⟩ := positiveRadius.common with333        typedD, typedR, positiveD, positiveR334      have typedS : Real(Q) by exact realS335      witness Q336      constructor337      . exact realS338      . constructor339        . exact positiveS340        . intros X realX member near341          have typedX : Real(X) by exact realX342          have nearF := openBall.mono at X, A, Q, D with343            typedX, assumption, typedS, typedD, near, sLeD344          have nearG := openBall.mono at X, A, Q, R with345            typedX, assumption, typedS, typedR, near, sLeR346          have mappedF := mapsF with X, realX, member, nearF347          have mappedG := mapsG with X, realX, member, nearG348          have fXReal := FunctionBetween.apply_closed with fFunction, realX349          have gXReal := FunctionBetween.apply_closed with gFunction, realX350          have typedFX : Real(f(X)) by exact fXReal351          have typedGX : Real(g(X)) by exact gXReal352          have productNear := openBall.mul_control with positiveE, mappedF, mappedG353          have valueX := pointwiseMul.value with typedX, fFunction, gFunction, typedFX, typedGX354          have valueA := pointwiseMul.value at f, g, A with355            assumption, fFunction, gFunction, typedFA, typedGA356          rw valueX357        rwa valueA358359theorem ContinuousOn.add (f g S : Set)360  requires continuousF : ContinuousOn(f, S)361  requires continuousG : ContinuousOn(g, S)362  shows ContinuousOn(pointwiseAdd(f, g), S)363proof364  rcases continuousF with ⟨fFunction, subset, fEverywhere⟩365  rcases continuousG with ⟨gFunction, gSubset, gEverywhere⟩366  constructor367  . exact pointwiseAdd.function with fFunction, gFunction368  . constructor369    . exact subset370    . intros A member371      have realA : A ∈ ℝ by exact subset with A, member372      have atF := fEverywhere with A, member373      have atG := gEverywhere with A, member374      exact ContinuousWithinAt.add with atF, atG375376theorem ContinuousOn.mul (f g S : Set)377  requires continuousF : ContinuousOn(f, S)378  requires continuousG : ContinuousOn(g, S)379  shows ContinuousOn(pointwiseMul(f, g), S)380proof381  rcases continuousF with ⟨fFunction, subset, fEverywhere⟩382  rcases continuousG with ⟨gFunction, gSubset, gEverywhere⟩383  constructor384  . exact pointwiseMul.function with fFunction, gFunction385  . constructor386    . exact subset387    . intros A member388      have realA : A ∈ ℝ by exact subset with A, member389      have atF := fEverywhere with A, member390      have atG := gEverywhere with A, member391      exact ContinuousWithinAt.mul with atF, atG392