Grace/Cumulus/Complex/Descent.g17

Open in Workbench Download source

Imports

LocalPolynomial · Real.Power

Declarations

Source

1-- Quantitative descent along a complex direction, without root extraction.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.Descent8import LocalPolynomial9import Real.Power1011def complexScale (t : Real) (z : Euclidean.Point) : Set :=12  (t * Euclidean.x(z), t * Euclidean.y(z))1314section Complexes15notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)16notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)1718theorem complexScale.closed (t : Real) (z : Set)19  requires member : z ∈ ℂ20  shows complexScale(t, z) ∈ ℂ21proof22  have point := complex.point with *23  unfold complexScale24  apply complexCarrier.pair2526theorem complexScale.mul (t : Real) (z : Set)27  requires member : z ∈ ℂ28  shows complexScale(t, z) = ℂ[(t, realZero) * z]29proof30  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases at z with *31  rw shape32  unfold complexScale33  simp [Euclidean.x.pair, Euclidean.y.pair, complexMul.pair]34  have firstCoordinate : R[t * a - 0 * b] = R[t * a] by ring35  have secondCoordinate : R[t * b + 0 * a] = R[t * b] by ring36  rw [firstCoordinate, secondCoordinate]37  rfl3839theorem complexNormSquared.scale (t : Real) (z : Set)40  requires member : z ∈ ℂ41  shows complexNormSquared(complexScale(t, z)) = R[t * t * complexNormSquared(z)]42proof43  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases at z with *44  rw shape45  unfold complexScale46  simp [Euclidean.x.pair, Euclidean.y.pair, complexNormSquared.pair]47  ring4849theorem complexScale.dot_right (t : Real) (z w : Set)50  requires first : z ∈ ℂ51  requires second : w ∈ ℂ52  shows Euclidean.dot(z, complexScale(t, w)) = R[t * Euclidean.dot(z, w)]53proof54  obtain ⟨a, aReal, b, bReal, zShape⟩ := complexCarrier.cases at z with *55  obtain ⟨c, cReal, d, dReal, wShape⟩ := complexCarrier.cases at w with *56  rw [zShape, wShape]57  unfold complexScale58  simp [Euclidean.dot, Euclidean.x.pair, Euclidean.y.pair]59  ring6061theorem complexScale.product (t s : Real) (z w : Set)62  requires first : z ∈ ℂ63  requires second : w ∈ ℂ64  shows ℂ[complexScale(t, z) * complexScale(s, w)] = complexScale(R[t * s], ℂ[z * w])65proof66  obtain ⟨a, aReal, b, bReal, zShape⟩ := complexCarrier.cases at z with *67  obtain ⟨c, cReal, d, dReal, wShape⟩ := complexCarrier.cases at w with *68  rw [zShape, wShape]69  unfold complexScale70  simp [complexMul.pair, Euclidean.x.pair, Euclidean.y.pair]71  have firstCoordinate : R[(t * a) * (s * c) - (t * b) * (s * d)] = R[(t * s) * (a * c - b * d)] by ring72  have secondCoordinate : R[(t * a) * (s * d) + (t * b) * (s * c)] = R[(t * s) * (a * d + b * c)] by ring73  rw [firstCoordinate, secondCoordinate]74  rfl7576theorem complexScale.one (z : Set)77  requires member : z ∈ ℂ78  shows complexScale(realOne, z) = z79proof80  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases at z with *81  rw shape82  unfold complexScale83  simp [Euclidean.x.pair, Euclidean.y.pair, realMulValue.one_left]8485theorem complexScale.mul_right (t : Real) (z w : Set)86  requires first : z ∈ ℂ87  requires second : w ∈ ℂ88  shows ℂ[complexScale(t, z) * w] = complexScale(t, ℂ[z * w])89proof90  have product := complexScale.product at t, realOne, z, w with *91  rwa [complexScale.one, realMulValue.one_right] at product9293theorem complexScale.power (t : Real) (z : Set) (n : Nat)94  requires member : z ∈ ℂ95  shows ℂ[complexScale(t, z) ^ n] = complexScale(realPow(t, n), ℂ[z ^ n])96proof97  induction n98  | zero =>99    rw [monoidPow.zero, monoidPow.zero, realPow.zero]100    unfold complexScale101    unfold complexOne102    simp [Euclidean.x.pair, Euclidean.y.pair, realMulValue.one_left]103  | succ(k) using ih =>104    have ring := complexes.comm_ring105    have ordinary := IsCommRing.ring with ring106    have monoid := IsRing.multiplicative with ordinary107    rw [monoidPow.succ, monoidPow.succ, realPow.succ, ih]108    exact complexScale.product at t, realPow(t, k), z, ℂ[z ^ k] with *109110-- The threshold is explicit: half(-dot(z,w))/(abs(normSquared(w))+1).111theorem complexNormSquared.directional_descent (z w : Set) (t : Real)112  requires first : z ∈ ℂ113  requires second : w ∈ ℂ114  requires direction : Euclidean.dot(z, w) < realZero115  requires positive : realZero < t116  requires small : t < scaledRadius(R[-Euclidean.dot(z, w)], limitScale(complexNormSquared(w)))117  shows complexNormSquared(ℂ[z + complexScale(t, w)]) < complexNormSquared(z)118proof119  have pointZ := complex.point at z with *120  have pointW := complex.point at w with *121  have epsilon := realInv.negative_argument_positive at Euclidean.dot(z, w) with *122  have nonnegative : realZero ≤ t123    exact realLess.implies_le with *124  have control := scaledRadius.product_control with epsilon, nonnegative125  have shifted := realLess.add_left at R[t * complexNormSquared(w)], R[-Euclidean.dot(z, w)], Euclidean.dot(z, w) with *126  have cancel : R[Euclidean.dot(z, w) + -Euclidean.dot(z, w)] = realZero by ring127  rw cancel at shifted128  have combined := realLess.add at Euclidean.dot(z, w), realZero, R[Euclidean.dot(z, w) + t * complexNormSquared(w)], realZero with *129  rw realAddValue.zero_left at combined130  have normalize : R[Euclidean.dot(z, w) + (Euclidean.dot(z, w) + t * complexNormSquared(w))] = R[2 * Euclidean.dot(z, w) + t * complexNormSquared(w)]131    ring132  rw normalize at combined133  have negative : R[2 * Euclidean.dot(z, w) + t * complexNormSquared(w)] < realZero by exact combined134  have multiplied := realLess.mul_left_of_positive at R[2 * Euclidean.dot(z, w) + t * complexNormSquared(w)], realZero, t with *135  rw realMulValue.zero_right at multiplied136  have descent : R[2 * Euclidean.dot(z, complexScale(t, w)) + complexNormSquared(complexScale(t, w))] < realZero137    rw [complexScale.dot_right, complexNormSquared.scale]138    have regroup : R[2 * (t * Euclidean.dot(z, w)) + t * t * complexNormSquared(w)] = R[t * (2 * Euclidean.dot(z, w) + t * complexNormSquared(w))]139      ring140    rwa regroup141  exact complexNormSquared.strict_descent with *142143theorem complexNormSquared.descent_radius (z w : Set)144  requires first : z ∈ ℂ145  requires second : w ∈ ℂ146  requires direction : Euclidean.dot(z, w) < realZero147  shows ∃ d ∈ ℝ, realZero < d ∧148    (∀ t ∈ ℝ, realZero < t → t < d → complexNormSquared(ℂ[z + complexScale(t, w)]) < complexNormSquared(z))149proof150  have pointZ := complex.point at z with *151  have pointW := complex.point at w with *152  have epsilon := realInv.negative_argument_positive with *153  have scalePositive := limitScale.positive at complexNormSquared(w) with *154  have radiusIn : scaledRadius(R[-Euclidean.dot(z, w)], limitScale(complexNormSquared(w))) ∈ ℝ by typecheck155  have radiusPositive := scaledRadius.positive at R[-Euclidean.dot(z, w)], limitScale(complexNormSquared(w)) with *156  refine ⟨scaledRadius(R[-Euclidean.dot(z, w)], limitScale(complexNormSquared(w))), radiusIn, radiusPositive, ?_⟩157  intros t tIn positive small158  exact complexNormSquared.directional_descent with *159160theorem complexNormSquared.descent_step (z w : Set)161  requires first : z ∈ ℂ162  requires second : w ∈ ℂ163  requires direction : Euclidean.dot(z, w) < realZero164  shows ∃ t ∈ ℝ, realZero < t ∧ complexNormSquared(ℂ[z + complexScale(t, w)]) < complexNormSquared(z)165proof166  obtain ⟨d, dIn, positive, decreases⟩ := complexNormSquared.descent_radius at z, w with *167  have halfIn : half(d) ∈ ℝ by typecheck168  have halfPositive := half.positive with *169  have halfLess := half.lt_self with positive170  have smaller := decreases with half(d), halfPositive, halfLess171  refine ⟨half(d), halfIn, halfPositive, smaller⟩172173-- The local normal form restricted to an arbitrary real-scaled direction.174theorem complexPolynomial.ray_normal_form (c a : Set) (cs : List(ℂ))175  requires coefficient : c ∈ ℂ176  requires center : a ∈ ℂ177  shows ∃ n ∈ ℕ, ∃ ds, List(ℂ, ds) ∧ complexPolynomial(ds)(ℂ[0]) ≠ ℂ[0] ∧178    length{ℂ}(cs) = Grace.Core.Nat.Rec.add(n, length{ℂ}(ds)) ∧179    ComplexContinuous(complexPolynomial(ds)) ∧180    (∀ u ∈ ℂ, ∀ t ∈ ℝ, complexPolynomial(c :: cs)(ℂ[a + complexScale(t, u)]) = ℂ[complexPolynomial(c :: cs)(a) + complexScale(realPow(t, succ(n)), ℂ[u ^ succ(n) * complexPolynomial(ds)(complexScale(t, u))])])181proof182  obtain ⟨n, nIn, ds, dsList, nonzero, degree, continuous, expansion⟩ := complexPolynomial.local_normal_form at c, a, cs with *183  refine ⟨n, nIn, ds, dsList, nonzero, degree, continuous, ?_⟩184  intros u uIn t tIn185  have nNat := nat.omega.backward at n with *186  have ring := complexes.comm_ring187  have ordinary := IsCommRing.ring with ring188  have monoid := IsRing.multiplicative with ordinary189  have scaled := complexScale.closed at t, u with *190  have power := monoidPow.closed at ℂ, complexMul, complexOne, u, succ(n) with *191  have function := complexPolynomial.function at ds with *192  have value := FunctionBetween.apply_closed at complexPolynomial(ds), ℂ, ℂ, complexScale(t, u) with *193  have equation := expansion with complexScale(t, u)194  rw [equation, complexScale.power, complexScale.mul_right]195  rfl196197end Complexes198