Grace/Cumulus/Real/Analysis/Continuity.g17
Open in Workbench Download source
Imports
Sequences
Declarations
Source
1234567module Grace.Cumulus.Real.Analysis.Continuity8import Sequences91011predicate ContinuousAt (f : Set) (A : Real) :=12 FunctionBetween(f, ℝ, ℝ) ∧13 (∀ e ∈ ℝ, 0 < e →14 ∃ d ∈ ℝ, 0 < d ∧15 ∀ x ∈ ℝ, (x ∈ openBall(A, d) →16 f(x) ∈ openBall(f(A), e)))1718predicate Continuous (f : Set) :=19 FunctionBetween(f, ℝ, ℝ) ∧20 (∀ a ∈ ℝ, ContinuousAt(f, a))2122predicate Nonzero (A : Real) := A ≠ 02324def pointwiseNeg (f : Set) : Set :=25 compose(realNeg, f, ℝ, ℝ, ℝ)2627def pointwiseAdd (f g : Set) : Set :=28 compose(realAdd, pairFunctions(f, g, ℝ, ℝ, ℝ),29 ℝ, ℝ × ℝ, ℝ)3031def pointwiseSub (f g : Set) : Set :=32 pointwiseAdd(f, pointwiseNeg(g))3334def pointwiseMul (f g : Set) : Set :=35 compose(realMul, pairFunctions(f, g, ℝ, ℝ, ℝ),36 ℝ, ℝ × ℝ, ℝ)3738def pointwiseInv (f : Set) : Set :=39 compose(realInv, f, ℝ, ℝ, ℝ)4041def pointwiseDiv (f g : Set) : Set :=42 pointwiseMul(f, pointwiseInv(g))4344theorem pointwiseNeg.function (f : Set)45 requires function : f : ℝ → ℝ46 shows pointwiseNeg(f) : ℝ → ℝ47proof48 unfold pointwiseNeg49 exact compose.function with function, realNeg.function5051theorem pointwiseNeg.value (f : Set) (X : Real)52 requires function : f : ℝ → ℝ53 requires valueReal : Real(f(X))54 shows pointwiseNeg(f)(X) = -f(X)55proof56 have realX : X ∈ ℝ by simp [Real]57 have value := compose.apply with function, realNeg.function, realX58 simp [pointwiseNeg]5960theorem pointwiseAdd.function (f g : Set)61 requires fFunction : f : ℝ → ℝ62 requires gFunction : g : ℝ → ℝ63 shows pointwiseAdd(f, g) : ℝ → ℝ64proof65 have paired := pairFunctions.function with fFunction, gFunction66 unfold pointwiseAdd67 exact compose.function with paired, realAdd.function6869theorem pointwiseAdd.value (f g : Set) (X : Real)70 requires fFunction : f : ℝ → ℝ71 requires gFunction : g : ℝ → ℝ72 requires fValueReal : Real(f(X))73 requires gValueReal : Real(g(X))74 shows pointwiseAdd(f, g)(X) = f(X) + g(X)75proof76 have realX : X ∈ ℝ by simp [Real]77 have paired := pairFunctions.function with fFunction, gFunction78 have pairValue := pairFunctions.apply with fFunction, gFunction, realX79 have sumValue := compose.apply with paired, realAdd.function, realX80 unfold pointwiseAdd81 rw pairValue at sumValue82 simp [call2]8384theorem pointwiseMul.function (f g : Set)85 requires fFunction : f : ℝ → ℝ86 requires gFunction : g : ℝ → ℝ87 shows pointwiseMul(f, g) : ℝ → ℝ88proof89 have paired := pairFunctions.function with fFunction, gFunction90 unfold pointwiseMul91 exact compose.function with paired, realMul.function9293theorem pointwiseMul.value (f g : Set) (X : Real)94 requires fFunction : f : ℝ → ℝ95 requires gFunction : g : ℝ → ℝ96 requires fValueReal : Real(f(X))97 requires gValueReal : Real(g(X))98 shows pointwiseMul(f, g)(X) = f(X) * g(X)99proof100 have realX : X ∈ ℝ by simp [Real]101 have paired := pairFunctions.function with fFunction, gFunction102 have pairValue := pairFunctions.apply with fFunction, gFunction, realX103 have productValue := compose.apply with paired, realMul.function, realX104 unfold pointwiseMul105 rw pairValue at productValue106 simp [call2]107108theorem pointwiseInv.function (f : Set)109 requires function : f : ℝ → ℝ110 shows pointwiseInv(f) : ℝ → ℝ111proof112 unfold pointwiseInv113 exact compose.function with function, realInv.function114115theorem pointwiseInv.value (f : Set) (X : Real)116 requires function : f : ℝ → ℝ117 requires valueReal : Real(f(X))118 shows pointwiseInv(f)(X) = realInvValue(f(X))119proof120 have realX : X ∈ ℝ by simp [Real]121 have value := compose.apply with function, realInv.function, realX122 simp [pointwiseInv, realInvValue]123124125theorem positiveRadius.common (D R : Real)126 requires positiveD : 0 < D127 requires positiveR : 0 < R128 shows ∃ S ∈ ℝ, 0 < S ∧ S ≤ D ∧ S ≤ R129proof130 have realD : D ∈ ℝ by simp [Real]131 have realR : R ∈ ℝ by simp [Real]132 have equalityCases : D = R ∨ D ≠ R by tauto133 cases equalityCases with equal | distinct134 . witness D135 constructor136 . exact realD137 . constructor138 . exact positiveD139 . constructor140 . exact realLe.reflexive at D141 . rw ← equal142 exact realLe.reflexive with assumption143 . have comparison := realLess.connected_on with D, R, distinct144 cases comparison with dLessR | rLessD145 . witness D146 constructor147 . exact realD148 . constructor149 . exact positiveD150 . constructor151 . exact realLe.reflexive at D152 . exact realLess.implies_le at D, R with153 *{2}, dLessR154 . witness R155 constructor156 . exact realR157 . constructor158 . exact positiveR159 . constructor160 . exact realLess.implies_le at R, D with161 *{2}, rLessD162 . exact realLe.reflexive at R163164165166theorem openBall.mul_control (A B C D E : Real)167 requires positiveE : 0 < E168 requires nearA : A ∈ openBall(C, scaledRadius(E, limitScale(D)))169 requires nearB : B ∈ openBall(D,170 scaledRadius(E, scaledRadius(E, limitScale(D)) + abs(C)))171 shows A * B ∈ openBall(C * D, E)172proof173 have scaleDReal := limitScale.real at D with assumption174 have scaleDPositive := limitScale.positive at D with assumption175 have radiusAReal := scaledRadius.real at E, limitScale(D) with176 assumption, scaleDReal177 have radiusAPositive := scaledRadius.positive at E, limitScale(D) with178 assumption, scaleDReal, positiveE, scaleDPositive179 have absCReal := abs.real at C with assumption180 have boundReal := realAddValue.real at181 scaledRadius(E, limitScale(D)), abs(C) with radiusAReal, absCReal182 have radiusAboveAbsC := realLess.add_right at183 realZero, scaledRadius(E, limitScale(D)), abs(C) with184 realZero.real, radiusAReal, absCReal, radiusAPositive185 have zeroPlusAbsC := realAddValue.zero_left with absCReal186 rw zeroPlusAbsC at radiusAboveAbsC187 have boundPositive := realLe.transitive_less at188 realZero, abs(C), scaledRadius(E, limitScale(D)) + abs(C) with189 realZero.real, absCReal, boundReal,190 abs.nonnegative at C with assumption, radiusAboveAbsC191 have radiusBReal := scaledRadius.real at192 E, scaledRadius(E, limitScale(D)) + abs(C) with assumption, boundReal193 have dataA := openBall.membership.forward at194 C, scaledRadius(E, limitScale(D)), A with nearA195 have dataB := openBall.membership.forward at196 D, scaledRadius(E, scaledRadius(E, limitScale(D)) + abs(C)), B with nearB197 rcases dataA with ⟨realA, closeA⟩198 rcases dataB with ⟨realB, closeB⟩199200 have absAReal := abs.real at A with assumption201 have distACReal := dist.real at A, C with *202 have distBDReal := dist.real at B, D with *203 have absABound := abs.le_dist_add_abs at A, C with204 *{2}205 have closeAWithAbsC := realLess.add_right at206 dist(A, C), scaledRadius(E, limitScale(D)), abs(C) with207 distACReal, radiusAReal, absCReal, closeA208 have distPlusAbsReal := realAddValue.real at dist(A, C), abs(C) with209 distACReal, absCReal210 have aBounded := realLe.transitive_less at211 abs(A), dist(A, C) + abs(C),212 scaledRadius(E, limitScale(D)) + abs(C) with213 absAReal, distPlusAbsReal, boundReal,214 absABound, closeAWithAbsC215216 have aBoundedLe := realLess.implies_le at217 abs(A), scaledRadius(E, limitScale(D)) + abs(C) with218 absAReal, boundReal, aBounded219 have distBDNonnegative := dist.nonnegative at B, D with220 *{2}221 have firstWeak := realLe.mul_right_of_nonnegative at222 abs(A), scaledRadius(E, limitScale(D)) + abs(C), dist(B, D) with223 absAReal, boundReal, distBDReal, aBoundedLe, distBDNonnegative224 have firstStrict := realLess.mul_left_of_positive at225 dist(B, D),226 scaledRadius(E, scaledRadius(E, limitScale(D)) + abs(C)),227 scaledRadius(E, limitScale(D)) + abs(C) with228 distBDReal, radiusBReal, boundReal, closeB, boundPositive229 have firstTermReal := realMulValue.real at230 abs(A), dist(B, D) with absAReal, distBDReal231 have firstMiddleReal := realMulValue.real at232 scaledRadius(E, limitScale(D)) + abs(C), dist(B, D) with233 boundReal, distBDReal234 have firstUpperReal := realMulValue.real at235 scaledRadius(E, limitScale(D)) + abs(C),236 scaledRadius(E, scaledRadius(E, limitScale(D)) + abs(C)) with237 boundReal, radiusBReal238 have firstBelow := realLe.transitive_less at239 abs(A) * dist(B, D),240 (scaledRadius(E, limitScale(D)) + abs(C)) * dist(B, D),241 (scaledRadius(E, limitScale(D)) + abs(C)) *242 scaledRadius(E, scaledRadius(E, limitScale(D)) + abs(C)) with243 firstTermReal, firstMiddleReal, firstUpperReal,244 firstWeak, firstStrict245 have firstCancellation := scaledRadius.cancel at246 E, scaledRadius(E, limitScale(D)) + abs(C) with247 assumption, boundReal, boundPositive248 rw firstCancellation at firstBelow249250 have absDReal := abs.real at D with assumption251 have absDLess := abs.lt_limitScale at D with assumption252 have absDLe := realLess.implies_le at abs(D), limitScale(D) with253 absDReal, scaleDReal, absDLess254 have distACNonnegative := dist.nonnegative at A, C with255 *{2}256 have secondWeak := realLe.mul_right_of_nonnegative at257 abs(D), limitScale(D), dist(A, C) with258 absDReal, scaleDReal, distACReal, absDLe, distACNonnegative259 have secondStrict := realLess.mul_left_of_positive at260 dist(A, C), scaledRadius(E, limitScale(D)), limitScale(D) with261 distACReal, radiusAReal, scaleDReal, closeA, scaleDPositive262 have secondTermReal := realMulValue.real at263 abs(D), dist(A, C) with absDReal, distACReal264 have secondMiddleReal := realMulValue.real at265 limitScale(D), dist(A, C) with scaleDReal, distACReal266 have secondUpperReal := realMulValue.real at267 limitScale(D), scaledRadius(E, limitScale(D)) with268 scaleDReal, radiusAReal269 have secondBelow := realLe.transitive_less at270 abs(D) * dist(A, C),271 limitScale(D) * dist(A, C),272 limitScale(D) * scaledRadius(E, limitScale(D)) with273 secondTermReal, secondMiddleReal, secondUpperReal,274 secondWeak, secondStrict275 have secondCancellation := scaledRadius.cancel at276 E, limitScale(D) with assumption, scaleDReal, scaleDPositive277 rw secondCancellation at secondBelow278279 have estimate := dist.mul_mul at A, B, C, D with280 *{4}281 have halfReal := half.real at E with assumption282 have sumBelow := realLess.add at283 abs(A) * dist(B, D), half(E),284 abs(D) * dist(A, C), half(E) with285 firstTermReal, halfReal, secondTermReal, halfReal,286 firstBelow, secondBelow287 have doubled := half.add_self at E with assumption288 rw doubled at sumBelow289 have productReal := realMulValue.real at A, B with *290 have centerReal := realMulValue.real at C, D with *291 have totalDistanceReal := dist.real at A * B, C * D with292 productReal, centerReal293 have estimateSumReal := realAddValue.real at294 abs(A) * dist(B, D), abs(D) * dist(A, C) with295 firstTermReal, secondTermReal296 have within := realLe.transitive_less at297 dist(A * B, C * D),298 abs(A) * dist(B, D) + abs(D) * dist(A, C), E with299 totalDistanceReal, estimateSumReal, assumption,300 estimate, sumBelow301 apply openBall.membership.backward at C * D, E, A * B302 constructor303 exact productReal304 . exact within305306307theorem openBall.inv_control (A B E : Real)308 requires nonzeroB : B ≠ 0309 requires positiveE : 0 < E310 requires awayFromZero : A ∈ openBall(B, half(abs(B)))311 requires epsilonClose : A ∈ openBall(B, scaledRadius(E, inverseScale(B)))312 shows realInvValue(A) ∈ openBall(realInvValue(B), E)313proof314 have absBReal := abs.real at B with assumption315 have absBPositive := abs.positive_of_ne with assumption, nonzeroB316 have halfAbsBReal := half.real with absBReal317 have halfAbsBPositive := half.positive with absBReal, absBPositive318 have scaleReal := inverseScale.real at B with assumption319 have scalePositive := inverseScale.positive with assumption, nonzeroB320 have radiusReal := scaledRadius.real at E, inverseScale(B) with321 assumption, scaleReal322 have awayData := openBall.membership.forward at323 B, half(abs(B)), A with awayFromZero324 have epsilonData := openBall.membership.forward at325 B, scaledRadius(E, inverseScale(B)), A with epsilonClose326 rcases awayData with ⟨realA, closeZero⟩327 rcases epsilonData with ⟨realAAgain, closeE⟩328329 have lower := abs.half_lt_of_dist_lt_half with *{2}, nonzeroB, closeZero330 have nonzeroA : A ≠ 0331 intro equal332 have absoluteZero := abs.zero333 rw [equal, absoluteZero] at lower334 have zeroInReals : realZero ∈ ℝ335 exact realZero.real336 have irreflexive := realLess.irreflexive_on337 have cycle := realLess.transitive with realZero.real, halfAbsBReal, realZero.real, halfAbsBPositive, lower338 exact irreflexive with realZero, zeroInReals, cycle339340 have absAReal := abs.real at A with assumption341 have inverseBound := realInvValue.antitone_positive with halfAbsBReal, absAReal, halfAbsBPositive, lower342 have absInverseA := abs.inv with assumption, nonzeroA343 rw ← absInverseA at inverseBound344345 have inverseBReal := realInvValue.real at B with assumption346 have inverseBNonzero := realInvValue.nonzero with assumption, nonzeroB347 have absInverseBReal := abs.real with inverseBReal348 have absInverseBPositive := abs.positive_of_ne with inverseBReal, inverseBNonzero349 have factorBound := realLess.mul_right_of_positive at350 abs(realInvValue(A)), realInvValue(half(abs(B))),351 abs(realInvValue(B)) with352 abs.real at realInvValue(A) with realInvValue.real at A with assumption,353 realInvValue.real at half(abs(B)) with halfAbsBReal,354 absInverseBReal, inverseBound, absInverseBPositive355 have factorBoundScale : abs(realInvValue(A)) *356 abs(realInvValue(B)) < inverseScale(B)357 unfold inverseScale358 exact factorBound359360 have distanceReal := dist.real at A, B with *361 have factorReal := realMulValue.real at362 abs(realInvValue(A)), abs(realInvValue(B)) with363 abs.real at realInvValue(A) with realInvValue.real at A with assumption,364 absInverseBReal365 have distanceNonnegative := dist.nonnegative at A, B with366 *{2}367 have factorLe := realLess.implies_le with factorReal, scaleReal, factorBoundScale368 have weakProduct := realLe.mul_left_of_nonnegative with369 factorReal, scaleReal, distanceReal, factorLe, distanceNonnegative370 have strictProduct := realLess.mul_right_of_positive with371 distanceReal, radiusReal, scaleReal, closeE, scalePositive372 have lowerProductReal := realMulValue.real with distanceReal, factorReal373 have middleProductReal := realMulValue.real with distanceReal, scaleReal374 have upperProductReal := realMulValue.real with radiusReal, scaleReal375 have productBelow := realLe.transitive_less with376 lowerProductReal, middleProductReal, upperProductReal, weakProduct, strictProduct377 have cancellation := scaledRadius.cancel at378 E, inverseScale(B) with assumption, scaleReal, scalePositive379 have commute := realMulValue.commutative with radiusReal, scaleReal380 rw [commute, cancellation] at productBelow381 have halfBelowE := half.lt_self with assumption, positiveE382 have halfReal := half.real at E with assumption383 have productBelowE := realLess.transitive with384 lowerProductReal, halfReal, assumption, productBelow, halfBelowE385 have inverseDistance := dist.inv_inv with *{2}, nonzeroA, nonzeroB386 rw ← inverseDistance at productBelowE387 apply openBall.membership.backward388 constructor389 . have inverseAReal := realInvValue.real at A with assumption390 exact inverseAReal391 . exact productBelowE392393theorem ContinuousAt.function (f : Set) (A : Real)394 requires continuous : ContinuousAt(f, A)395 shows f : ℝ → ℝ396proof397 simp [ContinuousAt]398399400401402instance realFunction.value_type (f : Set) (X : Real)403 requires function : f : ℝ → ℝ404 shows Real(f(X))405proof406 have realX : X ∈ ℝ by simp [Real]407 unfold Real408 exact FunctionBetween.apply_closed with function, realX409410theorem Continuous.function (f : Set)411 requires continuous : Continuous(f)412 shows f : ℝ → ℝ413proof414 simp [Continuous]415416theorem ContinuousAt.maps_ball (f : Set) (A E : Real)417 requires continuous : ContinuousAt(f, A)418 requires positive : 0 < E419 shows ∃ D ∈ ℝ, 0 < D ∧420 ∀ x ∈ ℝ, (x ∈ openBall(A, D) →421 f(x) ∈ openBall(f(A), E))422proof423 rcases continuous with ⟨function, local⟩424 exact local with E, positive425426theorem Continuous.at (f : Set) (A : Real)427 requires continuous : Continuous(f)428 shows ContinuousAt(f, A)429proof430 rcases continuous with ⟨function, everywhere⟩431 have realA : A ∈ ℝ by simp [Real]432 exact everywhere with A, realA433434instance ContinuousAt.value_type (f : Set) (A : Real)435 requires continuous : ContinuousAt(f, A)436 shows Real(f(A))437proof438 have function := ContinuousAt.function with continuous439 have realA : A ∈ ℝ by simp [Real]440 unfold Real441 exact FunctionBetween.apply_closed with function, realA442443instance Continuous.value_type (f : Set) (A : Real)444 requires continuous : Continuous(f)445 shows Real(f(A))446proof447 have continuousAt := Continuous.at with continuous448 exact ContinuousAt.value_type with continuousAt449450theorem identity.continuous_at (A : Real)451 shows ContinuousAt(identity(ℝ), A)452proof453 have function := identity.function at ℝ454 have realA : A ∈ ℝ by simp [Real]455 have mappedA := identity.relates with realA456 have valueA := FunctionBetween.apply_value with function, mappedA457 constructor458 . exact function459 . intros E realE positive460 witness E461 constructor462 . exact realE463 . constructor464 . exact positive465 . intros X realX near466 have mappedX := identity.relates with realX467 have valueX := FunctionBetween.apply_value with function, realX, mappedX468 rwa [valueX, valueA]469470theorem identity.continuous471 shows Continuous(identity(ℝ))472proof473 constructor474 . exact identity.function at ℝ475 . intros A realA476 have typedA : Real(A) by exact realA477 exact identity.continuous_at with typedA478479480481theorem ContinuousAt.congr (f g : Set) (A : Real)482 requires continuous : ContinuousAt(f, A)483 requires gFunction : g : ℝ → ℝ484 requires equal : ∀ x ∈ ℝ, f(x) = g(x)485 shows ContinuousAt(g, A)486proof487 constructor488 . exact gFunction489 . intros E realE positive490 obtain ⟨D, realD, positiveD, maps⟩ := ContinuousAt.maps_ball with continuous, positive491 witness D492 constructor493 . exact realD494 . constructor495 . exact positiveD496 . intros X realX near497 have realA : A ∈ ℝ by simp [Real]498 have equalX := equal with X, realX499 have equalA := equal with A500 rw [← equalX, ← equalA]501 exact maps with X, realX, near502503504505theorem ContinuousAt.comp (g f : Set) (A : Real)506 requires continuousF : ContinuousAt(f, A)507 requires continuousG : ContinuousAt(g, f(A))508 shows ContinuousAt(compose(g, f, ℝ, ℝ, ℝ), A)509proof510 have fFunction := ContinuousAt.function with continuousF511 have realA : A ∈ ℝ by simp [Real]512 have fAReal := FunctionBetween.apply_closed with fFunction, realA513 have typedFA : Real(f(A)) by exact fAReal514 have gFunction := ContinuousAt.function with continuousG515 constructor516 . exact compose.function at g, f, ℝ, ℝ, ℝ with517 fFunction, gFunction518 . intros E realE positive519 obtain ⟨D, realD, positiveD, gMaps⟩ := ContinuousAt.maps_ball with continuousG, positive520 obtain ⟨R, realR, positiveR, fMaps⟩ := ContinuousAt.maps_ball with continuousF, positiveD521 witness R522 constructor523 . exact realR524 . constructor525 . exact positiveR526 . intros X realX near527 have fXReal := FunctionBetween.apply_closed with fFunction, realX528 have mappedF := fMaps with X, realX, near529 have mappedG := gMaps with f(X), fXReal, mappedF530 have atX := compose.apply with fFunction, gFunction, realX531 have atA := compose.apply with fFunction, gFunction, realA532 rwa [atX, atA]533534theorem ContinuousAt.add (f g : Set) (A : Real)535 requires continuousF : ContinuousAt(f, A)536 requires continuousG : ContinuousAt(g, A)537 shows ContinuousAt(pointwiseAdd(f, g), A)538proof539 have fFunction := ContinuousAt.function with continuousF540 have gFunction := ContinuousAt.function with continuousG541 have realA : A ∈ ℝ by simp [Real]542 constructor543 . exact pointwiseAdd.function with fFunction, gFunction544 . intros E realE positive545 have typedE : Real(E) by exact realE546 have radiusPositive := half.positive with positive547 obtain ⟨D, realD, positiveD, mapsF⟩ := ContinuousAt.maps_ball with continuousF, radiusPositive548 obtain ⟨R, realR, positiveR, mapsG⟩ := ContinuousAt.maps_ball with continuousG, radiusPositive549 have typedD : Real(D) by exact realD550 have typedR : Real(R) by exact realR551 obtain ⟨S, realS, positiveS, sLeD, sLeR⟩ := positiveRadius.common with552 typedD, typedR, positiveD, positiveR553 have typedS : Real(S) by exact realS554 witness S555 constructor556 . exact realS557 . constructor558 . exact positiveS559 . intros X realX near560 have typedX : Real(X) by exact realX561 have nearF := openBall.mono at X, A, S, D with562 typedX, assumption, typedS, typedD, near, sLeD563 have nearG := openBall.mono at X, A, S, R with564 typedX, assumption, typedS, typedR, near, sLeR565 have mappedF := mapsF with X, realX, nearF566 have mappedG := mapsG with X, realX, nearG567 have fXReal := FunctionBetween.apply_closed with fFunction, realX568 have gXReal := FunctionBetween.apply_closed with gFunction, realX569 have fAReal := FunctionBetween.apply_closed with fFunction, realA570 have gAReal := FunctionBetween.apply_closed with gFunction, realA571 have typedFX : Real(f(X)) by exact fXReal572 have typedGX : Real(g(X)) by exact gXReal573 have typedFA : Real(f(A)) by exact fAReal574 have typedGA : Real(g(A)) by exact gAReal575 have sumNear := openBall.add with mappedF, mappedG576 have doubled := half.add_self with typedE577 rw doubled at sumNear578 have valueX := pointwiseAdd.value with typedX, fFunction, gFunction, typedFX, typedGX579 have valueA := pointwiseAdd.value at f, g, A with580 assumption, fFunction, gFunction, typedFA, typedGA581 rwa [valueX, valueA]582583theorem ContinuousAt.mul (f g : Set) (A : Real)584 requires continuousF : ContinuousAt(f, A)585 requires continuousG : ContinuousAt(g, A)586 shows ContinuousAt(pointwiseMul(f, g), A)587proof588 have fFunction := ContinuousAt.function with continuousF589 have gFunction := ContinuousAt.function with continuousG590 have realA : A ∈ ℝ by simp [Real]591 have fAReal := FunctionBetween.apply_closed with fFunction, realA592 have gAReal := FunctionBetween.apply_closed with gFunction, realA593 have typedFA : Real(f(A)) by exact fAReal594 have typedGA : Real(g(A)) by exact gAReal595 constructor596 . exact pointwiseMul.function at f, g with fFunction, gFunction597 . intros E realE positiveE598 have typedE : Real(E) by exact realE599 have scaleGReal := limitScale.real with typedGA600 have scaleGPositive := limitScale.positive with typedGA601 have radiusFReal := scaledRadius.real with typedE, scaleGReal602 have radiusFPositive := scaledRadius.positive with positiveE, scaleGPositive603 have absFAReal := abs.real with typedFA604 have boundReal := realAddValue.real with radiusFReal, absFAReal605 have radiusAboveAbs := realLess.add_right with realZero.real, radiusFReal, absFAReal, radiusFPositive606 have zeroPlusAbs := realAddValue.zero_left with absFAReal607 rw zeroPlusAbs at radiusAboveAbs608 have boundPositive := realLe.transitive_less at609 realZero, abs(f(A)),610 scaledRadius(E, limitScale(g(A))) + abs(f(A)) with611 realZero.real, absFAReal, boundReal,612 abs.nonnegative at f(A) with typedFA, radiusAboveAbs613 have radiusGPositive := scaledRadius.positive with positiveE, boundPositive614 obtain ⟨D, realD, positiveD, mapsF⟩ := ContinuousAt.maps_ball with continuousF, radiusFPositive615 obtain ⟨R, realR, positiveR, mapsG⟩ := ContinuousAt.maps_ball with continuousG, radiusGPositive616 have typedD : Real(D) by exact realD617 have typedR : Real(R) by exact realR618 obtain ⟨S, realS, positiveS, sLeD, sLeR⟩ := positiveRadius.common with619 typedD, typedR, positiveD, positiveR620 have typedS : Real(S) by exact realS621 witness S622 constructor623 . exact realS624 . constructor625 . exact positiveS626 . intros X realX near627 have typedX : Real(X) by exact realX628 have nearF := openBall.mono at X, A, S, D with629 typedX, assumption, typedS, typedD, near, sLeD630 have nearG := openBall.mono at X, A, S, R with631 typedX, assumption, typedS, typedR, near, sLeR632 have mappedF := mapsF with X, realX, nearF633 have mappedG := mapsG with X, realX, nearG634 have fXReal := FunctionBetween.apply_closed with fFunction, realX635 have gXReal := FunctionBetween.apply_closed with gFunction, realX636 have typedFX : Real(f(X)) by exact fXReal637 have typedGX : Real(g(X)) by exact gXReal638 have productNear := openBall.mul_control with positiveE, mappedF, mappedG639 have valueX := pointwiseMul.value with typedX, fFunction, gFunction, typedFX, typedGX640 have valueA := pointwiseMul.value at f, g, A with641 assumption, fFunction, gFunction, typedFA, typedGA642 rwa [valueX, valueA]643644theorem ContinuousAt.inv (f : Set) (A : Real)645 requires continuous : ContinuousAt(f, A)646 requires nonzero : Nonzero(f(A))647 shows ContinuousAt(pointwiseInv(f), A)648proof649 unfold Nonzero at nonzero650 have function := ContinuousAt.function with continuous651 have realA : A ∈ ℝ by simp [Real]652 have fAReal := FunctionBetween.apply_closed with function, realA653 have typedFA : Real(f(A)) by exact fAReal654 constructor655 . exact pointwiseInv.function at f with function656 . intros E realE positiveE657 have absFAPositive := abs.positive_of_ne with nonzero658 have awayRadiusPositive := half.positive with absFAPositive659 have scalePositive := inverseScale.positive with nonzero660 have epsilonRadiusPositive := scaledRadius.positive with positiveE, scalePositive661 obtain ⟨D, realD, positiveD, mapsAway⟩ := ContinuousAt.maps_ball with continuous, awayRadiusPositive662 obtain ⟨R, realR, positiveR, mapsEpsilon⟩ := ContinuousAt.maps_ball with continuous, epsilonRadiusPositive663 have typedD : Real(D) by exact realD664 have typedR : Real(R) by exact realR665 obtain ⟨S, realS, positiveS, sLeD, sLeR⟩ := positiveRadius.common with666 typedD, typedR, positiveD, positiveR667 have typedS : Real(S) by exact realS668 witness S669 constructor670 . exact realS671 . constructor672 . exact positiveS673 . intros X realX near674 have typedX : Real(X) by exact realX675 have nearAway := openBall.mono at X, A, S, D with676 typedX, assumption, typedS, typedD, near, sLeD677 have nearEpsilon := openBall.mono at X, A, S, R with678 typedX, assumption, typedS, typedR, near, sLeR679 have mappedAway := mapsAway with X, realX, nearAway680 have mappedEpsilon := mapsEpsilon with X, realX, nearEpsilon681 have fXReal := FunctionBetween.apply_closed with function, realX682 have typedFX : Real(f(X)) by exact fXReal683 have inverseNear := openBall.inv_control with nonzero, positiveE, mappedAway, mappedEpsilon684 have valueX := pointwiseInv.value with typedX, function, typedFX685 have valueA := pointwiseInv.value at f, A with686 assumption, function, typedFA687 rwa [valueX, valueA]688689690691theorem ContinuousAt.converges (f u : Set) (L : Real)692 requires continuous : ContinuousAt(f, L)693 requires converges : ConvergesTo(u, L)694 shows ConvergesTo(695 compose(f, u, ℕ, ℝ, ℝ), f(L))696proof697 have fFunction := ContinuousAt.function with continuous698 have sequence := ConvergesTo.sequence with converges699 unfold RealSequence at sequence700 have realL : L ∈ ℝ by simp [Real]701 have fLReal := FunctionBetween.apply_closed with fFunction702 constructor703 . unfold RealSequence704 exact compose.function with sequence, fFunction705 . intros E realE positive706 obtain ⟨D, realD, positiveD, maps⟩ := ContinuousAt.maps_ball with continuous, positive707 obtain ⟨N, naturalN, close⟩ := ConvergesTo.eventually with converges, positiveD708 witness N709 constructor710 . exact naturalN711 . intros n indexNatural nAfterN712 have unReal := FunctionBetween.apply_closed with sequence, indexNatural713 have near := close with n, indexNatural, nAfterN714 have mapped := maps with u(n), unReal, near715 have value := compose.apply with sequence, fFunction, indexNatural716 rwa value717718theorem realNeg.continuous_at (A : Real)719 shows ContinuousAt(realNeg, A)720proof721 constructor722 . exact realNeg.function723 . intros E realE positive724 have typedE : Real(E) by exact realE725 witness E726 constructor727 . exact realE728 . constructor729 . exact positive730 . intros X realX near731 have typedX : Real(X) by exact realX732 have nearData := openBall.membership.forward at A, E, X with near733 rcases nearData with ⟨_, within⟩734 have symmetry := dist.neg at X, A with typedX, assumption735 have negAReal := realNegValue.real at A736 apply openBall.membership.backward737 constructor738 . have negXReal := realNegValue.real with typedX739 exact negXReal740 . rw ← symmetry at within741 exact within742743theorem realNeg.continuous744 shows Continuous(realNeg)745proof746 constructor747 . exact realNeg.function748 . intros A realA749 have typedA : Real(A) by exact realA750 exact realNeg.continuous_at with typedA751752theorem ContinuousAt.neg (f : Set) (A : Real)753 requires continuous : ContinuousAt(f, A)754 shows ContinuousAt(pointwiseNeg(f), A)755proof756 have function := ContinuousAt.function with continuous757 have realA : A ∈ ℝ by simp [Real]758 have fAReal := FunctionBetween.apply_closed with function, realA759 have typedFA : Real(f(A)) by exact fAReal760 unfold pointwiseNeg761 exact ContinuousAt.comp at realNeg, f, A with762 continuous, realNeg.continuous_at at f(A) with typedFA763764theorem pointwiseSub.function (f g : Set)765 requires fFunction : f : ℝ → ℝ766 requires gFunction : g : ℝ → ℝ767 shows pointwiseSub(f, g) : ℝ → ℝ768proof769 have negFunction := pointwiseNeg.function with gFunction770 unfold pointwiseSub771 exact pointwiseAdd.function with fFunction, negFunction772773theorem pointwiseSub.value (f g : Set) (X : Real)774 requires fFunction : f : ℝ → ℝ775 requires gFunction : g : ℝ → ℝ776 requires fValueReal : Real(f(X))777 requires gValueReal : Real(g(X))778 shows pointwiseSub(f, g)(X) = f(X) - g(X)779proof780 have negFunction := pointwiseNeg.function with gFunction781 have negValueReal := realNegValue.real with gValueReal782 have negValue := pointwiseNeg.value at g, X with783 assumption, gFunction, gValueReal784 have pointNegReal : Real(pointwiseNeg(g)(X)) by rwa negValue785 have sumValue := pointwiseAdd.value at f, pointwiseNeg(g), X with786 assumption, fFunction, negFunction, fValueReal, pointNegReal787 unfold pointwiseSub788 rw negValue at sumValue789 simp [realSubValue]790791theorem pointwiseDiv.function (f g : Set)792 requires fFunction : f : ℝ → ℝ793 requires gFunction : g : ℝ → ℝ794 shows pointwiseDiv(f, g) : ℝ → ℝ795proof796 have inverseFunction := pointwiseInv.function with gFunction797 unfold pointwiseDiv798 exact pointwiseMul.function with fFunction, inverseFunction799800theorem pointwiseDiv.value (f g : Set) (X : Real)801 requires fFunction : f : ℝ → ℝ802 requires gFunction : g : ℝ → ℝ803 requires fValueReal : Real(f(X))804 requires gValueReal : Real(g(X))805 shows pointwiseDiv(f, g)(X) = f(X) / g(X)806proof807 have inverseFunction := pointwiseInv.function with gFunction808 have inverseValueReal := realInvValue.real with gValueReal809 have inverseValue := pointwiseInv.value at g, X with810 assumption, gFunction, gValueReal811 have pointInverseReal : Real(pointwiseInv(g)(X)) by rwa inverseValue812 have productValue := pointwiseMul.value at f, pointwiseInv(g), X with813 assumption, fFunction, inverseFunction,814 fValueReal, pointInverseReal815 have division := realDiv.eq_mul_inv with fValueReal, gValueReal816 unfold pointwiseDiv817 rw inverseValue at productValue818 rw division819 exact productValue820821theorem ContinuousAt.sub (f g : Set) (A : Real)822 requires continuousF : ContinuousAt(f, A)823 requires continuousG : ContinuousAt(g, A)824 shows ContinuousAt(pointwiseSub(f, g), A)825proof826 have negContinuous := ContinuousAt.neg with continuousG827 unfold pointwiseSub828 exact ContinuousAt.add with continuousF, negContinuous829830theorem ContinuousAt.div (f g : Set) (A : Real)831 requires continuousF : ContinuousAt(f, A)832 requires continuousG : ContinuousAt(g, A)833 requires nonzero : Nonzero(g(A))834 shows ContinuousAt(pointwiseDiv(f, g), A)835proof836 have inverseContinuous := ContinuousAt.inv with continuousG, nonzero837 unfold pointwiseDiv838 exact ContinuousAt.mul with continuousF, inverseContinuous839840theorem Continuous.neg (f : Set)841 requires continuous : Continuous(f)842 shows Continuous(pointwiseNeg(f))843proof844 rcases continuous with ⟨function, everywhere⟩845 constructor846 . exact pointwiseNeg.function with function847 . intros A realA848 have continuousAt := everywhere with A, realA849 exact ContinuousAt.neg with continuousAt850851theorem Continuous.add (f g : Set)852 requires continuousF : Continuous(f)853 requires continuousG : Continuous(g)854 shows Continuous(pointwiseAdd(f, g))855proof856 rcases continuousF with ⟨fFunction, fEverywhere⟩857 rcases continuousG with ⟨gFunction, gEverywhere⟩858 constructor859 . exact pointwiseAdd.function with fFunction, gFunction860 . intros A realA861 have continuousFA := fEverywhere with A, realA862 have continuousGA := gEverywhere with A, realA863 exact ContinuousAt.add with continuousFA, continuousGA864865theorem Continuous.sub (f g : Set)866 requires continuousF : Continuous(f)867 requires continuousG : Continuous(g)868 shows Continuous(pointwiseSub(f, g))869proof870 unfold pointwiseSub871 exact Continuous.add at f, pointwiseNeg(g) with872 continuousF, Continuous.neg at g with continuousG873874theorem Continuous.mul (f g : Set)875 requires continuousF : Continuous(f)876 requires continuousG : Continuous(g)877 shows Continuous(pointwiseMul(f, g))878proof879 rcases continuousF with ⟨fFunction, fEverywhere⟩880 rcases continuousG with ⟨gFunction, gEverywhere⟩881 constructor882 . exact pointwiseMul.function with fFunction, gFunction883 . intros A realA884 have continuousFA := fEverywhere with A, realA885 have continuousGA := gEverywhere with A, realA886 exact ContinuousAt.mul with continuousFA, continuousGA887888theorem Continuous.inv (f : Set)889 requires continuous : Continuous(f)890 requires nonzero : ∀ A ∈ ℝ, Nonzero(f(A))891 shows Continuous(pointwiseInv(f))892proof893 rcases continuous with ⟨function, everywhere⟩894 constructor895 . exact pointwiseInv.function with function896 . intros A realA897 have continuousAt := everywhere with A, realA898 have nonzeroAt := nonzero with A, realA899 exact ContinuousAt.inv with continuousAt, nonzeroAt900901theorem Continuous.div (f g : Set)902 requires continuousF : Continuous(f)903 requires continuousG : Continuous(g)904 requires nonzero : ∀ A ∈ ℝ, Nonzero(g(A))905 shows Continuous(pointwiseDiv(f, g))906proof907 have inverseContinuous := Continuous.inv with continuousG, nonzero908 unfold pointwiseDiv909 exact Continuous.mul with continuousF, inverseContinuous910911912predicate TendsToAt (f : Set) (L A : Real) :=913 FunctionBetween(f, ℝ, ℝ) ∧914 (∀ e ∈ ℝ, 0 < e →915 ∃ d ∈ ℝ, 0 < d ∧916 ∀ x ∈ ℝ, (x ≠ A → x ∈ openBall(A, d) →917 f(x) ∈ openBall(L, e)))918919theorem TendsToAt.function (f : Set) (L A : Real)920 requires limit : TendsToAt(f, L, A)921 shows f : ℝ → ℝ922proof923 simp [TendsToAt]924925theorem TendsToAt.eventually (f : Set) (L A E : Real)926 requires limit : TendsToAt(f, L, A)927 requires positive : 0 < E928 shows ∃ D ∈ ℝ, 0 < D ∧929 ∀ x ∈ ℝ, (x ≠ A → x ∈ openBall(A, D) →930 f(x) ∈ openBall(L, E))931proof932 rcases limit with ⟨function, local⟩933 exact local with E, positive934935936theorem ContinuousAt.tends_to (f : Set) (A : Real)937 requires continuous : ContinuousAt(f, A)938 shows TendsToAt(f, f(A), A)939proof940 have function := ContinuousAt.function with continuous941 constructor942 . exact function943 . intros E realE positive944 obtain ⟨D, realD, positiveD, maps⟩ := ContinuousAt.maps_ball with continuous, positive945 witness D946 constructor947 . exact realD948 . constructor949 . exact positiveD950 . intros X realX distinct near951 exact maps with X, realX, near952953theorem identity.tends_to_at (A : Real)954 shows TendsToAt(identity(ℝ), A, A)955proof956 have continuous := identity.continuous_at at A957 have limit := ContinuousAt.tends_to with continuous958 have realA : A ∈ ℝ by simp [Real]959 have mapped := identity.relates with realA960 have value := FunctionBetween.apply_value at961 identity(ℝ), ℝ, ℝ, A, A with962 identity.function at ℝ, realA, mapped963 rwa value at limit964965966967theorem TendsToAt.continuous_at (f : Set) (L A : Real)968 requires limit : TendsToAt(f, L, A)969 requires value : f(A) = L970 shows ContinuousAt(f, A)971proof972 have function := TendsToAt.function with limit973 have realA : A ∈ ℝ by simp [Real]974 have fAReal := FunctionBetween.apply_closed with function975 constructor976 . exact function977 . intros E realE positive978 obtain ⟨D, realD, positiveD, maps⟩ := TendsToAt.eventually with limit, positive979 witness D980 constructor981 . exact realD982 . constructor983 . exact positiveD984 . intros X realX near985 have equalityCases : X = A ∨ X ≠ A by tauto986 cases equalityCases with equal | distinct987 . rw equal988 exact openBall.center with positive989 . have mapped := maps with X, realX, distinct, near990 rwa value991992993994theorem TendsToAt.congr (f g : Set) (L A : Real)995 requires limit : TendsToAt(f, L, A)996 requires gFunction : g : ℝ → ℝ997 requires equalAway : ∀ x ∈ ℝ, (x ≠ A → g(x) = f(x))998 shows TendsToAt(g, L, A)999proof1000 constructor1001 . exact gFunction1002 . intros E realE positive1003 obtain ⟨D, realD, positiveD, maps⟩ := TendsToAt.eventually with limit, positive1004 witness D1005 constructor1006 . exact realD1007 . constructor1008 . exact positiveD1009 . intros X realX distinct near1010 have equal := equalAway with X, realX, distinct1011 rw equal1012 exact maps with X, realX, distinct, near10131014theorem TendsToAt.neg (f : Set) (L A : Real)1015 requires limit : TendsToAt(f, L, A)1016 shows TendsToAt(pointwiseNeg(f), -L, A)1017proof1018 have function := TendsToAt.function with limit1019 have negLReal := realNegValue.real at L1020 constructor1021 . exact pointwiseNeg.function with function1022 . intros E realE positive1023 have typedE : Real(E) by exact realE1024 obtain ⟨D, realD, positiveD, maps⟩ := TendsToAt.eventually with limit, positive1025 witness D1026 constructor1027 . exact realD1028 . constructor1029 . exact positiveD1030 . intros X realX distinct near1031 have mapped := maps with X, realX, distinct, near1032 have fXInReals := FunctionBetween.apply_closed with function, realX1033 have typedFX : Real(f(X)) by exact fXInReals1034 have value := pointwiseNeg.value with function1035 have negDistance := dist.neg at f(X), L with1036 typedFX, assumption1037 apply openBall.membership.backward1038 have mappedData := openBall.membership.forward at1039 L, E, f(X) with mapped1040 rcases mappedData with ⟨realFX, within⟩1041 constructor1042 . rw value1043 exact realNegValue.real with typedFX1044 . rw [value, negDistance]1045 exact within10461047theorem TendsToAt.add (f g : Set) (L M A : Real)1048 requires limitF : TendsToAt(f, L, A)1049 requires limitG : TendsToAt(g, M, A)1050 shows TendsToAt(pointwiseAdd(f, g), L + M, A)1051proof1052 have fFunction := TendsToAt.function with limitF1053 have gFunction := TendsToAt.function with limitG1054 constructor1055 . exact pointwiseAdd.function with fFunction, gFunction1056 . intros E realE positive1057 have typedE : Real(E) by exact realE1058 have radiusPositive := half.positive with positive1059 obtain ⟨D, realD, positiveD, mapsF⟩ := TendsToAt.eventually with limitF, radiusPositive1060 obtain ⟨R, realR, positiveR, mapsG⟩ := TendsToAt.eventually with limitG, radiusPositive1061 have typedD : Real(D) by exact realD1062 have typedR : Real(R) by exact realR1063 obtain ⟨S, realS, positiveS, sLeD, sLeR⟩ := positiveRadius.common with1064 typedD, typedR, positiveD, positiveR1065 have typedS : Real(S) by exact realS1066 witness S1067 constructor1068 . exact realS1069 . constructor1070 . exact positiveS1071 . intros X realX distinct near1072 have typedX : Real(X) by exact realX1073 have nearF := openBall.mono at X, A, S, D with1074 typedX, assumption, typedS, typedD, near, sLeD1075 have nearG := openBall.mono at X, A, S, R with1076 typedX, assumption, typedS, typedR, near, sLeR1077 have mappedF := mapsF with X, realX, distinct, nearF1078 have mappedG := mapsG with X, realX, distinct, nearG1079 have fXInReals := FunctionBetween.apply_closed with fFunction, realX1080 have gXInReals := FunctionBetween.apply_closed with gFunction, realX1081 have typedGX : Real(g(X)) by exact gXInReals1082 have sumNear := openBall.add with mappedF, mappedG1083 have doubled := half.add_self with typedE1084 rw doubled at sumNear1085 have value := pointwiseAdd.value with fFunction, gFunction1086 rwa value10871088108910901091theorem TendsToAt.mul (f g : Set) (L M A : Real)1092 requires limitF : TendsToAt(f, L, A)1093 requires limitG : TendsToAt(g, M, A)1094 shows TendsToAt(pointwiseMul(f, g), L * M, A)1095proof1096 have fFunction := TendsToAt.function with limitF1097 have gFunction := TendsToAt.function with limitG1098 constructor1099 . exact pointwiseMul.function with fFunction, gFunction1100 . intros E realE positiveE1101 have typedE : Real(E) by exact realE1102 have scaleMReal := limitScale.real at M1103 have scaleMPositive := limitScale.positive at M1104 have radiusFReal := scaledRadius.real with typedE, scaleMReal1105 have radiusFPositive := scaledRadius.positive with positiveE, scaleMPositive1106 have absLReal := abs.real at L1107 have boundReal := realAddValue.real with radiusFReal, absLReal1108 have radiusAboveAbs := realLess.add_right with realZero.real, radiusFReal, absLReal, radiusFPositive1109 have zeroPlusAbs := realAddValue.zero_left with absLReal1110 rw zeroPlusAbs at radiusAboveAbs1111 have boundPositive := realLe.transitive_less at1112 realZero, abs(L), scaledRadius(E, limitScale(M)) + abs(L) with1113 realZero.real, absLReal, boundReal,1114 abs.nonnegative at L with assumption, radiusAboveAbs1115 have radiusGPositive := scaledRadius.positive with positiveE, boundPositive1116 obtain ⟨D, realD, positiveD, mapsF⟩ := TendsToAt.eventually with limitF, radiusFPositive1117 obtain ⟨R, realR, positiveR, mapsG⟩ := TendsToAt.eventually with limitG, radiusGPositive1118 have typedD : Real(D) by exact realD1119 have typedR : Real(R) by exact realR1120 obtain ⟨S, realS, positiveS, sLeD, sLeR⟩ := positiveRadius.common with1121 typedD, typedR, positiveD, positiveR1122 have typedS : Real(S) by exact realS1123 witness S1124 constructor1125 . exact realS1126 . constructor1127 . exact positiveS1128 . intros X realX distinct near1129 have typedX : Real(X) by exact realX1130 have nearF := openBall.mono at X, A, S, D with1131 typedX, assumption, typedS, typedD, near, sLeD1132 have nearG := openBall.mono at X, A, S, R with1133 typedX, assumption, typedS, typedR, near, sLeR1134 have mappedF := mapsF with X, realX, distinct, nearF1135 have mappedG := mapsG with X, realX, distinct, nearG1136 have fXReal := FunctionBetween.apply_closed with fFunction, realX1137 have gXReal := FunctionBetween.apply_closed with gFunction, realX1138 have typedGX : Real(g(X)) by exact gXReal1139 have productNear := openBall.mul_control with positiveE, mappedF, mappedG1140 have value := pointwiseMul.value with fFunction, gFunction1141 rwa value11421143theorem TendsToAt.sub (f g : Set) (L M A : Real)1144 requires limitF : TendsToAt(f, L, A)1145 requires limitG : TendsToAt(g, M, A)1146 shows TendsToAt(pointwiseSub(f, g), L - M, A)1147proof1148 have negLimit := TendsToAt.neg with limitG1149 have sumLimit := TendsToAt.add with limitF, negLimit1150 unfold pointwiseSub1151 unfold realSubValue1152 exact sumLimit115311541155theorem openBall.punctured_real (A R : Real)1156 requires positive : 0 < R1157 shows ∃ X ∈ ℝ, X ≠ A ∧ X ∈ openBall(A, R)1158proof1159 have halfReal := half.real at R1160 have halfPositive := half.positive with positive1161 have halfLess := half.lt_self with positive1162 have xReal := realAddValue.real at A, half(R) with assumption, halfReal1163 have realX : A + half(R) ∈ ℝ by exact xReal1164 have offset : (A + half(R)) - A = half(R) by ring1165 have distinct : A + half(R) ≠ A1166 intro equal1167 rw equal at offset1168 have self := realSubValue.self at A1169 rw self at offset1170 rw ← offset at halfPositive1171 exact IsOrderedField.irreflexive with reals.ordered_field, halfPositive1172 have halfNonnegative := realLess.implies_le with halfPositive1173 have absHalf := abs.of_nonnegative with halfNonnegative1174 have near : A + half(R) ∈ openBall(A, R)1175 have distanceLess : dist(A + half(R), A) < R1176 unfold dist1177 rwa [offset, absHalf]1178 have data : A + half(R) ∈ ℝ ∧ dist(A + half(R), A) < R1179 constructor1180 . exact realX1181 . exact distanceLess1182 exact openBall.membership.backward with data1183 witness A + half(R)1184 refine ⟨realX, distinct, near⟩11851186theorem TendsToAt.unique (f : Set) (L M A : Real)1187 requires first : TendsToAt(f, L, A)1188 requires second : TendsToAt(f, M, A)1189 shows L = M1190proof1191 by_contra unequal1192 have positiveDistance := dist.positive_of_ne with unequal1193 have radiusPositive := half.positive with positiveDistance1194 obtain ⟨D, realD, positiveD, mapsL⟩ := TendsToAt.eventually with first, radiusPositive1195 obtain ⟨E, realE, positiveE, mapsM⟩ := TendsToAt.eventually with second, radiusPositive1196 have typedD : Real(D) by exact realD1197 have typedE : Real(E) by exact realE1198 obtain ⟨R, realR, positiveR, rLeD, rLeE⟩ := positiveRadius.common with positiveD, positiveE1199 have typedR : Real(R) by exact realR1200 obtain ⟨X, realX, distinct, near⟩ := openBall.punctured_real at A, R with1201 positiveR1202 have typedX : Real(X) by exact realX1203 have nearD := openBall.mono at X, A, R, D with1204 typedX, assumption, typedR, typedD, near, rLeD1205 have nearE := openBall.mono at X, A, R, E with1206 typedX, assumption, typedR, typedE, near, rLeE1207 have nearL := mapsL with X, realX, distinct, nearD1208 have nearM := mapsM with X, realX, distinct, nearE1209 have function := TendsToAt.function with first1210 have valueReal := FunctionBetween.apply_closed with function, realX1211 have equal := openBall.half_radius_unique with nearL, nearM1212 exact unequal with equal121312141215predicate Positive (A : Real) := 0 < A1216predicate Negative (A : Real) := A < 01217predicate Below (A B : Real) := A < B12181219theorem Positive.characterization (A : Real)1220 shows Positive(A) ↔ 0 < A1221proof1222 simp [Positive]12231224theorem Negative.characterization (A : Real)1225 shows Negative(A) ↔ A < 01226proof1227 simp [Negative]12281229theorem Below.characterization (A B : Real)1230 shows Below(A, B) ↔ A < B1231proof1232 simp [Below]12331234123512361237theorem ContinuousAt.eventually_positive (f : Set) (A : Real)1238 requires continuous : ContinuousAt(f, A)1239 requires positive : Positive(f(A))1240 shows ∃ D ∈ ℝ, 0 < D ∧1241 ∀ x ∈ ℝ, (x ∈ openBall(A, D) → Positive(f(x)))1242proof1243 unfold Positive at positive1244 have function := ContinuousAt.function with continuous1245 have valueReal := ContinuousAt.value_type with continuous1246 obtain ⟨D, realD, positiveD, maps⟩ := ContinuousAt.maps_ball with continuous, positive1247 witness D1248 constructor1249 . exact realD1250 . constructor1251 . exact positiveD1252 . intros X realX near1253 unfold Positive1254 have fXReal := FunctionBetween.apply_closed with function, realX1255 have mapped := maps with X, realX, near1256 obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with mapped1257 have selfDifference := realSubValue.self with valueReal1258 rwa selfDifference at lower12591260theorem ContinuousAt.eventually_negative (f : Set) (A : Real)1261 requires continuous : ContinuousAt(f, A)1262 requires negative : Negative(f(A))1263 shows ∃ D ∈ ℝ, 0 < D ∧1264 ∀ x ∈ ℝ, (x ∈ openBall(A, D) → Negative(f(x)))1265proof1266 unfold Negative at negative1267 have function := ContinuousAt.function with continuous1268 have valueReal := ContinuousAt.value_type with continuous1269 have negativeView := realLess.characterization.forward with negative1270 have reversedView := RealLess.neg_reverse with negativeView1271 have reversed := realLess.characterization.backward with reversedView1272 have negZero := realNegValue.zero1273 rw negZero at reversed1274 obtain ⟨D, realD, positiveD, maps⟩ := ContinuousAt.maps_ball with continuous, reversed1275 witness D1276 constructor1277 . exact realD1278 . constructor1279 . exact positiveD1280 . intros X realX near1281 unfold Negative1282 have fXReal := FunctionBetween.apply_closed with function, realX1283 have mapped := maps with X, realX, near1284 obtain ⟨lower, upper⟩ := openBall.order_characterization.forward with mapped1285 have inverse := realAddValue.neg_right with valueReal1286 rwa inverse at upper1287128812891290theorem ContinuousAt.eventually_nonzero (f : Set) (A : Real)1291 requires continuous : ContinuousAt(f, A)1292 requires nonzero : Nonzero(f(A))1293 shows ∃ D ∈ ℝ, 0 < D ∧1294 ∀ x ∈ ℝ, (x ∈ openBall(A, D) → Nonzero(f(x)))1295proof1296 have function := ContinuousAt.function with continuous1297 have valueReal := ContinuousAt.value_type with continuous1298 have valueInReals : f(A) ∈ ℝ by exact valueReal1299 have zeroInReals : realZero ∈ ℝ by exact realZero.real1300 have comparison := realLess.connected_on1301 specialize comparison with1302 f(A), valueInReals, realZero, zeroInReals, nonzero1303 cases comparison with negative | positive1304 . have negativeAt := Negative.characterization.backward at1305 f(A) with negative1306 obtain ⟨D, realD, positiveD, staysNegative⟩ := ContinuousAt.eventually_negative with1307 continuous, negativeAt1308 witness D1309 constructor1310 . exact realD1311 . constructor1312 . exact positiveD1313 . intros X realX near1314 unfold Nonzero1315 have below := staysNegative with X, realX, near1316 unfold Negative at below1317 have fXReal := FunctionBetween.apply_closed with function, realX1318 exact IsOrderedField.ne_of_less with reals.ordered_field, fXReal, below1319 . have positiveAt := Positive.characterization.backward at1320 f(A) with positive1321 obtain ⟨R, realR, positiveR, staysPositive⟩ := ContinuousAt.eventually_positive with1322 continuous, positiveAt1323 witness R1324 constructor1325 . exact realR1326 . constructor1327 . exact positiveR1328 . intros X realX near1329 unfold Nonzero1330 have above := staysPositive with X, realX, near1331 unfold Positive at above1332 intro equal1333 rw equal at above1334 exact IsOrderedField.irreflexive with reals.ordered_field, above1335133613371338theorem ContinuousAt.eventually_lt (f g : Set) (A : Real)1339 requires continuousF : ContinuousAt(f, A)1340 requires continuousG : ContinuousAt(g, A)1341 requires less : Below(f(A), g(A))1342 shows ∃ D ∈ ℝ, 0 < D ∧1343 ∀ x ∈ ℝ, (x ∈ openBall(A, D) → Below(f(x), g(x)))1344proof1345 unfold Below at less1346 have fFunction := ContinuousAt.function with continuousF1347 have gFunction := ContinuousAt.function with continuousG1348 have fAReal := ContinuousAt.value_type with continuousF1349 have gAReal := ContinuousAt.value_type with continuousG1350 have differenceContinuous := ContinuousAt.sub with continuousG, continuousF1351 have valueAtA := pointwiseSub.value at g, f, A with1352 assumption, gFunction, fFunction, gAReal, fAReal1353 have positiveDifference := realLess.iff_pos_sub.forward with fAReal, gAReal, less1354 rw ← valueAtA at positiveDifference1355 have differencePositive := Positive.characterization.backward with positiveDifference1356 obtain ⟨D, realD, positiveD, staysPositive⟩ := ContinuousAt.eventually_positive with1357 differenceContinuous, differencePositive1358 witness D1359 constructor1360 . exact realD1361 . constructor1362 . exact positiveD1363 . intros X realX near1364 unfold Below1365 have typedX : Real(X) by exact realX1366 have fXReal := FunctionBetween.apply_closed with fFunction, realX1367 have gXReal := FunctionBetween.apply_closed with gFunction, realX1368 have typedFX : Real(f(X)) by exact fXReal1369 have typedGX : Real(g(X)) by exact gXReal1370 have positiveAtX := staysPositive with X, realX, near1371 unfold Positive at positiveAtX1372 have valueAtX := pointwiseSub.value with typedX, gFunction, fFunction, typedGX, typedFX1373 rw valueAtX at positiveAtX1374 exact realLess.iff_pos_sub.backward with positiveAtX1375