From 1546c04154cae9cd49ae2a3312e070a5924b3d18 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sat, 20 Feb 2016 13:17:10 -0500
Subject: [PATCH] feat(library/theories/analysis/complex_norm): instantiate
 complex numbers as a real normed vector space

---
 library/algebra/ordered_ring.lean            |  5 ++
 library/data/complex.lean                    | 14 +---
 library/theories/analysis/analysis.md        |  1 +
 library/theories/analysis/complex_norm.lean  | 70 ++++++++++++++++++++
 library/theories/analysis/inner_product.lean |  2 +-
 5 files changed, 79 insertions(+), 13 deletions(-)
 create mode 100644 library/theories/analysis/complex_norm.lean

diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index 5161b9cd3..489a4f6a3 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -722,6 +722,11 @@ section
     apply zero_lt_one
   end
 
+  lemma eq_zero_of_mul_self_add_mul_self_eq_zero {x y : A} (H : x * x + y * y = 0) : x = 0 :=
+  have x * x ≤ (0 : A), from calc
+    x * x ≤ x * x + y * y : le_add_of_nonneg_right (mul_self_nonneg y)
+      ... = 0             : H,
+  eq_zero_of_mul_self_eq_zero (le.antisymm this (mul_self_nonneg x))
 end
 
 /- TODO: Multiplication and one, starting with mult_right_le_one_le. -/
diff --git a/library/data/complex.lean b/library/data/complex.lean
index 1c4e9592f..8acf0147a 100644
--- a/library/data/complex.lean
+++ b/library/data/complex.lean
@@ -185,16 +185,6 @@ has_sub.mk has_sub.sub
 theorem of_real_sub (x y : ℝ) : of_real (x - y) = of_real x - of_real y :=
 rfl
 
--- TODO: move these
-private lemma eq_zero_of_mul_self_eq_zero {x : ℝ} (H : x * x = 0) : x = 0 :=
- iff.mp !or_self (!eq_zero_or_eq_zero_of_mul_eq_zero H)
-
-private lemma eq_zero_of_sum_square_eq_zero {x y : ℝ} (H : x * x + y * y = 0) : x = 0 :=
-have x * x ≤ (0 : ℝ), from calc
-  x * x ≤ x * x + y * y : le_add_of_nonneg_right (mul_self_nonneg y)
-    ... = 0             : H,
-eq_zero_of_mul_self_eq_zero (le.antisymm this (mul_self_nonneg x))
-
 /- complex modulus and conjugate-/
 
 definition cmod (z : ℂ) : ℝ :=
@@ -208,8 +198,8 @@ by rewrite [↑cmod, re_of_real, im_of_real, mul_zero, add_zero]
 theorem eq_zero_of_cmod_eq_zero {z : ℂ} (H : cmod z = 0) : z = 0 :=
 have H1 : (complex.re z) * (complex.re z) + (complex.im z) * (complex.im z) = 0,
   from H,
-have H2 : complex.re z = 0, from eq_zero_of_sum_square_eq_zero H1,
-have H3 : complex.im z = 0, from eq_zero_of_sum_square_eq_zero (!add.comm ▸ H1),
+have H2 : complex.re z = 0, from eq_zero_of_mul_self_add_mul_self_eq_zero H1,
+have H3 : complex.im z = 0, from eq_zero_of_mul_self_add_mul_self_eq_zero (!add.comm ▸ H1),
 show z = 0, from complex.eq H2 H3
 
 definition conj (z : ℂ) : ℂ := complex.mk (complex.re z) (-(complex.im z))
diff --git a/library/theories/analysis/analysis.md b/library/theories/analysis/analysis.md
index dc6ee82d4..ad0a2f328 100644
--- a/library/theories/analysis/analysis.md
+++ b/library/theories/analysis/analysis.md
@@ -7,3 +7,4 @@ theories.analysis
 * [ivt](ivt.lean) : the intermediate value theorem
 * [sqrt](sqrt.lean) : the sqrt function on the reals
 * [inner_product](inner_product.lean) : real inner product spaces
+* [complex_norm](complex_norm.lean) : the complex numbers as a real normed vector space
diff --git a/library/theories/analysis/complex_norm.lean b/library/theories/analysis/complex_norm.lean
new file mode 100644
index 000000000..1a161308c
--- /dev/null
+++ b/library/theories/analysis/complex_norm.lean
@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad
+
+Instantiate the complex numbers as a normed space, by temporarily making it an inner product space
+over the reals.
+-/
+import theories.analysis.inner_product data.complex
+open nat real complex analysis classical
+noncomputable theory
+
+namespace complex
+  namespace real_inner_product_space
+    definition smul (a : ℝ) (z : ℂ) : ℂ := complex.mk (a * re z) (a * im z)
+
+    definition ip (z w : ℂ) : ℝ := re z * re w + im z * im w
+
+    proposition smul_left_distrib (a : ℝ) (z w : ℂ) : smul a (z + w) = smul a z + smul a w :=
+    by rewrite [↑smul, *re_add, *im_add, *left_distrib]
+
+    proposition smul_right_distrib (a b : ℝ) (z : ℂ) : smul (a + b) z = smul a z + smul b z :=
+    by rewrite [↑smul, *right_distrib]
+
+    proposition mul_smul (a b : ℝ) (z : ℂ) : smul (a * b) z = smul a (smul b z) :=
+    by rewrite [↑smul, *mul.assoc]
+
+    proposition one_smul (z : ℂ) : smul 1 z = z := by rewrite [↑smul, *one_mul, complex.eta]
+
+    proposition inner_add_left (x y z : ℂ) : ip (x + y) z = ip x z + ip y z :=
+    by rewrite [↑ip, re_add, im_add, *right_distrib, *add.assoc, add.left_comm (re y * re z)]
+
+    proposition inner_smul_left (a : ℝ) (x y : ℂ) : ip (smul a x) y = a * ip x y :=
+    by rewrite [↑ip, ↑smul, left_distrib, *mul.assoc]
+
+    proposition inner_comm (x y : ℂ) : ip x y = ip y x :=
+    by rewrite [↑ip, mul.comm, mul.comm (im x)]
+
+    proposition inner_self_nonneg (x : ℂ) : ip x x ≥ 0 :=
+    add_nonneg (mul_self_nonneg (re x)) (mul_self_nonneg (im x))
+
+    proposition eq_zero_of_inner_self_eq_zero {x : ℂ} (H : ip x x = 0) : x = 0 :=
+    have re x = 0, from eq_zero_of_mul_self_add_mul_self_eq_zero H,
+    have im x = 0, from eq_zero_of_mul_self_add_mul_self_eq_zero
+                         (by rewrite [↑ip at H, add.comm at H]; exact H),
+    by+ rewrite [-complex.eta, `re x = 0`, `im x = 0`]
+  end real_inner_product_space
+
+  protected definition real_inner_product_space [reducible] : inner_product_space ℂ :=
+  ⦃ inner_product_space, complex.discrete_field,
+    smul               := real_inner_product_space.smul,
+    inner              := real_inner_product_space.ip,
+    smul_left_distrib  := real_inner_product_space.smul_left_distrib,
+    smul_right_distrib := real_inner_product_space.smul_right_distrib,
+    mul_smul           := real_inner_product_space.mul_smul,
+    one_smul           := real_inner_product_space.one_smul,
+    inner_add_left     := real_inner_product_space.inner_add_left,
+    inner_smul_left    := real_inner_product_space.inner_smul_left,
+    inner_comm         := real_inner_product_space.inner_comm,
+    inner_self_nonneg  := real_inner_product_space.inner_self_nonneg,
+    eq_zero_of_inner_self_eq_zero := @real_inner_product_space.eq_zero_of_inner_self_eq_zero
+  ⦄
+
+  local attribute complex.real_inner_product_space [trans_instance]
+
+  protected definition normed_vector_space [trans_instance] [reducible] : normed_vector_space ℂ :=
+  _
+
+  theorem norm_squared_eq_cmod (z : ℂ) : ∥ z ∥^2 = cmod z := by rewrite norm_squared
+end complex
diff --git a/library/theories/analysis/inner_product.lean b/library/theories/analysis/inner_product.lean
index 571eeedbc..c294d8bd3 100644
--- a/library/theories/analysis/inner_product.lean
+++ b/library/theories/analysis/inner_product.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad