English
For x,y ∈ E, 0 ≤ ⟪x,y⟫ and ω(x,y)=0 if and only if x and y point in the same ray (SameRay).
Русский
Для x,y ∈ E верно: 0 ≤ ⟪x,y⟫ и ω(x,y)=0 тогда и только тогда, когда x и y направлены в одну полуось (SameRay).
LaTeX
$$0 \\le \\langle x,y\\rangle \\wedge \\omega(x,y) = 0 \\iff \\text{SameRay}_{\\mathbb{R}}(x,y)$$
Lean4
theorem nonneg_inner_and_areaForm_eq_zero_iff_sameRay (x y : E) : 0 ≤ ⟪x, y⟫ ∧ ω x y = 0 ↔ SameRay ℝ x y :=
by
by_cases hx : x = 0
· simp [hx]
constructor
· let a : ℝ := (o.basisRightAngleRotation x hx).repr y 0
let b : ℝ := (o.basisRightAngleRotation x hx).repr y 1
suffices ↑0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • J x)
by
rw [← (o.basisRightAngleRotation x hx).sum_repr y]
simp only [Fin.sum_univ_succ, coe_basisRightAngleRotation, Matrix.cons_val_zero, Fin.succ_zero_eq_one',
Finset.univ_eq_empty, Finset.sum_empty, areaForm_apply_self, map_smul, map_add, real_inner_smul_right,
inner_add_right, Matrix.cons_val_one, Algebra.id.smul_eq_mul, areaForm_rightAngleRotation_right, mul_zero,
add_zero, zero_add, neg_zero, inner_rightAngleRotation_right, real_inner_self_eq_norm_sq]
exact this
rintro ⟨ha, hb⟩
have hx' : 0 < ‖x‖ := by simpa using hx
have ha' : 0 ≤ a := nonneg_of_mul_nonneg_left ha (by positivity)
have hb' : b = 0 := eq_zero_of_ne_zero_of_mul_right_eq_zero (pow_ne_zero 2 hx'.ne') hb
exact (SameRay.sameRay_nonneg_smul_right x ha').add_right <| by simp [hb']
· intro h
obtain ⟨r, hr, rfl⟩ := h.exists_nonneg_left hx
simp only [inner_smul_right, real_inner_self_eq_norm_sq, LinearMap.map_smulₛₗ, areaForm_apply_self,
Algebra.id.smul_eq_mul, mul_zero, and_true]
positivity
