Grace/Cumulus/Complex/Compactness.g17

Open in Workbench Download source

Imports

PolynomialGrowth · Real.Analysis.SequentialCompactness

Declarations

Source

1-- Closed complex disks: coordinate extraction and passage to the limit (ZF).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.Compactness8import PolynomialGrowth9import Real.Analysis.SequentialCompactness1011theorem StrictlyIncreasingNat.comp (k l : Set)12  requires first : StrictlyIncreasingNat(k)13  requires second : StrictlyIncreasingNat(l)14  shows StrictlyIncreasingNat(compose(k, l, ℕ, ℕ, ℕ))15proof16  have kFunction := StrictlyIncreasingNat.function at k with *17  have lFunction := StrictlyIncreasingNat.function at l with *18  have function := compose.function at k, l, ℕ, ℕ, ℕ with *19  rcases first with ⟨kf, kStrict⟩20  rcases second with ⟨lf, lStrict⟩21  refine ⟨function, ?_⟩22  intros m mIn n nIn before23  have lm := FunctionBetween.apply_closed at l, ℕ, ℕ, m with *24  have ln := FunctionBetween.apply_closed at l, ℕ, ℕ, n with *25  have step := lStrict with m, mIn, n, nIn, before26  have result := kStrict with l(m), lm, l(n), ln, step27  rwa [compose.apply, compose.apply]2829theorem subsequence.comp (u k l : Set)30  requires sequence : RealSequence(u)31  requires first : StrictlyIncreasingNat(k)32  requires second : StrictlyIncreasingNat(l)33  shows subsequence(subsequence(u, k), l) = subsequence(u, compose(k, l, ℕ, ℕ, ℕ))34proof35  have selected := subsequence.sequence at u, k with *36  have composite := StrictlyIncreasingNat.comp at k, l with *37  have left := subsequence.function at subsequence(u, k), l with *38  have right := subsequence.function at u, compose(k, l, ℕ, ℕ, ℕ) with *39  apply FunctionBetween.ext with left, right40  intros n nIn41  have nNat := nat.omega.backward at n with *42  have kFunction := StrictlyIncreasingNat.function at k with *43  have lFunction := StrictlyIncreasingNat.function at l with *44  have ln := FunctionBetween.apply_closed at l, ℕ, ℕ, n with *45  have lnNat := nat.omega.backward at l(n) with *46  have outer := subsequence.value at subsequence(u, k), l, n with *47  have inner := subsequence.value at u, k, l(n) with *48  have flat := subsequence.value at u, compose(k, l, ℕ, ℕ, ℕ), n with *49  have index := compose.apply at k, l, ℕ, ℕ, ℕ, n with *50  rw [outer, inner, flat, index]51  rfl5253-- Two extractions give one selector for both coordinates.54theorem closedRectangle.bolzano_weierstrass (u v : Set) (a b c d : Real)55  requires horizontal : RealSequence(u)56  requires vertical : RealSequence(v)57  requires horizontalBounds : TermsIn(u, closedInterval(a, b))58  requires verticalBounds : TermsIn(v, closedInterval(c, d))59  shows ∃ k, StrictlyIncreasingNat(k) ∧60    ∃ x ∈ ℝ, ∃ y ∈ ℝ,61      x ∈ closedInterval(a, b) ∧ y ∈ closedInterval(c, d) ∧62      ConvergesTo(subsequence(u, k), x) ∧ ConvergesTo(subsequence(v, k), y)63proof64  obtain ⟨k, kIncreasing, x, xIn, xBounds, xLimit⟩ := closedInterval.bolzano_weierstrass at u, a, b with *65  have selectedV := subsequence.sequence at v, k with *66  have selectedBounds := TermsIn.subsequence at v, k, closedInterval(c, d) with *67  obtain ⟨l, lIncreasing, y, yIn, yBounds, yLimit⟩ := closedInterval.bolzano_weierstrass at subsequence(v, k), c, d with *68  have preserved := ConvergesTo.subsequence at subsequence(u, k), l, x with *69  have increasing := StrictlyIncreasingNat.comp at k, l with *70  have uFlat := subsequence.comp at u, k, l with *71  have vFlat := subsequence.comp at v, k, l with *72  rw uFlat at preserved73  rw vFlat at yLimit74  refine ⟨compose(k, l, ℕ, ℕ, ℕ), increasing, x, xIn, y, yIn, xBounds, yBounds, preserved, yLimit⟩7576-- A coarse coordinate bound avoids square roots entirely.77theorem realLe.self_le_square_add_one (a : Real)78  shows a ≤ a * a + 179proof80  have squareNonnegative := realMulValue.square_nonnegative at a with *81  have unitNonnegative := realLess.implies_le with realZero.lt_one82  have bounds := realLe.nonnegative_sum_bounds at a * a, realOne with *83  have comparison : a ≤ realOne ∨ ¬(a ≤ realOne) by tauto84  cases comparison with small | large85  . exact realLe.transitive at a, realOne, a * a + 1 with *86  . have strict := realLess.of_not_le at a, realOne with *87    have above := realLess.implies_le at realOne, a with *88    have nonnegative := realLe.transitive at realZero, realOne, a with *89    have multiplied := realLe.mul_right_of_nonnegative at realOne, a, a with *90    rw realMulValue.one_left at multiplied91    exact realLe.transitive at a, a * a, a * a + 1 with *9293theorem realSquare.coordinate_bounds (a radius : Real)94  requires squareBound : a * a ≤ radius95  shows -(radius + 1) ≤ a ∧ a ≤ radius + 196proof97  have upper := realLe.self_le_square_add_one at a with *98  have shifted := realLe.add_right at a * a, radius, realOne with *99  have positiveBound := realLe.transitive at a, a * a + 1, radius + 1 with *100  have negativeUpper := realLe.self_le_square_add_one at -a with *101  have negativeSquare : (-a) * (-a) = a * a by ring102  rw negativeSquare at negativeUpper103  have negativeBound := realLe.transitive at -a, a * a + 1, radius + 1 with *104  have lower := realLe.neg_reverse at -a, radius + 1 with *105  rw realNegValue.involutive at lower106  refine ⟨lower, positiveBound⟩107108theorem complexNormSquared.coordinate_bounds (z : Set) (radius : Real)109  requires member : z ∈ complexCarrier110  requires bound : complexNormSquared(z) ≤ radius111  shows Euclidean.x(z) ∈ closedInterval(-(radius + 1), radius + 1) ∧112    Euclidean.y(z) ∈ closedInterval(-(radius + 1), radius + 1)113proof114  have point := complex.point with member115  have coordinates := Euclidean.coordinates at z with *116  have norm : complexNormSquared(z) = Euclidean.x(z) * Euclidean.x(z) + Euclidean.y(z) * Euclidean.y(z)117    unfold complexNormSquared118    unfold Euclidean.normSquared119    unfold Euclidean.dot120    rfl121  have xNonnegative := realMulValue.square_nonnegative at Euclidean.x(z) with *122  have yNonnegative := realMulValue.square_nonnegative at Euclidean.y(z) with *123  have sums := realLe.nonnegative_sum_bounds at Euclidean.x(z) * Euclidean.x(z), Euclidean.y(z) * Euclidean.y(z) with *124  rw norm at bound125  have xBound := realLe.transitive at Euclidean.x(z) * Euclidean.x(z), Euclidean.x(z) * Euclidean.x(z) + Euclidean.y(z) * Euclidean.y(z), radius with *126  have yBound := realLe.transitive at Euclidean.y(z) * Euclidean.y(z), Euclidean.x(z) * Euclidean.x(z) + Euclidean.y(z) * Euclidean.y(z), radius with *127  have xInterval := realSquare.coordinate_bounds at Euclidean.x(z), radius with *128  have yInterval := realSquare.coordinate_bounds at Euclidean.y(z), radius with *129  have xIn : Euclidean.x(z) ∈ ℝ by typecheck130  have yIn : Euclidean.y(z) ∈ ℝ by typecheck131  have lowerReal : Real(-(radius + 1)) by typecheck132  have upperReal : Real(radius + 1) by typecheck133  constructor134  . apply closedInterval.membership.backward at135    -(radius + 1), radius + 1, Euclidean.x(z)136    refine ⟨xIn, xInterval.left, xInterval.right⟩137  . apply closedInterval.membership.backward at138    -(radius + 1), radius + 1, Euclidean.y(z)139    refine ⟨yIn, yInterval.left, yInterval.right⟩140141-- Complex sequences use the same set-theoretic function graphs as real ones.142predicate ComplexSequence (u : Set) := FunctionBetween(u, ℕ, complexCarrier)143144defgraph complexSequenceX (u : Set) (n ∈ ℕ) : ℝ := Euclidean.x(u(n))145requires sequence : ComplexSequence(u)146proof147  have function : u : ℕ → complexCarrier148    unfold ComplexSequence at sequence149    exact sequence150  have value := FunctionBetween.apply_closed at u, ℕ, complexCarrier, n with *151  have point := complex.point with value152  have real := Euclidean.x.real at u(n) with *153  typecheck154155defgraph complexSequenceY (u : Set) (n ∈ ℕ) : ℝ := Euclidean.y(u(n))156requires sequence : ComplexSequence(u)157proof158  have function : u : ℕ → complexCarrier159    unfold ComplexSequence at sequence160    exact sequence161  have value := FunctionBetween.apply_closed at u, ℕ, complexCarrier, n with *162  have point := complex.point with value163  have real := Euclidean.y.real at u(n) with *164  typecheck165166predicate ComplexConvergesTo (u a : Set) :=167  ComplexSequence(u) ∧ a ∈ complexCarrier ∧168    ConvergesTo(complexSequenceX(u), Euclidean.x(a)) ∧169    ConvergesTo(complexSequenceY(u), Euclidean.y(a))170171def complexSubsequence (u k : Set) : Set := compose(u, k, ℕ, ℕ, complexCarrier)172173def closedComplexDisk (radius : Real) : Set :=174  { z ∈ complexCarrier | complexNormSquared(z) ≤ radius }175176theorem complexSequenceX.sequence (u : Set)177  requires sequence : ComplexSequence(u)178  shows RealSequence(complexSequenceX(u))179proof180  unfold RealSequence181  exact complexSequenceX.function with *182183theorem complexSequenceY.sequence (u : Set)184  requires sequence : ComplexSequence(u)185  shows RealSequence(complexSequenceY(u))186proof187  unfold RealSequence188  exact complexSequenceY.function with *189190theorem complexSubsequence.sequence (u k : Set)191  requires sequence : ComplexSequence(u)192  requires increasing : StrictlyIncreasingNat(k)193  shows ComplexSequence(complexSubsequence(u, k))194proof195  have selector := StrictlyIncreasingNat.function with increasing196  have function : u : ℕ → complexCarrier by exact sequence197  unfold ComplexSequence198  unfold complexSubsequence199  exact compose.function with *200201theorem complexSubsequence.value (u k : Set) (n : Nat)202  requires sequence : ComplexSequence(u)203  requires increasing : StrictlyIncreasingNat(k)204  shows complexSubsequence(u, k)(n) = u(k(n))205proof206  have selector := StrictlyIncreasingNat.function with increasing207  have function : u : ℕ → complexCarrier by exact sequence208  unfold complexSubsequence209  exact compose.apply with *210211theorem complexSequenceX.subsequence (u k : Set)212  requires sequence : ComplexSequence(u)213  requires increasing : StrictlyIncreasingNat(k)214  shows complexSequenceX(complexSubsequence(u, k)) = subsequence(complexSequenceX(u), k)215proof216  have selected := complexSubsequence.sequence with *217  have horizontal := complexSequenceX.sequence at u with *218  have left := complexSequenceX.function at complexSubsequence(u, k) with *219  have right := subsequence.function with *220  apply FunctionBetween.ext with left, right221  intros n member222  have natural := nat.omega.backward at n with *223  have selector := StrictlyIncreasingNat.function with increasing224  have kn := FunctionBetween.apply_closed at k, ℕ, ℕ, n with *225  have knNat := nat.omega.backward at k(n) with *226  rw [complexSequenceX.value, complexSubsequence.value, subsequence.value, complexSequenceX.value]227  rfl228229theorem complexSequenceY.subsequence (u k : Set)230  requires sequence : ComplexSequence(u)231  requires increasing : StrictlyIncreasingNat(k)232  shows complexSequenceY(complexSubsequence(u, k)) = subsequence(complexSequenceY(u), k)233proof234  have selected := complexSubsequence.sequence with *235  have vertical := complexSequenceY.sequence at u with *236  have left := complexSequenceY.function at complexSubsequence(u, k) with *237  have right := subsequence.function with *238  apply FunctionBetween.ext with left, right239  intros n member240  have natural := nat.omega.backward at n with *241  have selector := StrictlyIncreasingNat.function with increasing242  have kn := FunctionBetween.apply_closed at k, ℕ, ℕ, n with *243  have knNat := nat.omega.backward at k(n) with *244  rw [complexSequenceY.value, complexSubsequence.value, subsequence.value, complexSequenceY.value]245  rfl246247theorem ComplexSequence.disk_coordinate_bounds (u : Set) (radius : Real)248  requires sequence : ComplexSequence(u)249  requires terms : TermsIn(u, closedComplexDisk(radius))250  shows TermsIn(complexSequenceX(u), closedInterval(-(radius + 1), radius + 1)) ∧251    TermsIn(complexSequenceY(u), closedInterval(-(radius + 1), radius + 1))252proof253  have coordinates : ∀ n ∈ ℕ,254      complexSequenceX(u)(n) ∈ closedInterval(-(radius + 1), radius + 1) ∧255      complexSequenceY(u)(n) ∈ closedInterval(-(radius + 1), radius + 1)256    intros n member257    have natural := nat.omega.backward at n with *258    have term := terms with n, member259    have disk := closedComplexDisk.membership.forward with term260    have bounds := complexNormSquared.coordinate_bounds at u(n), radius with *261    rwa [complexSequenceX.value, complexSequenceY.value]262  constructor263    intros n member264    have both := coordinates with n, member265    exact both.left266    intros n member267    have both := coordinates with n, member268    exact both.right269270-- A polynomial inequality defining the disk is preserved by coordinate limits.271theorem ConvergesTo.sum_squares_le (u v : Set) (a b radius : Real)272  requires horizontal : ConvergesTo(u, a)273  requires vertical : ConvergesTo(v, b)274  requires bounds : ∀ n ∈ ℕ, (u(n):R) * u(n) + (v(n):R) * v(n) ≤ radius275  shows a * a + b * b ≤ radius276proof277  have uSequence := ConvergesTo.sequence at u, a with *278  have vSequence := ConvergesTo.sequence at v, b with *279  have uSquare := ConvergesTo.mul at u, u, a, a with *280  have vSquare := ConvergesTo.mul at v, v, b, b with *281  have sum := ConvergesTo.add at mulSequence(u, u), mulSequence(v, v), a * a, b * b with *282  have uSquareSequence := mulSequence.sequence at u, u with *283  have vSquareSequence := mulSequence.sequence at v, v with *284  have bounded : BoundedAboveBy(addSequence(mulSequence(u, u), mulSequence(v, v)), radius)285    intros n member286    have natural := nat.omega.backward at n with *287    have uReal := RealSequence.value at u, n with *288    have vReal := RealSequence.value at v, n with *289    have uSquareReal := RealSequence.value at mulSequence(u, u), n with *290    have vSquareReal := RealSequence.value at mulSequence(v, v), n with *291    rw [addSequence.value, mulSequence.value, mulSequence.value]292    have bound := bounds with n, member293    exact realLe.characterization.forward with bound294  exact ConvergesTo.le_constant with *295296theorem closedComplexDisk.contains_limit (u a : Set) (radius : Real)297  requires converges : ComplexConvergesTo(u, a)298  requires terms : TermsIn(u, closedComplexDisk(radius))299  shows a ∈ closedComplexDisk(radius)300proof301  rcases converges with ⟨sequence, member, horizontal, vertical⟩302  have point := complex.point with member303  have bounds : ∀ n ∈ ℕ,304      (complexSequenceX(u)(n):R) * complexSequenceX(u)(n) + (complexSequenceY(u)(n):R) * complexSequenceY(u)(n) ≤ radius305    intros n nIn306    have natural := nat.omega.backward at n with *307    have term := terms with n, nIn308    have disk := closedComplexDisk.membership.forward with term309    have bound := disk.right310    rw [complexSequenceX.value, complexSequenceY.value]311    unfold complexNormSquared at bound312    unfold Euclidean.normSquared at bound313    unfold Euclidean.dot at bound314    exact bound315  have limit := ConvergesTo.sum_squares_le with horizontal, vertical, bounds316  apply closedComplexDisk.membership.backward317  constructor318  . exact member319  . unfold complexNormSquared320    unfold Euclidean.normSquared321    unfold Euclidean.dot322    exact limit323324theorem TermsIn.complex_subsequence (u k S : Set)325  requires sequence : ComplexSequence(u)326  requires increasing : StrictlyIncreasingNat(k)327  requires terms : TermsIn(u, S)328  shows TermsIn(complexSubsequence(u, k), S)329proof330  intros n member331  have natural := nat.omega.backward at n with *332  have selector := StrictlyIncreasingNat.function with increasing333  have kn := FunctionBetween.apply_closed with *334  rw complexSubsequence.value335  exact terms with k(n), kn336337-- Every sequence in a closed disk has a subsequence converging inside that disk.338-- The radius need not be nonnegative: the empty-disk case is vacuous.339theorem closedComplexDisk.bolzano_weierstrass (u : Set) (radius : Real)340  requires sequence : ComplexSequence(u)341  requires terms : TermsIn(u, closedComplexDisk(radius))342  shows ∃ k, StrictlyIncreasingNat(k) ∧ ∃ a ∈ closedComplexDisk(radius),343    ComplexConvergesTo(complexSubsequence(u, k), a)344proof345  have horizontal := complexSequenceX.sequence at u with *346  have vertical := complexSequenceY.sequence at u with *347  have bounds := ComplexSequence.disk_coordinate_bounds at u, radius with *348  obtain ⟨k, increasing, x, xIn, y, yIn, xBounds, yBounds, xLimit, yLimit⟩ := closedRectangle.bolzano_weierstrass at complexSequenceX(u), complexSequenceY(u), -(radius + 1), radius + 1, -(radius + 1), radius + 1 with *349  have pair := complexCarrier.pair at x, y with *350  have selected := complexSubsequence.sequence at u, k with *351  have horizontalSelected := complexSequenceX.subsequence at u, k with *352  have verticalSelected := complexSequenceY.subsequence at u, k with *353  have converges : ComplexConvergesTo(complexSubsequence(u, k), (x, y))354    unfold ComplexConvergesTo355    refine ⟨selected, pair, ?_⟩356    constructor357    . rw [horizontalSelected, Euclidean.x.pair]358      exact xLimit359    . rw [verticalSelected, Euclidean.y.pair]360      exact yLimit361  have selectedTerms := TermsIn.complex_subsequence at u, k, closedComplexDisk(radius) with *362  have member := closedComplexDisk.contains_limit at complexSubsequence(u, k), (x, y), radius with *363  refine ⟨k, increasing, (x, y), member, converges⟩364365predicate ComplexSequentiallyCompact (S : Set) :=366  S ⊆ complexCarrier ∧367    (∀ u, ComplexSequence(u) → TermsIn(u, S) →368      ∃ k, StrictlyIncreasingNat(k) ∧ ∃ a ∈ S,369        ComplexConvergesTo(complexSubsequence(u, k), a))370371theorem closedComplexDisk.sequentially_compact (radius : Real)372  shows ComplexSequentiallyCompact(closedComplexDisk(radius))373proof374  constructor375    intros z member376    have disk := closedComplexDisk.membership.forward with member377    exact disk.left378  . intros u sequence terms379    exact closedComplexDisk.bolzano_weierstrass with *380381defgraph complexNormSequence (u : Set) (n ∈ ℕ) : ℝ := complexNormSquared(u(n))382requires sequence : ComplexSequence(u)383proof384  have function : u : ℕ → complexCarrier by exact sequence385  have value := FunctionBetween.apply_closed with *386  typecheck387388theorem complexNormSequence.coordinates (u : Set)389  requires sequence : ComplexSequence(u)390  shows complexNormSequence(u) = addSequence(391    mulSequence(complexSequenceX(u), complexSequenceX(u)),392    mulSequence(complexSequenceY(u), complexSequenceY(u)))393proof394  have horizontal := complexSequenceX.sequence with *395  have vertical := complexSequenceY.sequence with *396  have xx := mulSequence.sequence at complexSequenceX(u), complexSequenceX(u) with *397  have yy := mulSequence.sequence at complexSequenceY(u), complexSequenceY(u) with *398  have sum := addSequence.sequence at mulSequence(complexSequenceX(u), complexSequenceX(u)), mulSequence(complexSequenceY(u), complexSequenceY(u)) with *399  have left := complexNormSequence.function at u with *400  have right : addSequence(mulSequence(complexSequenceX(u), complexSequenceX(u)), mulSequence(complexSequenceY(u), complexSequenceY(u))) : ℕ → ℝ401    exact sum402  apply FunctionBetween.ext with left, right403  intros n member404  have natural := nat.omega.backward at n with *405  have xReal := RealSequence.value at complexSequenceX(u), n with *406  have yReal := RealSequence.value at complexSequenceY(u), n with *407  have xxReal := RealSequence.value at mulSequence(complexSequenceX(u), complexSequenceX(u)), n with *408  have yyReal := RealSequence.value at mulSequence(complexSequenceY(u), complexSequenceY(u)), n with *409  rw [complexNormSequence.value, addSequence.value, mulSequence.value, mulSequence.value, complexSequenceX.value, complexSequenceY.value]410  unfold complexNormSquared411  unfold Euclidean.normSquared412  unfold Euclidean.dot413  rfl414415theorem ComplexConvergesTo.norm_squared (u a : Set)416  requires converges : ComplexConvergesTo(u, a)417  shows ConvergesTo(complexNormSequence(u), complexNormSquared(a))418proof419  rcases converges with ⟨sequence, member, horizontal, vertical⟩420  have point := complex.point with member421  have xx := ConvergesTo.mul at complexSequenceX(u), complexSequenceX(u), Euclidean.x(a), Euclidean.x(a) with *422  have yy := ConvergesTo.mul at complexSequenceY(u), complexSequenceY(u), Euclidean.y(a), Euclidean.y(a) with *423  have sum := ConvergesTo.add at mulSequence(complexSequenceX(u), complexSequenceX(u)), mulSequence(complexSequenceY(u), complexSequenceY(u)), Euclidean.x(a) * Euclidean.x(a), Euclidean.y(a) * Euclidean.y(a) with *424  rw complexNormSequence.coordinates425  unfold complexNormSquared426  unfold Euclidean.normSquared427  unfold Euclidean.dot428  exact sum429