inner product lemmas for perpendicular vectors

Stream: Is there code for X?

[Eric Wieser]

Do we have a more general way to write these?

import Mathlib

open EuclideanGeometry
open scoped Finset RealInnerProductSpace

variable {V P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
variable [NormedAddTorsor V P]

theorem inner_vsub_left_eq_zero_symm {a b : P} {v : V} :
    ⟪a -ᵥ b, v⟫ = 0 ↔ ⟪b -ᵥ a, v⟫ = 0 := by
  rw [← neg_vsub_eq_vsub_rev, inner_neg_left, neg_eq_zero]

theorem inner_vsub_right_eq_zero_symm {v : V} {a b : P} :
    ⟪v, a -ᵥ b⟫ = 0 ↔ ⟪v, b -ᵥ a⟫ = 0 := by
  rw [← neg_vsub_eq_vsub_rev, inner_neg_right, neg_eq_zero]

theorem inner_eq_norm_sq_left_iff {v w : V} :
    ⟪v, w⟫ = ‖v‖ ^ 2 ↔ ⟪v, v - w⟫ = 0 := by
  rw [inner_sub_right, sub_eq_zero, real_inner_self_eq_norm_sq, eq_comm]

-- what's the canonical RHS here? Presumably we want to repeat this for `right`
theorem inner_vsub_left_eq_dist_sq_iff' (a b : P) (v : V):
    ⟪a -ᵥ b, v⟫ = dist a b ^ 2 ↔ ⟪a -ᵥ b, a -ᵥ b - v⟫ = 0 := by
  rw [dist_eq_norm_vsub V, inner_eq_norm_sq_left_iff]

-- there are a very large number of variants of this; which do we want?
theorem inner_vsub_vsub_left_eq_dist_sq_iff (a b c : P) :
    ⟪a -ᵥ b, a -ᵥ c⟫ = dist a b ^ 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0 := by
  rw [dist_eq_norm_vsub V, inner_eq_norm_sq_left_iff, vsub_sub_vsub_cancel_left,
    inner_vsub_right_eq_zero_symm]

[Eric Wieser]

cc @Joseph Myers, as this came up while reviewing #23752

[Joseph Myers]

Those all seem like reasonable lemmas for mathlib to me (making no assertions here about whether some of them might in fact also be true in complex inner product spaces, for example).

[Eric Wieser]

I'll make a PR

[Eric Wieser]

The problem with the complex inner product spaces is the extra coercion needed because dist is real-valued

[Eric Wieser]

#24968