Grace/Cumulus/Complex/SequenceAlgebra.g17

Open in Workbench Download source

Imports

MinimumDirection · Real.Analysis.Examples

Declarations

Source

1-- Coordinate assembly and fixed-direction scaling of convergent sequences.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.SequenceAlgebra8import MinimumDirection9import Real.Analysis.Examples1011def complexPairSequence (u v : Set) : Set := pairFunctions(u, v, ℕ, ℝ, ℝ)1213theorem complexPairSequence.sequence (u v : Set)14  requires horizontal : RealSequence(u)15  requires vertical : RealSequence(v)16  shows ComplexSequence(complexPairSequence(u, v))17proof18  unfold ComplexSequence19  unfold complexPairSequence20  unfold complexCarrier21  exact pairFunctions.function with *2223theorem complexPairSequence.value (u v : Set) (n : Nat)24  requires horizontal : RealSequence(u)25  requires vertical : RealSequence(v)26  shows complexPairSequence(u, v)(n) = (u(n), v(n))27proof28  unfold complexPairSequence29  exact pairFunctions.apply with *3031theorem complexPairSequence.x (u v : Set)32  requires horizontal : RealSequence(u)33  requires vertical : RealSequence(v)34  shows complexSequenceX(complexPairSequence(u, v)) = u35proof36  have sequence := complexPairSequence.sequence at u, v with *37  have left := complexSequenceX.function at complexPairSequence(u, v) with *38  have right : u : ℕ → ℝ by exact horizontal39  apply FunctionBetween.ext with left, right40  intros n nIn41  have nNat := nat.omega.backward at n with *42  have un := RealSequence.value at u, n with *43  have vn := RealSequence.value at v, n with *44  rw [complexSequenceX.value, complexPairSequence.value, Euclidean.x.pair]45  rfl4647theorem complexPairSequence.y (u v : Set)48  requires horizontal : RealSequence(u)49  requires vertical : RealSequence(v)50  shows complexSequenceY(complexPairSequence(u, v)) = v51proof52  have sequence := complexPairSequence.sequence at u, v with *53  have left := complexSequenceY.function at complexPairSequence(u, v) with *54  have right : v : ℕ → ℝ by exact vertical55  apply FunctionBetween.ext with left, right56  intros n nIn57  have nNat := nat.omega.backward at n with *58  have un := RealSequence.value at u, n with *59  have vn := RealSequence.value at v, n with *60  rw [complexSequenceY.value, complexPairSequence.value, Euclidean.y.pair]61  rfl6263theorem complexPairSequence.converges (u v : Set) (a b : Real)64  requires horizontal : ConvergesTo(u, a)65  requires vertical : ConvergesTo(v, b)66  shows ComplexConvergesTo(complexPairSequence(u, v), (a, b))67proof68  have uSequence := ConvergesTo.sequence at u, a with *69  have vSequence := ConvergesTo.sequence at v, b with *70  have sequence := complexPairSequence.sequence at u, v with *71  have member := complexCarrier.pair at a, b with *72  unfold ComplexConvergesTo73  refine ⟨sequence, member, ?_⟩74  constructor75  . rw [complexPairSequence.x, Euclidean.x.pair]76    exact horizontal77  . rw [complexPairSequence.y, Euclidean.y.pair]78    exact vertical7980def complexRaySequence (s z : Set) : Set := complexPairSequence(81  mulSequence(s, constantSequence(Euclidean.x(z))),82  mulSequence(s, constantSequence(Euclidean.y(z))))8384defgraph complexLeftMul (z : Set) (w ∈ complexCarrier) : complexCarrier := complexMul(z, w)85requires factor : z ∈ complexCarrier86proof87  have ring := complexes.comm_ring88  have ordinary := IsCommRing.ring with ring89  exact IsRing.mul_closed with *9091section Complexes92notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)93notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)9495theorem complexRaySequence.sequence (s z : Set)96  requires steps : RealSequence(s)97  requires member : z ∈ ℂ98  shows ComplexSequence(complexRaySequence(s, z))99proof100  have point := complex.point with *101  have cx := constantSequence.sequence at Euclidean.x(z) with *102  have cy := constantSequence.sequence at Euclidean.y(z) with *103  have sx := mulSequence.sequence at s, constantSequence(Euclidean.x(z)) with *104  have sy := mulSequence.sequence at s, constantSequence(Euclidean.y(z)) with *105  unfold complexRaySequence106  exact complexPairSequence.sequence with *107108theorem complexRaySequence.value (s z : Set) (n : Nat)109  requires steps : RealSequence(s)110  requires member : z ∈ ℂ111  shows complexRaySequence(s, z)(n) = complexScale(s(n), z)112proof113  have point := complex.point with *114  have cx := constantSequence.sequence at Euclidean.x(z) with *115  have cy := constantSequence.sequence at Euclidean.y(z) with *116  have sx := mulSequence.sequence at s, constantSequence(Euclidean.x(z)) with *117  have sy := mulSequence.sequence at s, constantSequence(Euclidean.y(z)) with *118  have sn := RealSequence.value at s, n with *119  have xn := RealSequence.value at constantSequence(Euclidean.x(z)), n with *120  have yn := RealSequence.value at constantSequence(Euclidean.y(z)), n with *121  unfold complexRaySequence122  rw [complexPairSequence.value, mulSequence.value, mulSequence.value, constantSequence.value, constantSequence.value]123  unfold complexScale124  rfl125126theorem complexRaySequence.converges_zero (s z : Set)127  requires steps : ConvergesTo(s, realZero)128  requires member : z ∈ ℂ129  shows ComplexConvergesTo(complexRaySequence(s, z), ℂ[0])130proof131  have point := complex.point with *132  have cx := constantSequence.converges at Euclidean.x(z) with *133  have cy := constantSequence.converges at Euclidean.y(z) with *134  have sx := ConvergesTo.mul at s, constantSequence(Euclidean.x(z)), realZero, Euclidean.x(z) with *135  have sy := ConvergesTo.mul at s, constantSequence(Euclidean.y(z)), realZero, Euclidean.y(z) with *136  rw realMulValue.zero_left at sx137  rw realMulValue.zero_left at sy138  unfold complexRaySequence139  unfold complexZero140  exact complexPairSequence.converges with *141142theorem complexLeftMul.continuous_at (z a : Set)143  requires member : z ∈ ℂ144  requires center : a ∈ ℂ145  shows ComplexContinuousAt(complexLeftMul(z), a)146proof147  have function := complexLeftMul.function at z with *148  have ring := complexes.comm_ring149  have ordinary := IsCommRing.ring with ring150  have scalePositive := limitScale.positive at complexNormSquared(z) with *151  unfold ComplexContinuousAt152  refine ⟨function, center, ?_⟩153  intros e eIn positive154  have radiusIn : scaledRadius(e, limitScale(complexNormSquared(z))) ∈ ℝ by typecheck155  have radiusPositive := scaledRadius.positive at e, limitScale(complexNormSquared(z)) with *156  refine ⟨scaledRadius(e, limitScale(complexNormSquared(z))), radiusIn, radiusPositive, ?_⟩157  intros x xIn near158  have negA := IsRing.neg_closed with ordinary, center159  have difference := IsRing.add_closed with ordinary, xIn, negA160  have nonnegative := complexNormSquared.nonnegative at ℂ[x - a] with *161  have control := scaledRadius.product_control with *162  rw [complexLeftMul.value, complexLeftMul.value]163  have distribute : ℂ[z * x - z * a] = ℂ[z * (x - a)] by ring164  rw [distribute, complexNormSquared.mul]165  have commute := realMulValue.commutative at complexNormSquared(z), complexNormSquared(ℂ[x - a]) with *166  rwa commute167168theorem realPow.positive (t : Real) (n : Nat)169  requires positive : realZero < t170  shows realZero < realPow(t, n)171proof172  induction n173  | zero =>174    rw realPow.zero175    exact realZero.lt_one176  | succ(k) using ih =>177    rw realPow.succ178    exact realMulValue.positive with *179180end Complexes181