From 51ad06e5a86554fc42398b6f90b021685ce36665 Mon Sep 17 00:00:00 2001
From: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Sat, 25 Sep 2021 06:48:09 +0000
Subject: [PATCH] refactor(analysis/inner_product_space/*): split big file
 (#9382)

This PR makes a new folder `analysis/inner_product_space/*` comprising several files splitting the old `analysis/normed_space/inner_product` (which had reached 2900 lines!).

https://leanprover.zulipchat.com/#narrow/stream/116395-maths
---
 .../calculus/conformal/inner_product.lean     |    2 +-
 src/analysis/calculus/specific_functions.lean |    2 +-
 src/analysis/convex/cone.lean                 |    2 +-
 .../basic.lean}                               | 1250 +----------------
 .../inner_product_space/calculus.lean         |  291 ++++
 .../conformal_linear_map.lean}                |    2 +-
 .../euclidean_dist.lean                       |    1 +
 .../inner_product_space/projection.lean       | 1020 ++++++++++++++
 src/analysis/normed_space/dual.lean           |    3 +-
 src/analysis/normed_space/pi_Lp.lean          |    2 +-
 src/analysis/quaternion.lean                  |    2 +-
 src/geometry/euclidean/basic.lean             |    6 +-
 src/geometry/manifold/instances/sphere.lean   |    1 +
 src/measure_theory/function/l2_space.lean     |    2 +-
 .../function/special_functions.lean           |    2 +-
 15 files changed, 1328 insertions(+), 1260 deletions(-)
 rename src/analysis/{normed_space/inner_product.lean => inner_product_space/basic.lean} (55%)
 create mode 100644 src/analysis/inner_product_space/calculus.lean
 rename src/analysis/{normed_space/conformal_linear_map/inner_product.lean => inner_product_space/conformal_linear_map.lean} (97%)
 rename src/analysis/{normed_space => inner_product_space}/euclidean_dist.lean (99%)
 create mode 100644 src/analysis/inner_product_space/projection.lean

diff --git a/src/analysis/calculus/conformal/inner_product.lean b/src/analysis/calculus/conformal/inner_product.lean
index 155458279add6..7d84a6b327469 100644
--- a/src/analysis/calculus/conformal/inner_product.lean
+++ b/src/analysis/calculus/conformal/inner_product.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yourong Zang
 -/
 import analysis.calculus.conformal.normed_space
-import analysis.normed_space.conformal_linear_map.inner_product
+import analysis.inner_product_space.conformal_linear_map
 
 /-!
 # Conformal maps between inner product spaces
diff --git a/src/analysis/calculus/specific_functions.lean b/src/analysis/calculus/specific_functions.lean
index 556c4d4d8375b..b7eba444bc49e 100644
--- a/src/analysis/calculus/specific_functions.lean
+++ b/src/analysis/calculus/specific_functions.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import analysis.calculus.iterated_deriv
-import analysis.normed_space.euclidean_dist
+import analysis.inner_product_space.euclidean_dist
 
 /-!
 # Infinitely smooth bump function
diff --git a/src/analysis/convex/cone.lean b/src/analysis/convex/cone.lean
index ad6a7ba568764..291d07ee878fd 100644
--- a/src/analysis/convex/cone.lean
+++ b/src/analysis/convex/cone.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Frédéric Dupuis
 -/
 import analysis.convex.basic
-import analysis.normed_space.inner_product
+import analysis.inner_product_space.basic
 
 /-!
 # Convex cones
diff --git a/src/analysis/normed_space/inner_product.lean b/src/analysis/inner_product_space/basic.lean
similarity index 55%
rename from src/analysis/normed_space/inner_product.lean
rename to src/analysis/inner_product_space/basic.lean
index 5348420699af6..e6ee61bfe5e83 100644
--- a/src/analysis/normed_space/inner_product.lean
+++ b/src/analysis/inner_product_space/basic.lean
@@ -1,11 +1,9 @@
 /-
 Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Zhouhang Zhou, Sébastien Gouëzel, Frédéric Dupuis, Heather Macbeth
+Authors: Zhouhang Zhou, Sébastien Gouëzel, Frédéric Dupuis
 -/
 import analysis.complex.basic
-import analysis.normed_space.bounded_linear_maps
-import analysis.special_functions.sqrt
 import linear_algebra.bilinear_form
 import linear_algebra.sesquilinear_form
 
@@ -28,15 +26,9 @@ product structure on `n → 𝕜` for `𝕜 = ℝ` or `ℂ`, see `euclidean_spac
   properties, most notably the Cauchy-Schwarz inequality. Here `𝕜` is understood to be either `ℝ`
   or `ℂ`, through the `is_R_or_C` typeclass.
 - We show that if `f i` is an inner product space for each `i`, then so is `Π i, f i`
-- Existence of orthogonal projection onto nonempty complete subspace:
-  Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace.
-  Then there exists a unique `v` in `K` that minimizes the distance `∥u - v∥` to `u`.
-  The point `v` is usually called the orthogonal projection of `u` onto `K`.
-- We define `orthonormal`, a predicate on a function `v : ι → E`.  We prove the existence of a
-  maximal orthonormal set, `exists_maximal_orthonormal`, and also prove that a maximal orthonormal
-  set is a basis (`maximal_orthonormal_iff_basis_of_finite_dimensional`), if `E` is finite-
-  dimensional, or in general (`maximal_orthonormal_iff_dense_span`) a set whose span is dense
-  (i.e., a Hilbert basis, although we do not make that definition).
+- We define `orthonormal`, a predicate on a function `v : ι → E`, and prove the existence of a
+  maximal orthonormal set, `exists_maximal_orthonormal`.  For the existence of orthonormal
+  bases, Hilbert bases, etc., see the file `analysis.inner_product_space.projection`.
 
 ## Notation
 
@@ -1510,856 +1502,9 @@ inner_product_space.is_R_or_C_to_real ℂ G
 
 end is_R_or_C_to_real
 
-section deriv
-
-/-!
-### Derivative of the inner product
-
-In this section we prove that the inner product and square of the norm in an inner space are
-infinitely `ℝ`-smooth. In order to state these results, we need a `normed_space ℝ E`
-instance. Though we can deduce this structure from `inner_product_space 𝕜 E`, this instance may be
-not definitionally equal to some other “natural” instance. So, we assume `[normed_space ℝ E]` and
-`[is_scalar_tower ℝ 𝕜 E]`. In both interesting cases `𝕜 = ℝ` and `𝕜 = ℂ` we have these instances.
-
--/
-
-variables [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E]
-
-lemma is_bounded_bilinear_map_inner : is_bounded_bilinear_map ℝ (λ p : E × E, ⟪p.1, p.2⟫) :=
-{ add_left := λ _ _ _, inner_add_left,
-  smul_left := λ r x y,
-    by simp only [← algebra_map_smul 𝕜 r x, algebra_map_eq_of_real, inner_smul_real_left],
-  add_right := λ _ _ _, inner_add_right,
-  smul_right := λ r x y,
-    by simp only [← algebra_map_smul 𝕜 r y, algebra_map_eq_of_real, inner_smul_real_right],
-  bound := ⟨1, zero_lt_one, λ x y,
-    by { rw [one_mul], exact norm_inner_le_norm x y, }⟩ }
-
-/-- Derivative of the inner product. -/
-def fderiv_inner_clm (p : E × E) : E × E →L[ℝ] 𝕜 := is_bounded_bilinear_map_inner.deriv p
-
-@[simp] lemma fderiv_inner_clm_apply (p x : E × E) :
-  fderiv_inner_clm  p x = ⟪p.1, x.2⟫ + ⟪x.1, p.2⟫ := rfl
-
-lemma times_cont_diff_inner {n} : times_cont_diff ℝ n (λ p : E × E, ⟪p.1, p.2⟫) :=
-is_bounded_bilinear_map_inner.times_cont_diff
-
-lemma times_cont_diff_at_inner {p : E × E} {n} :
-  times_cont_diff_at ℝ n (λ p : E × E, ⟪p.1, p.2⟫) p :=
-times_cont_diff_inner.times_cont_diff_at
-
-lemma differentiable_inner : differentiable ℝ (λ p : E × E, ⟪p.1, p.2⟫) :=
-is_bounded_bilinear_map_inner.differentiable_at
-
-variables {G : Type*} [normed_group G] [normed_space ℝ G]
-  {f g : G → E} {f' g' : G →L[ℝ] E} {s : set G} {x : G} {n : with_top ℕ}
-
-include 𝕜
-
-lemma times_cont_diff_within_at.inner (hf : times_cont_diff_within_at ℝ n f s x)
-  (hg : times_cont_diff_within_at ℝ n g s x) :
-  times_cont_diff_within_at ℝ n (λ x, ⟪f x, g x⟫) s x :=
-times_cont_diff_at_inner.comp_times_cont_diff_within_at x (hf.prod hg)
-
-lemma times_cont_diff_at.inner (hf : times_cont_diff_at ℝ n f x)
-  (hg : times_cont_diff_at ℝ n g x) :
-  times_cont_diff_at ℝ n (λ x, ⟪f x, g x⟫) x :=
-hf.inner hg
-
-lemma times_cont_diff_on.inner (hf : times_cont_diff_on ℝ n f s) (hg : times_cont_diff_on ℝ n g s) :
-  times_cont_diff_on ℝ n (λ x, ⟪f x, g x⟫) s :=
-λ x hx, (hf x hx).inner (hg x hx)
-
-lemma times_cont_diff.inner (hf : times_cont_diff ℝ n f) (hg : times_cont_diff ℝ n g) :
-  times_cont_diff ℝ n (λ x, ⟪f x, g x⟫) :=
-times_cont_diff_inner.comp (hf.prod hg)
-
-lemma has_fderiv_within_at.inner (hf : has_fderiv_within_at f f' s x)
-  (hg : has_fderiv_within_at g g' s x) :
-  has_fderiv_within_at (λ t, ⟪f t, g t⟫) ((fderiv_inner_clm (f x, g x)).comp $ f'.prod g') s x :=
-(is_bounded_bilinear_map_inner.has_fderiv_at (f x, g x)).comp_has_fderiv_within_at x (hf.prod hg)
-
-lemma has_fderiv_at.inner (hf : has_fderiv_at f f' x) (hg : has_fderiv_at g g' x) :
-  has_fderiv_at (λ t, ⟪f t, g t⟫) ((fderiv_inner_clm (f x, g x)).comp $ f'.prod g') x :=
-(is_bounded_bilinear_map_inner.has_fderiv_at (f x, g x)).comp x (hf.prod hg)
-
-lemma has_deriv_within_at.inner {f g : ℝ → E} {f' g' : E} {s : set ℝ} {x : ℝ}
-  (hf : has_deriv_within_at f f' s x) (hg : has_deriv_within_at g g' s x) :
-  has_deriv_within_at (λ t, ⟪f t, g t⟫) (⟪f x, g'⟫ + ⟪f', g x⟫) s x :=
-by simpa using (hf.has_fderiv_within_at.inner hg.has_fderiv_within_at).has_deriv_within_at
-
-lemma has_deriv_at.inner {f g : ℝ → E} {f' g' : E} {x : ℝ} :
-  has_deriv_at f f' x →  has_deriv_at g g' x →
-  has_deriv_at (λ t, ⟪f t, g t⟫) (⟪f x, g'⟫ + ⟪f', g x⟫) x :=
-by simpa only [← has_deriv_within_at_univ] using has_deriv_within_at.inner
-
-lemma differentiable_within_at.inner (hf : differentiable_within_at ℝ f s x)
-  (hg : differentiable_within_at ℝ g s x) :
-  differentiable_within_at ℝ (λ x, ⟪f x, g x⟫) s x :=
-((differentiable_inner _).has_fderiv_at.comp_has_fderiv_within_at x
-  (hf.prod hg).has_fderiv_within_at).differentiable_within_at
-
-lemma differentiable_at.inner (hf : differentiable_at ℝ f x) (hg : differentiable_at ℝ g x) :
-  differentiable_at ℝ (λ x, ⟪f x, g x⟫) x :=
-(differentiable_inner _).comp x (hf.prod hg)
-
-lemma differentiable_on.inner (hf : differentiable_on ℝ f s) (hg : differentiable_on ℝ g s) :
-  differentiable_on ℝ (λ x, ⟪f x, g x⟫) s :=
-λ x hx, (hf x hx).inner (hg x hx)
-
-lemma differentiable.inner (hf : differentiable ℝ f) (hg : differentiable ℝ g) :
-  differentiable ℝ (λ x, ⟪f x, g x⟫) :=
-λ x, (hf x).inner (hg x)
-
-lemma fderiv_inner_apply (hf : differentiable_at ℝ f x) (hg : differentiable_at ℝ g x) (y : G) :
-  fderiv ℝ (λ t, ⟪f t, g t⟫) x y = ⟪f x, fderiv ℝ g x y⟫ + ⟪fderiv ℝ f x y, g x⟫ :=
-by { rw [(hf.has_fderiv_at.inner hg.has_fderiv_at).fderiv], refl }
-
-lemma deriv_inner_apply {f g : ℝ → E} {x : ℝ} (hf : differentiable_at ℝ f x)
-  (hg : differentiable_at ℝ g x) :
-  deriv (λ t, ⟪f t, g t⟫) x = ⟪f x, deriv g x⟫ + ⟪deriv f x, g x⟫ :=
-(hf.has_deriv_at.inner hg.has_deriv_at).deriv
-
-lemma times_cont_diff_norm_sq : times_cont_diff ℝ n (λ x : E, ∥x∥ ^ 2) :=
-begin
-  simp only [sq, ← inner_self_eq_norm_sq],
-  exact (re_clm : 𝕜 →L[ℝ] ℝ).times_cont_diff.comp (times_cont_diff_id.inner times_cont_diff_id)
-end
-
-lemma times_cont_diff.norm_sq (hf : times_cont_diff ℝ n f) :
-  times_cont_diff ℝ n (λ x, ∥f x∥ ^ 2) :=
-times_cont_diff_norm_sq.comp hf
-
-lemma times_cont_diff_within_at.norm_sq (hf : times_cont_diff_within_at ℝ n f s x) :
-  times_cont_diff_within_at ℝ n (λ y, ∥f y∥ ^ 2) s x :=
-times_cont_diff_norm_sq.times_cont_diff_at.comp_times_cont_diff_within_at x hf
-
-lemma times_cont_diff_at.norm_sq (hf : times_cont_diff_at ℝ n f x) :
-  times_cont_diff_at ℝ n (λ y, ∥f y∥ ^ 2) x :=
-hf.norm_sq
-
-lemma times_cont_diff_at_norm {x : E} (hx : x ≠ 0) : times_cont_diff_at ℝ n norm x :=
-have ∥id x∥ ^ 2 ≠ 0, from pow_ne_zero _ (norm_pos_iff.2 hx).ne',
-by simpa only [id, sqrt_sq, norm_nonneg] using times_cont_diff_at_id.norm_sq.sqrt this
-
-lemma times_cont_diff_at.norm (hf : times_cont_diff_at ℝ n f x) (h0 : f x ≠ 0) :
-  times_cont_diff_at ℝ n (λ y, ∥f y∥) x :=
-(times_cont_diff_at_norm h0).comp x hf
-
-lemma times_cont_diff_at.dist (hf : times_cont_diff_at ℝ n f x) (hg : times_cont_diff_at ℝ n g x)
-  (hne : f x ≠ g x) :
-  times_cont_diff_at ℝ n (λ y, dist (f y) (g y)) x :=
-by { simp only [dist_eq_norm], exact (hf.sub hg).norm (sub_ne_zero.2 hne) }
-
-lemma times_cont_diff_within_at.norm (hf : times_cont_diff_within_at ℝ n f s x) (h0 : f x ≠ 0) :
-  times_cont_diff_within_at ℝ n (λ y, ∥f y∥) s x :=
-(times_cont_diff_at_norm h0).comp_times_cont_diff_within_at x hf
-
-lemma times_cont_diff_within_at.dist (hf : times_cont_diff_within_at ℝ n f s x)
-  (hg : times_cont_diff_within_at ℝ n g s x) (hne : f x ≠ g x) :
-  times_cont_diff_within_at ℝ n (λ y, dist (f y) (g y)) s x :=
-by { simp only [dist_eq_norm], exact (hf.sub hg).norm (sub_ne_zero.2 hne) }
-
-lemma times_cont_diff_on.norm_sq (hf : times_cont_diff_on ℝ n f s) :
-  times_cont_diff_on ℝ n (λ y, ∥f y∥ ^ 2) s :=
-(λ x hx, (hf x hx).norm_sq)
-
-lemma times_cont_diff_on.norm (hf : times_cont_diff_on ℝ n f s) (h0 : ∀ x ∈ s, f x ≠ 0) :
-  times_cont_diff_on ℝ n (λ y, ∥f y∥) s :=
-λ x hx, (hf x hx).norm (h0 x hx)
-
-lemma times_cont_diff_on.dist (hf : times_cont_diff_on ℝ n f s)
-  (hg : times_cont_diff_on ℝ n g s) (hne : ∀ x ∈ s, f x ≠ g x) :
-  times_cont_diff_on ℝ n (λ y, dist (f y) (g y)) s :=
-λ x hx, (hf x hx).dist (hg x hx) (hne x hx)
-
-lemma times_cont_diff.norm (hf : times_cont_diff ℝ n f) (h0 : ∀ x, f x ≠ 0) :
-  times_cont_diff ℝ n (λ y, ∥f y∥) :=
-times_cont_diff_iff_times_cont_diff_at.2 $ λ x, hf.times_cont_diff_at.norm (h0 x)
-
-lemma times_cont_diff.dist (hf : times_cont_diff ℝ n f) (hg : times_cont_diff ℝ n g)
-  (hne : ∀ x, f x ≠ g x) :
-  times_cont_diff ℝ n (λ y, dist (f y) (g y)) :=
-times_cont_diff_iff_times_cont_diff_at.2 $
-  λ x, hf.times_cont_diff_at.dist hg.times_cont_diff_at (hne x)
-
-lemma differentiable_at.norm_sq (hf : differentiable_at ℝ f x) :
-  differentiable_at ℝ (λ y, ∥f y∥ ^ 2) x :=
-(times_cont_diff_at_id.norm_sq.differentiable_at le_rfl).comp x hf
-
-lemma differentiable_at.norm (hf : differentiable_at ℝ f x) (h0 : f x ≠ 0) :
-  differentiable_at ℝ (λ y, ∥f y∥) x :=
-((times_cont_diff_at_norm h0).differentiable_at le_rfl).comp x hf
-
-lemma differentiable_at.dist (hf : differentiable_at ℝ f x) (hg : differentiable_at ℝ g x)
-  (hne : f x ≠ g x) :
-  differentiable_at ℝ (λ y, dist (f y) (g y)) x :=
-by { simp only [dist_eq_norm], exact (hf.sub hg).norm (sub_ne_zero.2 hne) }
-
-lemma differentiable.norm_sq (hf : differentiable ℝ f) : differentiable ℝ (λ y, ∥f y∥ ^ 2) :=
-λ x, (hf x).norm_sq
-
-lemma differentiable.norm (hf : differentiable ℝ f) (h0 : ∀ x, f x ≠ 0) :
-  differentiable ℝ (λ y, ∥f y∥) :=
-λ x, (hf x).norm (h0 x)
-
-lemma differentiable.dist (hf : differentiable ℝ f) (hg : differentiable ℝ g)
-  (hne : ∀ x, f x ≠ g x) :
-  differentiable ℝ (λ y, dist (f y) (g y)) :=
-λ x, (hf x).dist (hg x) (hne x)
-
-lemma differentiable_within_at.norm_sq (hf : differentiable_within_at ℝ f s x) :
-  differentiable_within_at ℝ (λ y, ∥f y∥ ^ 2) s x :=
-(times_cont_diff_at_id.norm_sq.differentiable_at le_rfl).comp_differentiable_within_at x hf
-
-lemma differentiable_within_at.norm (hf : differentiable_within_at ℝ f s x) (h0 : f x ≠ 0) :
-  differentiable_within_at ℝ (λ y, ∥f y∥) s x :=
-((times_cont_diff_at_id.norm h0).differentiable_at le_rfl).comp_differentiable_within_at x hf
-
-lemma differentiable_within_at.dist (hf : differentiable_within_at ℝ f s x)
-  (hg : differentiable_within_at ℝ g s x) (hne : f x ≠ g x) :
-  differentiable_within_at ℝ (λ y, dist (f y) (g y)) s x :=
-by { simp only [dist_eq_norm], exact (hf.sub hg).norm (sub_ne_zero.2 hne) }
-
-lemma differentiable_on.norm_sq (hf : differentiable_on ℝ f s) :
-  differentiable_on ℝ (λ y, ∥f y∥ ^ 2) s :=
-λ x hx, (hf x hx).norm_sq
-
-lemma differentiable_on.norm (hf : differentiable_on ℝ f s) (h0 : ∀ x ∈ s, f x ≠ 0) :
-  differentiable_on ℝ (λ y, ∥f y∥) s :=
-λ x hx, (hf x hx).norm (h0 x hx)
-
-lemma differentiable_on.dist (hf : differentiable_on ℝ f s) (hg : differentiable_on ℝ g s)
-  (hne : ∀ x ∈ s, f x ≠ g x) :
-  differentiable_on ℝ (λ y, dist (f y) (g y)) s :=
-λ x hx, (hf x hx).dist (hg x hx) (hne x hx)
-
-end deriv
-
-section continuous
-
-/-!
-### Continuity of the inner product
-
-Since the inner product is `ℝ`-smooth, it is continuous. We do not need a `[normed_space ℝ E]`
-structure to *state* this fact and its corollaries, so we introduce them in the proof instead.
--/
-
-lemma continuous_inner : continuous (λ p : E × E, ⟪p.1, p.2⟫) :=
-begin
-  letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜 E,
-  letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
-  exact differentiable_inner.continuous
-end
-
-variables {α : Type*}
-
-lemma filter.tendsto.inner {f g : α → E} {l : filter α} {x y : E} (hf : tendsto f l (𝓝 x))
-  (hg : tendsto g l (𝓝 y)) :
-  tendsto (λ t, ⟪f t, g t⟫) l (𝓝 ⟪x, y⟫) :=
-(continuous_inner.tendsto _).comp (hf.prod_mk_nhds hg)
-
-variables [topological_space α] {f g : α → E} {x : α} {s : set α}
-
-include 𝕜
-
-lemma continuous_within_at.inner (hf : continuous_within_at f s x)
-  (hg : continuous_within_at g s x) :
-  continuous_within_at (λ t, ⟪f t, g t⟫) s x :=
-hf.inner hg
-
-lemma continuous_at.inner (hf : continuous_at f x) (hg : continuous_at g x) :
-  continuous_at (λ t, ⟪f t, g t⟫) x :=
-hf.inner hg
-
-lemma continuous_on.inner (hf : continuous_on f s) (hg : continuous_on g s) :
-  continuous_on (λ t, ⟪f t, g t⟫) s :=
-λ x hx, (hf x hx).inner (hg x hx)
-
-lemma continuous.inner (hf : continuous f) (hg : continuous g) : continuous (λ t, ⟪f t, g t⟫) :=
-continuous_iff_continuous_at.2 $ λ x, hf.continuous_at.inner hg.continuous_at
-
-end continuous
-
-/-! ### Orthogonal projection in inner product spaces -/
-
 section orthogonal
-
-open filter
-
-/--
-Existence of minimizers
-Let `u` be a point in a real inner product space, and let `K` be a nonempty complete convex subset.
-Then there exists a (unique) `v` in `K` that minimizes the distance `∥u - v∥` to `u`.
- -/
--- FIXME this monolithic proof causes a deterministic timeout with `-T50000`
--- It should be broken in a sequence of more manageable pieces,
--- perhaps with individual statements for the three steps below.
-theorem exists_norm_eq_infi_of_complete_convex {K : set F} (ne : K.nonempty) (h₁ : is_complete K)
-  (h₂ : convex ℝ K) : ∀ u : F, ∃ v ∈ K, ∥u - v∥ = ⨅ w : K, ∥u - w∥ := assume u,
-begin
-  let δ := ⨅ w : K, ∥u - w∥,
-  letI : nonempty K := ne.to_subtype,
-  have zero_le_δ : 0 ≤ δ := le_cinfi (λ _, norm_nonneg _),
-  have δ_le : ∀ w : K, δ ≤ ∥u - w∥,
-    from cinfi_le ⟨0, set.forall_range_iff.2 $ λ _, norm_nonneg _⟩,
-  have δ_le' : ∀ w ∈ K, δ ≤ ∥u - w∥ := assume w hw, δ_le ⟨w, hw⟩,
-  -- Step 1: since `δ` is the infimum, can find a sequence `w : ℕ → K` in `K`
-  -- such that `∥u - w n∥ < δ + 1 / (n + 1)` (which implies `∥u - w n∥ --> δ`);
-  -- maybe this should be a separate lemma
-  have exists_seq : ∃ w : ℕ → K, ∀ n, ∥u - w n∥ < δ + 1 / (n + 1),
-  { have hδ : ∀n:ℕ, δ < δ + 1 / (n + 1), from
-      λ n, lt_add_of_le_of_pos (le_refl _) nat.one_div_pos_of_nat,
-    have h := λ n, exists_lt_of_cinfi_lt (hδ n),
-    let w : ℕ → K := λ n, classical.some (h n),
-    exact ⟨w, λ n, classical.some_spec (h n)⟩ },
-  rcases exists_seq with ⟨w, hw⟩,
-  have norm_tendsto : tendsto (λ n, ∥u - w n∥) at_top (nhds δ),
-  { have h : tendsto (λ n:ℕ, δ) at_top (nhds δ) := tendsto_const_nhds,
-    have h' : tendsto (λ n:ℕ, δ + 1 / (n + 1)) at_top (nhds δ),
-    { convert h.add tendsto_one_div_add_at_top_nhds_0_nat, simp only [add_zero] },
-    exact tendsto_of_tendsto_of_tendsto_of_le_of_le h h'
-      (λ x, δ_le _) (λ x, le_of_lt (hw _)) },
-  -- Step 2: Prove that the sequence `w : ℕ → K` is a Cauchy sequence
-  have seq_is_cauchy : cauchy_seq (λ n, ((w n):F)),
-  { rw cauchy_seq_iff_le_tendsto_0, -- splits into three goals
-    let b := λ n:ℕ, (8 * δ * (1/(n+1)) + 4 * (1/(n+1)) * (1/(n+1))),
-    use (λn, sqrt (b n)),
-    split,
-    -- first goal :  `∀ (n : ℕ), 0 ≤ sqrt (b n)`
-    assume n, exact sqrt_nonneg _,
-    split,
-    -- second goal : `∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ↑(w n) ↑(w m) ≤ sqrt (b N)`
-    assume p q N hp hq,
-    let wp := ((w p):F), let wq := ((w q):F),
-    let a := u - wq, let b := u - wp,
-    let half := 1 / (2:ℝ), let div := 1 / ((N:ℝ) + 1),
-    have : 4 * ∥u - half • (wq + wp)∥ * ∥u - half • (wq + wp)∥ + ∥wp - wq∥ * ∥wp - wq∥ =
-      2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) :=
-    calc
-      4 * ∥u - half•(wq + wp)∥ * ∥u - half•(wq + wp)∥ + ∥wp - wq∥ * ∥wp - wq∥
-          = (2*∥u - half•(wq + wp)∥) * (2 * ∥u - half•(wq + wp)∥) + ∥wp-wq∥*∥wp-wq∥ : by ring
-      ... = (absR ((2:ℝ)) * ∥u - half•(wq + wp)∥) * (absR ((2:ℝ)) * ∥u - half•(wq+wp)∥) +
-            ∥wp-wq∥*∥wp-wq∥ :
-      by { rw _root_.abs_of_nonneg, exact zero_le_two }
-      ... = ∥(2:ℝ) • (u - half • (wq + wp))∥ * ∥(2:ℝ) • (u - half • (wq + wp))∥ +
-            ∥wp-wq∥ * ∥wp-wq∥ :
-      by simp [norm_smul]
-      ... = ∥a + b∥ * ∥a + b∥ + ∥a - b∥ * ∥a - b∥ :
-      begin
-        rw [smul_sub, smul_smul, mul_one_div_cancel (_root_.two_ne_zero : (2 : ℝ) ≠ 0),
-            ← one_add_one_eq_two, add_smul],
-        simp only [one_smul],
-        have eq₁ : wp - wq = a - b, from (sub_sub_sub_cancel_left _ _ _).symm,
-        have eq₂ : u + u - (wq + wp) = a + b, show u + u - (wq + wp) = (u - wq) + (u - wp), abel,
-        rw [eq₁, eq₂],
-      end
-      ... = 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) : parallelogram_law_with_norm,
-    have eq : δ ≤ ∥u - half • (wq + wp)∥,
-    { rw smul_add,
-      apply δ_le', apply h₂,
-        repeat {exact subtype.mem _},
-        repeat {exact le_of_lt one_half_pos},
-        exact add_halves 1 },
-    have eq₁ : 4 * δ * δ ≤ 4 * ∥u - half • (wq + wp)∥ * ∥u - half • (wq + wp)∥,
-    { mono, mono, norm_num, apply mul_nonneg, norm_num, exact norm_nonneg _ },
-    have eq₂ : ∥a∥ * ∥a∥ ≤ (δ + div) * (δ + div) :=
-      mul_self_le_mul_self (norm_nonneg _)
-        (le_trans (le_of_lt $ hw q) (add_le_add_left (nat.one_div_le_one_div hq) _)),
-    have eq₂' : ∥b∥ * ∥b∥ ≤ (δ + div) * (δ + div) :=
-      mul_self_le_mul_self (norm_nonneg _)
-        (le_trans (le_of_lt $ hw p) (add_le_add_left (nat.one_div_le_one_div hp) _)),
-    rw dist_eq_norm,
-    apply nonneg_le_nonneg_of_sq_le_sq, { exact sqrt_nonneg _ },
-    rw mul_self_sqrt,
-    exact calc
-      ∥wp - wq∥ * ∥wp - wq∥ = 2 * (∥a∥*∥a∥ + ∥b∥*∥b∥) -
-        4 * ∥u - half • (wq+wp)∥ * ∥u - half • (wq+wp)∥ : by { rw ← this, simp }
-      ... ≤ 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) - 4 * δ * δ : sub_le_sub_left eq₁ _
-      ... ≤ 2 * ((δ + div) * (δ + div) + (δ + div) * (δ + div)) - 4 * δ * δ :
-        sub_le_sub_right (mul_le_mul_of_nonneg_left (add_le_add eq₂ eq₂') (by norm_num)) _
-      ... = 8 * δ * div + 4 * div * div : by ring,
-    exact add_nonneg
-      (mul_nonneg (mul_nonneg (by norm_num) zero_le_δ) (le_of_lt nat.one_div_pos_of_nat))
-      (mul_nonneg (mul_nonneg (by norm_num) nat.one_div_pos_of_nat.le) nat.one_div_pos_of_nat.le),
-    -- third goal : `tendsto (λ (n : ℕ), sqrt (b n)) at_top (𝓝 0)`
-    apply tendsto.comp,
-    { convert continuous_sqrt.continuous_at, exact sqrt_zero.symm },
-    have eq₁ : tendsto (λ (n : ℕ), 8 * δ * (1 / (n + 1))) at_top (nhds (0:ℝ)),
-    { convert (@tendsto_const_nhds _ _ _ (8 * δ) _).mul tendsto_one_div_add_at_top_nhds_0_nat,
-      simp only [mul_zero] },
-    have : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1))) at_top (nhds (0:ℝ)),
-    { convert (@tendsto_const_nhds _ _ _ (4:ℝ) _).mul tendsto_one_div_add_at_top_nhds_0_nat,
-      simp only [mul_zero] },
-    have eq₂ : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1)) * (1 / (n + 1))) at_top (nhds (0:ℝ)),
-    { convert this.mul tendsto_one_div_add_at_top_nhds_0_nat,
-      simp only [mul_zero] },
-    convert eq₁.add eq₂, simp only [add_zero] },
-  -- Step 3: By completeness of `K`, let `w : ℕ → K` converge to some `v : K`.
-  -- Prove that it satisfies all requirements.
-  rcases cauchy_seq_tendsto_of_is_complete h₁ (λ n, _) seq_is_cauchy with ⟨v, hv, w_tendsto⟩,
-  use v, use hv,
-  have h_cont : continuous (λ v, ∥u - v∥) :=
-    continuous.comp continuous_norm (continuous.sub continuous_const continuous_id),
-  have : tendsto (λ n, ∥u - w n∥) at_top (nhds ∥u - v∥),
-    convert (tendsto.comp h_cont.continuous_at w_tendsto),
-  exact tendsto_nhds_unique this norm_tendsto,
-  exact subtype.mem _
-end
-
-/-- Characterization of minimizers for the projection on a convex set in a real inner product
-space. -/
-theorem norm_eq_infi_iff_real_inner_le_zero {K : set F} (h : convex ℝ K) {u : F} {v : F}
-  (hv : v ∈ K) : ∥u - v∥ = (⨅ w : K, ∥u - w∥) ↔ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 :=
-iff.intro
-begin
-  assume eq w hw,
-  let δ := ⨅ w : K, ∥u - w∥, let p := ⟪u - v, w - v⟫_ℝ, let q := ∥w - v∥^2,
-  letI : nonempty K := ⟨⟨v, hv⟩⟩,
-  have zero_le_δ : 0 ≤ δ,
-    apply le_cinfi, intro, exact norm_nonneg _,
-  have δ_le : ∀ w : K, δ ≤ ∥u - w∥,
-    assume w, apply cinfi_le, use (0:ℝ), rintros _ ⟨_, rfl⟩, exact norm_nonneg _,
-  have δ_le' : ∀ w ∈ K, δ ≤ ∥u - w∥ := assume w hw, δ_le ⟨w, hw⟩,
-  have : ∀θ:ℝ, 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q,
-    assume θ hθ₁ hθ₂,
-    have : ∥u - v∥^2 ≤ ∥u - v∥^2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ*θ*∥w - v∥^2 :=
-    calc
-      ∥u - v∥^2 ≤ ∥u - (θ•w + (1-θ)•v)∥^2 :
-      begin
-        simp only [sq], apply mul_self_le_mul_self (norm_nonneg _),
-        rw [eq], apply δ_le',
-        apply h hw hv,
-        exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel'_right _ _],
-      end
-      ... = ∥(u - v) - θ • (w - v)∥^2 :
-      begin
-        have : u - (θ•w + (1-θ)•v) = (u - v) - θ • (w - v),
-        { rw [smul_sub, sub_smul, one_smul],
-          simp only [sub_eq_add_neg, add_comm, add_left_comm, add_assoc, neg_add_rev] },
-        rw this
-      end
-      ... = ∥u - v∥^2 - 2 * θ * inner (u - v) (w - v) + θ*θ*∥w - v∥^2 :
-      begin
-        rw [norm_sub_sq, inner_smul_right, norm_smul],
-        simp only [sq],
-        show ∥u-v∥*∥u-v∥-2*(θ*inner(u-v)(w-v))+absR (θ)*∥w-v∥*(absR (θ)*∥w-v∥)=
-                ∥u-v∥*∥u-v∥-2*θ*inner(u-v)(w-v)+θ*θ*(∥w-v∥*∥w-v∥),
-        rw abs_of_pos hθ₁, ring
-      end,
-    have eq₁ : ∥u-v∥^2-2*θ*inner(u-v)(w-v)+θ*θ*∥w-v∥^2=∥u-v∥^2+(θ*θ*∥w-v∥^2-2*θ*inner(u-v)(w-v)),
-      by abel,
-    rw [eq₁, le_add_iff_nonneg_right] at this,
-    have eq₂ : θ*θ*∥w-v∥^2-2*θ*inner(u-v)(w-v)=θ*(θ*∥w-v∥^2-2*inner(u-v)(w-v)), ring,
-    rw eq₂ at this,
-    have := le_of_sub_nonneg (nonneg_of_mul_nonneg_left this hθ₁),
-    exact this,
-  by_cases hq : q = 0,
-  { rw hq at this,
-    have : p ≤ 0,
-      have := this (1:ℝ) (by norm_num) (by norm_num),
-      linarith,
-    exact this },
-  { have q_pos : 0 < q,
-      apply lt_of_le_of_ne, exact sq_nonneg _, intro h, exact hq h.symm,
-    by_contradiction hp, rw not_le at hp,
-    let θ := min (1:ℝ) (p / q),
-    have eq₁ : θ*q ≤ p := calc
-      θ*q ≤ (p/q) * q : mul_le_mul_of_nonneg_right (min_le_right _ _) (sq_nonneg _)
-      ... = p : div_mul_cancel _ hq,
-    have : 2 * p ≤ p := calc
-      2 * p ≤ θ*q : by { refine this θ (lt_min (by norm_num) (div_pos hp q_pos)) (by norm_num) }
-      ... ≤ p : eq₁,
-    linarith }
-end
-begin
-  assume h,
-  letI : nonempty K := ⟨⟨v, hv⟩⟩,
-  apply le_antisymm,
-  { apply le_cinfi, assume w,
-    apply nonneg_le_nonneg_of_sq_le_sq (norm_nonneg _),
-    have := h w w.2,
-    exact calc
-      ∥u - v∥ * ∥u - v∥ ≤ ∥u - v∥ * ∥u - v∥ - 2 * inner (u - v) ((w:F) - v) : by linarith
-      ... ≤ ∥u - v∥^2 - 2 * inner (u - v) ((w:F) - v) + ∥(w:F) - v∥^2 :
-        by { rw sq, refine le_add_of_nonneg_right _, exact sq_nonneg _ }
-      ... = ∥(u - v) - (w - v)∥^2 : norm_sub_sq.symm
-      ... = ∥u - w∥ * ∥u - w∥ :
-        by { have : (u - v) - (w - v) = u - w, abel, rw [this, sq] } },
-  { show (⨅ (w : K), ∥u - w∥) ≤ (λw:K, ∥u - w∥) ⟨v, hv⟩,
-      apply cinfi_le, use 0, rintros y ⟨z, rfl⟩, exact norm_nonneg _ }
-end
-
 variables (K : submodule 𝕜 E)
 
-/--
-Existence of projections on complete subspaces.
-Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace.
-Then there exists a (unique) `v` in `K` that minimizes the distance `∥u - v∥` to `u`.
-This point `v` is usually called the orthogonal projection of `u` onto `K`.
--/
-theorem exists_norm_eq_infi_of_complete_subspace
-  (h : is_complete (↑K : set E)) : ∀ u : E, ∃ v ∈ K, ∥u - v∥ = ⨅ w : (K : set E), ∥u - w∥ :=
-begin
-  letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜 E,
-  letI : module ℝ E := restrict_scalars.module ℝ 𝕜 E,
-  letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
-  let K' : submodule ℝ E := submodule.restrict_scalars ℝ K,
-  exact exists_norm_eq_infi_of_complete_convex ⟨0, K'.zero_mem⟩ h K'.convex
-end
-
-/--
-Characterization of minimizers in the projection on a subspace, in the real case.
-Let `u` be a point in a real inner product space, and let `K` be a nonempty subspace.
-Then point `v` minimizes the distance `∥u - v∥` over points in `K` if and only if
-for all `w ∈ K`, `⟪u - v, w⟫ = 0` (i.e., `u - v` is orthogonal to the subspace `K`).
-This is superceded by `norm_eq_infi_iff_inner_eq_zero` that gives the same conclusion over
-any `is_R_or_C` field.
--/
-theorem norm_eq_infi_iff_real_inner_eq_zero (K : submodule ℝ F) {u : F} {v : F}
-  (hv : v ∈ K) : ∥u - v∥ = (⨅ w : (↑K : set F), ∥u - w∥) ↔ ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0 :=
-iff.intro
-begin
-  assume h,
-  have h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0,
-  { rwa [norm_eq_infi_iff_real_inner_le_zero] at h, exacts [K.convex, hv] },
-  assume w hw,
-  have le : ⟪u - v, w⟫_ℝ ≤ 0,
-    let w' := w + v,
-    have : w' ∈ K := submodule.add_mem _ hw hv,
-    have h₁ := h w' this,
-    have h₂ : w' - v = w, simp only [add_neg_cancel_right, sub_eq_add_neg],
-    rw h₂ at h₁, exact h₁,
-  have ge : ⟪u - v, w⟫_ℝ ≥ 0,
-    let w'' := -w + v,
-    have : w'' ∈ K := submodule.add_mem _ (submodule.neg_mem _ hw) hv,
-    have h₁ := h w'' this,
-    have h₂ : w'' - v = -w, simp only [neg_inj, add_neg_cancel_right, sub_eq_add_neg],
-    rw [h₂, inner_neg_right] at h₁,
-    linarith,
-    exact le_antisymm le ge
-end
-begin
-  assume h,
-  have : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0,
-    assume w hw,
-    let w' := w - v,
-    have : w' ∈ K := submodule.sub_mem _ hw hv,
-    have h₁ := h w' this,
-    exact le_of_eq h₁,
-  rwa norm_eq_infi_iff_real_inner_le_zero,
-  exacts [submodule.convex _, hv]
-end
-
-/--
-Characterization of minimizers in the projection on a subspace.
-Let `u` be a point in an inner product space, and let `K` be a nonempty subspace.
-Then point `v` minimizes the distance `∥u - v∥` over points in `K` if and only if
-for all `w ∈ K`, `⟪u - v, w⟫ = 0` (i.e., `u - v` is orthogonal to the subspace `K`)
--/
-theorem norm_eq_infi_iff_inner_eq_zero {u : E} {v : E}
-  (hv : v ∈ K) : ∥u - v∥ = (⨅ w : (↑K : set E), ∥u - w∥) ↔ ∀ w ∈ K, ⟪u - v, w⟫ = 0 :=
-begin
-  letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜 E,
-  letI : module ℝ E := restrict_scalars.module ℝ 𝕜 E,
-  letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
-  let K' : submodule ℝ E := K.restrict_scalars ℝ,
-  split,
-  { assume H,
-    have A : ∀ w ∈ K, re ⟪u - v, w⟫ = 0 := (norm_eq_infi_iff_real_inner_eq_zero K' hv).1 H,
-    assume w hw,
-    apply ext,
-    { simp [A w hw] },
-    { symmetry, calc
-      im (0 : 𝕜) = 0 : im.map_zero
-      ... = re ⟪u - v, (-I) • w⟫ : (A _ (K.smul_mem (-I) hw)).symm
-      ... = re ((-I) * ⟪u - v, w⟫) : by rw inner_smul_right
-      ... = im ⟪u - v, w⟫ : by simp } },
-  { assume H,
-    have : ∀ w ∈ K', ⟪u - v, w⟫_ℝ = 0,
-    { assume w hw,
-      rw [real_inner_eq_re_inner, H w hw],
-      exact zero_re' },
-    exact (norm_eq_infi_iff_real_inner_eq_zero K' hv).2 this }
-end
-
-section orthogonal_projection
-variables [complete_space K]
-
-/-- The orthogonal projection onto a complete subspace, as an
-unbundled function.  This definition is only intended for use in
-setting up the bundled version `orthogonal_projection` and should not
-be used once that is defined. -/
-def orthogonal_projection_fn (v : E) :=
-(exists_norm_eq_infi_of_complete_subspace K (complete_space_coe_iff_is_complete.mp ‹_›) v).some
-
-variables {K}
-
-/-- The unbundled orthogonal projection is in the given subspace.
-This lemma is only intended for use in setting up the bundled version
-and should not be used once that is defined. -/
-lemma orthogonal_projection_fn_mem (v : E) : orthogonal_projection_fn K v ∈ K :=
-(exists_norm_eq_infi_of_complete_subspace K
-  (complete_space_coe_iff_is_complete.mp ‹_›) v).some_spec.some
-
-/-- The characterization of the unbundled orthogonal projection.  This
-lemma is only intended for use in setting up the bundled version
-and should not be used once that is defined. -/
-lemma orthogonal_projection_fn_inner_eq_zero (v : E) :
-  ∀ w ∈ K, ⟪v - orthogonal_projection_fn K v, w⟫ = 0 :=
-begin
-  rw ←norm_eq_infi_iff_inner_eq_zero K (orthogonal_projection_fn_mem v),
-  exact (exists_norm_eq_infi_of_complete_subspace K
-    (complete_space_coe_iff_is_complete.mp ‹_›) v).some_spec.some_spec
-end
-
-/-- The unbundled orthogonal projection is the unique point in `K`
-with the orthogonality property.  This lemma is only intended for use
-in setting up the bundled version and should not be used once that is
-defined. -/
-lemma eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero
-  {u v : E} (hvm : v ∈ K) (hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0) :
-  orthogonal_projection_fn K u = v :=
-begin
-  rw [←sub_eq_zero, ←inner_self_eq_zero],
-  have hvs : orthogonal_projection_fn K u - v ∈ K :=
-    submodule.sub_mem K (orthogonal_projection_fn_mem u) hvm,
-  have huo : ⟪u - orthogonal_projection_fn K u, orthogonal_projection_fn K u - v⟫ = 0 :=
-    orthogonal_projection_fn_inner_eq_zero u _ hvs,
-  have huv : ⟪u - v, orthogonal_projection_fn K u - v⟫ = 0 := hvo _ hvs,
-  have houv : ⟪(u - v) - (u - orthogonal_projection_fn K u), orthogonal_projection_fn K u - v⟫ = 0,
-  { rw [inner_sub_left, huo, huv, sub_zero] },
-  rwa sub_sub_sub_cancel_left at houv
-end
-
-variables (K)
-
-lemma orthogonal_projection_fn_norm_sq (v : E) :
-  ∥v∥ * ∥v∥ = ∥v - (orthogonal_projection_fn K v)∥ * ∥v - (orthogonal_projection_fn K v)∥
-            + ∥orthogonal_projection_fn K v∥ * ∥orthogonal_projection_fn K v∥ :=
-begin
-  set p := orthogonal_projection_fn K v,
-  have h' : ⟪v - p, p⟫ = 0,
-  { exact orthogonal_projection_fn_inner_eq_zero _ _ (orthogonal_projection_fn_mem v) },
-  convert norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (v - p) p h' using 2;
-  simp,
-end
-
-/-- The orthogonal projection onto a complete subspace. -/
-def orthogonal_projection : E →L[𝕜] K :=
-linear_map.mk_continuous
-  { to_fun := λ v, ⟨orthogonal_projection_fn K v, orthogonal_projection_fn_mem v⟩,
-    map_add' := λ x y, begin
-      have hm : orthogonal_projection_fn K x + orthogonal_projection_fn K y ∈ K :=
-        submodule.add_mem K (orthogonal_projection_fn_mem x) (orthogonal_projection_fn_mem y),
-      have ho :
-        ∀ w ∈ K, ⟪x + y - (orthogonal_projection_fn K x + orthogonal_projection_fn K y), w⟫ = 0,
-      { intros w hw,
-        rw [add_sub_comm, inner_add_left, orthogonal_projection_fn_inner_eq_zero _ w hw,
-            orthogonal_projection_fn_inner_eq_zero _ w hw, add_zero] },
-      ext,
-      simp [eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero hm ho]
-    end,
-    map_smul' := λ c x, begin
-      have hm : c • orthogonal_projection_fn K x ∈ K :=
-        submodule.smul_mem K _ (orthogonal_projection_fn_mem x),
-      have ho : ∀ w ∈ K, ⟪c • x - c • orthogonal_projection_fn K x, w⟫ = 0,
-      { intros w hw,
-        rw [←smul_sub, inner_smul_left, orthogonal_projection_fn_inner_eq_zero _ w hw, mul_zero] },
-      ext,
-      simp [eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero hm ho]
-    end }
-  1
-  (λ x, begin
-    simp only [one_mul, linear_map.coe_mk],
-    refine le_of_pow_le_pow 2 (norm_nonneg _) (by norm_num) _,
-    change ∥orthogonal_projection_fn K x∥ ^ 2 ≤ ∥x∥ ^ 2,
-    nlinarith [orthogonal_projection_fn_norm_sq K x]
-  end)
-
-variables {K}
-
-@[simp]
-lemma orthogonal_projection_fn_eq (v : E) :
-  orthogonal_projection_fn K v = (orthogonal_projection K v : E) :=
-rfl
-
-/-- The characterization of the orthogonal projection.  -/
-@[simp]
-lemma orthogonal_projection_inner_eq_zero (v : E) :
-  ∀ w ∈ K, ⟪v - orthogonal_projection K v, w⟫ = 0 :=
-orthogonal_projection_fn_inner_eq_zero v
-
-/-- The orthogonal projection is the unique point in `K` with the
-orthogonality property. -/
-lemma eq_orthogonal_projection_of_mem_of_inner_eq_zero
-  {u v : E} (hvm : v ∈ K) (hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0) :
-  (orthogonal_projection K u : E) = v :=
-eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero hvm hvo
-
-/-- The orthogonal projections onto equal subspaces are coerced back to the same point in `E`. -/
-lemma eq_orthogonal_projection_of_eq_submodule
-  {K' : submodule 𝕜 E} [complete_space K'] (h : K = K') (u : E) :
-  (orthogonal_projection K u : E) = (orthogonal_projection K' u : E) :=
-begin
-  change orthogonal_projection_fn K u = orthogonal_projection_fn K' u,
-  congr,
-  exact h
-end
-
-/-- The orthogonal projection sends elements of `K` to themselves. -/
-@[simp] lemma orthogonal_projection_mem_subspace_eq_self (v : K) : orthogonal_projection K v = v :=
-by { ext, apply eq_orthogonal_projection_of_mem_of_inner_eq_zero; simp }
-
-/-- A point equals its orthogonal projection if and only if it lies in the subspace. -/
-lemma orthogonal_projection_eq_self_iff {v : E} :
-  (orthogonal_projection K v : E) = v ↔ v ∈ K :=
-begin
-  refine ⟨λ h, _, λ h, eq_orthogonal_projection_of_mem_of_inner_eq_zero h _⟩,
-  { rw ← h,
-    simp },
-  { simp }
-end
-
-/-- Orthogonal projection onto the `submodule.map` of a subspace. -/
-lemma orthogonal_projection_map_apply {E E' : Type*} [inner_product_space 𝕜 E]
-  [inner_product_space 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (p : submodule 𝕜 E) [finite_dimensional 𝕜 p]
-  (x : E') :
-  (orthogonal_projection (p.map (f.to_linear_equiv : E →ₗ[𝕜] E')) x : E')
-  = f (orthogonal_projection p (f.symm x)) :=
-begin
-  apply eq_orthogonal_projection_of_mem_of_inner_eq_zero,
-  { exact ⟨orthogonal_projection p (f.symm x), submodule.coe_mem _, by simp⟩, },
-  rintros w ⟨a, ha, rfl⟩,
-  suffices : inner (f (f.symm x - orthogonal_projection p (f.symm x))) (f a) = (0:𝕜),
-  { simpa using this },
-  rw f.inner_map_map,
-  exact orthogonal_projection_inner_eq_zero _ _ ha,
-end
-
-/-- The orthogonal projection onto the trivial submodule is the zero map. -/
-@[simp] lemma orthogonal_projection_bot : orthogonal_projection (⊥ : submodule 𝕜 E) = 0 :=
-by ext
-
-variables (K)
-
-/-- The orthogonal projection has norm `≤ 1`. -/
-lemma orthogonal_projection_norm_le : ∥orthogonal_projection K∥ ≤ 1 :=
-linear_map.mk_continuous_norm_le _ (by norm_num) _
-
-variables (𝕜)
-
-lemma smul_orthogonal_projection_singleton {v : E} (w : E) :
-  (∥v∥ ^ 2 : 𝕜) • (orthogonal_projection (𝕜 ∙ v) w : E) = ⟪v, w⟫ • v :=
-begin
-  suffices : ↑(orthogonal_projection (𝕜 ∙ v) ((∥v∥ ^ 2 : 𝕜) • w)) = ⟪v, w⟫ • v,
-  { simpa using this },
-  apply eq_orthogonal_projection_of_mem_of_inner_eq_zero,
-  { rw submodule.mem_span_singleton,
-    use ⟪v, w⟫ },
-  { intros x hx,
-    obtain ⟨c, rfl⟩ := submodule.mem_span_singleton.mp hx,
-    have hv : ↑∥v∥ ^ 2 = ⟪v, v⟫ := by { norm_cast, simp [norm_sq_eq_inner] },
-    simp [inner_sub_left, inner_smul_left, inner_smul_right, is_R_or_C.conj_div, mul_comm, hv,
-      inner_product_space.conj_sym, hv] }
-end
-
-/-- Formula for orthogonal projection onto a single vector. -/
-lemma orthogonal_projection_singleton {v : E} (w : E) :
-  (orthogonal_projection (𝕜 ∙ v) w : E) = (⟪v, w⟫ / ∥v∥ ^ 2) • v :=
-begin
-  by_cases hv : v = 0,
-  { rw [hv, eq_orthogonal_projection_of_eq_submodule submodule.span_zero_singleton],
-    { simp },
-    { apply_instance } },
-  have hv' : ∥v∥ ≠ 0 := ne_of_gt (norm_pos_iff.mpr hv),
-  have key : ((∥v∥ ^ 2 : 𝕜)⁻¹ * ∥v∥ ^ 2) • ↑(orthogonal_projection (𝕜 ∙ v) w)
-              = ((∥v∥ ^ 2 : 𝕜)⁻¹ * ⟪v, w⟫) • v,
-  { simp [mul_smul, smul_orthogonal_projection_singleton 𝕜 w] },
-  convert key;
-  field_simp [hv']
-end
-
-/-- Formula for orthogonal projection onto a single unit vector. -/
-lemma orthogonal_projection_unit_singleton {v : E} (hv : ∥v∥ = 1) (w : E) :
-  (orthogonal_projection (𝕜 ∙ v) w : E) = ⟪v, w⟫ • v :=
-by { rw ← smul_orthogonal_projection_singleton 𝕜 w, simp [hv] }
-
-end orthogonal_projection
-
-section reflection
-variables {𝕜} (K) [complete_space K]
-
-/-- Reflection in a complete subspace of an inner product space.  The word "reflection" is
-sometimes understood to mean specifically reflection in a codimension-one subspace, and sometimes
-more generally to cover operations such as reflection in a point.  The definition here, of
-reflection in a subspace, is a more general sense of the word that includes both those common
-cases. -/
-def reflection : E ≃ₗᵢ[𝕜] E :=
-{ norm_map' := begin
-    intros x,
-    let w : K := orthogonal_projection K x,
-    let v := x - w,
-    have : ⟪v, w⟫ = 0 := orthogonal_projection_inner_eq_zero x w w.2,
-    convert norm_sub_eq_norm_add this using 2,
-    { simp [bit0],
-      dsimp [w, v],
-      abel },
-    { simp [bit0] }
-  end,
-  ..linear_equiv.of_involutive
-      (bit0 (K.subtype.comp (orthogonal_projection K).to_linear_map) - linear_map.id)
-      (λ x, by simp [bit0]) }
-
-variables {K}
-
-/-- The result of reflecting. -/
-lemma reflection_apply (p : E) : reflection K p = bit0 ↑(orthogonal_projection K p) - p := rfl
-
-/-- Reflection is its own inverse. -/
-@[simp] lemma reflection_symm : (reflection K).symm = reflection K := rfl
-
-variables (K)
-
-/-- Reflecting twice in the same subspace. -/
-@[simp] lemma reflection_reflection (p : E) : reflection K (reflection K p) = p :=
-(reflection K).left_inv p
-
-/-- Reflection is involutive. -/
-lemma reflection_involutive : function.involutive (reflection K) := reflection_reflection K
-
-variables {K}
-
-/-- A point is its own reflection if and only if it is in the subspace. -/
-lemma reflection_eq_self_iff (x : E) : reflection K x = x ↔ x ∈ K :=
-begin
-  rw [←orthogonal_projection_eq_self_iff, reflection_apply, sub_eq_iff_eq_add', ← two_smul 𝕜,
-    ← two_smul' 𝕜],
-  refine (smul_right_injective E _).eq_iff,
-  exact two_ne_zero
-end
-
-lemma reflection_mem_subspace_eq_self {x : E} (hx : x ∈ K) : reflection K x = x :=
-(reflection_eq_self_iff x).mpr hx
-
-/-- Reflection in the `submodule.map` of a subspace. -/
-lemma reflection_map_apply {E E' : Type*} [inner_product_space 𝕜 E] [inner_product_space 𝕜 E']
-  (f : E ≃ₗᵢ[𝕜] E') (K : submodule 𝕜 E) [finite_dimensional 𝕜 K] (x : E') :
-  reflection (K.map (f.to_linear_equiv : E →ₗ[𝕜] E')) x = f (reflection K (f.symm x)) :=
-by simp [bit0, reflection_apply, orthogonal_projection_map_apply f K x]
-
-/-- Reflection in the `submodule.map` of a subspace. -/
-lemma reflection_map {E E' : Type*} [inner_product_space 𝕜 E] [inner_product_space 𝕜 E']
-  (f : E ≃ₗᵢ[𝕜] E') (K : submodule 𝕜 E) [finite_dimensional 𝕜 K] :
-  reflection (K.map (f.to_linear_equiv : E →ₗ[𝕜] E')) = f.symm.trans ((reflection K).trans f) :=
-linear_isometry_equiv.ext $ reflection_map_apply f K
-
-/-- Reflection through the trivial subspace {0} is just negation. -/
-@[simp] lemma reflection_bot : reflection (⊥ : submodule 𝕜 E) = linear_isometry_equiv.neg 𝕜 :=
-by ext; simp [reflection_apply]
-
-end reflection
-
 /-- The subspace of vectors orthogonal to a given subspace. -/
 def submodule.orthogonal : submodule 𝕜 E :=
 { carrier := {v | ∀ u ∈ K, ⟪u, v⟫ = 0},
@@ -2474,78 +1619,6 @@ lemma submodule.infi_orthogonal {ι : Type*} (K : ι → submodule 𝕜 E) : (
 lemma submodule.Inf_orthogonal (s : set $ submodule 𝕜 E) : (⨅ K ∈ s, Kᗮ) = (Sup s)ᗮ :=
 (submodule.orthogonal_gc 𝕜 E).l_Sup.symm
 
-/-- If `K₁` is complete and contained in `K₂`, `K₁` and `K₁ᗮ ⊓ K₂` span `K₂`. -/
-lemma submodule.sup_orthogonal_inf_of_is_complete {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂)
-  (hc : is_complete (K₁ : set E)) : K₁ ⊔ (K₁ᗮ ⊓ K₂) = K₂ :=
-begin
-  ext x,
-  rw submodule.mem_sup,
-  rcases exists_norm_eq_infi_of_complete_subspace K₁ hc x with ⟨v, hv, hvm⟩,
-  rw norm_eq_infi_iff_inner_eq_zero K₁ hv at hvm,
-  split,
-  { rintro ⟨y, hy, z, hz, rfl⟩,
-    exact K₂.add_mem (h hy) hz.2 },
-  { exact λ hx, ⟨v, hv, x - v, ⟨(K₁.mem_orthogonal' _).2 hvm, K₂.sub_mem hx (h hv)⟩,
-                 add_sub_cancel'_right _ _⟩ }
-end
-
-variables {K}
-
-/-- If `K` is complete, `K` and `Kᗮ` span the whole space. -/
-lemma submodule.sup_orthogonal_of_is_complete (h : is_complete (K : set E)) : K ⊔ Kᗮ = ⊤ :=
-begin
-  convert submodule.sup_orthogonal_inf_of_is_complete (le_top : K ≤ ⊤) h,
-  simp
-end
-
-/-- If `K` is complete, `K` and `Kᗮ` span the whole space. Version using `complete_space`. -/
-lemma submodule.sup_orthogonal_of_complete_space [complete_space K] : K ⊔ Kᗮ = ⊤ :=
-submodule.sup_orthogonal_of_is_complete (complete_space_coe_iff_is_complete.mp ‹_›)
-
-variables (K)
-
-/-- If `K` is complete, any `v` in `E` can be expressed as a sum of elements of `K` and `Kᗮ`. -/
-lemma submodule.exists_sum_mem_mem_orthogonal [complete_space K] (v : E) :
-  ∃ (y ∈ K) (z ∈ Kᗮ), v = y + z :=
-begin
-  have h_mem : v ∈ K ⊔ Kᗮ := by simp [submodule.sup_orthogonal_of_complete_space],
-  obtain ⟨y, hy, z, hz, hyz⟩ := submodule.mem_sup.mp h_mem,
-  exact ⟨y, hy, z, hz, hyz.symm⟩
-end
-
-/-- If `K` is complete, then the orthogonal complement of its orthogonal complement is itself. -/
-@[simp] lemma submodule.orthogonal_orthogonal [complete_space K] : Kᗮᗮ = K :=
-begin
-  ext v,
-  split,
-  { obtain ⟨y, hy, z, hz, rfl⟩ := K.exists_sum_mem_mem_orthogonal v,
-    intros hv,
-    have hz' : z = 0,
-    { have hyz : ⟪z, y⟫ = 0 := by simp [hz y hy, inner_eq_zero_sym],
-      simpa [inner_add_right, hyz] using hv z hz },
-    simp [hy, hz'] },
-  { intros hv w hw,
-    rw inner_eq_zero_sym,
-    exact hw v hv }
-end
-
-lemma submodule.orthogonal_orthogonal_eq_closure [complete_space E] :
-  Kᗮᗮ = K.topological_closure :=
-begin
-  refine le_antisymm _ _,
-  { convert submodule.orthogonal_orthogonal_monotone K.submodule_topological_closure,
-    haveI : complete_space K.topological_closure :=
-      K.is_closed_topological_closure.complete_space_coe,
-    rw K.topological_closure.orthogonal_orthogonal },
-  { exact K.topological_closure_minimal K.le_orthogonal_orthogonal Kᗮ.is_closed_orthogonal }
-end
-
-variables {K}
-
-/-- If `K` is complete, `K` and `Kᗮ` are complements of each other. -/
-lemma submodule.is_compl_orthogonal_of_is_complete (h : is_complete (K : set E)) : is_compl K Kᗮ :=
-⟨K.orthogonal_disjoint, le_of_eq (submodule.sup_orthogonal_of_is_complete h).symm⟩
-
 @[simp] lemma submodule.top_orthogonal_eq_bot : (⊤ : submodule 𝕜 E)ᗮ = ⊥ :=
 begin
   ext,
@@ -2559,15 +1632,6 @@ begin
   exact submodule.le_orthogonal_orthogonal ⊤
 end
 
-@[simp] lemma submodule.orthogonal_eq_bot_iff (hK : is_complete (K : set E)) :
-  Kᗮ = ⊥ ↔ K = ⊤ :=
-begin
-  refine ⟨_, by { rintro rfl, exact submodule.top_orthogonal_eq_bot }⟩,
-  intro h,
-  have : K ⊔ Kᗮ = ⊤ := submodule.sup_orthogonal_of_is_complete hK,
-  rwa [h, sup_comm, bot_sup_eq] at this,
-end
-
 @[simp] lemma submodule.orthogonal_eq_top_iff : Kᗮ = ⊤ ↔ K = ⊥ :=
 begin
   refine ⟨_, by { rintro rfl, exact submodule.bot_orthogonal_eq_top }⟩,
@@ -2576,310 +1640,4 @@ begin
   rwa [h, inf_comm, top_inf_eq] at this
 end
 
-/-- A point in `K` with the orthogonality property (here characterized in terms of `Kᗮ`) must be the
-orthogonal projection. -/
-lemma eq_orthogonal_projection_of_mem_orthogonal
-  [complete_space K] {u v : E} (hv : v ∈ K) (hvo : u - v ∈ Kᗮ) :
-  (orthogonal_projection K u : E) = v :=
-eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero hv (λ w, inner_eq_zero_sym.mp ∘ (hvo w))
-
-/-- A point in `K` with the orthogonality property (here characterized in terms of `Kᗮ`) must be the
-orthogonal projection. -/
-lemma eq_orthogonal_projection_of_mem_orthogonal'
-  [complete_space K] {u v z : E} (hv : v ∈ K) (hz : z ∈ Kᗮ) (hu : u = v + z) :
-  (orthogonal_projection K u : E) = v :=
-eq_orthogonal_projection_of_mem_orthogonal hv (by simpa [hu])
-
-/-- The orthogonal projection onto `K` of an element of `Kᗮ` is zero. -/
-lemma orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero
-  [complete_space K] {v : E} (hv : v ∈ Kᗮ) :
-  orthogonal_projection K v = 0 :=
-by { ext, convert eq_orthogonal_projection_of_mem_orthogonal _ _; simp [hv] }
-
-/-- The reflection in `K` of an element of `Kᗮ` is its negation. -/
-lemma reflection_mem_subspace_orthogonal_complement_eq_neg
-  [complete_space K] {v : E} (hv : v ∈ Kᗮ) :
-  reflection K v = - v :=
-by simp [reflection_apply, orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero hv]
-
-/-- The orthogonal projection onto `Kᗮ` of an element of `K` is zero. -/
-lemma orthogonal_projection_mem_subspace_orthogonal_precomplement_eq_zero
-  [complete_space E] {v : E} (hv : v ∈ K) :
-  orthogonal_projection Kᗮ v = 0 :=
-orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero (K.le_orthogonal_orthogonal hv)
-
-/-- The reflection in `Kᗮ` of an element of `K` is its negation. -/
-lemma reflection_mem_subspace_orthogonal_precomplement_eq_neg
-  [complete_space E] {v : E} (hv : v ∈ K) :
-  reflection Kᗮ v = -v :=
-reflection_mem_subspace_orthogonal_complement_eq_neg (K.le_orthogonal_orthogonal hv)
-
-/-- The orthogonal projection onto `(𝕜 ∙ v)ᗮ` of `v` is zero. -/
-lemma orthogonal_projection_orthogonal_complement_singleton_eq_zero [complete_space E] (v : E) :
-  orthogonal_projection (𝕜 ∙ v)ᗮ v = 0 :=
-orthogonal_projection_mem_subspace_orthogonal_precomplement_eq_zero
-  (submodule.mem_span_singleton_self v)
-
-/-- The reflection in `(𝕜 ∙ v)ᗮ` of `v` is `-v`. -/
-lemma reflection_orthogonal_complement_singleton_eq_neg [complete_space E] (v : E) :
-  reflection (𝕜 ∙ v)ᗮ v = -v :=
-reflection_mem_subspace_orthogonal_precomplement_eq_neg (submodule.mem_span_singleton_self v)
-
-variables (K)
-
-/-- In a complete space `E`, a vector splits as the sum of its orthogonal projections onto a
-complete submodule `K` and onto the orthogonal complement of `K`.-/
-lemma eq_sum_orthogonal_projection_self_orthogonal_complement
-  [complete_space E] [complete_space K] (w : E) :
-  w = (orthogonal_projection K w : E) + (orthogonal_projection Kᗮ w : E) :=
-begin
-  obtain ⟨y, hy, z, hz, hwyz⟩ := K.exists_sum_mem_mem_orthogonal w,
-  convert hwyz,
-  { exact eq_orthogonal_projection_of_mem_orthogonal' hy hz hwyz },
-  { rw add_comm at hwyz,
-    refine eq_orthogonal_projection_of_mem_orthogonal' hz _ hwyz,
-    simp [hy] }
-end
-
-/-- In a complete space `E`, the projection maps onto a complete subspace `K` and its orthogonal
-complement sum to the identity. -/
-lemma id_eq_sum_orthogonal_projection_self_orthogonal_complement
-  [complete_space E] [complete_space K] :
-  continuous_linear_map.id 𝕜 E
-  = K.subtypeL.comp (orthogonal_projection K)
-  + Kᗮ.subtypeL.comp (orthogonal_projection Kᗮ) :=
-by { ext w, exact eq_sum_orthogonal_projection_self_orthogonal_complement K w }
-
-/-- The orthogonal projection is self-adjoint. -/
-lemma inner_orthogonal_projection_left_eq_right [complete_space E]
-  [complete_space K] (u v : E) :
-  ⟪↑(orthogonal_projection K u), v⟫ = ⟪u, orthogonal_projection K v⟫ :=
-begin
-  nth_rewrite 0 eq_sum_orthogonal_projection_self_orthogonal_complement K v,
-  nth_rewrite 1 eq_sum_orthogonal_projection_self_orthogonal_complement K u,
-  rw [inner_add_left, inner_add_right,
-    submodule.inner_right_of_mem_orthogonal (submodule.coe_mem (orthogonal_projection K u))
-      (submodule.coe_mem (orthogonal_projection Kᗮ v)),
-    submodule.inner_left_of_mem_orthogonal (submodule.coe_mem (orthogonal_projection K v))
-      (submodule.coe_mem (orthogonal_projection Kᗮ u))],
-end
-
-open finite_dimensional
-
-/-- Given a finite-dimensional subspace `K₂`, and a subspace `K₁`
-containined in it, the dimensions of `K₁` and the intersection of its
-orthogonal subspace with `K₂` add to that of `K₂`. -/
-lemma submodule.finrank_add_inf_finrank_orthogonal {K₁ K₂ : submodule 𝕜 E}
-  [finite_dimensional 𝕜 K₂] (h : K₁ ≤ K₂) :
-  finrank 𝕜 K₁ + finrank 𝕜 (K₁ᗮ ⊓ K₂ : submodule 𝕜 E) = finrank 𝕜 K₂ :=
-begin
-  haveI := submodule.finite_dimensional_of_le h,
-  have hd := submodule.dim_sup_add_dim_inf_eq K₁ (K₁ᗮ ⊓ K₂),
-  rw [←inf_assoc, (submodule.orthogonal_disjoint K₁).eq_bot, bot_inf_eq, finrank_bot,
-      submodule.sup_orthogonal_inf_of_is_complete h
-        (submodule.complete_of_finite_dimensional _)] at hd,
-  rw add_zero at hd,
-  exact hd.symm
-end
-
-/-- Given a finite-dimensional subspace `K₂`, and a subspace `K₁`
-containined in it, the dimensions of `K₁` and the intersection of its
-orthogonal subspace with `K₂` add to that of `K₂`. -/
-lemma submodule.finrank_add_inf_finrank_orthogonal' {K₁ K₂ : submodule 𝕜 E}
-  [finite_dimensional 𝕜 K₂] (h : K₁ ≤ K₂) {n : ℕ} (h_dim : finrank 𝕜 K₁ + n = finrank 𝕜 K₂) :
-  finrank 𝕜 (K₁ᗮ ⊓ K₂ : submodule 𝕜 E) = n :=
-by { rw ← add_right_inj (finrank 𝕜 K₁),
-     simp [submodule.finrank_add_inf_finrank_orthogonal h, h_dim] }
-
-/-- Given a finite-dimensional space `E` and subspace `K`, the dimensions of `K` and `Kᗮ` add to
-that of `E`. -/
-lemma submodule.finrank_add_finrank_orthogonal [finite_dimensional 𝕜 E] {K : submodule 𝕜 E} :
-  finrank 𝕜 K + finrank 𝕜 Kᗮ = finrank 𝕜 E :=
-begin
-  convert submodule.finrank_add_inf_finrank_orthogonal (le_top : K ≤ ⊤) using 1,
-  { rw inf_top_eq },
-  { simp }
-end
-
-/-- Given a finite-dimensional space `E` and subspace `K`, the dimensions of `K` and `Kᗮ` add to
-that of `E`. -/
-lemma submodule.finrank_add_finrank_orthogonal' [finite_dimensional 𝕜 E] {K : submodule 𝕜 E} {n : ℕ}
-  (h_dim : finrank 𝕜 K + n = finrank 𝕜 E) :
-  finrank 𝕜 Kᗮ = n :=
-by { rw ← add_right_inj (finrank 𝕜 K), simp [submodule.finrank_add_finrank_orthogonal, h_dim] }
-
-local attribute [instance] fact_finite_dimensional_of_finrank_eq_succ
-
-/-- In a finite-dimensional inner product space, the dimension of the orthogonal complement of the
-span of a nonzero vector is one less than the dimension of the space. -/
-lemma finrank_orthogonal_span_singleton {n : ℕ} [_i : fact (finrank 𝕜 E = n + 1)]
-  {v : E} (hv : v ≠ 0) :
-  finrank 𝕜 (𝕜 ∙ v)ᗮ = n :=
-submodule.finrank_add_finrank_orthogonal' $ by simp [finrank_span_singleton hv, _i.elim, add_comm]
-
 end orthogonal
-
-section orthonormal_basis
-
-/-! ### Existence of Hilbert basis, orthonormal basis, etc. -/
-
-variables {𝕜 E} {v : set E}
-
-open finite_dimensional submodule set
-
-/-- An orthonormal set in an `inner_product_space` is maximal, if and only if the orthogonal
-complement of its span is empty. -/
-lemma maximal_orthonormal_iff_orthogonal_complement_eq_bot (hv : orthonormal 𝕜 (coe : v → E)) :
-  (∀ u ⊇ v, orthonormal 𝕜 (coe : u → E) → u = v) ↔ (span 𝕜 v)ᗮ = ⊥ :=
-begin
-  rw submodule.eq_bot_iff,
-  split,
-  { contrapose!,
-    -- ** direction 1: nonempty orthogonal complement implies nonmaximal
-    rintros ⟨x, hx', hx⟩,
-    -- take a nonzero vector and normalize it
-    let e := (∥x∥⁻¹ : 𝕜) • x,
-    have he : ∥e∥ = 1 := by simp [e, norm_smul_inv_norm hx],
-    have he' : e ∈ (span 𝕜 v)ᗮ := smul_mem' _ _ hx',
-    have he'' : e ∉ v,
-    { intros hev,
-      have : e = 0,
-      { have : e ∈ (span 𝕜 v) ⊓ (span 𝕜 v)ᗮ := ⟨subset_span hev, he'⟩,
-        simpa [(span 𝕜 v).inf_orthogonal_eq_bot] using this },
-      have : e ≠ 0 := hv.ne_zero ⟨e, hev⟩,
-      contradiction },
-    -- put this together with `v` to provide a candidate orthonormal basis for the whole space
-    refine ⟨v.insert e, v.subset_insert e, ⟨_, _⟩, (v.ne_insert_of_not_mem he'').symm⟩,
-    { -- show that the elements of `v.insert e` have unit length
-      rintros ⟨a, ha'⟩,
-      cases eq_or_mem_of_mem_insert ha' with ha ha,
-      { simp [ha, he] },
-      { exact hv.1 ⟨a, ha⟩ } },
-    { -- show that the elements of `v.insert e` are orthogonal
-      have h_end : ∀ a ∈ v, ⟪a, e⟫ = 0,
-      { intros a ha,
-        exact he' a (submodule.subset_span ha) },
-      rintros ⟨a, ha'⟩,
-      cases eq_or_mem_of_mem_insert ha' with ha ha,
-      { rintros ⟨b, hb'⟩ hab',
-        have hb : b ∈ v,
-        { refine mem_of_mem_insert_of_ne hb' _,
-          intros hbe',
-          apply hab',
-          simp [ha, hbe'] },
-        rw inner_eq_zero_sym,
-        simpa [ha] using h_end b hb },
-      rintros ⟨b, hb'⟩ hab',
-      cases eq_or_mem_of_mem_insert hb' with hb hb,
-      { simpa [hb] using h_end a ha },
-      have : (⟨a, ha⟩ : v) ≠ ⟨b, hb⟩,
-      { intros hab'',
-        apply hab',
-        simpa using hab'' },
-      exact hv.2 this } },
-    { -- ** direction 2: empty orthogonal complement implies maximal
-      simp only [subset.antisymm_iff],
-      rintros h u (huv : v ⊆ u) hu,
-      refine ⟨_, huv⟩,
-      intros x hxu,
-      refine ((mt (h x)) (hu.ne_zero ⟨x, hxu⟩)).imp_symm _,
-      intros hxv y hy,
-      have hxv' : (⟨x, hxu⟩ : u) ∉ (coe ⁻¹' v : set u) := by simp [huv, hxv],
-      obtain ⟨l, hl, rfl⟩ :
-        ∃ l ∈ finsupp.supported 𝕜 𝕜 (coe ⁻¹' v : set u), (finsupp.total ↥u E 𝕜 coe) l = y,
-      { rw ← finsupp.mem_span_image_iff_total,
-        simp [huv, inter_eq_self_of_subset_left, hy] },
-      exact hu.inner_finsupp_eq_zero hxv' hl }
-end
-
-/-- An orthonormal set in an `inner_product_space` is maximal, if and only if the closure of its
-span is the whole space. -/
-lemma maximal_orthonormal_iff_dense_span [complete_space E] (hv : orthonormal 𝕜 (coe : v → E)) :
-  (∀ u ⊇ v, orthonormal 𝕜 (coe : u → E) → u = v) ↔ (span 𝕜 v).topological_closure = ⊤ :=
-by rw [maximal_orthonormal_iff_orthogonal_complement_eq_bot hv, ← submodule.orthogonal_eq_top_iff,
-  (span 𝕜 v).orthogonal_orthogonal_eq_closure]
-
-/-- Any orthonormal subset can be extended to an orthonormal set whose span is dense. -/
-lemma exists_subset_is_orthonormal_dense_span
-  [complete_space E] (hv : orthonormal 𝕜 (coe : v → E)) :
-  ∃ u ⊇ v, orthonormal 𝕜 (coe : u → E) ∧ (span 𝕜 u).topological_closure = ⊤ :=
-begin
-  obtain ⟨u, hus, hu, hu_max⟩ := exists_maximal_orthonormal hv,
-  rw maximal_orthonormal_iff_dense_span hu at hu_max,
-  exact ⟨u, hus, hu, hu_max⟩
-end
-
-variables (𝕜 E)
-/-- An inner product space admits an orthonormal set whose span is dense. -/
-lemma exists_is_orthonormal_dense_span [complete_space E] :
-  ∃ u : set E, orthonormal 𝕜 (coe : u → E) ∧ (span 𝕜 u).topological_closure = ⊤ :=
-let ⟨u, hus, hu, hu_max⟩ := exists_subset_is_orthonormal_dense_span (orthonormal_empty 𝕜 E) in
-⟨u, hu, hu_max⟩
-variables {𝕜 E}
-
-/-- An orthonormal set in a finite-dimensional `inner_product_space` is maximal, if and only if it
-is a basis. -/
-lemma maximal_orthonormal_iff_basis_of_finite_dimensional
-  [finite_dimensional 𝕜 E] (hv : orthonormal 𝕜 (coe : v → E)) :
-  (∀ u ⊇ v, orthonormal 𝕜 (coe : u → E) → u = v) ↔ ∃ b : basis v 𝕜 E, ⇑b = coe :=
-begin
-  rw maximal_orthonormal_iff_orthogonal_complement_eq_bot hv,
-  have hv_compl : is_complete (span 𝕜 v : set E) := (span 𝕜 v).complete_of_finite_dimensional,
-  rw submodule.orthogonal_eq_bot_iff hv_compl,
-  have hv_coe : range (coe : v → E) = v := by simp,
-  split,
-  { refine λ h, ⟨basis.mk hv.linear_independent _, basis.coe_mk _ _⟩,
-    convert h },
-  { rintros ⟨h, coe_h⟩,
-    rw [← h.span_eq, coe_h, hv_coe] }
-end
-
-/-- In a finite-dimensional `inner_product_space`, any orthonormal subset can be extended to an
-orthonormal basis. -/
-lemma exists_subset_is_orthonormal_basis
-  [finite_dimensional 𝕜 E] (hv : orthonormal 𝕜 (coe : v → E)) :
-  ∃ (u ⊇ v) (b : basis u 𝕜 E), orthonormal 𝕜 b ∧ ⇑b = coe :=
-begin
-  obtain ⟨u, hus, hu, hu_max⟩ := exists_maximal_orthonormal hv,
-  obtain ⟨b, hb⟩ := (maximal_orthonormal_iff_basis_of_finite_dimensional hu).mp hu_max,
-  exact ⟨u, hus, b, by rwa hb, hb⟩
-end
-
-variables (𝕜 E)
-
-/-- Index for an arbitrary orthonormal basis on a finite-dimensional `inner_product_space`. -/
-def orthonormal_basis_index [finite_dimensional 𝕜 E] : set E :=
-classical.some (exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E))
-
-/-- A finite-dimensional `inner_product_space` has an orthonormal basis. -/
-def orthonormal_basis [finite_dimensional 𝕜 E] :
-  basis (orthonormal_basis_index 𝕜 E) 𝕜 E :=
-(exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some
-
-lemma orthonormal_basis_orthonormal [finite_dimensional 𝕜 E] :
-  orthonormal 𝕜 (orthonormal_basis 𝕜 E) :=
-(exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some_spec.1
-
-@[simp] lemma coe_orthonormal_basis [finite_dimensional 𝕜 E] :
-  ⇑(orthonormal_basis 𝕜 E) = coe :=
-(exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some_spec.2
-
-instance [finite_dimensional 𝕜 E] : fintype (orthonormal_basis_index 𝕜 E) :=
-is_noetherian.fintype_basis_index (orthonormal_basis 𝕜 E)
-
-variables {𝕜 E}
-
-/-- An `n`-dimensional `inner_product_space` has an orthonormal basis indexed by `fin n`. -/
-def fin_orthonormal_basis [finite_dimensional 𝕜 E] {n : ℕ} (hn : finrank 𝕜 E = n) :
-  basis (fin n) 𝕜 E :=
-have h : fintype.card (orthonormal_basis_index 𝕜 E) = n,
-by rw [← finrank_eq_card_basis (orthonormal_basis 𝕜 E), hn],
-(orthonormal_basis 𝕜 E).reindex (fintype.equiv_fin_of_card_eq h)
-
-lemma fin_orthonormal_basis_orthonormal [finite_dimensional 𝕜 E] {n : ℕ} (hn : finrank 𝕜 E = n) :
-  orthonormal 𝕜 (fin_orthonormal_basis hn) :=
-suffices orthonormal 𝕜 (orthonormal_basis _ _ ∘ equiv.symm _),
-by { simp only [fin_orthonormal_basis, basis.coe_reindex], assumption }, -- why doesn't simpa work?
-(orthonormal_basis_orthonormal 𝕜 E).comp _ (equiv.injective _)
-
-end orthonormal_basis
diff --git a/src/analysis/inner_product_space/calculus.lean b/src/analysis/inner_product_space/calculus.lean
new file mode 100644
index 0000000000000..5792a98328eb2
--- /dev/null
+++ b/src/analysis/inner_product_space/calculus.lean
@@ -0,0 +1,291 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import analysis.inner_product_space.basic
+import analysis.special_functions.sqrt
+
+/-!
+# Derivative of the inner product
+
+In this file we prove that the inner product and square of the norm in an inner space are
+infinitely `ℝ`-smooth. In order to state these results, we need a `normed_space ℝ E`
+instance. Though we can deduce this structure from `inner_product_space 𝕜 E`, this instance may be
+not definitionally equal to some other “natural” instance. So, we assume `[normed_space ℝ E]` and
+`[is_scalar_tower ℝ 𝕜 E]`. In both interesting cases `𝕜 = ℝ` and `𝕜 = ℂ` we have these instances.
+
+Currently, the continuity of the inner product is also proved in this file, as a consequence of the
+differentiability; however (TODO) this ought to be re-proved directly and moved to
+`analysis.inner_product_space.basic`.
+
+-/
+
+noncomputable theory
+
+open is_R_or_C real filter
+open_locale big_operators classical topological_space
+
+variables {𝕜 E F : Type*} [is_R_or_C 𝕜]
+variables [inner_product_space 𝕜 E] [inner_product_space ℝ F]
+local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
+
+section deriv
+
+variables [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E]
+
+lemma is_bounded_bilinear_map_inner : is_bounded_bilinear_map ℝ (λ p : E × E, ⟪p.1, p.2⟫) :=
+{ add_left := λ _ _ _, inner_add_left,
+  smul_left := λ r x y,
+    by simp only [← algebra_map_smul 𝕜 r x, algebra_map_eq_of_real, inner_smul_real_left],
+  add_right := λ _ _ _, inner_add_right,
+  smul_right := λ r x y,
+    by simp only [← algebra_map_smul 𝕜 r y, algebra_map_eq_of_real, inner_smul_real_right],
+  bound := ⟨1, zero_lt_one, λ x y,
+    by { rw [one_mul], exact norm_inner_le_norm x y, }⟩ }
+
+/-- Derivative of the inner product. -/
+def fderiv_inner_clm (p : E × E) : E × E →L[ℝ] 𝕜 := is_bounded_bilinear_map_inner.deriv p
+
+@[simp] lemma fderiv_inner_clm_apply (p x : E × E) :
+  fderiv_inner_clm  p x = ⟪p.1, x.2⟫ + ⟪x.1, p.2⟫ := rfl
+
+lemma times_cont_diff_inner {n} : times_cont_diff ℝ n (λ p : E × E, ⟪p.1, p.2⟫) :=
+is_bounded_bilinear_map_inner.times_cont_diff
+
+lemma times_cont_diff_at_inner {p : E × E} {n} :
+  times_cont_diff_at ℝ n (λ p : E × E, ⟪p.1, p.2⟫) p :=
+times_cont_diff_inner.times_cont_diff_at
+
+lemma differentiable_inner : differentiable ℝ (λ p : E × E, ⟪p.1, p.2⟫) :=
+is_bounded_bilinear_map_inner.differentiable_at
+
+variables {G : Type*} [normed_group G] [normed_space ℝ G]
+  {f g : G → E} {f' g' : G →L[ℝ] E} {s : set G} {x : G} {n : with_top ℕ}
+
+include 𝕜
+
+lemma times_cont_diff_within_at.inner (hf : times_cont_diff_within_at ℝ n f s x)
+  (hg : times_cont_diff_within_at ℝ n g s x) :
+  times_cont_diff_within_at ℝ n (λ x, ⟪f x, g x⟫) s x :=
+times_cont_diff_at_inner.comp_times_cont_diff_within_at x (hf.prod hg)
+
+lemma times_cont_diff_at.inner (hf : times_cont_diff_at ℝ n f x)
+  (hg : times_cont_diff_at ℝ n g x) :
+  times_cont_diff_at ℝ n (λ x, ⟪f x, g x⟫) x :=
+hf.inner hg
+
+lemma times_cont_diff_on.inner (hf : times_cont_diff_on ℝ n f s) (hg : times_cont_diff_on ℝ n g s) :
+  times_cont_diff_on ℝ n (λ x, ⟪f x, g x⟫) s :=
+λ x hx, (hf x hx).inner (hg x hx)
+
+lemma times_cont_diff.inner (hf : times_cont_diff ℝ n f) (hg : times_cont_diff ℝ n g) :
+  times_cont_diff ℝ n (λ x, ⟪f x, g x⟫) :=
+times_cont_diff_inner.comp (hf.prod hg)
+
+lemma has_fderiv_within_at.inner (hf : has_fderiv_within_at f f' s x)
+  (hg : has_fderiv_within_at g g' s x) :
+  has_fderiv_within_at (λ t, ⟪f t, g t⟫) ((fderiv_inner_clm (f x, g x)).comp $ f'.prod g') s x :=
+(is_bounded_bilinear_map_inner.has_fderiv_at (f x, g x)).comp_has_fderiv_within_at x (hf.prod hg)
+
+lemma has_fderiv_at.inner (hf : has_fderiv_at f f' x) (hg : has_fderiv_at g g' x) :
+  has_fderiv_at (λ t, ⟪f t, g t⟫) ((fderiv_inner_clm (f x, g x)).comp $ f'.prod g') x :=
+(is_bounded_bilinear_map_inner.has_fderiv_at (f x, g x)).comp x (hf.prod hg)
+
+lemma has_deriv_within_at.inner {f g : ℝ → E} {f' g' : E} {s : set ℝ} {x : ℝ}
+  (hf : has_deriv_within_at f f' s x) (hg : has_deriv_within_at g g' s x) :
+  has_deriv_within_at (λ t, ⟪f t, g t⟫) (⟪f x, g'⟫ + ⟪f', g x⟫) s x :=
+by simpa using (hf.has_fderiv_within_at.inner hg.has_fderiv_within_at).has_deriv_within_at
+
+lemma has_deriv_at.inner {f g : ℝ → E} {f' g' : E} {x : ℝ} :
+  has_deriv_at f f' x →  has_deriv_at g g' x →
+  has_deriv_at (λ t, ⟪f t, g t⟫) (⟪f x, g'⟫ + ⟪f', g x⟫) x :=
+by simpa only [← has_deriv_within_at_univ] using has_deriv_within_at.inner
+
+lemma differentiable_within_at.inner (hf : differentiable_within_at ℝ f s x)
+  (hg : differentiable_within_at ℝ g s x) :
+  differentiable_within_at ℝ (λ x, ⟪f x, g x⟫) s x :=
+((differentiable_inner _).has_fderiv_at.comp_has_fderiv_within_at x
+  (hf.prod hg).has_fderiv_within_at).differentiable_within_at
+
+lemma differentiable_at.inner (hf : differentiable_at ℝ f x) (hg : differentiable_at ℝ g x) :
+  differentiable_at ℝ (λ x, ⟪f x, g x⟫) x :=
+(differentiable_inner _).comp x (hf.prod hg)
+
+lemma differentiable_on.inner (hf : differentiable_on ℝ f s) (hg : differentiable_on ℝ g s) :
+  differentiable_on ℝ (λ x, ⟪f x, g x⟫) s :=
+λ x hx, (hf x hx).inner (hg x hx)
+
+lemma differentiable.inner (hf : differentiable ℝ f) (hg : differentiable ℝ g) :
+  differentiable ℝ (λ x, ⟪f x, g x⟫) :=
+λ x, (hf x).inner (hg x)
+
+lemma fderiv_inner_apply (hf : differentiable_at ℝ f x) (hg : differentiable_at ℝ g x) (y : G) :
+  fderiv ℝ (λ t, ⟪f t, g t⟫) x y = ⟪f x, fderiv ℝ g x y⟫ + ⟪fderiv ℝ f x y, g x⟫ :=
+by { rw [(hf.has_fderiv_at.inner hg.has_fderiv_at).fderiv], refl }
+
+lemma deriv_inner_apply {f g : ℝ → E} {x : ℝ} (hf : differentiable_at ℝ f x)
+  (hg : differentiable_at ℝ g x) :
+  deriv (λ t, ⟪f t, g t⟫) x = ⟪f x, deriv g x⟫ + ⟪deriv f x, g x⟫ :=
+(hf.has_deriv_at.inner hg.has_deriv_at).deriv
+
+lemma times_cont_diff_norm_sq : times_cont_diff ℝ n (λ x : E, ∥x∥ ^ 2) :=
+begin
+  simp only [sq, ← inner_self_eq_norm_sq],
+  exact (re_clm : 𝕜 →L[ℝ] ℝ).times_cont_diff.comp (times_cont_diff_id.inner times_cont_diff_id)
+end
+
+lemma times_cont_diff.norm_sq (hf : times_cont_diff ℝ n f) :
+  times_cont_diff ℝ n (λ x, ∥f x∥ ^ 2) :=
+times_cont_diff_norm_sq.comp hf
+
+lemma times_cont_diff_within_at.norm_sq (hf : times_cont_diff_within_at ℝ n f s x) :
+  times_cont_diff_within_at ℝ n (λ y, ∥f y∥ ^ 2) s x :=
+times_cont_diff_norm_sq.times_cont_diff_at.comp_times_cont_diff_within_at x hf
+
+lemma times_cont_diff_at.norm_sq (hf : times_cont_diff_at ℝ n f x) :
+  times_cont_diff_at ℝ n (λ y, ∥f y∥ ^ 2) x :=
+hf.norm_sq
+
+lemma times_cont_diff_at_norm {x : E} (hx : x ≠ 0) : times_cont_diff_at ℝ n norm x :=
+have ∥id x∥ ^ 2 ≠ 0, from pow_ne_zero _ (norm_pos_iff.2 hx).ne',
+by simpa only [id, sqrt_sq, norm_nonneg] using times_cont_diff_at_id.norm_sq.sqrt this
+
+lemma times_cont_diff_at.norm (hf : times_cont_diff_at ℝ n f x) (h0 : f x ≠ 0) :
+  times_cont_diff_at ℝ n (λ y, ∥f y∥) x :=
+(times_cont_diff_at_norm h0).comp x hf
+
+lemma times_cont_diff_at.dist (hf : times_cont_diff_at ℝ n f x) (hg : times_cont_diff_at ℝ n g x)
+  (hne : f x ≠ g x) :
+  times_cont_diff_at ℝ n (λ y, dist (f y) (g y)) x :=
+by { simp only [dist_eq_norm], exact (hf.sub hg).norm (sub_ne_zero.2 hne) }
+
+lemma times_cont_diff_within_at.norm (hf : times_cont_diff_within_at ℝ n f s x) (h0 : f x ≠ 0) :
+  times_cont_diff_within_at ℝ n (λ y, ∥f y∥) s x :=
+(times_cont_diff_at_norm h0).comp_times_cont_diff_within_at x hf
+
+lemma times_cont_diff_within_at.dist (hf : times_cont_diff_within_at ℝ n f s x)
+  (hg : times_cont_diff_within_at ℝ n g s x) (hne : f x ≠ g x) :
+  times_cont_diff_within_at ℝ n (λ y, dist (f y) (g y)) s x :=
+by { simp only [dist_eq_norm], exact (hf.sub hg).norm (sub_ne_zero.2 hne) }
+
+lemma times_cont_diff_on.norm_sq (hf : times_cont_diff_on ℝ n f s) :
+  times_cont_diff_on ℝ n (λ y, ∥f y∥ ^ 2) s :=
+(λ x hx, (hf x hx).norm_sq)
+
+lemma times_cont_diff_on.norm (hf : times_cont_diff_on ℝ n f s) (h0 : ∀ x ∈ s, f x ≠ 0) :
+  times_cont_diff_on ℝ n (λ y, ∥f y∥) s :=
+λ x hx, (hf x hx).norm (h0 x hx)
+
+lemma times_cont_diff_on.dist (hf : times_cont_diff_on ℝ n f s)
+  (hg : times_cont_diff_on ℝ n g s) (hne : ∀ x ∈ s, f x ≠ g x) :
+  times_cont_diff_on ℝ n (λ y, dist (f y) (g y)) s :=
+λ x hx, (hf x hx).dist (hg x hx) (hne x hx)
+
+lemma times_cont_diff.norm (hf : times_cont_diff ℝ n f) (h0 : ∀ x, f x ≠ 0) :
+  times_cont_diff ℝ n (λ y, ∥f y∥) :=
+times_cont_diff_iff_times_cont_diff_at.2 $ λ x, hf.times_cont_diff_at.norm (h0 x)
+
+lemma times_cont_diff.dist (hf : times_cont_diff ℝ n f) (hg : times_cont_diff ℝ n g)
+  (hne : ∀ x, f x ≠ g x) :
+  times_cont_diff ℝ n (λ y, dist (f y) (g y)) :=
+times_cont_diff_iff_times_cont_diff_at.2 $
+  λ x, hf.times_cont_diff_at.dist hg.times_cont_diff_at (hne x)
+
+lemma differentiable_at.norm_sq (hf : differentiable_at ℝ f x) :
+  differentiable_at ℝ (λ y, ∥f y∥ ^ 2) x :=
+(times_cont_diff_at_id.norm_sq.differentiable_at le_rfl).comp x hf
+
+lemma differentiable_at.norm (hf : differentiable_at ℝ f x) (h0 : f x ≠ 0) :
+  differentiable_at ℝ (λ y, ∥f y∥) x :=
+((times_cont_diff_at_norm h0).differentiable_at le_rfl).comp x hf
+
+lemma differentiable_at.dist (hf : differentiable_at ℝ f x) (hg : differentiable_at ℝ g x)
+  (hne : f x ≠ g x) :
+  differentiable_at ℝ (λ y, dist (f y) (g y)) x :=
+by { simp only [dist_eq_norm], exact (hf.sub hg).norm (sub_ne_zero.2 hne) }
+
+lemma differentiable.norm_sq (hf : differentiable ℝ f) : differentiable ℝ (λ y, ∥f y∥ ^ 2) :=
+λ x, (hf x).norm_sq
+
+lemma differentiable.norm (hf : differentiable ℝ f) (h0 : ∀ x, f x ≠ 0) :
+  differentiable ℝ (λ y, ∥f y∥) :=
+λ x, (hf x).norm (h0 x)
+
+lemma differentiable.dist (hf : differentiable ℝ f) (hg : differentiable ℝ g)
+  (hne : ∀ x, f x ≠ g x) :
+  differentiable ℝ (λ y, dist (f y) (g y)) :=
+λ x, (hf x).dist (hg x) (hne x)
+
+lemma differentiable_within_at.norm_sq (hf : differentiable_within_at ℝ f s x) :
+  differentiable_within_at ℝ (λ y, ∥f y∥ ^ 2) s x :=
+(times_cont_diff_at_id.norm_sq.differentiable_at le_rfl).comp_differentiable_within_at x hf
+
+lemma differentiable_within_at.norm (hf : differentiable_within_at ℝ f s x) (h0 : f x ≠ 0) :
+  differentiable_within_at ℝ (λ y, ∥f y∥) s x :=
+((times_cont_diff_at_id.norm h0).differentiable_at le_rfl).comp_differentiable_within_at x hf
+
+lemma differentiable_within_at.dist (hf : differentiable_within_at ℝ f s x)
+  (hg : differentiable_within_at ℝ g s x) (hne : f x ≠ g x) :
+  differentiable_within_at ℝ (λ y, dist (f y) (g y)) s x :=
+by { simp only [dist_eq_norm], exact (hf.sub hg).norm (sub_ne_zero.2 hne) }
+
+lemma differentiable_on.norm_sq (hf : differentiable_on ℝ f s) :
+  differentiable_on ℝ (λ y, ∥f y∥ ^ 2) s :=
+λ x hx, (hf x hx).norm_sq
+
+lemma differentiable_on.norm (hf : differentiable_on ℝ f s) (h0 : ∀ x ∈ s, f x ≠ 0) :
+  differentiable_on ℝ (λ y, ∥f y∥) s :=
+λ x hx, (hf x hx).norm (h0 x hx)
+
+lemma differentiable_on.dist (hf : differentiable_on ℝ f s) (hg : differentiable_on ℝ g s)
+  (hne : ∀ x ∈ s, f x ≠ g x) :
+  differentiable_on ℝ (λ y, dist (f y) (g y)) s :=
+λ x hx, (hf x hx).dist (hg x hx) (hne x hx)
+
+end deriv
+
+section continuous
+
+/-!
+### Continuity of the inner product
+
+Since the inner product is `ℝ`-smooth, it is continuous. We do not need a `[normed_space ℝ E]`
+structure to *state* this fact and its corollaries, so we introduce them in the proof instead.
+-/
+
+lemma continuous_inner : continuous (λ p : E × E, ⟪p.1, p.2⟫) :=
+begin
+  letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜 E,
+  letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
+  exact differentiable_inner.continuous
+end
+
+variables {α : Type*}
+
+lemma filter.tendsto.inner {f g : α → E} {l : filter α} {x y : E} (hf : tendsto f l (𝓝 x))
+  (hg : tendsto g l (𝓝 y)) :
+  tendsto (λ t, ⟪f t, g t⟫) l (𝓝 ⟪x, y⟫) :=
+(continuous_inner.tendsto _).comp (hf.prod_mk_nhds hg)
+
+variables [topological_space α] {f g : α → E} {x : α} {s : set α}
+
+include 𝕜
+
+lemma continuous_within_at.inner (hf : continuous_within_at f s x)
+  (hg : continuous_within_at g s x) :
+  continuous_within_at (λ t, ⟪f t, g t⟫) s x :=
+hf.inner hg
+
+lemma continuous_at.inner (hf : continuous_at f x) (hg : continuous_at g x) :
+  continuous_at (λ t, ⟪f t, g t⟫) x :=
+hf.inner hg
+
+lemma continuous_on.inner (hf : continuous_on f s) (hg : continuous_on g s) :
+  continuous_on (λ t, ⟪f t, g t⟫) s :=
+λ x hx, (hf x hx).inner (hg x hx)
+
+lemma continuous.inner (hf : continuous f) (hg : continuous g) : continuous (λ t, ⟪f t, g t⟫) :=
+continuous_iff_continuous_at.2 $ λ x, hf.continuous_at.inner hg.continuous_at
+
+end continuous
diff --git a/src/analysis/normed_space/conformal_linear_map/inner_product.lean b/src/analysis/inner_product_space/conformal_linear_map.lean
similarity index 97%
rename from src/analysis/normed_space/conformal_linear_map/inner_product.lean
rename to src/analysis/inner_product_space/conformal_linear_map.lean
index 3052599d23678..92b5728b5d2c7 100644
--- a/src/analysis/normed_space/conformal_linear_map/inner_product.lean
+++ b/src/analysis/inner_product_space/conformal_linear_map.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yourong Zang
 -/
 import analysis.normed_space.conformal_linear_map
-import analysis.normed_space.inner_product
+import analysis.inner_product_space.basic
 
 /-!
 # Conformal maps between inner product spaces
diff --git a/src/analysis/normed_space/euclidean_dist.lean b/src/analysis/inner_product_space/euclidean_dist.lean
similarity index 99%
rename from src/analysis/normed_space/euclidean_dist.lean
rename to src/analysis/inner_product_space/euclidean_dist.lean
index 868b49a78dfb8..a12cb896049c9 100644
--- a/src/analysis/normed_space/euclidean_dist.lean
+++ b/src/analysis/inner_product_space/euclidean_dist.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
+import analysis.inner_product_space.calculus
 import analysis.normed_space.pi_Lp
 
 /-!
diff --git a/src/analysis/inner_product_space/projection.lean b/src/analysis/inner_product_space/projection.lean
new file mode 100644
index 0000000000000..63e57dddde230
--- /dev/null
+++ b/src/analysis/inner_product_space/projection.lean
@@ -0,0 +1,1020 @@
+/-
+Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zhouhang Zhou, Frédéric Dupuis, Heather Macbeth
+-/
+import analysis.inner_product_space.basic
+import analysis.convex.basic
+
+/-!
+# The orthogonal projection
+
+Given a nonempty complete subspace `K` of an inner product space `E`, this file constructs
+`orthogonal_projection K : E →L[𝕜] K`, the orthogonal projection of `E` onto `K`.  This map
+satisfies: for any point `u` in `E`, the point `v = orthogonal_projection K u` in `K` minimizes the
+distance `∥u - v∥` to `u`.
+
+Also a linear isometry equivalence `reflection K : E ≃ₗᵢ[𝕜] E` is constructed, by choosing, for
+each `u : E`, the point `reflection K u` to satisfy
+`u + (reflection K u) = 2 • orthogonal_projection K u`.
+
+Basic API for `orthogonal_projection` and `reflection` is developed.
+
+Next, the orthogonal projection is used to prove a series of more subtle lemmas about the
+the orthogonal complement of complete subspaces of `E` (the orthogonal complement itself was
+defined in `analysis.inner_product_space.basic`); the lemma
+`submodule.sup_orthogonal_of_is_complete`, stating that for a complete subspace `K` of `E` we have
+`K ⊔ Kᗮ = ⊤`, is a typical example.
+
+The last section covers orthonormal bases, Hilbert bases, etc. The lemma
+`maximal_orthonormal_iff_dense_span`, whose proof requires the theory on the orthogonal complement
+developed earlier in this file, states that an orthonormal set in an inner product space is
+maximal, if and only if its span is dense (i.e., iff it is Hilbert basis, although we do not make
+that definition).  Various consequences are stated, including that if `E` is finite-dimensional
+then a maximal orthonormal set is a basis (`maximal_orthonormal_iff_basis_of_finite_dimensional`).
+
+## References
+
+The orthogonal projection construction is adapted from
+*  [Clément & Martin, *The Lax-Milgram Theorem. A detailed proof to be formalized in Coq*]
+*  [Clément & Martin, *A Coq formal proof of the Lax–Milgram theorem*]
+
+The Coq code is available at the following address: <http://www.lri.fr/~sboldo/elfic/index.html>
+-/
+
+noncomputable theory
+
+open is_R_or_C real filter
+open_locale big_operators classical topological_space
+
+variables {𝕜 E F : Type*} [is_R_or_C 𝕜]
+variables [inner_product_space 𝕜 E] [inner_product_space ℝ F]
+local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
+local notation `absR` := _root_.abs
+
+/-! ### Orthogonal projection in inner product spaces -/
+
+/--
+Existence of minimizers
+Let `u` be a point in a real inner product space, and let `K` be a nonempty complete convex subset.
+Then there exists a (unique) `v` in `K` that minimizes the distance `∥u - v∥` to `u`.
+ -/
+-- FIXME this monolithic proof causes a deterministic timeout with `-T50000`
+-- It should be broken in a sequence of more manageable pieces,
+-- perhaps with individual statements for the three steps below.
+theorem exists_norm_eq_infi_of_complete_convex {K : set F} (ne : K.nonempty) (h₁ : is_complete K)
+  (h₂ : convex ℝ K) : ∀ u : F, ∃ v ∈ K, ∥u - v∥ = ⨅ w : K, ∥u - w∥ := assume u,
+begin
+  let δ := ⨅ w : K, ∥u - w∥,
+  letI : nonempty K := ne.to_subtype,
+  have zero_le_δ : 0 ≤ δ := le_cinfi (λ _, norm_nonneg _),
+  have δ_le : ∀ w : K, δ ≤ ∥u - w∥,
+    from cinfi_le ⟨0, set.forall_range_iff.2 $ λ _, norm_nonneg _⟩,
+  have δ_le' : ∀ w ∈ K, δ ≤ ∥u - w∥ := assume w hw, δ_le ⟨w, hw⟩,
+  -- Step 1: since `δ` is the infimum, can find a sequence `w : ℕ → K` in `K`
+  -- such that `∥u - w n∥ < δ + 1 / (n + 1)` (which implies `∥u - w n∥ --> δ`);
+  -- maybe this should be a separate lemma
+  have exists_seq : ∃ w : ℕ → K, ∀ n, ∥u - w n∥ < δ + 1 / (n + 1),
+  { have hδ : ∀n:ℕ, δ < δ + 1 / (n + 1), from
+      λ n, lt_add_of_le_of_pos (le_refl _) nat.one_div_pos_of_nat,
+    have h := λ n, exists_lt_of_cinfi_lt (hδ n),
+    let w : ℕ → K := λ n, classical.some (h n),
+    exact ⟨w, λ n, classical.some_spec (h n)⟩ },
+  rcases exists_seq with ⟨w, hw⟩,
+  have norm_tendsto : tendsto (λ n, ∥u - w n∥) at_top (nhds δ),
+  { have h : tendsto (λ n:ℕ, δ) at_top (nhds δ) := tendsto_const_nhds,
+    have h' : tendsto (λ n:ℕ, δ + 1 / (n + 1)) at_top (nhds δ),
+    { convert h.add tendsto_one_div_add_at_top_nhds_0_nat, simp only [add_zero] },
+    exact tendsto_of_tendsto_of_tendsto_of_le_of_le h h'
+      (λ x, δ_le _) (λ x, le_of_lt (hw _)) },
+  -- Step 2: Prove that the sequence `w : ℕ → K` is a Cauchy sequence
+  have seq_is_cauchy : cauchy_seq (λ n, ((w n):F)),
+  { rw cauchy_seq_iff_le_tendsto_0, -- splits into three goals
+    let b := λ n:ℕ, (8 * δ * (1/(n+1)) + 4 * (1/(n+1)) * (1/(n+1))),
+    use (λn, sqrt (b n)),
+    split,
+    -- first goal :  `∀ (n : ℕ), 0 ≤ sqrt (b n)`
+    assume n, exact sqrt_nonneg _,
+    split,
+    -- second goal : `∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ↑(w n) ↑(w m) ≤ sqrt (b N)`
+    assume p q N hp hq,
+    let wp := ((w p):F), let wq := ((w q):F),
+    let a := u - wq, let b := u - wp,
+    let half := 1 / (2:ℝ), let div := 1 / ((N:ℝ) + 1),
+    have : 4 * ∥u - half • (wq + wp)∥ * ∥u - half • (wq + wp)∥ + ∥wp - wq∥ * ∥wp - wq∥ =
+      2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) :=
+    calc
+      4 * ∥u - half•(wq + wp)∥ * ∥u - half•(wq + wp)∥ + ∥wp - wq∥ * ∥wp - wq∥
+          = (2*∥u - half•(wq + wp)∥) * (2 * ∥u - half•(wq + wp)∥) + ∥wp-wq∥*∥wp-wq∥ : by ring
+      ... = (absR ((2:ℝ)) * ∥u - half•(wq + wp)∥) * (absR ((2:ℝ)) * ∥u - half•(wq+wp)∥) +
+            ∥wp-wq∥*∥wp-wq∥ :
+      by { rw _root_.abs_of_nonneg, exact zero_le_two }
+      ... = ∥(2:ℝ) • (u - half • (wq + wp))∥ * ∥(2:ℝ) • (u - half • (wq + wp))∥ +
+            ∥wp-wq∥ * ∥wp-wq∥ :
+      by simp [norm_smul]
+      ... = ∥a + b∥ * ∥a + b∥ + ∥a - b∥ * ∥a - b∥ :
+      begin
+        rw [smul_sub, smul_smul, mul_one_div_cancel (_root_.two_ne_zero : (2 : ℝ) ≠ 0),
+            ← one_add_one_eq_two, add_smul],
+        simp only [one_smul],
+        have eq₁ : wp - wq = a - b, from (sub_sub_sub_cancel_left _ _ _).symm,
+        have eq₂ : u + u - (wq + wp) = a + b, show u + u - (wq + wp) = (u - wq) + (u - wp), abel,
+        rw [eq₁, eq₂],
+      end
+      ... = 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) : parallelogram_law_with_norm,
+    have eq : δ ≤ ∥u - half • (wq + wp)∥,
+    { rw smul_add,
+      apply δ_le', apply h₂,
+        repeat {exact subtype.mem _},
+        repeat {exact le_of_lt one_half_pos},
+        exact add_halves 1 },
+    have eq₁ : 4 * δ * δ ≤ 4 * ∥u - half • (wq + wp)∥ * ∥u - half • (wq + wp)∥,
+    { mono, mono, norm_num, apply mul_nonneg, norm_num, exact norm_nonneg _ },
+    have eq₂ : ∥a∥ * ∥a∥ ≤ (δ + div) * (δ + div) :=
+      mul_self_le_mul_self (norm_nonneg _)
+        (le_trans (le_of_lt $ hw q) (add_le_add_left (nat.one_div_le_one_div hq) _)),
+    have eq₂' : ∥b∥ * ∥b∥ ≤ (δ + div) * (δ + div) :=
+      mul_self_le_mul_self (norm_nonneg _)
+        (le_trans (le_of_lt $ hw p) (add_le_add_left (nat.one_div_le_one_div hp) _)),
+    rw dist_eq_norm,
+    apply nonneg_le_nonneg_of_sq_le_sq, { exact sqrt_nonneg _ },
+    rw mul_self_sqrt,
+    exact calc
+      ∥wp - wq∥ * ∥wp - wq∥ = 2 * (∥a∥*∥a∥ + ∥b∥*∥b∥) -
+        4 * ∥u - half • (wq+wp)∥ * ∥u - half • (wq+wp)∥ : by { rw ← this, simp }
+      ... ≤ 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) - 4 * δ * δ : sub_le_sub_left eq₁ _
+      ... ≤ 2 * ((δ + div) * (δ + div) + (δ + div) * (δ + div)) - 4 * δ * δ :
+        sub_le_sub_right (mul_le_mul_of_nonneg_left (add_le_add eq₂ eq₂') (by norm_num)) _
+      ... = 8 * δ * div + 4 * div * div : by ring,
+    exact add_nonneg
+      (mul_nonneg (mul_nonneg (by norm_num) zero_le_δ) (le_of_lt nat.one_div_pos_of_nat))
+      (mul_nonneg (mul_nonneg (by norm_num) nat.one_div_pos_of_nat.le) nat.one_div_pos_of_nat.le),
+    -- third goal : `tendsto (λ (n : ℕ), sqrt (b n)) at_top (𝓝 0)`
+    apply tendsto.comp,
+    { convert continuous_sqrt.continuous_at, exact sqrt_zero.symm },
+    have eq₁ : tendsto (λ (n : ℕ), 8 * δ * (1 / (n + 1))) at_top (nhds (0:ℝ)),
+    { convert (@tendsto_const_nhds _ _ _ (8 * δ) _).mul tendsto_one_div_add_at_top_nhds_0_nat,
+      simp only [mul_zero] },
+    have : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1))) at_top (nhds (0:ℝ)),
+    { convert (@tendsto_const_nhds _ _ _ (4:ℝ) _).mul tendsto_one_div_add_at_top_nhds_0_nat,
+      simp only [mul_zero] },
+    have eq₂ : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1)) * (1 / (n + 1))) at_top (nhds (0:ℝ)),
+    { convert this.mul tendsto_one_div_add_at_top_nhds_0_nat,
+      simp only [mul_zero] },
+    convert eq₁.add eq₂, simp only [add_zero] },
+  -- Step 3: By completeness of `K`, let `w : ℕ → K` converge to some `v : K`.
+  -- Prove that it satisfies all requirements.
+  rcases cauchy_seq_tendsto_of_is_complete h₁ (λ n, _) seq_is_cauchy with ⟨v, hv, w_tendsto⟩,
+  use v, use hv,
+  have h_cont : continuous (λ v, ∥u - v∥) :=
+    continuous.comp continuous_norm (continuous.sub continuous_const continuous_id),
+  have : tendsto (λ n, ∥u - w n∥) at_top (nhds ∥u - v∥),
+    convert (tendsto.comp h_cont.continuous_at w_tendsto),
+  exact tendsto_nhds_unique this norm_tendsto,
+  exact subtype.mem _
+end
+
+/-- Characterization of minimizers for the projection on a convex set in a real inner product
+space. -/
+theorem norm_eq_infi_iff_real_inner_le_zero {K : set F} (h : convex ℝ K) {u : F} {v : F}
+  (hv : v ∈ K) : ∥u - v∥ = (⨅ w : K, ∥u - w∥) ↔ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 :=
+iff.intro
+begin
+  assume eq w hw,
+  let δ := ⨅ w : K, ∥u - w∥, let p := ⟪u - v, w - v⟫_ℝ, let q := ∥w - v∥^2,
+  letI : nonempty K := ⟨⟨v, hv⟩⟩,
+  have zero_le_δ : 0 ≤ δ,
+    apply le_cinfi, intro, exact norm_nonneg _,
+  have δ_le : ∀ w : K, δ ≤ ∥u - w∥,
+    assume w, apply cinfi_le, use (0:ℝ), rintros _ ⟨_, rfl⟩, exact norm_nonneg _,
+  have δ_le' : ∀ w ∈ K, δ ≤ ∥u - w∥ := assume w hw, δ_le ⟨w, hw⟩,
+  have : ∀θ:ℝ, 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q,
+    assume θ hθ₁ hθ₂,
+    have : ∥u - v∥^2 ≤ ∥u - v∥^2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ*θ*∥w - v∥^2 :=
+    calc
+      ∥u - v∥^2 ≤ ∥u - (θ•w + (1-θ)•v)∥^2 :
+      begin
+        simp only [sq], apply mul_self_le_mul_self (norm_nonneg _),
+        rw [eq], apply δ_le',
+        apply h hw hv,
+        exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel'_right _ _],
+      end
+      ... = ∥(u - v) - θ • (w - v)∥^2 :
+      begin
+        have : u - (θ•w + (1-θ)•v) = (u - v) - θ • (w - v),
+        { rw [smul_sub, sub_smul, one_smul],
+          simp only [sub_eq_add_neg, add_comm, add_left_comm, add_assoc, neg_add_rev] },
+        rw this
+      end
+      ... = ∥u - v∥^2 - 2 * θ * inner (u - v) (w - v) + θ*θ*∥w - v∥^2 :
+      begin
+        rw [norm_sub_sq, inner_smul_right, norm_smul],
+        simp only [sq],
+        show ∥u-v∥*∥u-v∥-2*(θ*inner(u-v)(w-v))+absR (θ)*∥w-v∥*(absR (θ)*∥w-v∥)=
+                ∥u-v∥*∥u-v∥-2*θ*inner(u-v)(w-v)+θ*θ*(∥w-v∥*∥w-v∥),
+        rw abs_of_pos hθ₁, ring
+      end,
+    have eq₁ : ∥u-v∥^2-2*θ*inner(u-v)(w-v)+θ*θ*∥w-v∥^2=∥u-v∥^2+(θ*θ*∥w-v∥^2-2*θ*inner(u-v)(w-v)),
+      by abel,
+    rw [eq₁, le_add_iff_nonneg_right] at this,
+    have eq₂ : θ*θ*∥w-v∥^2-2*θ*inner(u-v)(w-v)=θ*(θ*∥w-v∥^2-2*inner(u-v)(w-v)), ring,
+    rw eq₂ at this,
+    have := le_of_sub_nonneg (nonneg_of_mul_nonneg_left this hθ₁),
+    exact this,
+  by_cases hq : q = 0,
+  { rw hq at this,
+    have : p ≤ 0,
+      have := this (1:ℝ) (by norm_num) (by norm_num),
+      linarith,
+    exact this },
+  { have q_pos : 0 < q,
+      apply lt_of_le_of_ne, exact sq_nonneg _, intro h, exact hq h.symm,
+    by_contradiction hp, rw not_le at hp,
+    let θ := min (1:ℝ) (p / q),
+    have eq₁ : θ*q ≤ p := calc
+      θ*q ≤ (p/q) * q : mul_le_mul_of_nonneg_right (min_le_right _ _) (sq_nonneg _)
+      ... = p : div_mul_cancel _ hq,
+    have : 2 * p ≤ p := calc
+      2 * p ≤ θ*q : by { refine this θ (lt_min (by norm_num) (div_pos hp q_pos)) (by norm_num) }
+      ... ≤ p : eq₁,
+    linarith }
+end
+begin
+  assume h,
+  letI : nonempty K := ⟨⟨v, hv⟩⟩,
+  apply le_antisymm,
+  { apply le_cinfi, assume w,
+    apply nonneg_le_nonneg_of_sq_le_sq (norm_nonneg _),
+    have := h w w.2,
+    exact calc
+      ∥u - v∥ * ∥u - v∥ ≤ ∥u - v∥ * ∥u - v∥ - 2 * inner (u - v) ((w:F) - v) : by linarith
+      ... ≤ ∥u - v∥^2 - 2 * inner (u - v) ((w:F) - v) + ∥(w:F) - v∥^2 :
+        by { rw sq, refine le_add_of_nonneg_right _, exact sq_nonneg _ }
+      ... = ∥(u - v) - (w - v)∥^2 : norm_sub_sq.symm
+      ... = ∥u - w∥ * ∥u - w∥ :
+        by { have : (u - v) - (w - v) = u - w, abel, rw [this, sq] } },
+  { show (⨅ (w : K), ∥u - w∥) ≤ (λw:K, ∥u - w∥) ⟨v, hv⟩,
+      apply cinfi_le, use 0, rintros y ⟨z, rfl⟩, exact norm_nonneg _ }
+end
+
+variables (K : submodule 𝕜 E)
+
+/--
+Existence of projections on complete subspaces.
+Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace.
+Then there exists a (unique) `v` in `K` that minimizes the distance `∥u - v∥` to `u`.
+This point `v` is usually called the orthogonal projection of `u` onto `K`.
+-/
+theorem exists_norm_eq_infi_of_complete_subspace
+  (h : is_complete (↑K : set E)) : ∀ u : E, ∃ v ∈ K, ∥u - v∥ = ⨅ w : (K : set E), ∥u - w∥ :=
+begin
+  letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜 E,
+  letI : module ℝ E := restrict_scalars.module ℝ 𝕜 E,
+  letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
+  let K' : submodule ℝ E := submodule.restrict_scalars ℝ K,
+  exact exists_norm_eq_infi_of_complete_convex ⟨0, K'.zero_mem⟩ h K'.convex
+end
+
+/--
+Characterization of minimizers in the projection on a subspace, in the real case.
+Let `u` be a point in a real inner product space, and let `K` be a nonempty subspace.
+Then point `v` minimizes the distance `∥u - v∥` over points in `K` if and only if
+for all `w ∈ K`, `⟪u - v, w⟫ = 0` (i.e., `u - v` is orthogonal to the subspace `K`).
+This is superceded by `norm_eq_infi_iff_inner_eq_zero` that gives the same conclusion over
+any `is_R_or_C` field.
+-/
+theorem norm_eq_infi_iff_real_inner_eq_zero (K : submodule ℝ F) {u : F} {v : F}
+  (hv : v ∈ K) : ∥u - v∥ = (⨅ w : (↑K : set F), ∥u - w∥) ↔ ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0 :=
+iff.intro
+begin
+  assume h,
+  have h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0,
+  { rwa [norm_eq_infi_iff_real_inner_le_zero] at h, exacts [K.convex, hv] },
+  assume w hw,
+  have le : ⟪u - v, w⟫_ℝ ≤ 0,
+    let w' := w + v,
+    have : w' ∈ K := submodule.add_mem _ hw hv,
+    have h₁ := h w' this,
+    have h₂ : w' - v = w, simp only [add_neg_cancel_right, sub_eq_add_neg],
+    rw h₂ at h₁, exact h₁,
+  have ge : ⟪u - v, w⟫_ℝ ≥ 0,
+    let w'' := -w + v,
+    have : w'' ∈ K := submodule.add_mem _ (submodule.neg_mem _ hw) hv,
+    have h₁ := h w'' this,
+    have h₂ : w'' - v = -w, simp only [neg_inj, add_neg_cancel_right, sub_eq_add_neg],
+    rw [h₂, inner_neg_right] at h₁,
+    linarith,
+    exact le_antisymm le ge
+end
+begin
+  assume h,
+  have : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0,
+    assume w hw,
+    let w' := w - v,
+    have : w' ∈ K := submodule.sub_mem _ hw hv,
+    have h₁ := h w' this,
+    exact le_of_eq h₁,
+  rwa norm_eq_infi_iff_real_inner_le_zero,
+  exacts [submodule.convex _, hv]
+end
+
+/--
+Characterization of minimizers in the projection on a subspace.
+Let `u` be a point in an inner product space, and let `K` be a nonempty subspace.
+Then point `v` minimizes the distance `∥u - v∥` over points in `K` if and only if
+for all `w ∈ K`, `⟪u - v, w⟫ = 0` (i.e., `u - v` is orthogonal to the subspace `K`)
+-/
+theorem norm_eq_infi_iff_inner_eq_zero {u : E} {v : E}
+  (hv : v ∈ K) : ∥u - v∥ = (⨅ w : (↑K : set E), ∥u - w∥) ↔ ∀ w ∈ K, ⟪u - v, w⟫ = 0 :=
+begin
+  letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜 E,
+  letI : module ℝ E := restrict_scalars.module ℝ 𝕜 E,
+  letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
+  let K' : submodule ℝ E := K.restrict_scalars ℝ,
+  split,
+  { assume H,
+    have A : ∀ w ∈ K, re ⟪u - v, w⟫ = 0 := (norm_eq_infi_iff_real_inner_eq_zero K' hv).1 H,
+    assume w hw,
+    apply ext,
+    { simp [A w hw] },
+    { symmetry, calc
+      im (0 : 𝕜) = 0 : im.map_zero
+      ... = re ⟪u - v, (-I) • w⟫ : (A _ (K.smul_mem (-I) hw)).symm
+      ... = re ((-I) * ⟪u - v, w⟫) : by rw inner_smul_right
+      ... = im ⟪u - v, w⟫ : by simp } },
+  { assume H,
+    have : ∀ w ∈ K', ⟪u - v, w⟫_ℝ = 0,
+    { assume w hw,
+      rw [real_inner_eq_re_inner, H w hw],
+      exact zero_re' },
+    exact (norm_eq_infi_iff_real_inner_eq_zero K' hv).2 this }
+end
+
+section orthogonal_projection
+variables [complete_space K]
+
+/-- The orthogonal projection onto a complete subspace, as an
+unbundled function.  This definition is only intended for use in
+setting up the bundled version `orthogonal_projection` and should not
+be used once that is defined. -/
+def orthogonal_projection_fn (v : E) :=
+(exists_norm_eq_infi_of_complete_subspace K (complete_space_coe_iff_is_complete.mp ‹_›) v).some
+
+variables {K}
+
+/-- The unbundled orthogonal projection is in the given subspace.
+This lemma is only intended for use in setting up the bundled version
+and should not be used once that is defined. -/
+lemma orthogonal_projection_fn_mem (v : E) : orthogonal_projection_fn K v ∈ K :=
+(exists_norm_eq_infi_of_complete_subspace K
+  (complete_space_coe_iff_is_complete.mp ‹_›) v).some_spec.some
+
+/-- The characterization of the unbundled orthogonal projection.  This
+lemma is only intended for use in setting up the bundled version
+and should not be used once that is defined. -/
+lemma orthogonal_projection_fn_inner_eq_zero (v : E) :
+  ∀ w ∈ K, ⟪v - orthogonal_projection_fn K v, w⟫ = 0 :=
+begin
+  rw ←norm_eq_infi_iff_inner_eq_zero K (orthogonal_projection_fn_mem v),
+  exact (exists_norm_eq_infi_of_complete_subspace K
+    (complete_space_coe_iff_is_complete.mp ‹_›) v).some_spec.some_spec
+end
+
+/-- The unbundled orthogonal projection is the unique point in `K`
+with the orthogonality property.  This lemma is only intended for use
+in setting up the bundled version and should not be used once that is
+defined. -/
+lemma eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero
+  {u v : E} (hvm : v ∈ K) (hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0) :
+  orthogonal_projection_fn K u = v :=
+begin
+  rw [←sub_eq_zero, ←inner_self_eq_zero],
+  have hvs : orthogonal_projection_fn K u - v ∈ K :=
+    submodule.sub_mem K (orthogonal_projection_fn_mem u) hvm,
+  have huo : ⟪u - orthogonal_projection_fn K u, orthogonal_projection_fn K u - v⟫ = 0 :=
+    orthogonal_projection_fn_inner_eq_zero u _ hvs,
+  have huv : ⟪u - v, orthogonal_projection_fn K u - v⟫ = 0 := hvo _ hvs,
+  have houv : ⟪(u - v) - (u - orthogonal_projection_fn K u), orthogonal_projection_fn K u - v⟫ = 0,
+  { rw [inner_sub_left, huo, huv, sub_zero] },
+  rwa sub_sub_sub_cancel_left at houv
+end
+
+variables (K)
+
+lemma orthogonal_projection_fn_norm_sq (v : E) :
+  ∥v∥ * ∥v∥ = ∥v - (orthogonal_projection_fn K v)∥ * ∥v - (orthogonal_projection_fn K v)∥
+            + ∥orthogonal_projection_fn K v∥ * ∥orthogonal_projection_fn K v∥ :=
+begin
+  set p := orthogonal_projection_fn K v,
+  have h' : ⟪v - p, p⟫ = 0,
+  { exact orthogonal_projection_fn_inner_eq_zero _ _ (orthogonal_projection_fn_mem v) },
+  convert norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (v - p) p h' using 2;
+  simp,
+end
+
+/-- The orthogonal projection onto a complete subspace. -/
+def orthogonal_projection : E →L[𝕜] K :=
+linear_map.mk_continuous
+  { to_fun := λ v, ⟨orthogonal_projection_fn K v, orthogonal_projection_fn_mem v⟩,
+    map_add' := λ x y, begin
+      have hm : orthogonal_projection_fn K x + orthogonal_projection_fn K y ∈ K :=
+        submodule.add_mem K (orthogonal_projection_fn_mem x) (orthogonal_projection_fn_mem y),
+      have ho :
+        ∀ w ∈ K, ⟪x + y - (orthogonal_projection_fn K x + orthogonal_projection_fn K y), w⟫ = 0,
+      { intros w hw,
+        rw [add_sub_comm, inner_add_left, orthogonal_projection_fn_inner_eq_zero _ w hw,
+            orthogonal_projection_fn_inner_eq_zero _ w hw, add_zero] },
+      ext,
+      simp [eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero hm ho]
+    end,
+    map_smul' := λ c x, begin
+      have hm : c • orthogonal_projection_fn K x ∈ K :=
+        submodule.smul_mem K _ (orthogonal_projection_fn_mem x),
+      have ho : ∀ w ∈ K, ⟪c • x - c • orthogonal_projection_fn K x, w⟫ = 0,
+      { intros w hw,
+        rw [←smul_sub, inner_smul_left, orthogonal_projection_fn_inner_eq_zero _ w hw, mul_zero] },
+      ext,
+      simp [eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero hm ho]
+    end }
+  1
+  (λ x, begin
+    simp only [one_mul, linear_map.coe_mk],
+    refine le_of_pow_le_pow 2 (norm_nonneg _) (by norm_num) _,
+    change ∥orthogonal_projection_fn K x∥ ^ 2 ≤ ∥x∥ ^ 2,
+    nlinarith [orthogonal_projection_fn_norm_sq K x]
+  end)
+
+variables {K}
+
+@[simp]
+lemma orthogonal_projection_fn_eq (v : E) :
+  orthogonal_projection_fn K v = (orthogonal_projection K v : E) :=
+rfl
+
+/-- The characterization of the orthogonal projection.  -/
+@[simp]
+lemma orthogonal_projection_inner_eq_zero (v : E) :
+  ∀ w ∈ K, ⟪v - orthogonal_projection K v, w⟫ = 0 :=
+orthogonal_projection_fn_inner_eq_zero v
+
+/-- The orthogonal projection is the unique point in `K` with the
+orthogonality property. -/
+lemma eq_orthogonal_projection_of_mem_of_inner_eq_zero
+  {u v : E} (hvm : v ∈ K) (hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0) :
+  (orthogonal_projection K u : E) = v :=
+eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero hvm hvo
+
+/-- The orthogonal projections onto equal subspaces are coerced back to the same point in `E`. -/
+lemma eq_orthogonal_projection_of_eq_submodule
+  {K' : submodule 𝕜 E} [complete_space K'] (h : K = K') (u : E) :
+  (orthogonal_projection K u : E) = (orthogonal_projection K' u : E) :=
+begin
+  change orthogonal_projection_fn K u = orthogonal_projection_fn K' u,
+  congr,
+  exact h
+end
+
+/-- The orthogonal projection sends elements of `K` to themselves. -/
+@[simp] lemma orthogonal_projection_mem_subspace_eq_self (v : K) : orthogonal_projection K v = v :=
+by { ext, apply eq_orthogonal_projection_of_mem_of_inner_eq_zero; simp }
+
+/-- A point equals its orthogonal projection if and only if it lies in the subspace. -/
+lemma orthogonal_projection_eq_self_iff {v : E} :
+  (orthogonal_projection K v : E) = v ↔ v ∈ K :=
+begin
+  refine ⟨λ h, _, λ h, eq_orthogonal_projection_of_mem_of_inner_eq_zero h _⟩,
+  { rw ← h,
+    simp },
+  { simp }
+end
+
+/-- Orthogonal projection onto the `submodule.map` of a subspace. -/
+lemma orthogonal_projection_map_apply {E E' : Type*} [inner_product_space 𝕜 E]
+  [inner_product_space 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (p : submodule 𝕜 E) [finite_dimensional 𝕜 p]
+  (x : E') :
+  (orthogonal_projection (p.map (f.to_linear_equiv : E →ₗ[𝕜] E')) x : E')
+  = f (orthogonal_projection p (f.symm x)) :=
+begin
+  apply eq_orthogonal_projection_of_mem_of_inner_eq_zero,
+  { exact ⟨orthogonal_projection p (f.symm x), submodule.coe_mem _, by simp⟩, },
+  rintros w ⟨a, ha, rfl⟩,
+  suffices : inner (f (f.symm x - orthogonal_projection p (f.symm x))) (f a) = (0:𝕜),
+  { simpa using this },
+  rw f.inner_map_map,
+  exact orthogonal_projection_inner_eq_zero _ _ ha,
+end
+
+/-- The orthogonal projection onto the trivial submodule is the zero map. -/
+@[simp] lemma orthogonal_projection_bot : orthogonal_projection (⊥ : submodule 𝕜 E) = 0 :=
+by ext
+
+variables (K)
+
+/-- The orthogonal projection has norm `≤ 1`. -/
+lemma orthogonal_projection_norm_le : ∥orthogonal_projection K∥ ≤ 1 :=
+linear_map.mk_continuous_norm_le _ (by norm_num) _
+
+variables (𝕜)
+
+lemma smul_orthogonal_projection_singleton {v : E} (w : E) :
+  (∥v∥ ^ 2 : 𝕜) • (orthogonal_projection (𝕜 ∙ v) w : E) = ⟪v, w⟫ • v :=
+begin
+  suffices : ↑(orthogonal_projection (𝕜 ∙ v) ((∥v∥ ^ 2 : 𝕜) • w)) = ⟪v, w⟫ • v,
+  { simpa using this },
+  apply eq_orthogonal_projection_of_mem_of_inner_eq_zero,
+  { rw submodule.mem_span_singleton,
+    use ⟪v, w⟫ },
+  { intros x hx,
+    obtain ⟨c, rfl⟩ := submodule.mem_span_singleton.mp hx,
+    have hv : ↑∥v∥ ^ 2 = ⟪v, v⟫ := by { norm_cast, simp [norm_sq_eq_inner] },
+    simp [inner_sub_left, inner_smul_left, inner_smul_right, is_R_or_C.conj_div, mul_comm, hv,
+      inner_product_space.conj_sym, hv] }
+end
+
+/-- Formula for orthogonal projection onto a single vector. -/
+lemma orthogonal_projection_singleton {v : E} (w : E) :
+  (orthogonal_projection (𝕜 ∙ v) w : E) = (⟪v, w⟫ / ∥v∥ ^ 2) • v :=
+begin
+  by_cases hv : v = 0,
+  { rw [hv, eq_orthogonal_projection_of_eq_submodule submodule.span_zero_singleton],
+    { simp },
+    { apply_instance } },
+  have hv' : ∥v∥ ≠ 0 := ne_of_gt (norm_pos_iff.mpr hv),
+  have key : ((∥v∥ ^ 2 : 𝕜)⁻¹ * ∥v∥ ^ 2) • ↑(orthogonal_projection (𝕜 ∙ v) w)
+              = ((∥v∥ ^ 2 : 𝕜)⁻¹ * ⟪v, w⟫) • v,
+  { simp [mul_smul, smul_orthogonal_projection_singleton 𝕜 w] },
+  convert key;
+  field_simp [hv']
+end
+
+/-- Formula for orthogonal projection onto a single unit vector. -/
+lemma orthogonal_projection_unit_singleton {v : E} (hv : ∥v∥ = 1) (w : E) :
+  (orthogonal_projection (𝕜 ∙ v) w : E) = ⟪v, w⟫ • v :=
+by { rw ← smul_orthogonal_projection_singleton 𝕜 w, simp [hv] }
+
+end orthogonal_projection
+
+section reflection
+variables {𝕜} (K) [complete_space K]
+
+/-- Reflection in a complete subspace of an inner product space.  The word "reflection" is
+sometimes understood to mean specifically reflection in a codimension-one subspace, and sometimes
+more generally to cover operations such as reflection in a point.  The definition here, of
+reflection in a subspace, is a more general sense of the word that includes both those common
+cases. -/
+def reflection : E ≃ₗᵢ[𝕜] E :=
+{ norm_map' := begin
+    intros x,
+    let w : K := orthogonal_projection K x,
+    let v := x - w,
+    have : ⟪v, w⟫ = 0 := orthogonal_projection_inner_eq_zero x w w.2,
+    convert norm_sub_eq_norm_add this using 2,
+    { simp [bit0],
+      dsimp [w, v],
+      abel },
+    { simp [bit0] }
+  end,
+  ..linear_equiv.of_involutive
+      (bit0 (K.subtype.comp (orthogonal_projection K).to_linear_map) - linear_map.id)
+      (λ x, by simp [bit0]) }
+
+variables {K}
+
+/-- The result of reflecting. -/
+lemma reflection_apply (p : E) : reflection K p = bit0 ↑(orthogonal_projection K p) - p := rfl
+
+/-- Reflection is its own inverse. -/
+@[simp] lemma reflection_symm : (reflection K).symm = reflection K := rfl
+
+variables (K)
+
+/-- Reflecting twice in the same subspace. -/
+@[simp] lemma reflection_reflection (p : E) : reflection K (reflection K p) = p :=
+(reflection K).left_inv p
+
+/-- Reflection is involutive. -/
+lemma reflection_involutive : function.involutive (reflection K) := reflection_reflection K
+
+variables {K}
+
+/-- A point is its own reflection if and only if it is in the subspace. -/
+lemma reflection_eq_self_iff (x : E) : reflection K x = x ↔ x ∈ K :=
+begin
+  rw [←orthogonal_projection_eq_self_iff, reflection_apply, sub_eq_iff_eq_add', ← two_smul 𝕜,
+    ← two_smul' 𝕜],
+  refine (smul_right_injective E _).eq_iff,
+  exact two_ne_zero
+end
+
+lemma reflection_mem_subspace_eq_self {x : E} (hx : x ∈ K) : reflection K x = x :=
+(reflection_eq_self_iff x).mpr hx
+
+/-- Reflection in the `submodule.map` of a subspace. -/
+lemma reflection_map_apply {E E' : Type*} [inner_product_space 𝕜 E] [inner_product_space 𝕜 E']
+  (f : E ≃ₗᵢ[𝕜] E') (K : submodule 𝕜 E) [finite_dimensional 𝕜 K] (x : E') :
+  reflection (K.map (f.to_linear_equiv : E →ₗ[𝕜] E')) x = f (reflection K (f.symm x)) :=
+by simp [bit0, reflection_apply, orthogonal_projection_map_apply f K x]
+
+/-- Reflection in the `submodule.map` of a subspace. -/
+lemma reflection_map {E E' : Type*} [inner_product_space 𝕜 E] [inner_product_space 𝕜 E']
+  (f : E ≃ₗᵢ[𝕜] E') (K : submodule 𝕜 E) [finite_dimensional 𝕜 K] :
+  reflection (K.map (f.to_linear_equiv : E →ₗ[𝕜] E')) = f.symm.trans ((reflection K).trans f) :=
+linear_isometry_equiv.ext $ reflection_map_apply f K
+
+/-- Reflection through the trivial subspace {0} is just negation. -/
+@[simp] lemma reflection_bot : reflection (⊥ : submodule 𝕜 E) = linear_isometry_equiv.neg 𝕜 :=
+by ext; simp [reflection_apply]
+
+end reflection
+
+section orthogonal
+
+/-- If `K₁` is complete and contained in `K₂`, `K₁` and `K₁ᗮ ⊓ K₂` span `K₂`. -/
+lemma submodule.sup_orthogonal_inf_of_is_complete {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂)
+  (hc : is_complete (K₁ : set E)) : K₁ ⊔ (K₁ᗮ ⊓ K₂) = K₂ :=
+begin
+  ext x,
+  rw submodule.mem_sup,
+  rcases exists_norm_eq_infi_of_complete_subspace K₁ hc x with ⟨v, hv, hvm⟩,
+  rw norm_eq_infi_iff_inner_eq_zero K₁ hv at hvm,
+  split,
+  { rintro ⟨y, hy, z, hz, rfl⟩,
+    exact K₂.add_mem (h hy) hz.2 },
+  { exact λ hx, ⟨v, hv, x - v, ⟨(K₁.mem_orthogonal' _).2 hvm, K₂.sub_mem hx (h hv)⟩,
+                 add_sub_cancel'_right _ _⟩ }
+end
+
+variables {K}
+
+/-- If `K` is complete, `K` and `Kᗮ` span the whole space. -/
+lemma submodule.sup_orthogonal_of_is_complete (h : is_complete (K : set E)) : K ⊔ Kᗮ = ⊤ :=
+begin
+  convert submodule.sup_orthogonal_inf_of_is_complete (le_top : K ≤ ⊤) h,
+  simp
+end
+
+/-- If `K` is complete, `K` and `Kᗮ` span the whole space. Version using `complete_space`. -/
+lemma submodule.sup_orthogonal_of_complete_space [complete_space K] : K ⊔ Kᗮ = ⊤ :=
+submodule.sup_orthogonal_of_is_complete (complete_space_coe_iff_is_complete.mp ‹_›)
+
+variables (K)
+
+/-- If `K` is complete, any `v` in `E` can be expressed as a sum of elements of `K` and `Kᗮ`. -/
+lemma submodule.exists_sum_mem_mem_orthogonal [complete_space K] (v : E) :
+  ∃ (y ∈ K) (z ∈ Kᗮ), v = y + z :=
+begin
+  have h_mem : v ∈ K ⊔ Kᗮ := by simp [submodule.sup_orthogonal_of_complete_space],
+  obtain ⟨y, hy, z, hz, hyz⟩ := submodule.mem_sup.mp h_mem,
+  exact ⟨y, hy, z, hz, hyz.symm⟩
+end
+
+/-- If `K` is complete, then the orthogonal complement of its orthogonal complement is itself. -/
+@[simp] lemma submodule.orthogonal_orthogonal [complete_space K] : Kᗮᗮ = K :=
+begin
+  ext v,
+  split,
+  { obtain ⟨y, hy, z, hz, rfl⟩ := K.exists_sum_mem_mem_orthogonal v,
+    intros hv,
+    have hz' : z = 0,
+    { have hyz : ⟪z, y⟫ = 0 := by simp [hz y hy, inner_eq_zero_sym],
+      simpa [inner_add_right, hyz] using hv z hz },
+    simp [hy, hz'] },
+  { intros hv w hw,
+    rw inner_eq_zero_sym,
+    exact hw v hv }
+end
+
+lemma submodule.orthogonal_orthogonal_eq_closure [complete_space E] :
+  Kᗮᗮ = K.topological_closure :=
+begin
+  refine le_antisymm _ _,
+  { convert submodule.orthogonal_orthogonal_monotone K.submodule_topological_closure,
+    haveI : complete_space K.topological_closure :=
+      K.is_closed_topological_closure.complete_space_coe,
+    rw K.topological_closure.orthogonal_orthogonal },
+  { exact K.topological_closure_minimal K.le_orthogonal_orthogonal Kᗮ.is_closed_orthogonal }
+end
+
+variables {K}
+
+/-- If `K` is complete, `K` and `Kᗮ` are complements of each other. -/
+lemma submodule.is_compl_orthogonal_of_is_complete (h : is_complete (K : set E)) : is_compl K Kᗮ :=
+⟨K.orthogonal_disjoint, le_of_eq (submodule.sup_orthogonal_of_is_complete h).symm⟩
+
+@[simp] lemma submodule.orthogonal_eq_bot_iff (hK : is_complete (K : set E)) :
+  Kᗮ = ⊥ ↔ K = ⊤ :=
+begin
+  refine ⟨_, by { rintro rfl, exact submodule.top_orthogonal_eq_bot }⟩,
+  intro h,
+  have : K ⊔ Kᗮ = ⊤ := submodule.sup_orthogonal_of_is_complete hK,
+  rwa [h, sup_comm, bot_sup_eq] at this,
+end
+
+/-- A point in `K` with the orthogonality property (here characterized in terms of `Kᗮ`) must be the
+orthogonal projection. -/
+lemma eq_orthogonal_projection_of_mem_orthogonal
+  [complete_space K] {u v : E} (hv : v ∈ K) (hvo : u - v ∈ Kᗮ) :
+  (orthogonal_projection K u : E) = v :=
+eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero hv (λ w, inner_eq_zero_sym.mp ∘ (hvo w))
+
+/-- A point in `K` with the orthogonality property (here characterized in terms of `Kᗮ`) must be the
+orthogonal projection. -/
+lemma eq_orthogonal_projection_of_mem_orthogonal'
+  [complete_space K] {u v z : E} (hv : v ∈ K) (hz : z ∈ Kᗮ) (hu : u = v + z) :
+  (orthogonal_projection K u : E) = v :=
+eq_orthogonal_projection_of_mem_orthogonal hv (by simpa [hu])
+
+/-- The orthogonal projection onto `K` of an element of `Kᗮ` is zero. -/
+lemma orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero
+  [complete_space K] {v : E} (hv : v ∈ Kᗮ) :
+  orthogonal_projection K v = 0 :=
+by { ext, convert eq_orthogonal_projection_of_mem_orthogonal _ _; simp [hv] }
+
+/-- The reflection in `K` of an element of `Kᗮ` is its negation. -/
+lemma reflection_mem_subspace_orthogonal_complement_eq_neg
+  [complete_space K] {v : E} (hv : v ∈ Kᗮ) :
+  reflection K v = - v :=
+by simp [reflection_apply, orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero hv]
+
+/-- The orthogonal projection onto `Kᗮ` of an element of `K` is zero. -/
+lemma orthogonal_projection_mem_subspace_orthogonal_precomplement_eq_zero
+  [complete_space E] {v : E} (hv : v ∈ K) :
+  orthogonal_projection Kᗮ v = 0 :=
+orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero (K.le_orthogonal_orthogonal hv)
+
+/-- The reflection in `Kᗮ` of an element of `K` is its negation. -/
+lemma reflection_mem_subspace_orthogonal_precomplement_eq_neg
+  [complete_space E] {v : E} (hv : v ∈ K) :
+  reflection Kᗮ v = -v :=
+reflection_mem_subspace_orthogonal_complement_eq_neg (K.le_orthogonal_orthogonal hv)
+
+/-- The orthogonal projection onto `(𝕜 ∙ v)ᗮ` of `v` is zero. -/
+lemma orthogonal_projection_orthogonal_complement_singleton_eq_zero [complete_space E] (v : E) :
+  orthogonal_projection (𝕜 ∙ v)ᗮ v = 0 :=
+orthogonal_projection_mem_subspace_orthogonal_precomplement_eq_zero
+  (submodule.mem_span_singleton_self v)
+
+/-- The reflection in `(𝕜 ∙ v)ᗮ` of `v` is `-v`. -/
+lemma reflection_orthogonal_complement_singleton_eq_neg [complete_space E] (v : E) :
+  reflection (𝕜 ∙ v)ᗮ v = -v :=
+reflection_mem_subspace_orthogonal_precomplement_eq_neg (submodule.mem_span_singleton_self v)
+
+variables (K)
+
+/-- In a complete space `E`, a vector splits as the sum of its orthogonal projections onto a
+complete submodule `K` and onto the orthogonal complement of `K`.-/
+lemma eq_sum_orthogonal_projection_self_orthogonal_complement
+  [complete_space E] [complete_space K] (w : E) :
+  w = (orthogonal_projection K w : E) + (orthogonal_projection Kᗮ w : E) :=
+begin
+  obtain ⟨y, hy, z, hz, hwyz⟩ := K.exists_sum_mem_mem_orthogonal w,
+  convert hwyz,
+  { exact eq_orthogonal_projection_of_mem_orthogonal' hy hz hwyz },
+  { rw add_comm at hwyz,
+    refine eq_orthogonal_projection_of_mem_orthogonal' hz _ hwyz,
+    simp [hy] }
+end
+
+/-- In a complete space `E`, the projection maps onto a complete subspace `K` and its orthogonal
+complement sum to the identity. -/
+lemma id_eq_sum_orthogonal_projection_self_orthogonal_complement
+  [complete_space E] [complete_space K] :
+  continuous_linear_map.id 𝕜 E
+  = K.subtypeL.comp (orthogonal_projection K)
+  + Kᗮ.subtypeL.comp (orthogonal_projection Kᗮ) :=
+by { ext w, exact eq_sum_orthogonal_projection_self_orthogonal_complement K w }
+
+/-- The orthogonal projection is self-adjoint. -/
+lemma inner_orthogonal_projection_left_eq_right [complete_space E]
+  [complete_space K] (u v : E) :
+  ⟪↑(orthogonal_projection K u), v⟫ = ⟪u, orthogonal_projection K v⟫ :=
+begin
+  nth_rewrite 0 eq_sum_orthogonal_projection_self_orthogonal_complement K v,
+  nth_rewrite 1 eq_sum_orthogonal_projection_self_orthogonal_complement K u,
+  rw [inner_add_left, inner_add_right,
+    submodule.inner_right_of_mem_orthogonal (submodule.coe_mem (orthogonal_projection K u))
+      (submodule.coe_mem (orthogonal_projection Kᗮ v)),
+    submodule.inner_left_of_mem_orthogonal (submodule.coe_mem (orthogonal_projection K v))
+      (submodule.coe_mem (orthogonal_projection Kᗮ u))],
+end
+
+open finite_dimensional
+
+/-- Given a finite-dimensional subspace `K₂`, and a subspace `K₁`
+containined in it, the dimensions of `K₁` and the intersection of its
+orthogonal subspace with `K₂` add to that of `K₂`. -/
+lemma submodule.finrank_add_inf_finrank_orthogonal {K₁ K₂ : submodule 𝕜 E}
+  [finite_dimensional 𝕜 K₂] (h : K₁ ≤ K₂) :
+  finrank 𝕜 K₁ + finrank 𝕜 (K₁ᗮ ⊓ K₂ : submodule 𝕜 E) = finrank 𝕜 K₂ :=
+begin
+  haveI := submodule.finite_dimensional_of_le h,
+  have hd := submodule.dim_sup_add_dim_inf_eq K₁ (K₁ᗮ ⊓ K₂),
+  rw [←inf_assoc, (submodule.orthogonal_disjoint K₁).eq_bot, bot_inf_eq, finrank_bot,
+      submodule.sup_orthogonal_inf_of_is_complete h
+        (submodule.complete_of_finite_dimensional _)] at hd,
+  rw add_zero at hd,
+  exact hd.symm
+end
+
+/-- Given a finite-dimensional subspace `K₂`, and a subspace `K₁`
+containined in it, the dimensions of `K₁` and the intersection of its
+orthogonal subspace with `K₂` add to that of `K₂`. -/
+lemma submodule.finrank_add_inf_finrank_orthogonal' {K₁ K₂ : submodule 𝕜 E}
+  [finite_dimensional 𝕜 K₂] (h : K₁ ≤ K₂) {n : ℕ} (h_dim : finrank 𝕜 K₁ + n = finrank 𝕜 K₂) :
+  finrank 𝕜 (K₁ᗮ ⊓ K₂ : submodule 𝕜 E) = n :=
+by { rw ← add_right_inj (finrank 𝕜 K₁),
+     simp [submodule.finrank_add_inf_finrank_orthogonal h, h_dim] }
+
+/-- Given a finite-dimensional space `E` and subspace `K`, the dimensions of `K` and `Kᗮ` add to
+that of `E`. -/
+lemma submodule.finrank_add_finrank_orthogonal [finite_dimensional 𝕜 E] {K : submodule 𝕜 E} :
+  finrank 𝕜 K + finrank 𝕜 Kᗮ = finrank 𝕜 E :=
+begin
+  convert submodule.finrank_add_inf_finrank_orthogonal (le_top : K ≤ ⊤) using 1,
+  { rw inf_top_eq },
+  { simp }
+end
+
+/-- Given a finite-dimensional space `E` and subspace `K`, the dimensions of `K` and `Kᗮ` add to
+that of `E`. -/
+lemma submodule.finrank_add_finrank_orthogonal' [finite_dimensional 𝕜 E] {K : submodule 𝕜 E} {n : ℕ}
+  (h_dim : finrank 𝕜 K + n = finrank 𝕜 E) :
+  finrank 𝕜 Kᗮ = n :=
+by { rw ← add_right_inj (finrank 𝕜 K), simp [submodule.finrank_add_finrank_orthogonal, h_dim] }
+
+local attribute [instance] fact_finite_dimensional_of_finrank_eq_succ
+
+/-- In a finite-dimensional inner product space, the dimension of the orthogonal complement of the
+span of a nonzero vector is one less than the dimension of the space. -/
+lemma finrank_orthogonal_span_singleton {n : ℕ} [_i : fact (finrank 𝕜 E = n + 1)]
+  {v : E} (hv : v ≠ 0) :
+  finrank 𝕜 (𝕜 ∙ v)ᗮ = n :=
+submodule.finrank_add_finrank_orthogonal' $ by simp [finrank_span_singleton hv, _i.elim, add_comm]
+
+end orthogonal
+
+
+section orthonormal_basis
+
+/-! ### Existence of Hilbert basis, orthonormal basis, etc. -/
+
+variables {𝕜 E} {v : set E}
+
+open finite_dimensional submodule set
+
+/-- An orthonormal set in an `inner_product_space` is maximal, if and only if the orthogonal
+complement of its span is empty. -/
+lemma maximal_orthonormal_iff_orthogonal_complement_eq_bot (hv : orthonormal 𝕜 (coe : v → E)) :
+  (∀ u ⊇ v, orthonormal 𝕜 (coe : u → E) → u = v) ↔ (span 𝕜 v)ᗮ = ⊥ :=
+begin
+  rw submodule.eq_bot_iff,
+  split,
+  { contrapose!,
+    -- ** direction 1: nonempty orthogonal complement implies nonmaximal
+    rintros ⟨x, hx', hx⟩,
+    -- take a nonzero vector and normalize it
+    let e := (∥x∥⁻¹ : 𝕜) • x,
+    have he : ∥e∥ = 1 := by simp [e, norm_smul_inv_norm hx],
+    have he' : e ∈ (span 𝕜 v)ᗮ := smul_mem' _ _ hx',
+    have he'' : e ∉ v,
+    { intros hev,
+      have : e = 0,
+      { have : e ∈ (span 𝕜 v) ⊓ (span 𝕜 v)ᗮ := ⟨subset_span hev, he'⟩,
+        simpa [(span 𝕜 v).inf_orthogonal_eq_bot] using this },
+      have : e ≠ 0 := hv.ne_zero ⟨e, hev⟩,
+      contradiction },
+    -- put this together with `v` to provide a candidate orthonormal basis for the whole space
+    refine ⟨v.insert e, v.subset_insert e, ⟨_, _⟩, (v.ne_insert_of_not_mem he'').symm⟩,
+    { -- show that the elements of `v.insert e` have unit length
+      rintros ⟨a, ha'⟩,
+      cases eq_or_mem_of_mem_insert ha' with ha ha,
+      { simp [ha, he] },
+      { exact hv.1 ⟨a, ha⟩ } },
+    { -- show that the elements of `v.insert e` are orthogonal
+      have h_end : ∀ a ∈ v, ⟪a, e⟫ = 0,
+      { intros a ha,
+        exact he' a (submodule.subset_span ha) },
+      rintros ⟨a, ha'⟩,
+      cases eq_or_mem_of_mem_insert ha' with ha ha,
+      { rintros ⟨b, hb'⟩ hab',
+        have hb : b ∈ v,
+        { refine mem_of_mem_insert_of_ne hb' _,
+          intros hbe',
+          apply hab',
+          simp [ha, hbe'] },
+        rw inner_eq_zero_sym,
+        simpa [ha] using h_end b hb },
+      rintros ⟨b, hb'⟩ hab',
+      cases eq_or_mem_of_mem_insert hb' with hb hb,
+      { simpa [hb] using h_end a ha },
+      have : (⟨a, ha⟩ : v) ≠ ⟨b, hb⟩,
+      { intros hab'',
+        apply hab',
+        simpa using hab'' },
+      exact hv.2 this } },
+    { -- ** direction 2: empty orthogonal complement implies maximal
+      simp only [subset.antisymm_iff],
+      rintros h u (huv : v ⊆ u) hu,
+      refine ⟨_, huv⟩,
+      intros x hxu,
+      refine ((mt (h x)) (hu.ne_zero ⟨x, hxu⟩)).imp_symm _,
+      intros hxv y hy,
+      have hxv' : (⟨x, hxu⟩ : u) ∉ (coe ⁻¹' v : set u) := by simp [huv, hxv],
+      obtain ⟨l, hl, rfl⟩ :
+        ∃ l ∈ finsupp.supported 𝕜 𝕜 (coe ⁻¹' v : set u), (finsupp.total ↥u E 𝕜 coe) l = y,
+      { rw ← finsupp.mem_span_image_iff_total,
+        simp [huv, inter_eq_self_of_subset_left, hy] },
+      exact hu.inner_finsupp_eq_zero hxv' hl }
+end
+
+/-- An orthonormal set in an `inner_product_space` is maximal, if and only if the closure of its
+span is the whole space. -/
+lemma maximal_orthonormal_iff_dense_span [complete_space E] (hv : orthonormal 𝕜 (coe : v → E)) :
+  (∀ u ⊇ v, orthonormal 𝕜 (coe : u → E) → u = v) ↔ (span 𝕜 v).topological_closure = ⊤ :=
+by rw [maximal_orthonormal_iff_orthogonal_complement_eq_bot hv, ← submodule.orthogonal_eq_top_iff,
+  (span 𝕜 v).orthogonal_orthogonal_eq_closure]
+
+/-- Any orthonormal subset can be extended to an orthonormal set whose span is dense. -/
+lemma exists_subset_is_orthonormal_dense_span
+  [complete_space E] (hv : orthonormal 𝕜 (coe : v → E)) :
+  ∃ u ⊇ v, orthonormal 𝕜 (coe : u → E) ∧ (span 𝕜 u).topological_closure = ⊤ :=
+begin
+  obtain ⟨u, hus, hu, hu_max⟩ := exists_maximal_orthonormal hv,
+  rw maximal_orthonormal_iff_dense_span hu at hu_max,
+  exact ⟨u, hus, hu, hu_max⟩
+end
+
+variables (𝕜 E)
+/-- An inner product space admits an orthonormal set whose span is dense. -/
+lemma exists_is_orthonormal_dense_span [complete_space E] :
+  ∃ u : set E, orthonormal 𝕜 (coe : u → E) ∧ (span 𝕜 u).topological_closure = ⊤ :=
+let ⟨u, hus, hu, hu_max⟩ := exists_subset_is_orthonormal_dense_span (orthonormal_empty 𝕜 E) in
+⟨u, hu, hu_max⟩
+variables {𝕜 E}
+
+/-- An orthonormal set in a finite-dimensional `inner_product_space` is maximal, if and only if it
+is a basis. -/
+lemma maximal_orthonormal_iff_basis_of_finite_dimensional
+  [finite_dimensional 𝕜 E] (hv : orthonormal 𝕜 (coe : v → E)) :
+  (∀ u ⊇ v, orthonormal 𝕜 (coe : u → E) → u = v) ↔ ∃ b : basis v 𝕜 E, ⇑b = coe :=
+begin
+  rw maximal_orthonormal_iff_orthogonal_complement_eq_bot hv,
+  have hv_compl : is_complete (span 𝕜 v : set E) := (span 𝕜 v).complete_of_finite_dimensional,
+  rw submodule.orthogonal_eq_bot_iff hv_compl,
+  have hv_coe : range (coe : v → E) = v := by simp,
+  split,
+  { refine λ h, ⟨basis.mk hv.linear_independent _, basis.coe_mk _ _⟩,
+    convert h },
+  { rintros ⟨h, coe_h⟩,
+    rw [← h.span_eq, coe_h, hv_coe] }
+end
+
+/-- In a finite-dimensional `inner_product_space`, any orthonormal subset can be extended to an
+orthonormal basis. -/
+lemma exists_subset_is_orthonormal_basis
+  [finite_dimensional 𝕜 E] (hv : orthonormal 𝕜 (coe : v → E)) :
+  ∃ (u ⊇ v) (b : basis u 𝕜 E), orthonormal 𝕜 b ∧ ⇑b = coe :=
+begin
+  obtain ⟨u, hus, hu, hu_max⟩ := exists_maximal_orthonormal hv,
+  obtain ⟨b, hb⟩ := (maximal_orthonormal_iff_basis_of_finite_dimensional hu).mp hu_max,
+  exact ⟨u, hus, b, by rwa hb, hb⟩
+end
+
+variables (𝕜 E)
+
+/-- Index for an arbitrary orthonormal basis on a finite-dimensional `inner_product_space`. -/
+def orthonormal_basis_index [finite_dimensional 𝕜 E] : set E :=
+classical.some (exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E))
+
+/-- A finite-dimensional `inner_product_space` has an orthonormal basis. -/
+def orthonormal_basis [finite_dimensional 𝕜 E] :
+  basis (orthonormal_basis_index 𝕜 E) 𝕜 E :=
+(exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some
+
+lemma orthonormal_basis_orthonormal [finite_dimensional 𝕜 E] :
+  orthonormal 𝕜 (orthonormal_basis 𝕜 E) :=
+(exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some_spec.1
+
+@[simp] lemma coe_orthonormal_basis [finite_dimensional 𝕜 E] :
+  ⇑(orthonormal_basis 𝕜 E) = coe :=
+(exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some_spec.2
+
+instance [finite_dimensional 𝕜 E] : fintype (orthonormal_basis_index 𝕜 E) :=
+is_noetherian.fintype_basis_index (orthonormal_basis 𝕜 E)
+
+variables {𝕜 E}
+
+/-- An `n`-dimensional `inner_product_space` has an orthonormal basis indexed by `fin n`. -/
+def fin_orthonormal_basis [finite_dimensional 𝕜 E] {n : ℕ} (hn : finrank 𝕜 E = n) :
+  basis (fin n) 𝕜 E :=
+have h : fintype.card (orthonormal_basis_index 𝕜 E) = n,
+by rw [← finrank_eq_card_basis (orthonormal_basis 𝕜 E), hn],
+(orthonormal_basis 𝕜 E).reindex (fintype.equiv_fin_of_card_eq h)
+
+lemma fin_orthonormal_basis_orthonormal [finite_dimensional 𝕜 E] {n : ℕ} (hn : finrank 𝕜 E = n) :
+  orthonormal 𝕜 (fin_orthonormal_basis hn) :=
+suffices orthonormal 𝕜 (orthonormal_basis _ _ ∘ equiv.symm _),
+by { simp only [fin_orthonormal_basis, basis.coe_reindex], assumption }, -- why doesn't simpa work?
+(orthonormal_basis_orthonormal 𝕜 E).comp _ (equiv.injective _)
+
+end orthonormal_basis
diff --git a/src/analysis/normed_space/dual.lean b/src/analysis/normed_space/dual.lean
index 48cd58d573e11..f248e1230e4fa 100644
--- a/src/analysis/normed_space/dual.lean
+++ b/src/analysis/normed_space/dual.lean
@@ -3,8 +3,9 @@ Copyright (c) 2020 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth, Frédéric Dupuis
 -/
+import analysis.inner_product_space.projection
+import analysis.normed_space.bounded_linear_maps
 import analysis.normed_space.hahn_banach
-import analysis.normed_space.inner_product
 
 /-!
 # The topological dual of a normed space
diff --git a/src/analysis/normed_space/pi_Lp.lean b/src/analysis/normed_space/pi_Lp.lean
index 9720cf977fea3..40cd748399a2d 100644
--- a/src/analysis/normed_space/pi_Lp.lean
+++ b/src/analysis/normed_space/pi_Lp.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import analysis.mean_inequalities
-import analysis.normed_space.inner_product
+import analysis.inner_product_space.projection
 
 /-!
 # `L^p` distance on finite products of metric spaces
diff --git a/src/analysis/quaternion.lean b/src/analysis/quaternion.lean
index c4688009f216b..3ae29c43b58ef 100644
--- a/src/analysis/quaternion.lean
+++ b/src/analysis/quaternion.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import algebra.quaternion
-import analysis.normed_space.inner_product
+import analysis.inner_product_space.basic
 
 /-!
 # Quaternions as a normed algebra
diff --git a/src/geometry/euclidean/basic.lean b/src/geometry/euclidean/basic.lean
index da363f1bf2c98..76fb41e50c077 100644
--- a/src/geometry/euclidean/basic.lean
+++ b/src/geometry/euclidean/basic.lean
@@ -3,13 +3,9 @@ Copyright (c) 2020 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers, Manuel Candales
 -/
+import analysis.inner_product_space.projection
 import analysis.special_functions.trigonometric
-import algebra.quadratic_discriminant
-import analysis.normed_space.affine_isometry
-import data.matrix.notation
 import linear_algebra.affine_space.finite_dimensional
-import tactic.fin_cases
-import analysis.normed_space.inner_product
 
 /-!
 # Euclidean spaces
diff --git a/src/geometry/manifold/instances/sphere.lean b/src/geometry/manifold/instances/sphere.lean
index 1bc71762cb955..94926f3270231 100644
--- a/src/geometry/manifold/instances/sphere.lean
+++ b/src/geometry/manifold/instances/sphere.lean
@@ -5,6 +5,7 @@ Authors: Heather Macbeth
 -/
 import geometry.manifold.instances.real
 import analysis.complex.circle
+import analysis.inner_product_space.calculus
 
 /-!
 # Manifold structure on the sphere
diff --git a/src/measure_theory/function/l2_space.lean b/src/measure_theory/function/l2_space.lean
index 74051ccb673d9..ff3d49ae545a3 100644
--- a/src/measure_theory/function/l2_space.lean
+++ b/src/measure_theory/function/l2_space.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import analysis.normed_space.inner_product
+import analysis.inner_product_space.basic
 import measure_theory.integral.set_integral
 
 /-! # `L^2` space
diff --git a/src/measure_theory/function/special_functions.lean b/src/measure_theory/function/special_functions.lean
index a4cfabfd58e7b..fc35205369326 100644
--- a/src/measure_theory/function/special_functions.lean
+++ b/src/measure_theory/function/special_functions.lean
@@ -5,7 +5,7 @@ Authors: Yury Kudryashov
 -/
 
 import analysis.special_functions.pow
-import analysis.normed_space.inner_product
+import analysis.inner_product_space.calculus
 import measure_theory.constructions.borel_space
 
 /-!