Documentation

LeanPool.DistanceGeometry.Trilateration

Trilateration: sphere intersections of codimension-one center families #

A family of centers whose affine span is a hyperplane (the orthogonal complement of the center span is one-dimensional) localizes a point to at most two candidates: the intersection of the spheres {p | ∀ i, dist p (c i) = r i} has at most two elements.

This is the higher-dimensional analog of EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two (two circles meet in at most two points), and the combinatorial heart of the branch-and-prune algorithm for the Discretizable Molecular Distance Geometry Problem: a new vertex localized against enough already-placed neighbours has at most two placements, so the search tree has bounded branching.

The proof: for any two solutions p₁, p₂, equal distances to each center give ⟪c i -ᵥ c i₀, p₂ -ᵥ p₁⟫ = 0 (inner_vsub_vsub_of_dist_eq_of_dist_eq), so the difference vector lies in Wᗮ, where W = vectorSpan ℝ (range c). When Wᗮ is one-dimensional it cannot contain two linearly independent vectors, so any third solution's difference vector is a scalar multiple of p₂ -ᵥ p₁; feeding that into the distance equation through the quadratic dist_smul_vadd_eq_dist forces the third solution to coincide with p₁ or p₂.

Main results #

source
def DistanceGeometry.sphereIntersection {P : Type u_2} [MetricSpace P] {ι : Type u_3} (c : ι → P) (r : ι → ℝ) :
Set P

The intersection of the spheres of real-valued radii r about the centers c. If some r i is negative, the intersection is empty because distances are nonnegative.

Equations
Instances For
    source
    @[simp]
    theorem DistanceGeometry.mem_sphereIntersection {P : Type u_2} [MetricSpace P] {ι : Type u_3} {c : ι → P} {r : ι → ℝ} {p : P} :
    p ∈ sphereIntersection c r ↔ ∀ (i : ι), dist p (c i) = r i
    source
    theorem DistanceGeometry.encard_setOf_forall_dist_eq_le_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [FiniteDimensional ℝ V] {ι : Type u_3} {c : ι → P} [Nonempty ι] (hc : Module.finrank ℝ ↥(vectorSpan ℝ (Set.range c))ᗮ = 1) (r : ι → ℝ) :
    {p : P | ∀ (i : ι), dist p (c i) = r i}.encard ≤ 2

    If the orthogonal complement of the center span is one-dimensional (the centers span a hyperplane), the intersection of the spheres {p | ∀ i, dist p (c i) = r i} has at most two elements.

    Specialization: three affinely independent centers in EuclideanSpace ℝ (Fin 3) #

    source
    def DistanceGeometry.trilaterationSet (c : Fin 3 → EuclideanSpace ℝ (Fin 3)) (r : Fin 3 → ℝ) :
    Set (EuclideanSpace ℝ (Fin 3))

    The localization set of three centers c and real-valued radii r in EuclideanSpace ℝ (Fin 3): the intersection of the three spheres. A negative radius makes the set empty.

    Equations
    Instances For
      source
      theorem DistanceGeometry.trilateration_le_two {c : Fin 3 → EuclideanSpace ℝ (Fin 3)} (hc : AffineIndependent ℝ c) (r : Fin 3 → ℝ) :
      (trilaterationSet c r).encard ≤ 2

      Three affinely independent centers and three radii localize a point in EuclideanSpace ℝ (Fin 3) to at most two candidates: the intersection of the three spheres has at most two elements. The d = 3 analog of EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two.