Grace/Cumulus/Real/Analysis/Examples.g17

Open in Workbench Download source

Imports

Sequences · Power · Differentiation · SequentialCompactness

Declarations

Source

1-- Real analysis: Examples2-- 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.Examples8import Sequences9import Power10import Differentiation11import SequentialCompactness1213-- Section: Powers14def powSequence (u : Set, k : Nat) → Set15  | u, zero => constantSequence(realOne)16  | u, succ(k) => mulSequence(u, powSequence(u, k))1718theorem powSequence.sequence (u : Set, k : Nat)19  requires sequence : RealSequence(u)20  shows RealSequence(powSequence(u, k))21proof22  induction k23  | zero =>24    rw powSequence25    exact constantSequence.sequence with realOne.real26  | succ(j) using ih =>27    rw powSequence28    exact mulSequence.sequence with sequence, ih2930theorem powSequence.value (u : Set, k n : Nat)31  requires sequence : RealSequence(u)32  shows powSequence(u, k)[n] = uₙ ^ k33proof34  induction k35  | zero =>36    have constantValue := constantSequence.value at realOne, n with37      realOne.real, assumption38    rw powSequence39    rw constantValue40    rw realPow.zero41    rfl42  | succ(j) using ih =>43    have valueReal := RealSequence.value at u, n with sequence44    have powerSequence := powSequence.sequence at u, j with sequence45    have powerValueReal := RealSequence.value at powSequence(u, j), n with46      powerSequence47    have productValue := mulSequence.value at48      u, powSequence(u, j), n with49        sequence, powerSequence, valueReal, powerValueReal50    rw powSequence51    rw productValue52    rw ih53    rw realPow.succ54    rfl5556theorem ConvergesTo.pow (u : Set) (L : Real, k : Nat)57  requires converges : ConvergesTo(u, L)58  shows ConvergesTo(powSequence(u, k), L ^ k)59proof60  induction k61  | zero =>62    rw powSequence63    rw realPow.zero64    exact constantSequence.converges with realOne.real65  | succ(j) using ih =>66    rw powSequence67    rw realPow.succ68    exact ConvergesTo.mul at u, powSequence(u, j), L, L ^ j with69      converges, ih7071-- Section: Examples72theorem constantSequence.quotient_converges (A B : Real)73  requires nonzero : B ≠ 074  shows ConvergesTo(75    divSequence(constantSequence(A), constantSequence(B)), A / B)76proof77  exact ConvergesTo.div at78    constantSequence(A), constantSequence(B), A, B with79      constantSequence.converges at A with assumption,80      constantSequence.converges at B with assumption,81      nonzero8283-- In particular, the constant reciprocal sequence converges to 1/L.84theorem constantSequence.reciprocal_converges (L : Real)85  requires nonzero : L ≠ 086  shows ConvergesTo(87    divSequence(constantSequence(1), constantSequence(L)), 1 / L)88proof89  exact constantSequence.quotient_converges with realOne.real, nonzero9091-- Negation preserves every convergent sequence because it is continuous.92theorem convergentSequence.negation_example (u : Set) (L : Real)93  requires converges : ConvergesTo(u, L)94  shows ConvergesTo(compose(realNeg, u, ℕ, ℝ, ℝ), -L)95proof96  have mapped := ContinuousAt.converges at realNeg, u, L with97    realNeg.continuous_at at L with assumption, converges98  exact mapped99100-- The square function is continuous because it is the pointwise product of101-- the identity function with itself.102theorem squareFunction.continuous103  shows Continuous(pointwiseMul(identity(ℝ), identity(ℝ)))104proof105  exact Continuous.mul with identity.continuous, identity.continuous106107-- The reciprocal function is continuous at every nonzero real.108theorem reciprocalFunction.continuous_at (A : Real)109  requires nonzero : A ≠ 0110  shows ContinuousAt(pointwiseInv(identity(ℝ)), A)111proof112  have realA : A ∈ ℝ by simp [Real]113  have mappedA := identity.relates with realA114  have identityValue := FunctionBetween.apply_value at115    identity(ℝ), ℝ, ℝ, A, A with116      identity.function at ℝ, realA, mappedA117  have identityNonzero : Nonzero(identity(ℝ)(A))118    unfold Nonzero119    rwa identityValue120  exact ContinuousAt.inv at identity(ℝ), A with121    identity.continuous_at at A with assumption, identityNonzero122123-- Closed intervals are preserved by limits.  This first concrete order-limit124-- example says that a convergent sequence contained in [0, 1] has its limit125-- in the same interval.126theorem convergentSequence.unit_interval_limit (u : Set) (L : Real)127  requires converges : ConvergesTo(u, L)128  requires contained : UnitIntervalTerms(u)129  shows 0 ≤ L ∧ L ≤ 1130proof131  have lower : NonnegativeTerms(u)132    intros n nNatural133    obtain ⟨lower, upper⟩ := contained with n, nNatural134    exact lower135  have upper : BoundedAboveBy(u, realOne)136    intros n nNatural137    have bounds := contained with n, nNatural138    rcases bounds with ⟨lower, upper⟩139    exact upper140  constructor141  . exact ConvergesTo.nonnegative_of_nonnegative_terms at142      u, L with converges, lower143  . exact ConvergesTo.le_constant at u, L, realOne with144      realOne.real, converges, upper145146-- Natural powers preserve limits, with handwritten notation for147-- both the sequence terms and their limit.148theorem convergentSequence.power_example (u : Set) (L : Real, k : Nat)149  requires converges : ConvergesTo(u, L)150  shows ConvergesTo(powSequence(u, k), L ^ k)151proof152  exact ConvergesTo.pow with converges153154-- Completeness gives a canonical limit to every bounded nondecreasing real155-- sequence: the supremum of its range.156theorem boundedNondecreasingSequence.converges (u : Set) (B : Real)157  requires sequence : RealSequence(u)158  requires increasing : Nondecreasing(u)159  requires bounded : BoundedAboveBy(u, B)160  shows ConvergesTo(u, realSup(range(u)))161proof162  exact Nondecreasing.converges_to_supremum with sequence, increasing, bounded163164-- The identity function tends to A as x tends to A through the punctured165-- neighborhood used by the derivative definition.166theorem identityFunction.limit_example (A : Real)167  shows TendsToAt(identity(ℝ), A, A)168proof169  exact identity.tends_to_at with assumption170171-- A strict comparison at one point persists throughout a neighborhood.172theorem continuousFunctions.order_persists (f g : Set) (A : Real)173  requires continuousF : ContinuousAt(f, A)174  requires continuousG : ContinuousAt(g, A)175  requires below : Below(f(A), g(A))176  shows ∃ D ∈ ℝ, 0 < D ∧177    ∀ x ∈ ℝ, (x ∈ openBall(A, D) → Below(f(x), g(x)))178proof179  exact ContinuousAt.eventually_lt with continuousF, continuousG, below180181-- The difference quotient of a constant function tends to zero.182theorem derivative.constant_example (C A : Real)183  shows HasDerivativeAt(constantRealFunction(C), realZero, A)184proof185  exact constantRealFunction.has_derivative_at with *{2}186187-- The difference quotient of x ↦ x tends to one at every point.188theorem derivative.identity_example (A : Real)189  shows HasDerivativeAt(identity(ℝ), realOne, A)190proof191  exact identity.has_derivative_at with assumption192193-- Linearity combines checked derivatives as on paper.194theorem derivative.doubled_identity (A : Real)195  shows HasDerivativeAt(196    pointwiseAdd(identity(ℝ), identity(ℝ)), (2:R), A)197proof198  have doubled := HasDerivativeAt.add at199    identity(ℝ), identity(ℝ), realOne, realOne, A with200      identity.has_derivative_at at A with assumption,201      identity.has_derivative_at at A with assumption202  have two : (1:R) + 1 = (2:R) by ring203  rw two at doubled204  exact doubled205206-- Differentiability immediately supplies the continuity needed by later207-- analysis arguments.208theorem derivative.identity_is_continuous (A : Real)209  shows ContinuousAt(identity(ℝ), A)210proof211  exact HasDerivativeAt.continuous_at at212    identity(ℝ), realOne, A with213      identity.has_derivative_at at A with assumption214215-- The product rule gives (x²)'(A) = A + A.216theorem derivative.square (A : Real)217  shows HasDerivativeAt(218    pointwiseMul(identity(ℝ), identity(ℝ)), A + A, A)219proof220  have derivative := HasDerivativeAt.mul at221    identity(ℝ), identity(ℝ), realOne, realOne, A with222      identity.has_derivative_at at A with assumption,223      identity.has_derivative_at with assumption224  have realA : A ∈ ℝ by simp [Real]225  have mapped := identity.relates with realA226  have value := FunctionBetween.apply_value at227    identity(ℝ), ℝ, ℝ, A, A with228      identity.function at ℝ, realA, mapped229  unfold realAddValue at derivative230  unfold realMulValue at derivative231  rw value at derivative232  have oneLeft := realMulValue.one_left at A233  have oneRight := realMulValue.one_right at A234  unfold call2 at oneLeft235  unfold call2 at oneRight236  rw [oneLeft, oneRight] at derivative237  unfold call2238  exact derivative239