feat(analysis/inner_product_space): ext lemmas for dense subspaces (#…

…17450)

src/analysis/inner_product_space/basic.lean

@@ -2249,6 +2249,23 @@ end
 lemma mem_orthogonal_singleton_of_inner_left (u : E) {v : E} (hv : ⟪v, u⟫ = 0) : v ∈ (𝕜 ∙ u)ᗮ :=
 mem_orthogonal_singleton_of_inner_right u $ inner_eq_zero_sym.2 hv
 
+lemma submodule.sub_mem_orthogonal_of_inner_left {x y : E}
+  (h : ∀ (v : K), ⟪x, v⟫ = ⟪y, v⟫) : x - y ∈ Kᗮ :=
+begin
+  rw submodule.mem_orthogonal',
+  intros u hu,
+  rw [inner_sub_left, sub_eq_zero],
+  exact h ⟨u, hu⟩,
+end
+
+lemma submodule.sub_mem_orthogonal_of_inner_right {x y : E}
+  (h : ∀ (v : K), ⟪(v : E), x⟫ = ⟪(v : E), y⟫) : x - y ∈ Kᗮ :=
+begin
+  intros u hu,
+  rw [inner_sub_right, sub_eq_zero],
+  exact h ⟨u, hu⟩,
+end
+
 variables (K)
 
 /-- `K` and `Kᗮ` have trivial intersection. -/

src/analysis/inner_product_space/projection.lean

@@ -856,6 +856,38 @@ begin
   { rw [h, submodule.bot_orthogonal_eq_top] }
 end
 
+namespace dense
+
+open submodule
+
+variables {x y : E} [complete_space E]
+
+/-- If `S` is dense and `x - y ∈ Kᗮ`, then `x = y`. -/
+lemma eq_of_sub_mem_orthogonal (hK : dense (K : set E)) (h : x - y ∈ Kᗮ) : x = y :=
+begin
+  rw [dense_iff_topological_closure_eq_top, topological_closure_eq_top_iff] at hK,
+  rwa [hK, submodule.mem_bot, sub_eq_zero] at h,
+end
+
+lemma eq_zero_of_mem_orthogonal (hK : dense (K : set E)) (h : x ∈ Kᗮ) : x = 0 :=
+hK.eq_of_sub_mem_orthogonal (by rwa [sub_zero])
+
+lemma eq_of_inner_left (hK : dense (K : set E)) (h : ∀ v : K, ⟪x, v⟫ = ⟪y, v⟫) : x = y :=
+hK.eq_of_sub_mem_orthogonal (submodule.sub_mem_orthogonal_of_inner_left h)
+
+lemma eq_zero_of_inner_left (hK : dense (K : set E)) (h : ∀ v : K, ⟪x, v⟫ = 0) : x = 0 :=
+hK.eq_of_inner_left (λ v, by rw [inner_zero_left, h v])
+
+lemma eq_of_inner_right (hK : dense (K : set E))
+  (h : ∀ v : K, ⟪(v : E), x⟫ = ⟪(v : E), y⟫) : x = y :=
+hK.eq_of_sub_mem_orthogonal (submodule.sub_mem_orthogonal_of_inner_right h)
+
+lemma eq_zero_of_inner_right (hK : dense (K : set E))
+  (h : ∀ v : K, ⟪(v : E), x⟫ = 0) : x = 0 :=
+hK.eq_of_inner_right (λ v, by rw [inner_zero_right, h v])
+
+end dense
+
 /-- 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) :