English
The inner product between two vectors is zero if and only if the first is zero or the second is a scalar multiple of a π/2 rotation of the first vector.
Русский
Скалярное произведение двух векторов равно нулю тогда и только тогда, когда первый вектор нулевой или второй вектор является скаляром кратной π/2 вращению первого вектора.
LaTeX
$$⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ r ∈ ℝ, y = r • o.rotation(π/2) x$$
Lean4
/-- The inner product between two vectors is zero if and only if the first vector is zero or
the second is a multiple of a `π / 2` rotation of that vector. -/
theorem inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two {x y : V} :
⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ r : ℝ, r • o.rotation (π / 2 : ℝ) x = y :=
by
rw [← o.eq_zero_or_oangle_eq_iff_inner_eq_zero]
refine ⟨fun h => ?_, fun h => ?_⟩
· rcases h with (rfl | rfl | h | h)
· exact Or.inl rfl
· exact Or.inr ⟨0, zero_smul _ _⟩
· obtain ⟨r, _, rfl⟩ :=
(o.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero (o.left_ne_zero_of_oangle_eq_pi_div_two h)
(o.right_ne_zero_of_oangle_eq_pi_div_two h) _).1
h
exact Or.inr ⟨r, rfl⟩
· obtain ⟨r, _, rfl⟩ :=
(o.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero (o.left_ne_zero_of_oangle_eq_neg_pi_div_two h)
(o.right_ne_zero_of_oangle_eq_neg_pi_div_two h) _).1
h
refine Or.inr ⟨-r, ?_⟩
rw [neg_smul, ← smul_neg, o.neg_rotation_pi_div_two]
· rcases h with (rfl | ⟨r, rfl⟩)
· exact Or.inl rfl
· by_cases hx : x = 0; · exact Or.inl hx
rcases lt_trichotomy r 0 with (hr | rfl | hr)
· refine Or.inr (Or.inr (Or.inr ?_))
rw [o.oangle_smul_right_of_neg _ _ hr, o.neg_rotation_pi_div_two, o.oangle_rotation_self_right hx]
· exact Or.inr (Or.inl (zero_smul _ _))
· refine Or.inr (Or.inr (Or.inl ?_))
rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right hx]
