English
Same as dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq but phrased in the affine-simplex setting.
Русский
То же отношение для квадрата расстояния в рамках аффинного симплекса.
LaTeX
$$$$\text{As above for } s:\text{Simplex},\ p_1\in\operatorname{affineSpan}(\mathrm{range}(s.points)):\ dist(p_1,p_2)^2 = \cdots.$$$$
Lean4
/-- The signed distance between two points `p` and `q`, in the direction of a reference vector `v`.
It is the size of `q - p` in the direction of `v`.
In the degenerate case `v = 0`, it returns `0`.
TODO: once we have a topology on `P →ᴬ[ℝ] ℝ`, the type should be `P →ᴬ[ℝ] P →ᴬ[ℝ] ℝ`.
-/
noncomputable def signedDist (v : V) : P →ᵃ[ℝ] P →ᴬ[ℝ] ℝ
where
toFun p := (innerSL ℝ (normalize v)).toContinuousAffineMap.comp (ContinuousAffineMap.id ℝ P -ᵥ .const ℝ P p)
linear := signedDistLinear v
map_vadd' p
v' := by
ext q
rw [signedDistLinear_apply]
simp [vsub_vadd_eq_vsub_sub, inner_sub_right, ← sub_eq_neg_add]
