English
For all v,p,q, signedDist v p q = dist p q holds if and only if q −ᵥ p lies in the nonnegative span of v.
Русский
Для любых v,p,q равенство signedDist v p q = dist p q эквивалентно тому, что q −ᵥ p лежит в невырожденном линейном сочетании с неотрицательным коэффициентом по v.
LaTeX
$$signedDist v p q = dist p q \Leftrightarrow q -ᵥ p ∈ \mathbb{R}_{\ge 0} \cdot v$$
Lean4
theorem signedDist_eq_dist_iff_vsub_mem_span : signedDist v p q = dist p q ↔ q -ᵥ p ∈ ℝ≥0 ∙ v :=
by
rw [Submodule.mem_span_singleton]
rw [signedDist_apply_apply, dist_eq_norm_vsub', NormedSpace.normalize, real_inner_smul_left]
by_cases h : v = 0
· simp [h, eq_comm (a := (0 : ℝ)), eq_comm (a := (0 : V))]
rw [inv_mul_eq_iff_eq_mul₀ (by positivity)]
rw [inner_eq_norm_mul_iff_real]
simp only [smul_def]
refine ⟨fun h => ?_, fun ⟨c, h⟩ => ?_⟩
· simp only [NNReal.exists, coe_mk, exists_prop]
use ‖v‖⁻¹ * ‖q -ᵥ p‖
constructor
· positivity
· rw [← smul_smul, h, smul_smul, inv_mul_cancel₀ (by positivity), one_smul]
· rw [← h, norm_smul, smul_smul, mul_comm]
simp
