Grace/Cumulus/Complex/MinimumDirection.g17

Open in Workbench Download source

Imports

Descent

Declarations

Source

1-- Passage to the leading direction at a squared-norm minimum.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.MinimumDirection8import Descent910def complexDotSequence (z u : Set) : Set := addSequence(11  mulSequence(constantSequence(Euclidean.x(z)), complexSequenceX(u)),12  mulSequence(constantSequence(Euclidean.y(z)), complexSequenceY(u)))1314def normalizedNormSequence (z s u : Set) : Set := addSequence(15  mulSequence(constantSequence((2:R)), complexDotSequence(z, u)),16  mulSequence(s, complexNormSequence(u)))1718section Complexes19notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)20notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)2122theorem complexDotSequence.sequence (z u : Set)23  requires member : z ∈ ℂ24  requires sequence : ComplexSequence(u)25  shows RealSequence(complexDotSequence(z, u))26proof27  have point := complex.point with *28  have cx := constantSequence.sequence at Euclidean.x(z) with *29  have cy := constantSequence.sequence at Euclidean.y(z) with *30  have ux := complexSequenceX.sequence with *31  have uy := complexSequenceY.sequence with *32  have xx := mulSequence.sequence at constantSequence(Euclidean.x(z)), complexSequenceX(u) with *33  have yy := mulSequence.sequence at constantSequence(Euclidean.y(z)), complexSequenceY(u) with *34  unfold complexDotSequence35  exact addSequence.sequence with *3637theorem complexDotSequence.value (z u : Set) (n : Nat)38  requires member : z ∈ ℂ39  requires sequence : ComplexSequence(u)40  shows complexDotSequence(z, u)(n) = Euclidean.dot(z, u(n))41proof42  have point := complex.point with *43  have cx := constantSequence.sequence at Euclidean.x(z) with *44  have cy := constantSequence.sequence at Euclidean.y(z) with *45  have ux := complexSequenceX.sequence with *46  have uy := complexSequenceY.sequence with *47  have xx := mulSequence.sequence at constantSequence(Euclidean.x(z)), complexSequenceX(u) with *48  have yy := mulSequence.sequence at constantSequence(Euclidean.y(z)), complexSequenceY(u) with *49  have cxn := RealSequence.value at constantSequence(Euclidean.x(z)), n with *50  have cyn := RealSequence.value at constantSequence(Euclidean.y(z)), n with *51  have uxn := RealSequence.value at complexSequenceX(u), n with *52  have uyn := RealSequence.value at complexSequenceY(u), n with *53  have xxn := RealSequence.value at mulSequence(constantSequence(Euclidean.x(z)), complexSequenceX(u)), n with *54  have yyn := RealSequence.value at mulSequence(constantSequence(Euclidean.y(z)), complexSequenceY(u)), n with *55  unfold complexDotSequence56  rw [addSequence.value, mulSequence.value, mulSequence.value, constantSequence.value, constantSequence.value, complexSequenceX.value, complexSequenceY.value]57  unfold Euclidean.dot58  rfl5960theorem ComplexConvergesTo.dot (z u a : Set)61  requires member : z ∈ ℂ62  requires converges : ComplexConvergesTo(u, a)63  shows ConvergesTo(complexDotSequence(z, u), Euclidean.dot(z, a))64proof65  obtain ⟨sequence, center, horizontal, vertical⟩ := converges66  have pointZ := complex.point at z with *67  have pointA := complex.point at a with *68  have cx := constantSequence.converges at Euclidean.x(z) with *69  have cy := constantSequence.converges at Euclidean.y(z) with *70  have xx := ConvergesTo.mul at constantSequence(Euclidean.x(z)), complexSequenceX(u), Euclidean.x(z), Euclidean.x(a) with *71  have yy := ConvergesTo.mul at constantSequence(Euclidean.y(z)), complexSequenceY(u), Euclidean.y(z), Euclidean.y(a) with *72  have sum := ConvergesTo.add at mulSequence(constantSequence(Euclidean.x(z)), complexSequenceX(u)), mulSequence(constantSequence(Euclidean.y(z)), complexSequenceY(u)), R[Euclidean.x(z) * Euclidean.x(a)], R[Euclidean.y(z) * Euclidean.y(a)] with *73  unfold complexDotSequence74  unfold Euclidean.dot75  exact sum7677-- Cancel a positive step from the exact squared-norm expansion.78theorem complexNormSquared.minimum_step (z w : Set) (t : Real)79  requires first : z ∈ ℂ80  requires second : w ∈ ℂ81  requires positive : realZero < t82  requires minimum : complexNormSquared(z) ≤ complexNormSquared(ℂ[z + complexScale(t, w)])83  shows realZero ≤ R[2 * Euclidean.dot(z, w) + t * complexNormSquared(w)]84proof85  have pointZ := complex.point at z with *86  have pointW := complex.point at w with *87  have identity := complexNormSquared.perturbation at z, complexScale(t, w) with *88  rw [complexScale.dot_right, complexNormSquared.scale] at identity89  rw identity at minimum90  have shifted := realLe.add_right at complexNormSquared(z), R[complexNormSquared(z) + 2 * (t * Euclidean.dot(z, w)) + t * t * complexNormSquared(w)], R[-complexNormSquared(z)] with *91  have left : R[complexNormSquared(z) + -complexNormSquared(z)] = R[0 * t] by ring92  have right : R[(complexNormSquared(z) + 2 * (t * Euclidean.dot(z, w)) + t * t * complexNormSquared(w)) + -complexNormSquared(z)] = R[(2 * Euclidean.dot(z, w) + t * complexNormSquared(w)) * t]93    ring94  rw [left, right] at shifted95  exact realLe.mul_right_cancel_positive at realZero, R[2 * Euclidean.dot(z, w) + t * complexNormSquared(w)], t with *9697theorem normalizedNormSequence.converges (z s u a : Set)98  requires member : z ∈ ℂ99  requires steps : ConvergesTo(s, realZero)100  requires directions : ComplexConvergesTo(u, a)101  shows ConvergesTo(normalizedNormSequence(z, s, u), R[2 * Euclidean.dot(z, a)])102proof103  have center : a ∈ ℂ104    obtain ⟨sequence, center, horizontal, vertical⟩ := directions105    exact center106  have pointZ := complex.point at z with *107  have pointA := complex.point at a with *108  have two := constantSequence.converges at R[2] with *109  have dot := ComplexConvergesTo.dot at z, u, a with *110  have norm := ComplexConvergesTo.norm_squared with *111  have linear := ConvergesTo.mul at constantSequence(R[2]), complexDotSequence(z, u), R[2], Euclidean.dot(z, a) with *112  have quadratic := ConvergesTo.mul at s, complexNormSequence(u), realZero, complexNormSquared(a) with *113  have sum := ConvergesTo.add at mulSequence(constantSequence(R[2]), complexDotSequence(z, u)), mulSequence(s, complexNormSequence(u)), R[2 * Euclidean.dot(z, a)], R[0 * complexNormSquared(a)] with *114  rw [realMulValue.zero_left, realAddValue.zero_right] at sum115  unfold normalizedNormSequence116  exact sum117118theorem normalizedNormSequence.value (z s u : Set) (n : Nat)119  requires member : z ∈ ℂ120  requires steps : RealSequence(s)121  requires directions : ComplexSequence(u)122  shows normalizedNormSequence(z, s, u)(n) = R[2 * Euclidean.dot(z, u(n)) + s(n) * complexNormSquared(u(n))]123proof124  have two := constantSequence.sequence at R[2] with *125  have dot := complexDotSequence.sequence with *126  have norm : RealSequence(complexNormSequence(u))127    unfold RealSequence128    exact complexNormSequence.function with *129  have linear := mulSequence.sequence at constantSequence(R[2]), complexDotSequence(z, u) with *130  have quadratic := mulSequence.sequence at s, complexNormSequence(u) with *131  have tn := RealSequence.value at constantSequence(R[2]), n with *132  have dn := RealSequence.value at complexDotSequence(z, u), n with *133  have sn := RealSequence.value at s, n with *134  have nn := RealSequence.value at complexNormSequence(u), n with *135  have ln := RealSequence.value at mulSequence(constantSequence(R[2]), complexDotSequence(z, u)), n with *136  have qn := RealSequence.value at mulSequence(s, complexNormSequence(u)), n with *137  unfold normalizedNormSequence138  rw [addSequence.value, mulSequence.value, mulSequence.value, constantSequence.value, complexDotSequence.value, complexNormSequence.value]139  rfl140141-- Varying directions are allowed: their limit controls the first-order sign.142theorem complexNormSquared.minimum_direction (z s u a : Set)143  requires member : z ∈ ℂ144  requires steps : ConvergesTo(s, realZero)145  requires directions : ComplexConvergesTo(u, a)146  requires positive : ∀ n ∈ ℕ, realZero < s(n)147  requires minimum : ∀ n ∈ ℕ, complexNormSquared(z) ≤ complexNormSquared(ℂ[z + complexScale(s(n), u(n))])148  shows realZero ≤ Euclidean.dot(z, a)149proof150  have limit := normalizedNormSequence.converges with *151  have stepSequence := ConvergesTo.sequence at s, realZero with *152  obtain ⟨sequence, center, horizontal, vertical⟩ := directions153  have function : u : ℕ → ℂ by exact sequence154  have pointZ := complex.point at z with *155  have pointA := complex.point at a with *156  have nonnegative : NonnegativeTerms(normalizedNormSequence(z, s, u))157    intros n nIn158    have nNat := nat.omega.backward at n with *159    have sn := RealSequence.value with *160    have un := FunctionBetween.apply_closed with *161    have stepPositive := positive with n, nIn162    have least := minimum with n, nIn163    rw normalizedNormSequence.value164    have bound := complexNormSquared.minimum_step with *165    exact realLe.characterization.forward with bound166  have doubled := ConvergesTo.nonnegative_of_nonnegative_terms with *167  have twoPositive : (0:R) < 2 by linarith168  have left : realZero = R[0 * 2] by ring169  have right : R[2 * Euclidean.dot(z, a)] = R[Euclidean.dot(z, a) * 2] by ring170  rw [left, right] at doubled171  exact realLe.mul_right_cancel_positive with *172173end Complexes174