Grace/Cumulus/Complex/SequentialContinuity.g17

Open in Workbench Download source

Imports

Compactness

Declarations

Source

1-- Coordinate convergence and squared-distance continuity describe the same limits.2-- 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.Complex.SequentialContinuity8import Compactness910theorem realSquare.abs_lt_of_lt_square (a e : Real)11  requires positive : realZero < e12  requires small : a * a < e * e13  shows abs(a) < e14proof15  have nonnegative := abs.nonnegative at a with *16  have eNonnegative := realLess.implies_le at realZero, e with *17  have squareNonnegative := realMulValue.square_nonnegative at a with *18  have squareAbs := abs.of_nonnegative at a * a with *19  have multiplicative := abs.mul at a, a with *20  have square : abs(a) * abs(a) = a * a by cc21  have comparison : e ≤ abs(a) ∨ ¬(e ≤ abs(a)) by tauto22  cases comparison with large | notLarge23  . have first := realLe.mul_left_of_nonnegative at e, abs(a), e with *24    have second := realLe.mul_right_of_nonnegative at e, abs(a), abs(a) with *25    have bound := realLe.transitive at e * e, e * abs(a), abs(a) * abs(a) with *26    rw square at bound27    have impossible := realLess.transitive_le at a * a, e * e, a * a with *28    have irrefl := realLess.irreflexive_on29    exfalso30    exact irrefl with a * a, impossible31  . exact realLess.of_not_le at e, abs(a) with *3233def complexDistanceSequence (u a : Set) : Set :=34  addSequence(35    mulSequence(subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a)))),36    mulSequence(subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a)))))3738def complexMappedSequence (f u : Set) : Set := compose(f, u, ℕ, complexCarrier, complexCarrier)3940section Complexes41notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)42notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)4344theorem complexNormSquared.difference_coordinates (z a : Set)45  requires first : z ∈ ℂ46  requires second : a ∈ ℂ47  shows complexNormSquared(ℂ[z - a]) = R[(Euclidean.x(z) - Euclidean.x(a)) * (Euclidean.x(z) - Euclidean.x(a)) + (Euclidean.y(z) - Euclidean.y(a)) * (Euclidean.y(z) - Euclidean.y(a))]48proof49  have zPoint := complex.point with first50  have aPoint := complex.point with second51  rw [complexNormSquared.difference_distance, Euclidean.distanceSquared.coordinates]52  ring5354theorem complexNormSquared.small_coordinates (z a : Set) (e : Real)55  requires first : z ∈ ℂ56  requires second : a ∈ ℂ57  requires positive : R[0] < e58  requires small : complexNormSquared(ℂ[z - a]) < R[e * e]59  shows Euclidean.x(z) ∈ openBall(Euclidean.x(a), e) ∧ Euclidean.y(z) ∈ openBall(Euclidean.y(a), e)60proof61  have zPoint := complex.point with first62  have aPoint := complex.point with second63  have ax := Euclidean.x.real at a with *64  have ay := Euclidean.y.real at a with *65  have xx := realMulValue.square_nonnegative at R[Euclidean.x(z) - Euclidean.x(a)] with *66  have yy := realMulValue.square_nonnegative at R[Euclidean.y(z) - Euclidean.y(a)] with *67  have sums := realLe.nonnegative_sum_bounds at R[(Euclidean.x(z) - Euclidean.x(a)) * (Euclidean.x(z) - Euclidean.x(a))], R[(Euclidean.y(z) - Euclidean.y(a)) * (Euclidean.y(z) - Euclidean.y(a))] with *68  rw complexNormSquared.difference_coordinates at small69  have xSmall := realLe.transitive_less at R[(Euclidean.x(z) - Euclidean.x(a)) * (Euclidean.x(z) - Euclidean.x(a))], R[(Euclidean.x(z) - Euclidean.x(a)) * (Euclidean.x(z) - Euclidean.x(a)) + (Euclidean.y(z) - Euclidean.y(a)) * (Euclidean.y(z) - Euclidean.y(a))], R[e * e] with *70  have ySmall := realLe.transitive_less at R[(Euclidean.y(z) - Euclidean.y(a)) * (Euclidean.y(z) - Euclidean.y(a))], R[(Euclidean.x(z) - Euclidean.x(a)) * (Euclidean.x(z) - Euclidean.x(a)) + (Euclidean.y(z) - Euclidean.y(a)) * (Euclidean.y(z) - Euclidean.y(a))], R[e * e] with *71  have xAbs := realSquare.abs_lt_of_lt_square at R[Euclidean.x(z) - Euclidean.x(a)], e with *72  have yAbs := realSquare.abs_lt_of_lt_square at R[Euclidean.y(z) - Euclidean.y(a)], e with *73  have xIn : Euclidean.x(z) ∈ ℝ by typecheck74  have yIn : Euclidean.y(z) ∈ ℝ by typecheck75  constructor76  . apply openBall.membership.backward77    constructor78    . exact xIn79    . unfold dist80      unfold realSubValue81      exact xAbs82  . apply openBall.membership.backward83    constructor84    . exact yIn85    . unfold dist86      unfold realSubValue87      exact yAbs888990theorem complexDistanceSequence.converges_zero (u a : Set)91  requires converges : ComplexConvergesTo(u, a)92  shows ConvergesTo(complexDistanceSequence(u, a), R[0])93proof94  rcases converges with ⟨sequence, member, horizontal, vertical⟩95  have point := complex.point with member96  have xConstant := constantSequence.converges at Euclidean.x(a) with *97  have yConstant := constantSequence.converges at Euclidean.y(a) with *98  have xDiff := ConvergesTo.sub at complexSequenceX(u), constantSequence(Euclidean.x(a)), Euclidean.x(a), Euclidean.x(a) with *99  have yDiff := ConvergesTo.sub at complexSequenceY(u), constantSequence(Euclidean.y(a)), Euclidean.y(a), Euclidean.y(a) with *100  unfold realSubValue at xDiff101  unfold realSubValue at yDiff102  have xx := ConvergesTo.mul at subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), R[Euclidean.x(a) - Euclidean.x(a)], R[Euclidean.x(a) - Euclidean.x(a)] with *103  have yy := ConvergesTo.mul at subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), R[Euclidean.y(a) - Euclidean.y(a)], R[Euclidean.y(a) - Euclidean.y(a)] with *104  have sum := ConvergesTo.add at mulSequence(subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a)))), mulSequence(subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a)))), R[(Euclidean.x(a) - Euclidean.x(a)) * (Euclidean.x(a) - Euclidean.x(a))], R[(Euclidean.y(a) - Euclidean.y(a)) * (Euclidean.y(a) - Euclidean.y(a))] with *105  have zero : R[(Euclidean.x(a) - Euclidean.x(a)) * (Euclidean.x(a) - Euclidean.x(a)) + (Euclidean.y(a) - Euclidean.y(a)) * (Euclidean.y(a) - Euclidean.y(a))] = R[0]106    ring107  rw zero at sum108  unfold complexDistanceSequence109  exact sum110111theorem complexDistanceSequence.value (u a : Set) (n : Nat)112  requires sequence : ComplexSequence(u)113  requires center : a ∈ ℂ114  shows complexDistanceSequence(u, a)(n) = complexNormSquared(ℂ[u(n) - a])115proof116  have point := complex.point with center117  have horizontal := complexSequenceX.sequence with *118  have vertical := complexSequenceY.sequence with *119  have xConstant := constantSequence.sequence at Euclidean.x(a) with *120  have yConstant := constantSequence.sequence at Euclidean.y(a) with *121  have xDiff := subSequence.sequence at complexSequenceX(u), constantSequence(Euclidean.x(a)) with *122  have yDiff := subSequence.sequence at complexSequenceY(u), constantSequence(Euclidean.y(a)) with *123  have xx := mulSequence.sequence at subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))) with *124  have yy := mulSequence.sequence at subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))) with *125  have xReal := RealSequence.value at complexSequenceX(u), n with *126  have yReal := RealSequence.value at complexSequenceY(u), n with *127  have cxReal := RealSequence.value at constantSequence(Euclidean.x(a)), n with *128  have cyReal := RealSequence.value at constantSequence(Euclidean.y(a)), n with *129  have dxReal := RealSequence.value at subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), n with *130  have dyReal := RealSequence.value at subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), n with *131  have xxReal := RealSequence.value at mulSequence(subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a))), subSequence(complexSequenceX(u), constantSequence(Euclidean.x(a)))), n with *132  have yyReal := RealSequence.value at mulSequence(subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a))), subSequence(complexSequenceY(u), constantSequence(Euclidean.y(a)))), n with *133  have function : u : ℕ → ℂ by exact sequence134  have member := FunctionBetween.apply_closed at u, ℕ, ℂ, n with *135  unfold complexDistanceSequence136  rw [addSequence.value, mulSequence.value, mulSequence.value, subSequence.value, subSequence.value, constantSequence.value, constantSequence.value, complexSequenceX.value, complexSequenceY.value, complexNormSquared.difference_coordinates]137  simp [realSubValue]138139theorem ComplexConvergesTo.eventually_squared_distance (u a : Set) (e : Real)140  requires converges : ComplexConvergesTo(u, a)141  requires positive : R[0] < e142  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → complexNormSquared(ℂ[u(n) - a]) < e143proof144  have distanceLimit := complexDistanceSequence.converges_zero with *145  have distanceSequence := ConvergesTo.sequence at complexDistanceSequence(u, a), R[0] with *146  obtain ⟨N, natural, close⟩ := ConvergesTo.eventually at complexDistanceSequence(u, a), R[0], e with *147  rcases converges with ⟨sequence, member, horizontal, vertical⟩148  refine ⟨N, natural, ?_⟩149  intros n nIn after150  have nNat := nat.omega.backward at n with *151  have termReal := RealSequence.value with *152  have near := close with n, nIn, after153  have interval := openBall.order_characterization.forward with *154  have upper := interval.right155  rwa [realAddValue.zero_left, complexDistanceSequence.value] at upper156157theorem ComplexConvergesTo.of_squared_distance (u a : Set)158  requires sequence : ComplexSequence(u)159  requires center : a ∈ ℂ160  requires close : ∀ e ∈ ℝ, R[0] < e → ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → complexNormSquared(ℂ[u(n) - a]) < e161  shows ComplexConvergesTo(u, a)162proof163  have point := complex.point with center164  have horizontal := complexSequenceX.sequence with *165  have vertical := complexSequenceY.sequence with *166  have function : u : ℕ → ℂ by exact sequence167  have both : ∀ e ∈ ℝ, R[0] < e → ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n →168      complexSequenceX(u)(n) ∈ openBall(Euclidean.x(a), e) ∧ complexSequenceY(u)(n) ∈ openBall(Euclidean.y(a), e)169    intros e eIn positive170    have squarePositive := realMulValue.positive with *171    obtain ⟨N, natural, small⟩ := close with R[e * e], squarePositive172    refine ⟨N, natural, ?_⟩173    intros n nIn after174    have nNat := nat.omega.backward at n with *175    have member := FunctionBetween.apply_closed at u, ℕ, ℂ, n with *176    have distance := small with n, nIn, after177    have coordinates := complexNormSquared.small_coordinates with *178    rwa [complexSequenceX.value, complexSequenceY.value]179  unfold ComplexConvergesTo180  refine ⟨sequence, center, ?_⟩181  constructor182  . unfold ConvergesTo183    refine ⟨horizontal, ?_⟩184    intros e eIn positive185    obtain ⟨N, natural, closeBoth⟩ := both with e, eIn, positive186    refine ⟨N, natural, ?_⟩187    intros n nIn after188    have near := closeBoth with n, nIn, after189    exact near.left190  . unfold ConvergesTo191    refine ⟨vertical, ?_⟩192    intros e eIn positive193    obtain ⟨N, natural, closeBoth⟩ := both with e, eIn, positive194    refine ⟨N, natural, ?_⟩195    intros n nIn after196    have near := closeBoth with n, nIn, after197    exact near.right198199theorem complexMappedSequence.sequence (f u : Set)200  requires function : f : ℂ → ℂ201  requires sequence : ComplexSequence(u)202  shows ComplexSequence(complexMappedSequence(f, u))203proof204  have uFunction : u : ℕ → ℂ by exact sequence205  unfold ComplexSequence206  unfold complexMappedSequence207  exact compose.function with *208209theorem complexMappedSequence.value (f u : Set) (n : Nat)210  requires function : f : ℂ → ℂ211  requires sequence : ComplexSequence(u)212  shows complexMappedSequence(f, u)(n) = f(u(n))213proof214  have uFunction : u : ℕ → ℂ by exact sequence215  unfold complexMappedSequence216  exact compose.apply with *217218theorem ComplexContinuousAt.converges (f u a : Set)219  requires continuous : ComplexContinuousAt(f, a)220  requires converges : ComplexConvergesTo(u, a)221  shows ComplexConvergesTo(complexMappedSequence(f, u), f(a))222proof223  have convergesAgain := converges224  rcases converges with ⟨sequence, center, horizontal, vertical⟩225  rcases continuous with ⟨function, centerAgain, local⟩226  have mapped := complexMappedSequence.sequence with *227  have image := FunctionBetween.apply_closed with *228  have uFunction : u : ℕ → ℂ by exact sequence229  apply ComplexConvergesTo.of_squared_distance with mapped, image230  intros e eIn positive231  obtain ⟨d, dIn, dPositive, nearImage⟩ := local with e, eIn, positive232  obtain ⟨N, natural, nearInput⟩ := ComplexConvergesTo.eventually_squared_distance at u, a, d with *233  refine ⟨N, natural, ?_⟩234  intros n nIn after235  have nNat := nat.omega.backward at n with *236  have member := FunctionBetween.apply_closed at u, ℕ, ℂ, n with *237  have near := nearInput with n, nIn, after238  rw complexMappedSequence.value239  exact nearImage with u(n), member, near240241theorem complexPolynomial.converges (u a : Set) (cs : List(ℂ))242  requires converges : ComplexConvergesTo(u, a)243  shows ComplexConvergesTo(complexMappedSequence(complexPolynomial(cs), u), complexPolynomial(cs)(a))244proof245  have center : a ∈ ℂ246    rcases converges with ⟨sequence, center, horizontal, vertical⟩247    exact center248  have continuous := complexPolynomial.continuous_at with *249  exact ComplexContinuousAt.converges with *250251theorem complexPolynomial.norm_converges (u a : Set) (cs : List(ℂ))252  requires converges : ComplexConvergesTo(u, a)253  shows ConvergesTo(complexNormSequence(complexMappedSequence(complexPolynomial(cs), u)), complexNormSquared(complexPolynomial(cs)(a)))254proof255  have mapped := complexPolynomial.converges with *256  exact ComplexConvergesTo.norm_squared with *257258end Complexes259