theorem radial_ne_bot_of_mono_g0_finite {n : ℕ} {g : (Fin 1 → ℝ) → EReal} (hg_mono : MonotoneOn g nonnegRay) (hg0 : ∃ (c : ℝ), g 0 = ↑c) (x : Fin n → ℝ) : (g fun (x_1 : Fin 1) => euclidNorm n x) ≠ ⊥

If g is monotone on nonnegRay and g 0 is finite, then x ↦ g (euclidNorm n x) never takes the value ⊥.

theorem radial_convex_of_convexOn_monoOn (n : ℕ) {g : (Fin 1 → ℝ) → EReal} (hg_conv : ConvexFunctionOn nonnegRay g) (hg_mono : MonotoneOn g nonnegRay) (hg0 : ∃ (c : ℝ), g 0 = ↑c) : have f := fun (x : Fin n → ℝ) => g fun (x_1 : Fin 1) => euclidNorm n x; ConvexFunction f

Convexity of the radial composition x ↦ g (‖x‖) from convexity and monotonicity of g on the nonnegative ray, assuming g 0 is finite.

theorem radial_lsc_of_lscOn (n : ℕ) (g : (Fin 1 → ℝ) → EReal) (hg : LowerSemicontinuousOn g nonnegRay) : have f := fun (x : Fin n → ℝ) => g fun (x_1 : Fin 1) => euclidNorm n x; LowerSemicontinuous f

Lower semicontinuity of g on nonnegRay implies lower semicontinuity of the radial composition x ↦ g (‖x‖).

theorem radial_proper_of_mono_g0_finite (n : ℕ) {g : (Fin 1 → ℝ) → EReal} (hg_mono : MonotoneOn g nonnegRay) (hg0 : ∃ (c : ℝ), g 0 = ↑c) (hf_conv : have f := fun (x : Fin n → ℝ) => g fun (x_1 : Fin 1) => euclidNorm n x; ConvexFunction f) : have f := fun (x : Fin n → ℝ) => g fun (x_1 : Fin 1) => euclidNorm n x; ProperConvexFunctionOn Set.univ f

Properness of the radial function follows from finiteness at 0 and monotonicity of g on the ray, once convexity is known.

theorem radial_ray_props_of_closedProperConvex (n : ℕ) (hn : 0 < n) (g : (Fin 1 → ℝ) → EReal) : have f := fun (x : Fin n → ℝ) => g fun (x_1 : Fin 1) => euclidNorm n x; LowerSemicontinuous f ∧ ConvexFunction f ∧ ProperConvexFunctionOn Set.univ f → ConvexFunctionOn nonnegRay g ∧ MonotoneOn g nonnegRay ∧ LowerSemicontinuousOn g nonnegRay ∧ ∃ (c : ℝ), g 0 = ↑c

From closed proper convexity of the radial function x ↦ g (‖x‖), recover the one-dimensional ray conditions on g.

theorem radial_closedProperConvex_iff (n : ℕ) (hn : 0 < n) (g : (Fin 1 → ℝ) → EReal) : have f := fun (x : Fin n → ℝ) => g fun (x_1 : Fin 1) => euclidNorm n x; LowerSemicontinuous f ∧ ConvexFunction f ∧ ProperConvexFunctionOn Set.univ f ↔ ConvexFunctionOn {r : Fin 1 → ℝ | 0 ≤ r 0} g ∧ MonotoneOn g {r : Fin 1 → ℝ | 0 ≤ r 0} ∧ LowerSemicontinuousOn g {r : Fin 1 → ℝ | 0 ≤ r 0} ∧ ∃ (c : ℝ), g 0 = ↑c

noncomputable def monotoneConjugate (n : ℕ) (g : (Fin n → NNReal) → ℝ) : (Fin n → NNReal) → ℝ

Defn 12.4: Let g be a function on the nonnegative orthant ℝ^n_+. Its monotone conjugate g⁺ is defined for y* ∈ ℝ^n_+ by g⁺(y*) = sup_{y ≥ 0} (⟪y, y*⟫ - g y).

Equations

• monotoneConjugate n g yStar = sSup (Set.range fun (y : Fin n → NNReal) => ((fun (i : Fin n) => ↑(y i)) ⬝ᵥ fun (i : Fin n) => ↑(yStar i)) - g y)

noncomputable def monotoneConjugateEReal (n : ℕ) (g : (Fin n → NNReal) → ℝ) : (Fin n → NNReal) → EReal

EReal-valued monotone conjugate: same supremum, but living in [-∞, ∞] so it can take ⊤.

Equations

• monotoneConjugateEReal n g yStar = sSup (Set.range fun (y : Fin n → NNReal) => ↑((fun (i : Fin n) => ↑(y i)) ⬝ᵥ fun (i : Fin n) => ↑(yStar i)) - ↑(g y))

def absVecNN (n : ℕ) (x : Fin n → ℝ) : Fin n → NNReal

Text 12.3.6: For x : ℝ^n, define abs x = (|x₁|, …, |xₙ|) as an element of the nonnegative orthant ℝ^n_+ (modeled as Fin n → NNReal).

Equations

• absVecNN n x i = ⟨|x i|, ⋯⟩

theorem absVecNN_coe (n : ℕ) (y : Fin n → NNReal) : (absVecNN n fun (i : Fin n) => ↑(y i)) = y

Coercing a nonnegative vector to Real and taking componentwise absolute values recovers it.

theorem absVecNN_neg (n : ℕ) (x : Fin n → ℝ) : absVecNN n (-x) = absVecNN n x

Componentwise absolute values ignore global sign changes.

theorem lowerSemicontinuous_coe_real_toEReal {α : Type u_1} [TopologicalSpace α] {h : α → ℝ} : LowerSemicontinuous h → LowerSemicontinuous fun (x : α) => ↑(h x)

Lower semicontinuity is preserved by coercion Real → EReal.

theorem lowerSemicontinuous_of_coe_real_toEReal {α : Type u_1} [TopologicalSpace α] {h : α → ℝ} : (LowerSemicontinuous fun (x : α) => ↑(h x)) → LowerSemicontinuous h

Lower semicontinuity of Real → EReal coercions implies lower semicontinuity of the real map.

theorem continuous_coeVecNN (n : ℕ) : Continuous fun (y : Fin n → NNReal) (i : Fin n) => ↑(y i)

The coercion Fin n → NNReal → Fin n → Real is continuous.

theorem continuous_absVecNN (n : ℕ) : Continuous (absVecNN n)

The map x ↦ absVecNN n x is continuous.

theorem abs_combo_le (a b t : ℝ) (ht0 : 0 ≤ t) (ht1 : 0 ≤ 1 - t) : |(1 - t) * a + t * b| ≤ (1 - t) * |a| + t * |b|

Pointwise triangle inequality for affine combinations: | (1-t)x + t y | is bounded by the corresponding convex combination of |x| and |y| when t ∈ [0,1].

theorem exists_sign_choice_dotProduct_eq (n : ℕ) (xStar : Fin n → ℝ) (y : Fin n → NNReal) : ∃ (x : Fin n → ℝ), absVecNN n x = y ∧ x ⬝ᵥ xStar = (fun (i : Fin n) => ↑(y i)) ⬝ᵥ fun (i : Fin n) => ↑(absVecNN n xStar i)

Choose signs so that x ⬝ᵥ xStar becomes |x| ⬝ᵥ |xStar|.

theorem closedProperConvex_abs_comp_iff (n : ℕ) (g : (Fin n → NNReal) → ℝ) : have f := fun (x : Fin n → ℝ) => ↑(g (absVecNN n x)); LowerSemicontinuous f ∧ ConvexFunction f ∧ ProperConvexFunctionOn Set.univ f ↔ LowerSemicontinuous g ∧ ConvexOn NNReal Set.univ g ∧ (∃ (c : ℝ), g 0 = c) ∧ Monotone g

Text 12.3.6 (1): Let f : ℝ^n → ℝ be of the form f(x) = g(abs x) with g : ℝ^n_+ → ℝ and abs x = (|x₁|, …, |xₙ|).

Then f is closed proper convex on ℝ^n iff g is lower semicontinuous, convex, finite at 0, and non-decreasing (i.e. 0 ≤ y ≤ y' → g y ≤ g y').

theorem fenchelConjugate_abs_comp_eq_monotoneConjugate (n : ℕ) (g : (Fin n → NNReal) → ℝ) : have f := fun (x : Fin n → ℝ) => ↑(g (absVecNN n x)); ∀ (xStar : Fin n → ℝ), fenchelConjugate n f xStar = monotoneConjugateEReal n g (absVecNN n xStar)

Text 12.3.6 (2): The conjugate of f(x) = g(abs x) is f*(x*) = g⁺(abs x*), where g⁺ is the EReal-valued monotone conjugate (here g⁺ = monotoneConjugateEReal n g).