Closest point on a line to a point not on it

Stream: Is there code for X?

[Apurva Nakade]

Do we have a theorem that says that the closest point on a line $L$ to a point $P$ not on it is obtained by dropping a perpendicular from the point $P$ to $L$?

[Yaël Dillies]

Isn't that Hilbert's projection theorem?

[Apurva Nakade]

Yaël Dillies said:

Isn't that Hilbert's projection theorem?

is this in mathlib?

[Yaël Dillies]

Not yet

[Apurva Nakade]

Thanks!

[Apurva Nakade]

I'm reading the wiki page for Hilbert's projection theorem ... I think this result provides a characterization of the closest point is not a direct corollary of it.

[Apurva Nakade]

I accidentally ended up proving this while doing some linear programming stuff only to realize later that it might've already been in mathlib. Here's my code so far:

import analysis.convex.cone
noncomputable theory

variables {H : Type*} [inner_product_space ℝ H]

section closed_convex_cone

-- Reference: https://ti.inf.ethz.ch/ew/lehre/ApproxSDP09/notes/conelp.pdf

/-- Given a closed convex cone K and a point b not in K, if z is the point in K closest to b then
z - b is perpendicular to z. -/
theorem closest_point_perp
  {K : convex_cone ℝ H} (hK : is_closed (K : set H))
  {b : H} (disj : b ∉ K)
  {z : H} (hzK : z ∈ (K : set H))
  (h_inf : metric.inf_dist b (K : set H) = dist b z) : ⟪z - b, z⟫_ℝ = 0 :=
begin
  let y := z - b,
  by_cases hz : z = 0,
  { -- If z is zero, we're done.
    rw [hz, inner_zero_right] },
  begin
    -- In the case z ≠ 0, we provide a proof by contradiction. The proof strategy is to show that
    -- for a sufficiently small constant α, point z' = (1 - α) • z lies in K and is closer to b than
    -- z, thereby contradicting h_inf.
    by_contra' hyz,

    -- We will pick a different scaling factor depending on the sign of ⟪y, z⟫_ℝ.
    obtain (hyz_neg | hyz_pos) := ne.lt_or_lt hyz, clear hyz,

    -- Case 1: ⟪y, z⟫_ℝ < 0.
    let α := (∥z∥ ^ 2)⁻¹ * ⟪y, z⟫_ℝ,
    have hα : α < 0 :=
      linarith.mul_neg hyz_neg (inv_pos.2 (sq_pos_of_ne_zero _ (norm_ne_zero_iff.2 hz))),
    -- Scale z by (1 - α) to obtain z'.
    let z' := (1 - α) • z,
    -- Show that z' is in K.
    have hz' : z' ∈ (K : set H) := K.smul_mem (sub_pos.2 (lt_trans hα zero_lt_one)) hzK,
    -- Auxiliary lemma for computation of dist b z'.
    have h_aux : -(2 * ⟪y, α • z⟫_ℝ - ∥α • z∥^2) < 0, by
    begin
      rw [real_inner_smul_right, norm_smul, real.norm_eq_abs, abs_of_neg hα, neg_mul, neg_sq],
      ring_nf,
      refine mul_neg_of_pos_of_neg _ hα,
      calc 0 < - ⟪y, z⟫_ℝ : by rwa [lt_neg, neg_zero]
      ... = (1 - 2) * ⟪y, z⟫_ℝ : by norm_num
      ... = ∥z∥ ^ 2 * α - 2 * ⟪y, z⟫_ℝ : by rw [sub_mul, ← mul_assoc,
              mul_inv_cancel (ne_of_gt (sq_pos_of_ne_zero _ (norm_ne_zero_iff.2 hz)))]
    end,

    -- Case 2: ⟪y, z⟫_ℝ > 0.
    swap 2,
    let α := min ((∥z∥ ^ 2)⁻¹ * ⟪y, z⟫_ℝ) 0.5,
    have hα : 0 < α :=
      lt_min_iff.2 ⟨ mul_pos (inv_pos.2 (sq_pos_of_ne_zero _ (norm_ne_zero_iff.2 hz))) hyz_pos,
        one_half_pos ⟩,
    -- Scale z by (1 - α) to obtain z'.
    let z' := (1 - α) • z,
    -- Show that z' is in K.
    have hz' : z' ∈ (K : set H)
             := K.smul_mem (sub_pos.2 (min_lt_of_right_lt one_half_lt_one)) hzK,
    -- Auxiliary lemma for computation of dist b z'.
    have h_aux : -(2 * ⟪y, α • z⟫_ℝ - ∥α • z∥^2) < 0, by
    begin
      rw [real_inner_smul_right, norm_smul, real.norm_eq_abs, abs_of_pos hα],
      ring_nf,
      refine mul_neg_of_neg_of_pos _ hα,
      calc ∥z∥ ^ 2 * α - 2 * ⟪y, z⟫_ℝ
          ≤ ∥z∥ ^ 2 * ((∥z∥ ^ 2)⁻¹ * ⟪y, z⟫_ℝ) - 2 * ⟪y, z⟫_ℝ : by {
          rw [sub_le_sub_iff_right, mul_le_mul_left (sq_pos_of_ne_zero _ (norm_ne_zero_iff.2 hz))],
          exact min_le_left _ _ }
      ... = (∥z∥ ^ 2 * (∥z∥ ^ 2)⁻¹) * ⟪y, z⟫_ℝ - 2 * ⟪y, z⟫_ℝ : by rw mul_assoc
      ... = 1 * ⟪y, z⟫_ℝ - 2 * ⟪y, z⟫_ℝ
          : by rw mul_inv_cancel (ne_of_gt (sq_pos_of_ne_zero _ (norm_ne_zero_iff.2 hz)))
      ... = - ⟪y, z⟫_ℝ : by { rw ← sub_mul, norm_num }
      ... < 0 : neg_lt_zero.2 hyz_pos,
    end,

    -- In both cases, distance between b and z' is less than the distance between b and z.
    repeat begin
      have hbzz' : dist b z' ^ 2 < dist b z ^ 2 := calc (dist b z')^2
          = ∥(1 - α) • z - b∥^2 : by rw dist_eq_norm'
      ... = ∥z - α • z - b∥^2 : by rw [sub_smul, one_smul]
      ... = ∥(z - b) - α • z∥^2 : by abel
      ... = ∥y∥^2 - 2 * ⟪y, α • z⟫_ℝ + ∥α • z∥^2
          : by simp_rw [norm_sq_eq_inner, real_inner_sub_sub_self, is_R_or_C.re_to_real]
      ... = ∥y∥^2 - (2 * ⟪y, α • z⟫_ℝ - ∥α • z∥^2) : by rw sub_add
      ... < ∥y∥^2 : add_lt_iff_neg_left.mpr h_aux
      ... = (dist b z)^2 : by rw dist_eq_norm',
      have hbz' : metric.inf_dist b (K : set H) ≤ dist b z'
                := @metric.inf_dist_le_dist_of_mem _ _ _ b _ hz',
      rw [h_inf, ← @abs_dist _ _ b z, ← @abs_dist _ _ b z', ← sq_le_sq] at hbz',
      exact not_lt_of_le hbz' hbzz',
    end,
  end
end

end closed_convex_cone

[Yaël Dillies]

This is generalizable away from cones.

[Apurva Nakade]

I don't think this is true. The wikipedia proof in fact assumes that the convex set is a subspace which is weaker than a convex cone.

[Apurva Nakade]

"Proof of characterization of minimum point when {\displaystyle C}C is a closed vector subspace."

[Apurva Nakade]

Do you have a reference in mind?

[Yaël Dillies]

Ah for the orthogonality sure.

[Heather Macbeth]

@Apurva Nakade It can be much shorter. You should use docs#orthogonal_projection.

[Heather Macbeth]

Depending on your needs (if the line doesn't pass through the origin), possibly docs#euclidean_geometry.orthogonal_projection

[Apurva Nakade]

Heather Macbeth said:

Apurva Nakade It can be much shorter. You should use docs#orthogonal_projection.

Thank you! I'll try to rewrite it using orthogonal projection. I think this version ought to be sufficient. The line does pass through the origin with a minor twist that we want only positive scalars. But I think it should be manageable.

[Apurva Nakade]

Yaël Dillies said:

Isn't that Hilbert's projection theorem?

Is this Hilbert's projection theorem: docs#exists_norm_eq_infi_of_complete_convex ?

[Apurva Nakade]

I feel like the doc string should be more descriptive for such an important theorem lol

[Apurva Nakade]

The next theorem is exactly what i've been looking for docs#norm_eq_infi_iff_real_inner_eq_zero :O