Grace/Cumulus/Complex/Norm.g17

Open in Workbench Download source

Imports

Field · Geometry.Plane

Declarations

• complex.point theorem derivation
• complex.of_point theorem derivation
• complexNormSquared def
• complexNormSquared.real theorem derivation
• complexNormSquared.pair theorem derivation
• complexNormSquared.nonnegative theorem derivation
• complexNormSquared.zero_iff theorem derivation
• complexNormSquared.positive theorem derivation
• complexNormSquared.zero theorem derivation
• complexNormSquared.one theorem derivation
• complexNormSquared.mul theorem derivation
• complexNormSquared.neg theorem derivation
• complexNormSquared.parallelogram theorem derivation
• complexNormSquared.add_bound theorem derivation
• complexNormSquared.perturbation theorem derivation
• complexNormSquared.strict_descent theorem derivation

Source

1-- Squared complex modulus and its Euclidean geometry, without square roots (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.Norm8import Field9import Geometry.Plane1011theorem complex.point (z : Set)12  requires member : z ∈ complexCarrier13  shows Euclidean.Point(z)14proof15  obtain ⟨a, aReal, b, bReal, coordinates⟩ := complexCarrier.cases at z with *16  rw coordinates17  exact Euclidean.pair.point with *1819theorem complex.of_point (z : Euclidean.Point)20  shows z ∈ complexCarrier21proof22  have coordinates := Euclidean.coordinates at z with *23  rw coordinates24  exact complexCarrier.pair with *2526def complexNormSquared (z : Euclidean.Point) : Real := Euclidean.normSquared(z)2728theorem complexNormSquared.real (z : Set)29  requires member : z ∈ complexCarrier30  shows Real(complexNormSquared(z))31proof32  have point := complex.point with *33  unfold complexNormSquared34  exact Euclidean.normSquared.real with *3536theorem complexNormSquared.pair (a b : Real)37  shows complexNormSquared((a, b)) = a * a + b * b38proof39  have horizontal := Euclidean.x.pair at a, b with *40  have vertical := Euclidean.y.pair at a, b with *41  simp [complexNormSquared, Euclidean.normSquared, Euclidean.dot]4243theorem complexNormSquared.nonnegative (z : Set)44  requires member : z ∈ complexCarrier45  shows 0 ≤ complexNormSquared(z)46proof47  have point := complex.point with *48  unfold complexNormSquared49  exact Euclidean.normSquared.nonnegative with *5051theorem complexNormSquared.zero_iff (z : Set)52  requires member : z ∈ complexCarrier53  shows complexNormSquared(z) = 0 ↔ z = complexZero54proof55  obtain ⟨a, aReal, b, bReal, coordinates⟩ := complexCarrier.cases at z with *56  have norm := complexNormSquared.pair at a, b with *57  have vanishing := complex.norm_zero_iff at a, b with *58  rw [coordinates, norm]59  constructor60  . intro zeroNorm61    have parts := vanishing.forward with zeroNorm62    unfold complexZero63    cc64  . intro zeroPoint65    unfold complexZero at zeroPoint66    have parts := orderedPair.injective with zeroPoint67    rw [parts.left, parts.right]68    ring6970theorem complexNormSquared.positive (z : Set)71  requires member : z ∈ complexCarrier72  requires nonzero : z ≠ complexZero73  shows 0 < complexNormSquared(z)74proof75  have nonnegative := complexNormSquared.nonnegative with *76  have nonvanishing : complexNormSquared(z) ≠ 077    intro zeroNorm78    have zeroPoint := complexNormSquared.zero_iff.forward with *79    exact nonzero with zeroPoint80  exact Real.positive_of_nonnegative_of_ne_zero with *8182section Arithmetic83notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)84notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)8586theorem complexNormSquared.zero87  shows complexNormSquared(ℂ[0]) = R[0]88proof89  unfold complexZero90  rw complexNormSquared.pair91  ring9293theorem complexNormSquared.one94  shows complexNormSquared(ℂ[1]) = R[1]95proof96  unfold complexOne97  rw complexNormSquared.pair98  ring99100theorem complexNormSquared.mul (z w : Set)101  requires first : z ∈ ℂ102  requires second : w ∈ ℂ103  shows complexNormSquared(ℂ[z * w]) = R[complexNormSquared(z) * complexNormSquared(w)]104proof105  obtain ⟨a, aReal, b, bReal, zPair⟩ := complexCarrier.cases at z with *106  obtain ⟨c, cReal, d, dReal, wPair⟩ := complexCarrier.cases at w with *107  rw [zPair, wPair, complexMul.pair, complexNormSquared.pair, complexNormSquared.pair, complexNormSquared.pair]108  ring109110theorem complexNormSquared.neg (z : Set)111  requires member : z ∈ ℂ112  shows complexNormSquared(ℂ[-z]) = complexNormSquared(z)113proof114  obtain ⟨a, aReal, b, bReal, coordinates⟩ := complexCarrier.cases at z with *115  rw [coordinates, complexNeg.pair, complexNormSquared.pair, complexNormSquared.pair]116  ring117118theorem complexNormSquared.parallelogram (z w : Set)119  requires first : z ∈ ℂ120  requires second : w ∈ ℂ121  shows R[complexNormSquared(ℂ[z + w]) + complexNormSquared(ℂ[z - w])] = R[2 * (complexNormSquared(z) + complexNormSquared(w))]122proof123  obtain ⟨a, aReal, b, bReal, zPair⟩ := complexCarrier.cases at z with *124  obtain ⟨c, cReal, d, dReal, wPair⟩ := complexCarrier.cases at w with *125  rw [zPair, wPair]126  simp [complexAdd.pair, complexNeg.pair, complexNormSquared.pair]127  ring128129theorem complexNormSquared.add_bound (z w : Set)130  requires first : z ∈ ℂ131  requires second : w ∈ ℂ132  shows complexNormSquared(ℂ[z + w]) ≤ R[2 * (complexNormSquared(z) + complexNormSquared(w))]133proof134  have field := complexes.is_field135  have ring := IsField.comm_ring with field136  have ordinary := IsCommRing.ring with ring137  have negated := IsRing.neg_closed with ordinary, second138  have difference := IsRing.add_closed with ordinary, first, negated139  have sum := IsRing.add_closed with ordinary, first, second140  have nonnegative := complexNormSquared.nonnegative with difference141  have identity := complexNormSquared.parallelogram with first, second142  have bound := realLe.add_left at realZero, complexNormSquared(ℂ[z - w]), complexNormSquared(ℂ[z + w]) with *143  rwa [realAddValue.zero_right, identity] at bound144145theorem complexNormSquared.perturbation (z w : Set)146  requires first : z ∈ ℂ147  requires second : w ∈ ℂ148  shows complexNormSquared(ℂ[z + w]) = R[complexNormSquared(z) + 2 * Euclidean.dot(z, w) + complexNormSquared(w)]149proof150  obtain ⟨a, aReal, b, bReal, zPair⟩ := complexCarrier.cases at z with *151  obtain ⟨c, cReal, d, dReal, wPair⟩ := complexCarrier.cases at w with *152  rw [zPair, wPair]153  simp [complexAdd.pair, complexNormSquared.pair, Euclidean.dot, Euclidean.x.pair, Euclidean.y.pair]154  ring155156theorem complexNormSquared.strict_descent (z w : Set)157  requires first : z ∈ ℂ158  requires second : w ∈ ℂ159  requires descent : R[2 * Euclidean.dot(z, w) + complexNormSquared(w)] < R[0]160  shows complexNormSquared(ℂ[z + w]) < complexNormSquared(z)161proof162  have pointZ := complex.point at z with *163  have pointW := complex.point at w with *164  have decreasing := realLess.add_left at R[2 * Euclidean.dot(z, w) + complexNormSquared(w)], realZero, complexNormSquared(z) with *165  have identity := complexNormSquared.perturbation at z, w with *166  have regroup : complexNormSquared(ℂ[z + w]) = R[complexNormSquared(z) + (2 * Euclidean.dot(z, w) + complexNormSquared(w))]167    rw identity168    ring169  rwa [← regroup, realAddValue.zero_right] at decreasing170171end Arithmetic172