theorem euclidean_subdifferentialAt_weighted_dist_eq_piecewise {d : ℕ} (ω : ℝ) (hω : 0 ≤ ω) (a x : EuclideanSpace ℝ (Fin d)) : euclideanSubdifferentialAt (fun (y : EuclideanSpace ℝ (Fin d)) => ω * dist y a) x = if x = a then Metric.closedBall 0 ω else {ω • ‖x - a‖⁻¹ • (x - a)}

Helper for Proposition 3.32: for the weighted one-site term fun y ↦ ω * dist y a with nonnegative weight ω, the Euclidean subdifferential is the singleton normalized direction away from the site and the closed Euclidean ball closedBall (0 : E) ω at the site.

theorem euclidean_subdifferentialAt_fermatWeberObjective_eq_finset_sum_piecewise {m d : ℕ} (ω : Fin m → ℝ) (hω : ∀ (i : Fin m), 0 ≤ ω i) (a : Fin m → EuclideanSpace ℝ (Fin d)) (x : EuclideanSpace ℝ (Fin d)) : euclideanSubdifferentialAt (fermatWeberObjective ω a) x = ∑ i : Fin m, if x = a i then Metric.closedBall 0 (ω i) else {ω i • ‖x - a i‖⁻¹ • (x - a i)}

Proposition 3.32: the Euclidean subdifferential of the Fermat-Weber objective fun x ↦ ∑ i, ω i * ‖x - a i‖ is the finite Minkowski sum of the single-term subdifferentials, so each summand contributes the normalized vector ω i • ((‖x - a i‖)⁻¹ • (x - a i)) away from its site and the closed Euclidean ball closedBall (0 : E) (ω i) at its site; this remains valid for nonnegative weights, with ω i = 0 giving the singleton {0} in both cases.

theorem euclidean_subdifferentialAt_fermatWeberObjective_eq_singleton_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) : euclideanSubdifferentialAt (fermatWeberObjective ω a) x = {∑ i : Fin m, ω i • ‖x - a i‖⁻¹ • (x - a i)}

Consequence of Proposition 3.32: under nonnegative weights, if x is not one of the sites a i, then the Euclidean subdifferential of fermatWeberObjective ω a is the singleton containing the weighted sum of the normalized displacement vectors.

theorem euclidean_subdifferentialAt_fermatWeberObjective_eq_image_closedBall_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) : euclideanSubdifferentialAt (fermatWeberObjective ω a) (a j) = (fun (v : EuclideanSpace ℝ (Fin d)) => ∑ i ∈ Finset.univ.erase j, ω i • ‖a j - a i‖⁻¹ • (a j - a i) + v) '' Metric.closedBall 0 (ω j)

Consequence of Proposition 3.32: under nonnegative weights and pairwise distinct sites, the Euclidean subdifferential of fermatWeberObjective ω a at the site a j is the translate of closedBall (0 : E) (ω j) by the residual weighted sum over the remaining sites.