The Cauchy-Schwarz inequality in complex inner product spaces

src/complex-numbers.lagda.md

@@ -19,5 +19,6 @@ open import complex-numbers.multiplication-complex-numbers public
 open import complex-numbers.multiplicative-inverses-nonzero-complex-numbers public
 open import complex-numbers.nonzero-complex-numbers public
 open import complex-numbers.raising-universe-levels-complex-numbers public
+open import complex-numbers.real-complex-numbers public
 open import complex-numbers.similarity-complex-numbers public
 ```

src/complex-numbers/addition-complex-numbers.lagda.md

@@ -8,9 +8,11 @@ module complex-numbers.addition-complex-numbers where
 
 ```agda
 open import complex-numbers.complex-numbers
+open import complex-numbers.conjugation-complex-numbers
 open import complex-numbers.similarity-complex-numbers
 
 open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.universe-levels
@@ -102,3 +104,56 @@ abstract
   preserves-sim-add-ℂ (a~a' , b~b') (c~c' , d~d') =
     ( preserves-sim-add-ℝ a~a' c~c' , preserves-sim-add-ℝ b~b' d~d')
 ```
+
+### The sum of `z` and `conjugate-ℂ z` is double `re-ℂ z`
+
+```agda
+abstract
+  right-add-conjugate-ℂ :
+    {l : Level} (z : ℂ l) → z +ℂ conjugate-ℂ z ＝ complex-ℝ (re-ℂ z +ℝ re-ℂ z)
+  right-add-conjugate-ℂ (a +iℂ b) = eq-ℂ refl (eq-right-inverse-law-add-ℝ b)
+```
+
+### Swapping laws for addition on complex numbers
+
+```agda
+module _
+  {l1 l2 l3 : Level} (x : ℂ l1) (y : ℂ l2) (z : ℂ l3)
+  where
+
+  abstract
+    right-swap-add-ℂ :
+      (x +ℂ y) +ℂ z ＝ (x +ℂ z) +ℂ y
+    right-swap-add-ℂ =
+      equational-reasoning
+        (x +ℂ y) +ℂ z
+        ＝ x +ℂ (y +ℂ z) by associative-add-ℂ x y z
+        ＝ x +ℂ (z +ℂ y) by ap (x +ℂ_) (commutative-add-ℂ y z)
+        ＝ (x +ℂ z) +ℂ y by inv (associative-add-ℂ x z y)
+
+    left-swap-add-ℂ :
+      x +ℂ (y +ℂ z) ＝ y +ℂ (x +ℂ z)
+    left-swap-add-ℂ =
+      equational-reasoning
+        x +ℂ (y +ℂ z)
+        ＝ (x +ℂ y) +ℂ z by inv (associative-add-ℂ x y z)
+        ＝ (y +ℂ x) +ℂ z by ap (_+ℂ z) (commutative-add-ℂ x y)
+        ＝ y +ℂ (x +ℂ z) by associative-add-ℂ y x z
+```
+
+### Interchange laws for addition on complex numbers
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (x : ℂ l1) (y : ℂ l2) (z : ℂ l3) (w : ℂ l4)
+  where
+
+  abstract
+    interchange-law-add-add-ℂ : (x +ℂ y) +ℂ (z +ℂ w) ＝ (x +ℂ z) +ℂ (y +ℂ w)
+    interchange-law-add-add-ℂ =
+      equational-reasoning
+        (x +ℂ y) +ℂ (z +ℂ w)
+        ＝ x +ℂ (y +ℂ (z +ℂ w)) by associative-add-ℂ _ _ _
+        ＝ x +ℂ (z +ℂ (y +ℂ w)) by ap (x +ℂ_) (left-swap-add-ℂ y z w)
+        ＝ (x +ℂ z) +ℂ (y +ℂ w) by inv (associative-add-ℂ x z (y +ℂ w))
+```

src/complex-numbers/complex-numbers.lagda.md

@@ -9,6 +9,8 @@ module complex-numbers.complex-numbers where
 ```agda
 open import complex-numbers.gaussian-integers
 
+open import elementary-number-theory.natural-numbers
+
 open import foundation.action-on-identifications-functions
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
@@ -20,6 +22,7 @@ open import foundation.universe-levels
 
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.negation-real-numbers
+open import real-numbers.positive-real-numbers
 open import real-numbers.raising-universe-levels-real-numbers
 open import real-numbers.rational-real-numbers
 ```
@@ -67,14 +70,17 @@ eq-ℂ = eq-pair
 
 ```agda
 complex-ℝ : {l : Level} → ℝ l → ℂ l
-complex-ℝ {l} a = (a , raise-ℝ l zero-ℝ)
+complex-ℝ {l} a = (a , raise-zero-ℝ l)
+
+complex-ℝ⁺ : {l : Level} → ℝ⁺ l → ℂ l
+complex-ℝ⁺ a = complex-ℝ (real-ℝ⁺ a)
 ```
 
 ### The imaginary embedding of real numbers into the complex numbers
 
 ```agda
 im-complex-ℝ : {l : Level} → ℝ l → ℂ l
-im-complex-ℝ {l} a = (raise-ℝ l zero-ℝ , a)
+im-complex-ℝ {l} a = (raise-zero-ℝ l , a)
 ```
 
 ### The canonical embedding of Gaussian integers into the complex numbers
@@ -84,6 +90,13 @@ complex-ℤ[i] : ℤ[i] → ℂ lzero
 complex-ℤ[i] (a , b) = (real-ℤ a , real-ℤ b)
 ```
 
+### The canonical embedding of natural numbers into the complex numbers
+
+```agda
+complex-ℕ : ℕ → ℂ lzero
+complex-ℕ n = complex-ℝ (real-ℕ n)
+```
+
 ### Important complex numbers
 
 ```agda
@@ -115,6 +128,14 @@ neg-ℂ : {l : Level} → ℂ l → ℂ l
 neg-ℂ (a , b) = (neg-ℝ a , neg-ℝ b)
 ```
 
+### Negation is an involution
+
+```agda
+abstract
+  neg-neg-ℂ : {l : Level} (z : ℂ l) → neg-ℂ (neg-ℂ z) ＝ z
+  neg-neg-ℂ (a +iℂ b) = eq-ℂ (neg-neg-ℝ a) (neg-neg-ℝ b)
+```
+
 ### `complex-ℝ one-ℝ` is equal to `one-ℂ`
 
 ```agda

src/complex-numbers/conjugation-complex-numbers.lagda.md

@@ -8,11 +8,15 @@ module complex-numbers.conjugation-complex-numbers where
 
 ```agda
 open import complex-numbers.complex-numbers
+open import complex-numbers.raising-universe-levels-complex-numbers
 
+open import foundation.action-on-identifications-functions
 open import foundation.identity-types
 open import foundation.universe-levels
 
+open import real-numbers.dedekind-real-numbers
 open import real-numbers.negation-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
 ```
 
 </details>
@@ -40,3 +44,31 @@ abstract
     {l : Level} (z : ℂ l) → conjugate-ℂ (conjugate-ℂ z) ＝ z
   is-involution-conjugate-ℂ (a +iℂ b) = eq-ℂ refl (neg-neg-ℝ b)
 ```
+
+### Conjugating raised complex numbers
+
+```agda
+abstract
+  conjugate-raise-ℂ :
+    {l0 : Level} (l : Level) (z : ℂ l0) →
+    conjugate-ℂ (raise-ℂ l z) ＝ raise-ℂ l (conjugate-ℂ z)
+  conjugate-raise-ℂ l (a +iℂ b) = eq-ℂ refl (neg-raise-ℝ l b)
+```
+
+### The conjugate of `one-ℂ` is `one-ℂ`
+
+```agda
+abstract
+  conjugate-one-ℂ : conjugate-ℂ one-ℂ ＝ one-ℂ
+  conjugate-one-ℂ = eq-ℂ refl neg-zero-ℝ
+```
+
+### The conjugate of `complex-ℝ x` is `complex-ℝ x`
+
+```agda
+abstract
+  conjugate-complex-ℝ :
+    {l : Level} (x : ℝ l) → conjugate-ℂ (complex-ℝ x) ＝ complex-ℝ x
+  conjugate-complex-ℝ {l} x =
+    eq-ℂ refl (neg-raise-ℝ _ _ ∙ ap (raise-ℝ l) neg-zero-ℝ)
+```

src/complex-numbers/magnitude-complex-numbers.lagda.md

@@ -12,6 +12,7 @@ module complex-numbers.magnitude-complex-numbers where
 open import complex-numbers.complex-numbers
 open import complex-numbers.conjugation-complex-numbers
 open import complex-numbers.multiplication-complex-numbers
+open import complex-numbers.raising-universe-levels-complex-numbers
 open import complex-numbers.similarity-complex-numbers
 
 open import foundation.action-on-identifications-functions
@@ -208,6 +209,27 @@ abstract
               ( square-ℝ c +ℝ square-ℝ d))
 ```
 
+### The magnitude of a real number as a complex number is its absolute value
+
+```agda
+abstract
+  squared-magnitude-complex-ℝ :
+    {l : Level} (x : ℝ l) → squared-magnitude-ℂ (complex-ℝ x) ＝ square-ℝ x
+  squared-magnitude-complex-ℝ {l} x =
+    equational-reasoning
+      square-ℝ x +ℝ square-ℝ (raise-zero-ℝ l)
+      ＝ square-ℝ x +ℝ raise-zero-ℝ l
+        by ap-add-ℝ refl (square-raise-zero-ℝ l)
+      ＝ square-ℝ x
+        by right-raise-zero-law-add-ℝ (square-ℝ x)
+
+  magnitude-complex-ℝ :
+    {l : Level} (x : ℝ l) → magnitude-ℂ (complex-ℝ x) ＝ abs-ℝ x
+  magnitude-complex-ℝ {l} x =
+    ( ap real-sqrt-ℝ⁰⁺ (eq-ℝ⁰⁺ _ _ (squared-magnitude-complex-ℝ x))) ∙
+    ( inv (eq-abs-sqrt-square-ℝ x))
+```
+
 ### The magnitude of `zw` is the product of the magnitudes of `z` and `w`
 
 ```agda
@@ -230,33 +252,21 @@ abstract
         by ap real-ℝ⁰⁺ (distributive-sqrt-mul-ℝ⁰⁺ _ _)
 ```
 
-### The magnitude of a real number as a complex number is its absolute value
+### The magnitude of a complex number multiplied on the left by an embedded real number
 
 ```agda
 abstract
-  magnitude-complex-ℝ :
-    {l : Level} (x : ℝ l) → magnitude-ℂ (complex-ℝ x) ＝ abs-ℝ x
-  magnitude-complex-ℝ {l} x =
-    equational-reasoning
-      real-sqrt-ℝ⁰⁺
-        ( nonnegative-square-ℝ x +ℝ⁰⁺ nonnegative-square-ℝ (raise-ℝ l zero-ℝ))
-      ＝
-        real-sqrt-ℝ⁰⁺
-          ( nonnegative-square-ℝ x +ℝ⁰⁺ nonnegative-square-ℝ zero-ℝ)
-        by
-          ap
-            ( real-sqrt-ℝ⁰⁺)
-            ( eq-ℝ⁰⁺ _ _
-              ( eq-sim-ℝ
-                ( preserves-sim-left-add-ℝ _ _ _
-                  ( preserves-sim-square-ℝ
-                    ( symmetric-sim-ℝ (sim-raise-ℝ l zero-ℝ))))))
-      ＝ real-sqrt-ℝ⁰⁺ (nonnegative-square-ℝ x +ℝ⁰⁺ zero-ℝ⁰⁺)
-        by ap real-sqrt-ℝ⁰⁺ (eq-ℝ⁰⁺ _ _ (ap-add-ℝ refl square-zero-ℝ))
-      ＝ real-sqrt-ℝ⁰⁺ (nonnegative-square-ℝ x)
-        by ap real-sqrt-ℝ⁰⁺ (eq-ℝ⁰⁺ _ _ (right-unit-law-add-ℝ _))
-      ＝ abs-ℝ x
-        by inv (eq-abs-sqrt-square-ℝ x)
+  magnitude-left-mul-complex-ℝ :
+    {l1 l2 : Level} (x : ℝ l1) (z : ℂ l2) →
+    magnitude-ℂ (complex-ℝ x *ℂ z) ＝ abs-ℝ x *ℝ magnitude-ℂ z
+  magnitude-left-mul-complex-ℝ x z =
+    distributive-magnitude-mul-ℂ _ z ∙ ap-mul-ℝ (magnitude-complex-ℝ x) refl
+
+  magnitude-left-mul-complex-ℝ⁺ :
+    {l1 l2 : Level} (x : ℝ⁺ l1) (z : ℂ l2) →
+    magnitude-ℂ (complex-ℝ⁺ x *ℂ z) ＝ real-ℝ⁺ x *ℝ magnitude-ℂ z
+  magnitude-left-mul-complex-ℝ⁺ x⁺@(x , _) z =
+    magnitude-left-mul-complex-ℝ x z ∙ ap-mul-ℝ (abs-real-ℝ⁺ x⁺) refl
 ```
 
 ### Similar complex numbers have similar magnitudes
@@ -276,12 +286,47 @@ abstract
     sim-ℂ z w → sim-ℝ (magnitude-ℂ z) (magnitude-ℂ w)
   preserves-sim-magnitude-ℂ z~w =
     preserves-sim-sqrt-ℝ⁰⁺ _ _ (preserves-sim-squared-magnitude-ℂ z~w)
+
+  squared-magnitude-raise-ℂ :
+    {l0 : Level} (l : Level) (z : ℂ l0) →
+    squared-magnitude-ℂ (raise-ℂ l z) ＝ raise-ℝ l (squared-magnitude-ℂ z)
+  squared-magnitude-raise-ℂ l z =
+    eq-sim-ℝ
+      ( similarity-reasoning-ℝ
+        squared-magnitude-ℂ (raise-ℂ l z)
+        ~ℝ squared-magnitude-ℂ z
+          by preserves-sim-squared-magnitude-ℂ (sim-raise-ℂ' l z)
+        ~ℝ raise-ℝ l (squared-magnitude-ℂ z)
+          by sim-raise-ℝ l _)
+
+  magnitude-raise-ℂ :
+    {l0 : Level} (l : Level) (z : ℂ l0) →
+    magnitude-ℂ (raise-ℂ l z) ＝ raise-ℝ l (magnitude-ℂ z)
+  magnitude-raise-ℂ l z =
+    eq-sim-ℝ
+      ( similarity-reasoning-ℝ
+        magnitude-ℂ (raise-ℂ l z)
+        ~ℝ magnitude-ℂ z
+          by preserves-sim-magnitude-ℂ (sim-raise-ℂ' l z)
+        ~ℝ raise-ℝ l (magnitude-ℂ z)
+          by sim-raise-ℝ l _)
 ```
 
 ### The magnitude of `one-ℂ` is `one-ℝ`
 
 ```agda
 abstract
+  squared-magnitude-one-ℂ : squared-magnitude-ℂ one-ℂ ＝ one-ℝ
+  squared-magnitude-one-ℂ =
+    equational-reasoning
+      squared-magnitude-ℂ one-ℂ
+      ＝ squared-magnitude-ℂ (complex-ℝ one-ℝ)
+        by ap squared-magnitude-ℂ (inv eq-complex-one-ℝ)
+      ＝ square-ℝ one-ℝ
+        by squared-magnitude-complex-ℝ one-ℝ
+      ＝ one-ℝ
+        by right-unit-law-mul-ℝ one-ℝ
+
   magnitude-one-ℂ : magnitude-ℂ one-ℂ ＝ one-ℝ
   magnitude-one-ℂ =
     equational-reasoning
@@ -293,3 +338,17 @@ abstract
       ＝ one-ℝ
         by abs-real-ℝ⁺ one-ℝ⁺
 ```
+
+### The magnitude of `-z` is equal to the magnitude of `z`
+
+```agda
+abstract
+  squared-magnitude-neg-ℂ :
+    {l : Level} (z : ℂ l) →
+    squared-magnitude-ℂ (neg-ℂ z) ＝ squared-magnitude-ℂ z
+  squared-magnitude-neg-ℂ (a +iℂ b) = ap-add-ℝ (square-neg-ℝ a) (square-neg-ℝ b)
+
+  magnitude-neg-ℂ :
+    {l : Level} (z : ℂ l) → magnitude-ℂ (neg-ℂ z) ＝ magnitude-ℂ z
+  magnitude-neg-ℂ z = ap real-sqrt-ℝ⁰⁺ (eq-ℝ⁰⁺ _ _ (squared-magnitude-neg-ℂ z))
+```