theorem range_term_neg_sqrt_sq_sub_sq_simp (a : ℝ) (x xStar : Fin 1 → ℝ) : (↑(x ⬝ᵥ xStar) - if |x 0| ≤ a then ↑(-√(a ^ 2 - x 0 ^ 2)) else ⊤) = if |x 0| ≤ a then ↑(x 0 * xStar 0 + √(a ^ 2 - x 0 ^ 2)) else ⊥

Simplify the Fenchel-conjugate range term for the function x ↦ if |x| ≤ a then -√(a^2-x^2) else +∞ in dimension 1.

theorem mul_add_sqrt_sq_sub_sq_le {a x s : ℝ} (ha : 0 ≤ a) (hx : |x| ≤ a) : x * s + √(a ^ 2 - x ^ 2) ≤ a * √(1 + s ^ 2)

A Cauchy–Schwarz-type bound for the range terms x*s + √(a^2-x^2) under the constraint |x| ≤ a and a ≥ 0.

theorem exists_argmax_mul_add_sqrt_sq_sub_sq (a s : ℝ) (ha : 0 ≤ a) : ∃ (x0 : ℝ), |x0| ≤ a ∧ x0 * s + √(a ^ 2 - x0 ^ 2) = a * √(1 + s ^ 2)

A concrete point x0 achieving the upper bound in mul_add_sqrt_sq_sub_sq_le.

theorem fenchelConjugate_neg_sqrt_sq_sub_sq (a : ℝ) (ha : 0 ≤ a) (xStar : Fin 1 → ℝ) : fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => if |x 0| ≤ a then ↑(-√(a ^ 2 - x 0 ^ 2)) else ⊤) xStar = ↑(a * √(1 + xStar 0 ^ 2))

Text 12.2.7: Let f : ℝ → [-∞, +∞] be the extended-real function f(x) = -√(a^2 - x^2) for |x| ≤ a (with a ≥ 0) and f(x) = +∞ otherwise. Then its conjugate is given by f*(x*) = a * √(1 + x*^2). Here the conjugate is represented by fenchelConjugate.

theorem fenchelConjugate_neg_log_sub_oneHalf (xStar : Fin 1 → ℝ) : fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => if 0 < x 0 then ↑(-Real.log (x 0) - 1 / 2) else ⊤) xStar = if xStar 0 < 0 then ↑(-Real.log (-xStar 0) - 1 / 2) else ⊤

Text 12.2.8: Consider f(x) = -log x - 1/2 for x > 0 (and +∞ otherwise). The conjugate is given by f*(x*) = -log(-x*) - 1/2 if x* < 0 and f*(x*) = +∞ if x* ≥ 0. Here the conjugate is represented by fenchelConjugate.

noncomputable def quadraticHalfInner (n : ℕ) : (Fin n → ℝ) → EReal

The quadratic function w(x) = (1/2) * ⟪x, x⟫ on ℝ^n, written on coordinates x : Fin n → ℝ and valued in EReal.

Equations

• quadraticHalfInner n x = ↑(1 / 2 * x ⬝ᵥ x)