noncomputable def continuousLocationOptimalValue (p n : ℕ) (m : Fin p → ℝ) (c : Fin p → Fin n → ℝ) (rbar : ℝ) : ℝ

Definition 1.4.2.1. Let p ≥ 1 and let m_j > 0 be weights. Given locations c_j ∈ ℝ^n for j = 1, ..., p and a radius \bar r > 0, define the continuous location problem by the optimal value f* = min_x { f(x) := ∑_{j=1}^p m_j ‖x - c_j‖_1 : ‖x‖_1 ≤ \bar r } (4.15).

theorem continuousLocation.norm_const_fin (n : ℕ) (hn : 0 < n) (r : ℝ) : ‖fun (x : Fin n) => r‖ = ‖r‖

On Fin n → ℝ with the Pi (sup) norm, constant functions have the same norm as their value, provided the index type is nonempty.

theorem continuousLocation.norm_const_one_fin (n : ℕ) (hn : 0 < n) : ‖fun (x : Fin n) => 1‖ = 1

The constant 1 function on Fin n has norm 1 when n > 0.

theorem continuousLocation.D1_eq_half_rbar_sq (n : ℕ) (rbar : ℝ) (hn : 0 < n) (hrbar : 0 ≤ rbar) : have Q1 := {x : Fin n → ℝ | ‖x‖ ≤ rbar}; have d1 := fun (x : Fin n → ℝ) => 1 / 2 * ‖x‖ ^ 2; sSup (d1 '' Q1) = 1 / 2 * rbar ^ 2

The prox-diameter term D1 for d1(x) = (1/2)‖x‖^2 on the ball ‖x‖ ≤ rbar.

theorem continuousLocation.D2_eq_half_P (p n : ℕ) (m : Fin p → ℝ) (hn : 0 < n) (hm : ∀ (j : Fin p), 0 ≤ m j) : have Q2 := {u : Fin p → Fin n → ℝ | ∀ (j : Fin p), ‖u j‖ ≤ 1}; have norm2 := fun (u : Fin p → Fin n → ℝ) => √(∑ j : Fin p, m j * ‖u j‖ ^ 2); have d2 := fun (u : Fin p → Fin n → ℝ) => 1 / 2 * norm2 u ^ 2; have P := ∑ j : Fin p, m j; sSup (d2 '' Q2) = 1 / 2 * P

The prox-diameter term D2 for d2(u) = (1/2)‖u‖_2^2 with ‖u‖_2^2 = ∑ m_j ‖u_j‖^2 over the set ‖u_j‖ ≤ 1.

theorem continuousLocation.rate_sqrt_simplify (P rbar : ℝ) (hP : 0 ≤ P) (hrbar : 0 ≤ rbar) (N : ℕ) : 4 * √P / (↑N + 1) * √(1 / 2 * rbar ^ 2 * (1 / 2 * P)) = 2 * P * rbar / (↑N + 1)

Algebraic simplification used in the final step of Proposition 1.4.2.1.

theorem continuousLocation.ftilde_bound_from_f_bound {P fval fstar rbar : ℝ} {N : ℕ} (hP : 0 ≤ P) (hrbar : 0 ≤ rbar) (h : fval - fstar ≤ 2 * P * rbar / (↑N + 1)) : 1 / P * fval - 1 / P * fstar ≤ 2 * rbar / (↑N + 1)

Convert an f-bound into the corresponding bound for the rescaled objective ftilde.

theorem continuousLocation_euclidean_prox_rate (p n : ℕ) (m : Fin p → ℝ) (c : Fin p → Fin n → ℝ) (rbar : ℝ) (A : (Fin n → ℝ) →L[ℝ] (Fin p → Fin n → ℝ) →L[ℝ] ℝ) (N : ℕ) (xhat : Fin n → ℝ) (hn : 0 < n) (hrbar : 0 ≤ rbar) (hm : ∀ (j : Fin p), 0 ≤ m j) : have Q1 := {x : Fin n → ℝ | ‖x‖ ≤ rbar}; have d1 := fun (x : Fin n → ℝ) => 1 / 2 * ‖x‖ ^ 2; have Q2 := {u : Fin p → Fin n → ℝ | ∀ (j : Fin p), ‖u j‖ ≤ 1}; have norm2 := fun (u : Fin p → Fin n → ℝ) => √(∑ j : Fin p, m j * ‖u j‖ ^ 2); have d2 := fun (u : Fin p → Fin n → ℝ) => 1 / 2 * norm2 u ^ 2; have D1 := sSup (d1 '' Q1); have D2 := sSup (d2 '' Q2); have P := ∑ j : Fin p, m j; have A' := { toFun := fun (x : Fin n → ℝ) => ↑(A x), map_add' := ⋯, map_smul' := ⋯ }; have f := fun (x : Fin n → ℝ) => ∑ j : Fin p, m j * ‖x - c j‖; have fstar := continuousLocationOptimalValue p n m c rbar; have ftilde := fun (x : Fin n → ℝ) => 1 / P * f x; have ftilde_star := 1 / P * fstar; OperatorNormDef A' = √P → f xhat - fstar ≤ 4 * OperatorNormDef A' / (↑N + 1) * √(D1 * D2) → D1 = 1 / 2 * rbar ^ 2 ∧ D2 = 1 / 2 * P ∧ f xhat - fstar ≤ 2 * P * rbar / (↑N + 1) ∧ ftilde xhat - ftilde_star ≤ 2 * rbar / (↑N + 1)

Proposition 1.4.2.1. In the setting of Definition 1.4.2.1, take ‖·‖_1 to be the Euclidean norm on ℝ^n and d1(x) = (1/2) ‖x‖_1^2 on Q1 = {x : ‖x‖_1 ≤ rbar}. Then σ1 = 1 and D1 = max_{x ∈ Q1} d1(x) = (1/2) rbar^2. Let E2 = (E1*)^p and Q2 = {u = (u_1, ..., u_p) : ‖u_j‖_{1,*} ≤ 1}. Choose ‖u‖_2 = (∑_{j=1}^p m_j ‖u_j‖_{1,*}^2)^{1/2} and d2(u) = (1/2) ‖u‖_2^2. Then σ2 = 1 and, with P = ∑ m_j, D2 = max_{u ∈ Q2} d2(u) = (1/2) P and ‖A‖_{1,2} = P^{1/2}. Since fhat ≡ 0 in (4.1), the estimate (4.3) yields the rate f(xhat) - f* ≤ 2 P rbar / (N+1) (4.16), and for tilde f = (1/P) f we have tilde f(xhat) - tilde f* ≤ 2 rbar / (N+1).

theorem d2_eq_half_sum_weighted_norm_sq (p n : ℕ) (m : Fin p → ℝ) (hm : ∀ (j : Fin p), 0 ≤ m j) (u : Fin p → Fin n → ℝ) : 1 / 2 * √(∑ j : Fin p, m j * ‖u j‖ ^ 2) ^ 2 = 1 / 2 * ∑ j : Fin p, m j * ‖u j‖ ^ 2

Under nonnegative weights, the prox-term d2(u) = (1/2) * (sqrt (∑ m_j ‖u_j‖^2))^2 simplifies to the weighted sum d2(u) = (1/2) * ∑ m_j ‖u_j‖^2.

noncomputable def signVec {n : ℕ} (y : Fin n → ℝ) : Fin n → ℝ

The coordinatewise sign vector, with entries ±1, used to saturate the ‖·‖∞ unit ball.

theorem abs_apply_le_norm {n : ℕ} (u : Fin n → ℝ) (i : Fin n) : |u i| ≤ ‖u‖

For the Pi (sup) norm on Fin n → ℝ, each coordinate is bounded by the total norm.

theorem norm_signVec_le_one {n : ℕ} (y : Fin n → ℝ) : ‖signVec y‖ ≤ 1

The signVec has ‖signVec y‖ ≤ 1 in the Pi (sup) norm.

theorem sum_signVec_mul {n : ℕ} (y : Fin n → ℝ) : ∑ i : Fin n, signVec y i * y i = ∑ i : Fin n, |y i|

signVec attains the dual pairing with the ‖·‖∞ unit ball: ∑ sign(y_i) * y_i = ∑ |y_i|.

theorem dot_le_norm_mul_sum_abs {n : ℕ} (u y : Fin n → ℝ) : ∑ i : Fin n, u i * y i ≤ ‖u‖ * ∑ i : Fin n, |y i|

For the Pi (sup) norm on Fin n → ℝ, the dot product is bounded by ‖u‖ * ∑ |y_i|.

theorem psi_mu_piecewise (μ τ : ℝ) (hμ : 0 < μ) (hτ : 0 ≤ τ) : sSup ((fun (γ : ℝ) => γ * τ - 1 / 2 * μ * γ ^ 2) '' Set.Icc 0 1) = if τ ≤ μ then τ ^ 2 / (2 * μ) else τ - μ / 2

Piecewise evaluation of ψμ(τ) = max_{γ∈[0,1]} (γ τ - (μ/2) γ^2) for μ > 0 and τ ≥ 0.

theorem continuousLocation_smoothedFunction_explicit (p n : ℕ) (m : Fin p → ℝ) (c : Fin p → Fin n → ℝ) (μ : ℝ) (A : (Fin n → ℝ) →L[ℝ] (Fin p → Fin n → ℝ) →L[ℝ] ℝ) (phihat : (Fin p → Fin n → ℝ) → ℝ) (hμ : 0 < μ) (hm : ∀ (j : Fin p), 0 ≤ m j) (hA : ∀ (x : Fin n → ℝ) (u : Fin p → Fin n → ℝ), (A x) u = ∑ j : Fin p, m j * ∑ i : Fin n, u j i * x i) (hphihat : ∀ (u : Fin p → Fin n → ℝ), phihat u = ∑ j : Fin p, m j * ∑ i : Fin n, u j i * c j i) : have Q2 := {u : Fin p → Fin n → ℝ | ∀ (j : Fin p), ‖u j‖ ≤ 1}; have norm2 := fun (u : Fin p → Fin n → ℝ) => √(∑ j : Fin p, m j * ‖u j‖ ^ 2); have d2 := fun (u : Fin p → Fin n → ℝ) => 1 / 2 * norm2 u ^ 2; have fμ := SmoothedMaxFunction Q2 A phihat d2 μ; have ψμ := fun (τ : ℝ) => sSup ((fun (γ : ℝ) => γ * τ - 1 / 2 * μ * γ ^ 2) '' Set.Icc 0 1); (∀ (x : Fin n → ℝ), fμ x = ∑ j : Fin p, m j * ψμ (∑ i : Fin n, |x i - c j i|)) ∧ ∀ (τ : ℝ), 0 ≤ τ → ψμ τ = if τ ≤ μ then τ ^ 2 / (2 * μ) else τ - μ / 2

Proposition 1.4.2.2. In the setting of Proposition 1.4.2.1, the smoothed function f_μ admits the explicit representation f_μ(x) = ∑_{j=1}^p m_j ψ_μ(‖x - c_j‖_1), where ψ_μ : [0,∞) → ℝ is given by ψ_μ(τ) = max_{γ ∈ [0,1]} {γ τ - (1/2) μ γ^2} and equals the piecewise formula in (4.17): ψ_μ(τ) = τ^2/(2 μ) for 0 ≤ τ ≤ μ, and ψ_μ(τ) = τ - μ/2 for μ ≤ τ.