Grace/Cumulus/Real/Analysis/LHopital.g17

Open in Workbench Download source

Imports

CauchyMeanValue

Declarations

Source

1-- Real analysis: L'Hôpital's rule2-- 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.LHopital8import CauchyMeanValue910-- Section: Preparations11theorem openBall.right_between (A C X E : Real)12  requires member : X ∈ openBall(A, E)13  requires left : A < C14  requires right : C < X15  shows C ∈ openBall(A, E)16proof17  obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with member18  have data : A - E < C ∧ C < A + E19    constructor20    . linarith21    . linarith22  exact openBall.order_characterization.backward with data2324theorem openBall.left_between (A C X E : Real)25  requires member : X ∈ openBall(A, E)26  requires left : X < C27  requires right : C < A28  shows C ∈ openBall(A, E)29proof30  obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with member31  have data : A - E < C ∧ C < A + E32    constructor33    . linarith34    . linarith35  exact openBall.order_characterization.backward with data3637theorem closedInterval.subset_ball_right (A X W : Real)38  requires member : X ∈ openBall(A, W)39  requires positive : 0 < W40  shows closedInterval(A, X) ⊆ openBall(A, W)41proof42  intros Y memberY43  obtain ⟨realY, lower, upper⟩ := closedInterval.membership.forward with memberY44  have typedY : Real(Y) by exact realY45  obtain ⟨lowerX, upperX⟩ := openBall.order_characterization.forward with member46  have data : A - W < Y ∧ Y < A + W47    constructor48    . linarith49    . linarith50  exact openBall.order_characterization.backward with data5152theorem closedInterval.subset_ball_left (X A W : Real)53  requires member : X ∈ openBall(A, W)54  requires positive : 0 < W55  shows closedInterval(X, A) ⊆ openBall(A, W)56proof57  intros Y memberY58  obtain ⟨realY, lower, upper⟩ := closedInterval.membership.forward with memberY59  have typedY : Real(Y) by exact realY60  obtain ⟨lowerX, upperX⟩ := openBall.order_characterization.forward with member61  have data : A - W < Y ∧ Y < A + W62    constructor63    . linarith64    . linarith65  exact openBall.order_characterization.backward with data6667-- Section: OneSidedQuotients68-- To the right of A, the quotient f/g at X is the quotient of the69-- derivatives at some point strictly between A and X.70theorem LHopital.right (f g : ℝ → ℝ) (A W X : Real)71  requires radius : 0 < W72  requires differentiableF : ∀ Y ∈ openBall(A, W), DifferentiableAt(f, Y)73  requires differentiableG : ∀ Y ∈ openBall(A, W), DifferentiableAt(g, Y)74  requires nonzero : ∀ Y ∈ openBall(A, W), Y ≠ A → g′(Y) ≠ (0:R)75  requires zeroF : f(A) = 076  requires zeroG : g(A) = 077  requires member : X ∈ openBall(A, W)78  requires right : A < X79  shows ∃ C ∈ ℝ, A < C ∧ C < X ∧80    pointwiseDiv(f, g)(X) = pointwiseDiv(f′, g′)(C)81proof82  have realA : A ∈ ℝ by simp [Real]83  have realX : X ∈ ℝ by simp [Real]84  have fFunction : f : ℝ → ℝ by assumption85  have gFunction : g : ℝ → ℝ by assumption86  have subset := closedInterval.subset_ball_right at A, X, W with member, radius87  have intervalReal := closedInterval.subset_reals at A, X with *88  have onIntervalF : ∀ Y ∈ closedInterval(A, X), DifferentiableAt(f, Y)89    intros Y memberY90    have inBall := subset with Y, memberY91    exact differentiableF with Y, inBall92  have onIntervalG : ∀ Y ∈ closedInterval(A, X), DifferentiableAt(g, Y)93    intros Y memberY94    have inBall := subset with Y, memberY95    exact differentiableG with Y, inBall96  have continuousF := ContinuousOn.of_differentiable with97    fFunction, intervalReal, onIntervalF98  have continuousG := ContinuousOn.of_differentiable with99    gFunction, intervalReal, onIntervalG100  have interiorF : ∀ C ∈ ℝ, A < C → C < X → DifferentiableAt(f, C)101    intros C realC left rightC102    have typedC : Real(C) by exact realC103    have inBall := openBall.right_between at A, C, X, W with104      member, left, rightC105    exact differentiableF with C, inBall106  have interiorG : ∀ C ∈ ℝ, A < C → C < X → DifferentiableAt(g, C)107    intros C realC left rightC108    have typedC : Real(C) by exact realC109    have inBall := openBall.right_between at A, C, X, W with110      member, left, rightC111    exact differentiableG with C, inBall112  have typedFX : Real(f(X))113    exact FunctionBetween.apply_closed with fFunction, realX114  have typedGX : Real(g(X))115    exact FunctionBetween.apply_closed with gFunction, realX116  have nonzeroGX : g(X) ≠ (0:R)117    intro vanishes118    have endpoints : g(A) = g(X)119      rw [zeroG, vanishes]120      rfl121    have unfoldedG : ∀ C ∈ ℝ, A < C → C < X → ∃ D ∈ ℝ, HasDerivativeAt(g, D, C)122      intros C realC left rightC123      have differentiableAt := interiorG with C, realC, left, rightC124      unfold DifferentiableAt at differentiableAt125      exact differentiableAt126    obtain ⟨C, realC, left, rightC, zeroDerivative⟩ := Rolle.theorem with127      right, continuousG, endpoints, unfoldedG128    have typedC : Real(C) by exact realC129    have value := derivative.of_has_derivative with zeroDerivative130    have inBall := openBall.right_between at A, C, X, W with131      member, left, rightC132    have distinct : C ≠ A133      intro equal134      rw equal at left135      linarith136    have nonzeroC := nonzero with C, inBall, distinct137    exact nonzeroC with value138  obtain ⟨C, realC, left, rightC, equation⟩ := CauchyMeanValue.theorem with139    fFunction, gFunction, right, continuousF, continuousG, interiorF, interiorG140  have typedC : Real(C) by exact realC141  have inBall := openBall.right_between at A, C, X, W with member, left, rightC142  have distinct : C ≠ A143    intro equal144    rw equal at left145    linarith146  have nonzeroC := nonzero with C, inBall, distinct147  have typedDF := derivative.real at f, C148  have typedDG := derivative.real at g, C149  have cross : derivative(f)(C) * g(X) = derivative(g)(C) * f(X)150    rw [zeroF, zeroG] at equation151    linear_combination equation152  have quotientValue := pointwiseDiv.value at f, g, X with153    fFunction, gFunction, typedFX, typedGX154  have derivativeFFunction := derivative.function at f155  have derivativeGFunction := derivative.function at g156  have derivativeQuotient := pointwiseDiv.value at157    derivative(f), derivative(g), C with158      derivativeFFunction, derivativeGFunction, typedDF, typedDG159  have equal := realDiv.eq_of_cross at160    f(X), g(X), derivative(f)(C), derivative(g)(C) with161      typedFX, typedGX, typedDF, typedDG, nonzeroGX, nonzeroC, cross162  witness C163  refine ⟨realC, left, rightC, _⟩164  rw [quotientValue, derivativeQuotient]165  exact equal166167theorem LHopital.left (f g : ℝ → ℝ) (A W X : Real)168  requires radius : 0 < W169  requires differentiableF : ∀ Y ∈ openBall(A, W), DifferentiableAt(f, Y)170  requires differentiableG : ∀ Y ∈ openBall(A, W), DifferentiableAt(g, Y)171  requires nonzero : ∀ Y ∈ openBall(A, W), Y ≠ A → g′(Y) ≠ (0:R)172  requires zeroF : f(A) = 0173  requires zeroG : g(A) = 0174  requires member : X ∈ openBall(A, W)175  requires left : X < A176  shows ∃ C ∈ ℝ, X < C ∧ C < A ∧177    pointwiseDiv(f, g)(X) = pointwiseDiv(f′, g′)(C)178proof179  have realA : A ∈ ℝ by simp [Real]180  have realX : X ∈ ℝ by simp [Real]181  have fFunction : f : ℝ → ℝ by assumption182  have gFunction : g : ℝ → ℝ by assumption183  have subset := closedInterval.subset_ball_left at X, A, W with member, radius184  have intervalReal := closedInterval.subset_reals at X, A with *185  have onIntervalF : ∀ Y ∈ closedInterval(X, A), DifferentiableAt(f, Y)186    intros Y memberY187    have inBall := subset with Y, memberY188    exact differentiableF with Y, inBall189  have onIntervalG : ∀ Y ∈ closedInterval(X, A), DifferentiableAt(g, Y)190    intros Y memberY191    have inBall := subset with Y, memberY192    exact differentiableG with Y, inBall193  have continuousF := ContinuousOn.of_differentiable with194    fFunction, intervalReal, onIntervalF195  have continuousG := ContinuousOn.of_differentiable with196    gFunction, intervalReal, onIntervalG197  have interiorF : ∀ C ∈ ℝ, X < C → C < A → DifferentiableAt(f, C)198    intros C realC leftC rightC199    have typedC : Real(C) by exact realC200    have inBall := openBall.left_between at A, C, X, W with201      member, leftC, rightC202    exact differentiableF with C, inBall203  have interiorG : ∀ C ∈ ℝ, X < C → C < A → DifferentiableAt(g, C)204    intros C realC leftC rightC205    have typedC : Real(C) by exact realC206    have inBall := openBall.left_between at A, C, X, W with207      member, leftC, rightC208    exact differentiableG with C, inBall209  have typedFX : Real(f(X))210    exact FunctionBetween.apply_closed with fFunction, realX211  have typedGX : Real(g(X))212    exact FunctionBetween.apply_closed with gFunction, realX213  have nonzeroGX : g(X) ≠ (0:R)214    intro vanishes215    have endpoints : g(X) = g(A)216      rw [zeroG, vanishes]217      rfl218    have unfoldedG : ∀ C ∈ ℝ, X < C → C < A → ∃ D ∈ ℝ, HasDerivativeAt(g, D, C)219      intros C realC leftC rightC220      have differentiableAt := interiorG with C, realC, leftC, rightC221      unfold DifferentiableAt at differentiableAt222      exact differentiableAt223    obtain ⟨C, realC, leftC, rightC, zeroDerivative⟩ := Rolle.theorem with224      left, continuousG, endpoints, unfoldedG225    have typedC : Real(C) by exact realC226    have value := derivative.of_has_derivative with zeroDerivative227    have inBall := openBall.left_between at A, C, X, W with228      member, leftC, rightC229    have distinct : C ≠ A230      intro equal231      rw equal at rightC232      linarith233    have nonzeroC := nonzero with C, inBall, distinct234    exact nonzeroC with value235  obtain ⟨C, realC, leftC, rightC, equation⟩ := CauchyMeanValue.theorem with236    fFunction, gFunction, left, continuousF, continuousG, interiorF, interiorG237  have typedC : Real(C) by exact realC238  have inBall := openBall.left_between at A, C, X, W with member, leftC, rightC239  have distinct : C ≠ A240    intro equal241    rw equal at rightC242    linarith243  have nonzeroC := nonzero with C, inBall, distinct244  have typedDF := derivative.real at f, C245  have typedDG := derivative.real at g, C246  have cross : derivative(f)(C) * g(X) = derivative(g)(C) * f(X)247    rw [zeroF, zeroG] at equation248    symm249    linear_combination equation250  have quotientValue := pointwiseDiv.value at f, g, X with251    fFunction, gFunction, typedFX, typedGX252  have derivativeFFunction := derivative.function at f253  have derivativeGFunction := derivative.function at g254  have derivativeQuotient := pointwiseDiv.value at255    derivative(f), derivative(g), C with256      derivativeFFunction, derivativeGFunction, typedDF, typedDG257  have equal := realDiv.eq_of_cross at258    f(X), g(X), derivative(f)(C), derivative(g)(C) with259      typedFX, typedGX, typedDF, typedDG, nonzeroGX, nonzeroC, cross260  witness C261  refine ⟨realC, leftC, rightC, _⟩262  rw [quotientValue, derivativeQuotient]263  exact equal264265-- Section: LHopital266-- L'Hôpital's rule in the 0/0 form at a point: when f and g are267-- differentiable near A with f(A) = g(A) = 0 and g′ nonzero away from A,268-- f′/g′ → L at A forces f/g → L at A.269theorem LHopital.theorem (f g : ℝ → ℝ) (A L W : Real)270  requires radius : 0 < W271  requires differentiableF : ∀ X ∈ openBall(A, W), DifferentiableAt(f, X)272  requires differentiableG : ∀ X ∈ openBall(A, W), DifferentiableAt(g, X)273  requires nonzero : ∀ X ∈ openBall(A, W), X ≠ A → g′(X) ≠ (0:R)274  requires zeroF : f(A) = 0275  requires zeroG : g(A) = 0276  requires limit : TendsToAt(pointwiseDiv(f′, g′), L, A)277  shows TendsToAt(pointwiseDiv(f, g), L, A)278proof279  have fFunction : f : ℝ → ℝ by assumption280  have gFunction : g : ℝ → ℝ by assumption281  have quotientFunction := pointwiseDiv.function with fFunction, gFunction282  constructor283  . exact quotientFunction284  . intros E realE positive285    obtain ⟨D, realD, positiveD, maps⟩ := TendsToAt.eventually with286      limit, positive287    have typedD : Real(D) by exact realD288    obtain ⟨S, realS, positiveS, belowD, belowW⟩ :=289      positiveRadius.common with positiveD, radius290    have typedS : Real(S) by exact realS291    witness S292    refine ⟨realS, positiveS, _⟩293    intros X realX distinct near294    have typedX : Real(X) by exact realX295    have nearD := openBall.mono with near, belowD296    have nearW := openBall.mono with near, belowW297    have order := realLess.trichotomy at X, A298    rcases order with below | equal | above299    . obtain ⟨C, realC, leftC, rightC, value⟩ := LHopital.left with300        fFunction, gFunction, radius, differentiableF, differentiableG, nonzero,301        zeroF, zeroG, nearW, below302      have typedC : Real(C) by exact realC303      have inBallD := openBall.left_between at A, C, X, D with304        nearD, leftC, rightC305      have distinctC : C ≠ A306        intro equalC307        rw equalC at rightC308        linarith309      have mapped := maps with C, realC, distinctC, inBallD310      rw value311      exact mapped312    . exfalso313      exact distinct with equal314    . obtain ⟨C, realC, leftC, rightC, value⟩ := LHopital.right with315        fFunction, gFunction, radius, differentiableF, differentiableG, nonzero,316        zeroF, zeroG, nearW, above317      have typedC : Real(C) by exact realC318      have inBallD := openBall.right_between at A, C, X, D with319        nearD, leftC, rightC320      have distinctC : C ≠ A321        intro equalC322        rw equalC at leftC323        linarith324      have mapped := maps with C, realC, distinctC, inBallD325      rw value326      exact mapped327