refactor(analysis/normed_space/real_inner_product,geometry/euclidean)…

…: orthogonal projection hypotheses (#3952)

As advised by Patrick in #3932, define `orthogonal_projection` (for
both real inner product spaces and Euclidean affine spaces) without
taking hypotheses of the subspace being nonempty and complete,
defaulting to the identity map if those conditions are not satisfied,
so making `orthogonal_projection` more convenient to use with those
properties only being needed on lemmas but not simply to refer to the
orthogonal projection at all.

The hypotheses are removed from lemmas that don't need them because
they are still true with the identity map.  Some `nonempty` hypotheses
are also removed where they follow from another hypothesis that gives
a point or a nonempty set of points in the subspace.

The unbundled `orthogonal_projection_fn` that's used only to prove
properties needed to define a bundled linear or affine map still takes
the original hypotheses, then a bundled map taking those hypotheses is
defined under a new name, then that map is used to define plain
`orthogonal_projection` which does not take any of those hypotheses
and is the version expected to be used in all lemmas after it has been
defined.

src/analysis/normed_space/real_inner_product.lean

@@ -45,6 +45,7 @@ noncomputable theory
 
 open real set
 open_locale big_operators
+open_locale classical
 open_locale topological_space
 
 universes u v w
@@ -965,8 +966,12 @@ begin
   rwa sub_sub_sub_cancel_left at houv
 end
 
-/-- The orthogonal projection onto a complete subspace. -/
-def orthogonal_projection {K : submodule ℝ α} (h : is_complete (K : set α)) : linear_map ℝ α α :=
+/-- The orthogonal projection onto a complete subspace.  For most
+purposes, `orthogonal_projection`, which removes the `is_complete`
+hypothesis and is the identity map when the subspace is not complete,
+should be used instead. -/
+def orthogonal_projection_of_complete {K : submodule ℝ α} (h : is_complete (K : set α)) :
+  linear_map ℝ α α :=
 { to_fun := orthogonal_projection_fn h,
   map_add' := λ x y, begin
     have hm : orthogonal_projection_fn h x + orthogonal_projection_fn h y ∈ K :=
@@ -987,26 +992,51 @@ def orthogonal_projection {K : submodule ℝ α} (h : is_complete (K : set α))
     rw eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero h hm ho
   end }
 
+/-- The orthogonal projection onto a subspace, which is expected to be
+complete.  If the subspace is not complete, this uses the identity map
+instead. -/
+def orthogonal_projection (K : submodule ℝ α) : linear_map ℝ α α :=
+if h : is_complete (K : set α) then orthogonal_projection_of_complete h else linear_map.id
+
+/-- The definition of `orthogonal_projection` using `if`. -/
+lemma orthogonal_projection_def (K : submodule ℝ α) :
+  orthogonal_projection K =
+    if h : is_complete (K : set α) then orthogonal_projection_of_complete h else linear_map.id :=
+rfl
+
 @[simp]
 lemma orthogonal_projection_fn_eq {K : submodule ℝ α} (h : is_complete (K : set α)) (v : α) :
-  orthogonal_projection_fn h v = orthogonal_projection h v := rfl
+  orthogonal_projection_fn h v = orthogonal_projection K v :=
+by { rw [orthogonal_projection_def, dif_pos h], refl }
+
 /-- The orthogonal projection is in the given subspace. -/
 lemma orthogonal_projection_mem {K : submodule ℝ α} (h : is_complete (K : set α)) (v : α) :
-  orthogonal_projection h v ∈ K :=
-orthogonal_projection_fn_mem h v
+  orthogonal_projection K v ∈ K :=
+begin
+  rw ←orthogonal_projection_fn_eq h,
+  exact orthogonal_projection_fn_mem h v
+end
 
 /-- The characterization of the orthogonal projection.  -/
 @[simp]
-lemma orthogonal_projection_inner_eq_zero {K : submodule ℝ α} (h : is_complete (K : set α))
-  (v : α) : ∀ w ∈ K, inner (v - orthogonal_projection h v) w = 0 :=
-orthogonal_projection_fn_inner_eq_zero h v
+lemma orthogonal_projection_inner_eq_zero (K : submodule ℝ α) (v : α) :
+  ∀ w ∈ K, inner (v - orthogonal_projection K v) w = 0 :=
+begin
+  simp_rw orthogonal_projection_def,
+  split_ifs,
+  { exact orthogonal_projection_fn_inner_eq_zero h v },
+  { simp },
+end
 
 /-- The orthogonal projection is the unique point in `K` with the
 orthogonality property. -/
 lemma eq_orthogonal_projection_of_mem_of_inner_eq_zero {K : submodule ℝ α}
   (h : is_complete (K : set α)) {u v : α} (hvm : v ∈ K) (hvo : ∀ w ∈ K, inner (u - v) w = 0) :
-  v = orthogonal_projection h u :=
-eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero h hvm hvo
+  v = orthogonal_projection K u :=
+begin
+  rw ←orthogonal_projection_fn_eq h,
+  exact eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero h hvm hvo
+end
 
 /-- The subspace of vectors orthogonal to a given subspace. -/
 def submodule.orthogonal (K : submodule ℝ α) : submodule ℝ α :=

src/geometry/euclidean/basic.lean

@@ -471,76 +471,111 @@ subspace, whose direction is complete. The corresponding linear map
 (mapping a vector to the difference between the projections of two
 points whose difference is that vector) is the `orthogonal_projection`
 for real inner product spaces, onto the direction of the affine
-subspace being projected onto. -/
-def orthogonal_projection {s : affine_subspace ℝ P} (hn : (s : set P).nonempty)
-    (hc : is_complete (s.direction : set V)) : affine_map ℝ P P :=
+subspace being projected onto. For most purposes,
+`orthogonal_projection`, which removes the `nonempty` and
+`is_complete` hypotheses and is the identity map when either of those
+hypotheses fails, should be used instead. -/
+def orthogonal_projection_of_nonempty_of_complete {s : affine_subspace ℝ P}
+  (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) : affine_map ℝ P P :=
 { to_fun := orthogonal_projection_fn hn hc,
-  linear := orthogonal_projection hc,
+  linear := orthogonal_projection s.direction,
   map_vadd' := λ p v, begin
-    have hs : (orthogonal_projection hc) v +ᵥ orthogonal_projection_fn hn hc p ∈ s :=
+    have hs : (orthogonal_projection s.direction) v +ᵥ orthogonal_projection_fn hn hc p ∈ s :=
       vadd_mem_of_mem_direction (orthogonal_projection_mem hc _)
                                 (orthogonal_projection_fn_mem hn hc p),
-    have ho : (orthogonal_projection hc) v +ᵥ orthogonal_projection_fn hn hc p ∈
+    have ho : (orthogonal_projection s.direction) v +ᵥ orthogonal_projection_fn hn hc p ∈
       mk' (v +ᵥ p) s.direction.orthogonal,
     { rw [←vsub_right_mem_direction_iff_mem (self_mem_mk' _ _) _, direction_mk',
           vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm, add_sub_assoc],
       refine submodule.add_mem _ (orthogonal_projection_fn_vsub_mem_direction_orthogonal hn hc p) _,
       rw submodule.mem_orthogonal',
       intros w hw,
-      rw [←neg_sub, inner_neg_left, orthogonal_projection_inner_eq_zero hc _ w hw, neg_zero] },
-    have hm : (orthogonal_projection hc) v +ᵥ orthogonal_projection_fn hn hc p ∈
+      rw [←neg_sub, inner_neg_left, orthogonal_projection_inner_eq_zero _ _ w hw, neg_zero] },
+    have hm : (orthogonal_projection s.direction) v +ᵥ orthogonal_projection_fn hn hc p ∈
       ({orthogonal_projection_fn hn hc (v +ᵥ p)} : set P),
     { rw ←inter_eq_singleton_orthogonal_projection_fn hn hc (v +ᵥ p),
       exact set.mem_inter hs ho },
     rw set.mem_singleton_iff at hm,
     exact hm.symm
   end }
 
+/-- The orthogonal projection of a point onto an affine subspace,
+which is expected to be nonempty and complete.  The corresponding
+linear map (mapping a vector to the difference between the projections
+of two points whose difference is that vector) is the
+`orthogonal_projection` for real inner product spaces, onto the
+direction of the affine subspace being projected onto.  If the
+subspace is empty or not complete, this uses the identity map
+instead. -/
+def orthogonal_projection (s : affine_subspace ℝ P) : affine_map ℝ P P :=
+if h : (s : set P).nonempty ∧ is_complete (s.direction : set V) then
+  orthogonal_projection_of_nonempty_of_complete h.1 h.2 else affine_map.id ℝ P
+
+/-- The definition of `orthogonal_projection` using `if`. -/
+lemma orthogonal_projection_def (s : affine_subspace ℝ P) :
+  orthogonal_projection s = if h : (s : set P).nonempty ∧ is_complete (s.direction : set V) then
+    orthogonal_projection_of_nonempty_of_complete h.1 h.2 else affine_map.id ℝ P :=
+rfl
+
 @[simp] lemma orthogonal_projection_fn_eq {s : affine_subspace ℝ P} (hn : (s : set P).nonempty)
   (hc : is_complete (s.direction : set V)) (p : P) :
-  orthogonal_projection_fn hn hc p = orthogonal_projection hn hc p := rfl
-
+  orthogonal_projection_fn hn hc p = orthogonal_projection s p :=
+by { rw [orthogonal_projection_def, dif_pos (and.intro hn hc)], refl }
+
+@[simp] lemma orthogonal_projection_of_nonempty_of_complete_eq {s : affine_subspace ℝ P}
+  (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) (p : P) :
+  orthogonal_projection_of_nonempty_of_complete hn hc p = orthogonal_projection s p :=
+by rw [orthogonal_projection_def, dif_pos (and.intro hn hc)]
+
 /-- The intersection of the subspace and the orthogonal subspace
 through the given point is the `orthogonal_projection` of that point
 onto the subspace. -/
 lemma inter_eq_singleton_orthogonal_projection {s : affine_subspace ℝ P}
     (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) (p : P) :
-  (s : set P) ∩ (mk' p s.direction.orthogonal) = {orthogonal_projection hn hc p} :=
-inter_eq_singleton_orthogonal_projection_fn hn hc p
+  (s : set P) ∩ (mk' p s.direction.orthogonal) = {orthogonal_projection s p} :=
+begin
+  rw ←orthogonal_projection_fn_eq hn hc,
+  exact inter_eq_singleton_orthogonal_projection_fn hn hc p
+end
 
 /-- The `orthogonal_projection` lies in the given subspace. -/
 lemma orthogonal_projection_mem {s : affine_subspace ℝ P} (hn : (s : set P).nonempty)
-    (hc : is_complete (s.direction : set V)) (p : P) : orthogonal_projection hn hc p ∈ s :=
-orthogonal_projection_fn_mem hn hc p
+    (hc : is_complete (s.direction : set V)) (p : P) : orthogonal_projection s p ∈ s :=
+begin
+  rw ←orthogonal_projection_fn_eq hn hc,
+  exact orthogonal_projection_fn_mem hn hc p
+end
 
 /-- The `orthogonal_projection` lies in the orthogonal subspace. -/
-lemma orthogonal_projection_mem_orthogonal {s : affine_subspace ℝ P}
-    (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) (p : P) :
-  orthogonal_projection hn hc p ∈ mk' p s.direction.orthogonal :=
-orthogonal_projection_fn_mem_orthogonal hn hc p
+lemma orthogonal_projection_mem_orthogonal (s : affine_subspace ℝ P) (p : P) :
+  orthogonal_projection s p ∈ mk' p s.direction.orthogonal :=
+begin
+  rw orthogonal_projection_def,
+  split_ifs,
+  { exact orthogonal_projection_fn_mem_orthogonal h.1 h.2 p },
+  { exact self_mem_mk' _ _ }
+end
 
 /-- Subtracting a point in the given subspace from the
 `orthogonal_projection` produces a result in the direction of the
 given subspace. -/
 lemma orthogonal_projection_vsub_mem_direction {s : affine_subspace ℝ P}
-    (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) {p1 : P} (p2 : P)
-    (hp1 : p1 ∈ s) :
-  orthogonal_projection hn hc p2 -ᵥ p1 ∈ s.direction :=
-vsub_mem_direction (orthogonal_projection_mem hn hc p2) hp1
+    (hc : is_complete (s.direction : set V)) {p1 : P} (p2 : P) (hp1 : p1 ∈ s) :
+  orthogonal_projection s p2 -ᵥ p1 ∈ s.direction :=
+vsub_mem_direction (orthogonal_projection_mem ⟨p1, hp1⟩ hc p2) hp1
 
 /-- Subtracting the `orthogonal_projection` from a point in the given
 subspace produces a result in the direction of the given subspace. -/
 lemma vsub_orthogonal_projection_mem_direction {s : affine_subspace ℝ P}
-    (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) {p1 : P} (p2 : P)
-    (hp1 : p1 ∈ s) :
-  p1 -ᵥ orthogonal_projection hn hc p2 ∈ s.direction :=
-vsub_mem_direction hp1 (orthogonal_projection_mem hn hc p2)
+    (hc : is_complete (s.direction : set V)) {p1 : P} (p2 : P) (hp1 : p1 ∈ s) :
+  p1 -ᵥ orthogonal_projection s p2 ∈ s.direction :=
+vsub_mem_direction hp1 (orthogonal_projection_mem ⟨p1, hp1⟩ hc p2)
 
 /-- A point equals its orthogonal projection if and only if it lies in
 the subspace. -/
 lemma orthogonal_projection_eq_self_iff {s : affine_subspace ℝ P}
     (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) {p : P} :
-  orthogonal_projection hn hc p = p ↔ p ∈ s :=
+  orthogonal_projection s p = p ↔ p ∈ s :=
 begin
   split,
   { exact λ h, h ▸ orthogonal_projection_mem hn hc p },
@@ -553,72 +588,77 @@ end
 /-- The distance to a point's orthogonal projection is 0 iff it lies in the subspace. -/
 lemma dist_orthogonal_projection_eq_zero_iff {s : affine_subspace ℝ P}
   (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) {p : P} :
-  dist p (orthogonal_projection hn hc p) = 0 ↔ p ∈ s :=
-by rw [dist_comm, dist_eq_zero, orthogonal_projection_eq_self_iff]
+  dist p (orthogonal_projection s p) = 0 ↔ p ∈ s :=
+by rw [dist_comm, dist_eq_zero, orthogonal_projection_eq_self_iff hn hc]
 
 /-- The distance between a point and its orthogonal projection is
 nonzero if it does not lie in the subspace. -/
 lemma dist_orthogonal_projection_ne_zero_of_not_mem {s : affine_subspace ℝ P}
     (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) {p : P} (hp : p ∉ s) :
-  dist p (orthogonal_projection hn hc p) ≠ 0 :=
+  dist p (orthogonal_projection s p) ≠ 0 :=
 mt (dist_orthogonal_projection_eq_zero_iff hn hc).mp hp
 
 /-- Subtracting `p` from its `orthogonal_projection` produces a result
 in the orthogonal direction. -/
-lemma orthogonal_projection_vsub_mem_direction_orthogonal {s : affine_subspace ℝ P}
-    (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) (p : P) :
-  orthogonal_projection hn hc p -ᵥ p ∈ s.direction.orthogonal :=
-orthogonal_projection_fn_vsub_mem_direction_orthogonal hn hc p
+lemma orthogonal_projection_vsub_mem_direction_orthogonal (s : affine_subspace ℝ P) (p : P) :
+  orthogonal_projection s p -ᵥ p ∈ s.direction.orthogonal :=
+begin
+  rw orthogonal_projection_def,
+  split_ifs,
+  { exact orthogonal_projection_fn_vsub_mem_direction_orthogonal h.1 h.2 p },
+  { simp }
+end
 
 /-- Subtracting the `orthogonal_projection` from `p` produces a result
 in the orthogonal direction. -/
-lemma vsub_orthogonal_projection_mem_direction_orthogonal {s : affine_subspace ℝ P}
-    (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) (p : P) :
-  p -ᵥ orthogonal_projection hn hc p ∈ s.direction.orthogonal :=
+lemma vsub_orthogonal_projection_mem_direction_orthogonal (s : affine_subspace ℝ P) (p : P) :
+  p -ᵥ orthogonal_projection s p ∈ s.direction.orthogonal :=
 direction_mk' p s.direction.orthogonal ▸
-  vsub_mem_direction (self_mem_mk' _ _) (orthogonal_projection_mem_orthogonal hn hc p)
+  vsub_mem_direction (self_mem_mk' _ _) (orthogonal_projection_mem_orthogonal s p)
 
 /-- Adding a vector to a point in the given subspace, then taking the
 orthogonal projection, produces the original point if the vector was
 in the orthogonal direction. -/
 lemma orthogonal_projection_vadd_eq_self {s : affine_subspace ℝ P}
-    (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) {p : P} (hp : p ∈ s)
-    {v : V} (hv : v ∈ s.direction.orthogonal) : orthogonal_projection hn hc (v +ᵥ p) = p :=
+    (hc : is_complete (s.direction : set V)) {p : P} (hp : p ∈ s) {v : V}
+    (hv : v ∈ s.direction.orthogonal) : orthogonal_projection s (v +ᵥ p) = p :=
 begin
-  have h := vsub_orthogonal_projection_mem_direction_orthogonal hn hc (v +ᵥ p),
+  have h := vsub_orthogonal_projection_mem_direction_orthogonal s (v +ᵥ p),
   rw [vadd_vsub_assoc, submodule.add_mem_iff_right _ hv] at h,
   refine (eq_of_vsub_eq_zero _).symm,
   refine submodule.disjoint_def.1 s.direction.orthogonal_disjoint _ _ h,
-  exact vsub_mem_direction hp (orthogonal_projection_mem hn hc (v +ᵥ p))
+  exact vsub_mem_direction hp (orthogonal_projection_mem ⟨p, hp⟩ hc (v +ᵥ p))
 end
 
 /-- Adding a vector to a point in the given subspace, then taking the
 orthogonal projection, produces the original point if the vector is a
 multiple of the result of subtracting a point's orthogonal projection
 from that point. -/
 lemma orthogonal_projection_vadd_smul_vsub_orthogonal_projection {s : affine_subspace ℝ P}
-    (hn : (s : set P).nonempty) (hc : is_complete (s.direction : set V)) {p1 : P} (p2 : P)
-    (r : ℝ) (hp : p1 ∈ s) :
-  orthogonal_projection hn hc (r • (p2 -ᵥ orthogonal_projection hn hc p2 : V) +ᵥ p1) = p1 :=
-orthogonal_projection_vadd_eq_self hn hc hp
-  (submodule.smul_mem _ _ (vsub_orthogonal_projection_mem_direction_orthogonal hn hc _))
+    (hc : is_complete (s.direction : set V)) {p1 : P} (p2 : P) (r : ℝ) (hp : p1 ∈ s) :
+  orthogonal_projection s (r • (p2 -ᵥ orthogonal_projection s p2 : V) +ᵥ p1) = p1 :=
+orthogonal_projection_vadd_eq_self hc hp
+  (submodule.smul_mem _ _ (vsub_orthogonal_projection_mem_direction_orthogonal s _))
 
-/-- The square of the distance from a point in `s` to `p` equals the
+/-- The square of the distance from a point in `s` to `p2` equals the
 sum of the squares of the distances of the two points to the
 `orthogonal_projection`. -/
 lemma dist_square_eq_dist_orthogonal_projection_square_add_dist_orthogonal_projection_square
-    {s : affine_subspace ℝ P} (hn : (s : set P).nonempty)
-    (hc : is_complete (s.direction : set V)) {p1 : P} (p2 : P) (hp1 : p1 ∈ s) :
+    {s : affine_subspace ℝ P} {p1 : P} (p2 : P) (hp1 : p1 ∈ s) :
   dist p1 p2 * dist p1 p2 =
-    dist p1 (orthogonal_projection hn hc p2) * dist p1 (orthogonal_projection hn hc p2) +
-    dist p2 (orthogonal_projection hn hc p2) * dist p2 (orthogonal_projection hn hc p2) :=
+    dist p1 (orthogonal_projection s p2) * dist p1 (orthogonal_projection s p2) +
+    dist p2 (orthogonal_projection s p2) * dist p2 (orthogonal_projection s p2) :=
 begin
   rw [metric_space.dist_comm p2 _, dist_eq_norm_vsub V p1 _, dist_eq_norm_vsub V p1 _,
-    dist_eq_norm_vsub V _ p2, ← vsub_add_vsub_cancel p1 (orthogonal_projection hn hc p2) p2,
+    dist_eq_norm_vsub V _ p2, ← vsub_add_vsub_cancel p1 (orthogonal_projection s p2) p2,
     norm_add_square_eq_norm_square_add_norm_square_iff_inner_eq_zero],
-  exact submodule.inner_right_of_mem_orthogonal
-    (vsub_orthogonal_projection_mem_direction hn hc p2 hp1)
-    (orthogonal_projection_vsub_mem_direction_orthogonal hn hc p2)
+  rw orthogonal_projection_def,
+  split_ifs,
+  { rw orthogonal_projection_of_nonempty_of_complete_eq,
+    exact submodule.inner_right_of_mem_orthogonal
+     (vsub_orthogonal_projection_mem_direction h.2 p2 hp1)
+     (orthogonal_projection_vsub_mem_direction_orthogonal s p2) },
+  { simp }
 end
 
 /-- The square of the distance between two points constructed by