noncomputable def fermatWeberBalanceTerm {m d : ℕ} (ω : Fin m → ℝ) (a : Fin m → EuclideanSpace ℝ (Fin d)) (x : EuclideanSpace ℝ (Fin d)) (i : Fin m) : EuclideanSpace ℝ (Fin d)

The weighted normalized displacement vector from the site a i to x appearing in the Fermat--Weber balance condition.

noncomputable def fermatWeberResidualBalance {m d : ℕ} (ω : Fin m → ℝ) (a : Fin m → EuclideanSpace ℝ (Fin d)) (j : Fin m) : EuclideanSpace ℝ (Fin d)

The residual balance vector at the site a j, obtained by summing the weighted normalized displacement vectors from the remaining sites to a j.

@[simp]

theorem fermatWeberBalanceTerm_apply {m d : ℕ} (ω : Fin m → ℝ) (a : Fin m → EuclideanSpace ℝ (Fin d)) (x : EuclideanSpace ℝ (Fin d)) (i : Fin m) : fermatWeberBalanceTerm ω a x i = ω i • ‖x - a i‖⁻¹ • (x - a i)

@[simp]

theorem fermatWeberResidualBalance_eq_sum_erase {m d : ℕ} (ω : Fin m → ℝ) (a : Fin m → EuclideanSpace ℝ (Fin d)) (j : Fin m) : fermatWeberResidualBalance ω a j = (Finset.univ.erase j).sum (fermatWeberBalanceTerm ω a (a j))

theorem isMinOn_fermatWeberObjective_iff_balance_of_not_mem_range {m d : ℕ} (ω : Fin m → ℝ) (hω : ∀ (i : Fin m), 0 ≤ ω i) (a : Fin m → EuclideanSpace ℝ (Fin d)) (x : EuclideanSpace ℝ (Fin d)) (hx : x ∉ Set.range a) : IsMinOn (fermatWeberObjective ω a) Set.univ x ↔ ∑ i : Fin m, fermatWeberBalanceTerm ω a x i = 0

Helper for Proposition 3.33: under nonnegative weights, a point x outside Set.range a globally minimizes the Fermat--Weber objective if and only if the weighted normalized displacement vectors balance to zero.

theorem isMinOn_fermatWeberObjective_iff_residualBound_at_site {m d : ℕ} (ω : Fin m → ℝ) (hω : ∀ (i : Fin m), 0 ≤ ω i) (a : Fin m → EuclideanSpace ℝ (Fin d)) (ha : Function.Injective a) (j : Fin m) : IsMinOn (fermatWeberObjective ω a) Set.univ (a j) ↔ ‖fermatWeberResidualBalance ω a j‖ ≤ ω j

Helper for Proposition 3.33: under nonnegative weights and pairwise distinct sites, a j globally minimizes the Fermat--Weber objective if and only if the residual balance over the remaining sites has norm at most ω j.

theorem isMinOn_fermatWeberObjective_iff_balance_or_site_bound {m d : ℕ} (ω : Fin m → ℝ) (a : Fin m → EuclideanSpace ℝ (Fin d)) (ha : Function.Injective a) (hω : ∀ (i : Fin m), 0 ≤ ω i) (x : EuclideanSpace ℝ (Fin d)) : IsMinOn (fermatWeberObjective ω a) Set.univ x ↔ x ∉ Set.range a ∧ ∑ i : Fin m, fermatWeberBalanceTerm ω a x i = 0 ∨ ∃ (j : Fin m), x = a j ∧ ‖fermatWeberResidualBalance ω a j‖ ≤ ω j

Proposition 3.33: for pairwise distinct sites and nonnegative weights, a point globally minimizes the Fermat--Weber objective if and only if either it is not one of the sites and the weighted normalized displacement vectors sum to zero, or it equals a site a_j and the norm of the corresponding residual sum over the remaining sites is at most ω_j.