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

EReal-valued monotone conjugate for an EReal-valued function on ℝ^n_+ (modeled as Fin n → NNReal). This version allows the input function to take the value ⊤, so it can be iterated.

Equations

• monotoneConjugateERealEReal 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)

theorem monotoneConjugate_properties_and_involutive (n : ℕ) (g : (Fin n → NNReal) → ℝ) (hg_mono : Monotone g) (hg_lsc : LowerSemicontinuous g) (hg_convex : ConvexOn NNReal Set.univ g) (hg0 : ∃ (c : ℝ), g 0 = c) : have gPlus := monotoneConjugateEReal n g; (Monotone gPlus ∧ LowerSemicontinuous gPlus ∧ (∀ (x y : Fin n → NNReal) (a b : NNReal), a + b = 1 → gPlus (a • x + b • y) ≤ ↑↑a * gPlus x + ↑↑b * gPlus y) ∧ ∃ (c : ℝ), gPlus 0 = ↑c) ∧ monotoneConjugateERealEReal n gPlus = fun (y : Fin n → NNReal) => ↑(g y)

Theorem 12.4. Let g be a non-decreasing lower semicontinuous convex function on the nonnegative orthant ℝ^n_+ (modeled as Fin n → NNReal) such that g 0 is finite.

Then the monotone conjugate g⁺ (here g⁺ = monotoneConjugateEReal n g) has the same properties, and the monotone conjugate of g⁺ is g (as an EReal-valued function).