Grace/Cumulus/Complex/Continuity.g17

Open in Workbench Download source

Imports

PolynomialBounds · Real.Analysis.Continuity

Declarations

Source

1-- Squared-modulus epsilon/delta continuity over the concrete complex field.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.Continuity8import PolynomialBounds9import Real.Analysis.Continuity1011-- Positive thresholds for squared distances describe the usual complex topology.12predicate ComplexContinuousAt (f a : Set) :=13  FunctionBetween(f, complexCarrier, complexCarrier) ∧ a ∈ complexCarrier ∧14  (∀ e ∈ ℝ, realZero < e → ∃ d ∈ ℝ, realZero < d ∧15    (∀ x ∈ complexCarrier,16      complexNormSquared(complexAdd(x, complexNeg(a))) < d →17      complexNormSquared(complexAdd(f(x), complexNeg(f(a)))) < e))1819predicate ComplexContinuous (f : Set) :=20  FunctionBetween(f, complexCarrier, complexCarrier) ∧21  (∀ a ∈ complexCarrier, ComplexContinuousAt(f, a))2223-- A bounded nonnegative factor can be absorbed into an explicit epsilon radius.24theorem scaledRadius.product_control (e b t : Real)25  requires epsilon : 0 < e26  requires nonnegative : 0 ≤ t27  requires small : t < scaledRadius(e, limitScale(b))28  shows t * b < e29proof30  have scalePositive := limitScale.positive at b with *31  have upper := abs.upper at b with *32  have larger := abs.lt_limitScale at b with *33  have bLess := realLe.transitive_less at b, abs(b), limitScale(b) with *34  have bLe := realLess.implies_le at b, limitScale(b) with *35  have comparison := realLe.mul_left_of_nonnegative at b, limitScale(b), t with *36  have multiplied := realLess.mul_right_of_positive at t, scaledRadius(e, limitScale(b)), limitScale(b) with *37  have commuted := realMulValue.commutative at scaledRadius(e, limitScale(b)), limitScale(b) with *38  have cancel := scaledRadius.cancel at e, limitScale(b) with *39  rw [commuted, cancel] at multiplied40  have halfLess := half.lt_self at e with *41  have belowHalf := realLe.transitive_less at t * b, t * limitScale(b), half(e) with *42  exact realLess.transitive with *4344def complexNeighborhoodRadius (a : Euclidean.Point) : Real :=45  (2:R) * (complexNormSquared(a) + realOne)4647theorem complexNeighborhoodRadius.nonnegative (a : Set)48  requires center : a ∈ complexCarrier49  shows realZero ≤ complexNeighborhoodRadius(a)50proof51  have point := complex.point with center52  have normNonnegative := complexNormSquared.nonnegative with center53  have oneNonnegative := realLess.implies_le with realZero.real, realOne.real, realZero.lt_one54  unfold complexNeighborhoodRadius55  exact realLe.two_sum_nonnegative with *5657section Complexes58notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)59notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)6061theorem complexNormSquared.difference_distance (z w : Set)62  requires first : z ∈ ℂ63  requires second : w ∈ ℂ64  shows complexNormSquared(ℂ[z - w]) = Euclidean.distanceSquared(z, w)65proof66  obtain ⟨a, aReal, b, bReal, zPair⟩ := complexCarrier.cases at z with *67  obtain ⟨c, cReal, d, dReal, wPair⟩ := complexCarrier.cases at w with *68  have firstPoint := Euclidean.pair.point at a, b with *69  have secondPoint := Euclidean.pair.point at c, d with *70  rw [zPair, wPair]71  simp [complexAdd.pair, complexNeg.pair, complexNormSquared.pair, Euclidean.distanceSquared.coordinates, Euclidean.x.pair, Euclidean.y.pair]72  ring7374theorem complexNormSquared.nearby_disk (a x : Set)75  requires center : a ∈ ℂ76  requires element : x ∈ ℂ77  requires near : complexNormSquared(ℂ[x - a]) < R[1]78  shows complexNormSquared(x) ≤ complexNeighborhoodRadius(a)79proof80  have field := complexes.is_field81  have ring := IsField.comm_ring with field82  have ordinary := IsCommRing.ring with ring83  have negated := IsRing.neg_closed with ordinary, center84  have displacement := IsRing.add_closed with ordinary, element, negated85  have bound := realLess.implies_le with *86  have addition := complexNormSquared.add_bound at a, ℂ[x - a] with *87  have sum : ℂ[a + (x - a)] = x by ring88  rw sum at addition89  have translated := realLe.add_left at complexNormSquared(ℂ[x - a]), realOne, complexNormSquared(a) with *90  have doubled := realLe.double_bound with bound91  unfold complexNeighborhoodRadius92  exact realLe.transitive with *9394theorem complexPolynomial.cons_continuous_at (a c : Set) (cs : List(complexCarrier))95  requires center : a ∈ ℂ96  requires coefficient : c ∈ ℂ97  shows ComplexContinuousAt(complexPolynomial(c :: cs), a)98proof99  have function := complexPolynomial.function at c :: cs with *100  have point := complex.point with center101  have radiusNonnegative := complexNeighborhoodRadius.nonnegative with center102  obtain ⟨b, bIn, bNonnegative, estimate⟩ := complexPolynomial.difference_bound_on_disk at a, c, complexNeighborhoodRadius(a), cs with *103  unfold ComplexContinuousAt104  refine ⟨function, center, ?_⟩105  intros e eIn epsilon106  have scalePositive := limitScale.positive at b with *107  have scaledPositive := scaledRadius.positive at e, limitScale(b) with *108  have unitPositive := realZero.lt_one109  obtain ⟨d, dIn, dPositive, dUnit, dScaled⟩ := positiveRadius.common at realOne, scaledRadius(e, limitScale(b)) with *110  refine ⟨d, dIn, dPositive, ?_⟩111  intros x member close112  have field := complexes.is_field113  have ring := IsField.comm_ring with field114  have ordinary := IsCommRing.ring with ring115  have negated := IsRing.neg_closed with ordinary, center116  have displacement := IsRing.add_closed with ordinary, member, negated117  have displacementNonnegative := complexNormSquared.nonnegative with displacement118  have near := realLess.transitive_le at complexNormSquared(ℂ[x - a]), d, realOne with *119  have inside := complexNormSquared.nearby_disk with *120  have bound := estimate with x, member, inside121  have small := realLess.transitive_le at complexNormSquared(ℂ[x - a]), d, scaledRadius(e, limitScale(b)) with *122  have controlled := scaledRadius.product_control with epsilon, small123  have imageX := FunctionBetween.apply_closed at complexPolynomial(c :: cs), complexCarrier, complexCarrier, x with *124  have imageA := FunctionBetween.apply_closed at complexPolynomial(c :: cs), complexCarrier, complexCarrier, a with *125  have negImage := IsRing.neg_closed with ordinary, imageA126  have imageDifference := IsRing.add_closed with ordinary, imageX, negImage127  exact realLe.transitive_less with *128129theorem complexFunction.constant_continuous_at (f a z : Set)130  requires function : f : ℂ → ℂ131  requires center : a ∈ ℂ132  requires value : z ∈ ℂ133  requires constant : ∀ x ∈ ℂ, f(x) = z134  shows ComplexContinuousAt(f, a)135proof136  unfold ComplexContinuousAt137  refine ⟨function, center, ?_⟩138  intros e eIn epsilon139  have unitIn : realOne ∈ ℝ by typecheck140  refine ⟨realOne, unitIn, realZero.lt_one, ?_⟩141  intros x member close142  have xValue := constant with x, member143  have aValue := constant with a, center144  rw [xValue, aValue]145  have field := complexes.is_field146  have ring := IsField.comm_ring with field147  have cancel : ℂ[z - z] = ℂ[0] by ring148  rwa [cancel, complexNormSquared.zero]149150theorem complexPolynomial.continuous_at (a : Set) (cs : List(complexCarrier))151  requires center : a ∈ ℂ152  shows ComplexContinuousAt(complexPolynomial(cs), a)153proof154  have shape := List.cases with *155  cases shape with emptyShape | nonemptyShape156  . rw emptyShape157    have empty : List(complexCarrier, []) by typecheck158    have function := complexPolynomial.function at [] with *159    have field := complexes.is_field160    have ring := IsField.comm_ring with field161    have unit : ℂ[1] ∈ ℂ by typecheck162    have constant : ∀ x ∈ ℂ, complexPolynomial([])(x) = ℂ[1]163      intros x member164      rw [complexPolynomial.value, monicValue]165      rfl166    exact complexFunction.constant_continuous_at with *167  . obtain ⟨c, coefficient, tail, list, consShape⟩ := nonemptyShape168    rw consShape169    exact complexPolynomial.cons_continuous_at with *170171theorem complexPolynomial.continuous (cs : List(complexCarrier))172  shows ComplexContinuous(complexPolynomial(cs))173proof174  have function := complexPolynomial.function at cs with *175  unfold ComplexContinuous176  refine ⟨function, ?_⟩177  intros a center178  exact complexPolynomial.continuous_at with *179180end Complexes181