English
Characterization of minimizers for projection in a convex set: equality of norms corresponds to a certain inner product inequality; equivalently, a certain inner product is nonpositive for all w ∈ K.
Русский
Характеризация минимизаторов проекции в выпуклом множестве: равенство норм эквивалентно неотростковому неравенству по скалярам; эквивалентно, что некоторый скалярный произведение неотрицательно для всех w ∈ K.
LaTeX
$$$\\text{norm\_eq\_iInf\_iff\_real\_inner\_le\_zero}$$$
Lean4
/-- Characterization of minimizers for the projection on a convex set in a real inner product
space. -/
theorem norm_eq_iInf_iff_real_inner_le_zero {K : Set F} (h : Convex ℝ K) {u : F} {v : F} (hv : v ∈ K) :
(‖u - v‖ = ⨅ w : K, ‖u - w‖) ↔ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 :=
by
letI : Nonempty K := ⟨⟨v, hv⟩⟩
constructor
· intro eq w hw
let δ := ⨅ w : K, ‖u - w‖
let p := ⟪u - v, w - v⟫_ℝ
let q := ‖w - v‖ ^ 2
have δ_le (w : K) : δ ≤ ‖u - w‖ := ciInf_le ⟨0, fun _ ⟨_, h⟩ => h ▸ norm_nonneg _⟩ _
have δ_le' (w) (hw : w ∈ K) : δ ≤ ‖u - w‖ := δ_le ⟨w, hw⟩
have (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1) : 2 * p ≤ θ * q :=
by
have : ‖u - v‖ ^ 2 ≤ ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 :=
calc
‖u - v‖ ^ 2
_ ≤ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2 := by
simp only [sq]; apply mul_self_le_mul_self (norm_nonneg _)
rw [eq]; apply δ_le'
apply h hw hv
exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel _ _]
_ = ‖u - v - θ • (w - v)‖ ^ 2 :=
by
have : u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v) :=
by
rw [smul_sub, sub_smul, one_smul]
simp only [sub_eq_add_neg, add_comm, add_left_comm, add_assoc, neg_add_rev]
rw [this]
_ = ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 :=
by
rw [@norm_sub_sq ℝ, inner_smul_right, norm_smul]
simp only [sq]
change
‖u - v‖ * ‖u - v‖ - 2 * (θ * ⟪u - v, w - v⟫_ℝ) + absR θ * ‖w - v‖ * (absR θ * ‖w - v‖) =
‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)
rw [abs_of_pos hθ₁]; ring
have eq₁ :
‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 =
‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ) :=
by abel
rw [eq₁, le_add_iff_nonneg_right] at this
have eq₂ : θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ = θ * (θ * ‖w - v‖ ^ 2 - 2 * ⟪u - v, w - v⟫_ℝ) := by
ring
rw [eq₂] at this
exact le_of_sub_nonneg (nonneg_of_mul_nonneg_right this hθ₁)
by_cases hq : q = 0
· rw [hq] at this
have : p ≤ 0 := by
have := this (1 : ℝ) (by simp) (by simp)
linarith
exact this
· have q_pos : 0 < q := lt_of_le_of_ne (sq_nonneg _) fun h ↦ hq h.symm
by_contra hp
rw [not_le] at hp
let θ := min (1 : ℝ) (p / q)
have eq₁ : θ * q ≤ p :=
calc
θ * q ≤ p / q * q := mul_le_mul_of_nonneg_right (min_le_right _ _) (sq_nonneg _)
_ = p := div_mul_cancel₀ _ hq
have : 2 * p ≤ p :=
calc
2 * p ≤ θ * q := by exact this θ (lt_min (by simp) (div_pos hp q_pos)) (by simp [θ])
_ ≤ p := eq₁
linarith
· intro h
apply le_antisymm
· apply le_ciInf
intro w
apply nonneg_le_nonneg_of_sq_le_sq (norm_nonneg _)
have := h w w.2
calc
‖u - v‖ * ‖u - v‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, w - v⟫_ℝ := by linarith
_ ≤ ‖u - v‖ ^ 2 - 2 * ⟪u - v, w - v⟫_ℝ + ‖w - v‖ ^ 2 :=
by
rw [sq]
refine le_add_of_nonneg_right ?_
exact sq_nonneg _
_ = ‖u - v - (w - v)‖ ^ 2 := (@norm_sub_sq ℝ _ _ _ _ _ _).symm
_ = ‖u - w‖ * ‖u - w‖ := by
have : u - v - (w - v) = u - w := by abel
rw [this, sq]
· change ⨅ w : K, ‖u - w‖ ≤ (fun w : K => ‖u - w‖) ⟨v, hv⟩
apply ciInf_le
use 0
rintro y ⟨z, rfl⟩
exact norm_nonneg _
