theorem exp_linear_sub_exp_le_conjugateValue {a x : ℝ} (ha : 0 < a) : x * a - Real.exp x ≤ a * Real.log a - a

A standard inequality for the exponential function: for a > 0, the function x ↦ x * a - exp x is bounded above by a * log a - a.

theorem exists_gt_linear_sub_exp_of_neg {a μ : ℝ} (ha : a < 0) : ∃ (x : ℝ), μ < x * a - Real.exp x

If a < 0, the function x ↦ x * a - exp x is unbounded above.

theorem exists_gt_neg_exp_of_neg_mu {μ : ℝ} (hμ : μ < 0) : ∃ (x : ℝ), μ < -Real.exp x

For any negative μ, one can make -exp x exceed μ by choosing x very negative.

theorem fenchelConjugate_exp_pos_case (xStar : Fin 1 → ℝ) (ha : 0 < xStar 0) : fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => ↑(Real.exp (x 0))) xStar = ↑(xStar 0 * Real.log (xStar 0) - xStar 0)

The xStar 0 > 0 case for the conjugate of x ↦ exp (x 0) in dimension 1.

theorem fenchelConjugate_exp_zero_case (xStar : Fin 1 → ℝ) (ha0 : xStar 0 = 0) : fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => ↑(Real.exp (x 0))) xStar = 0

The xStar 0 = 0 case for the conjugate of x ↦ exp (x 0) in dimension 1.

theorem fenchelConjugate_exp_neg_case (xStar : Fin 1 → ℝ) (ha : xStar 0 < 0) : fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => ↑(Real.exp (x 0))) xStar = ⊤

The xStar 0 < 0 case for the conjugate of x ↦ exp (x 0) in dimension 1.

theorem fenchelConjugate_exp (xStar : Fin 1 → ℝ) : fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => ↑(Real.exp (x 0))) xStar = if xStar 0 > 0 then ↑(xStar 0 * Real.log (xStar 0) - xStar 0) else if xStar 0 = 0 then 0 else ⊤

Text 12.2.4: The conjugate function of the exponential function f(x) = e^x on ℝ is given by the piecewise formula f*(x^*) = x^* log x^* - x^* if x^* > 0, f*(0) = 0, and f*(x^*) = +∞ if x^* < 0.

theorem holderConjugate_of_oneDiv_add_oneDiv_eq_one (p q : ℝ) (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) : p.HolderConjugate q

Turn the hypotheses 1 < p and 1/p + 1/q = 1 into p.HolderConjugate q.

theorem range_term_le_conj_bound_oneDiv_mul_abs_rpow {p q a x : ℝ} (hpq : p.HolderConjugate q) : x * a - 1 / p * |x|.rpow p ≤ 1 / q * |a|.rpow q

Young's inequality rearranged as an upper bound for the Fenchel-conjugate range terms.

theorem opt_value_oneDiv_mul_abs_rpow {p q : ℝ} (hpq : p.HolderConjugate q) (a : ℝ) : have x0 := if 0 ≤ a then |a|.rpow (q - 1) else -|a|.rpow (q - 1); x0 * a - 1 / p * |x0|.rpow p = 1 / q * |a|.rpow q

Value of x*a - (1/p)*|x|^p at the explicit maximizer x = sign(a) * |a|^(q-1).

theorem fenchelConjugate_oneDiv_mul_abs_rpow (p q : ℝ) (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) (xStar : Fin 1 → ℝ) : fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => ↑(1 / p * |x 0|.rpow p)) xStar = ↑(1 / q * |xStar 0|.rpow q)

Text 12.2.5: Let p ∈ (1, +∞). The conjugate of the function f(x) = (1/p) * |x|^p on ℝ is given by f*(x*) = (1/q) * |x*|^q, where 1/p + 1/q = 1.

theorem q_neg_and_coeff_identities_of_oneDiv_add_oneDiv_eq_one {p q : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (hpq : 1 / p + 1 / q = 1) : q ≠ 0 ∧ q < 0 ∧ 1 / p - 1 = -(1 / q) ∧ (q - 1) * p = q

Basic identities for q when 0 < p < 1 and 1/p + 1/q = 1.

theorem rpow_le_affine_at_one_of_lt_one {p t : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (ht : 0 ≤ t) : t.rpow p ≤ 1 - p + p * t

For 0 < p < 1 and t ≥ 0, we have the tangent-line upper bound t^p ≤ (1 - p) + p * t.

theorem opt_value_neg_oneDiv_mul_rpow {p q a : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (hpq : 1 / p + 1 / q = 1) (ha : a < 0) : have x0 := |a|.rpow (q - 1); x0 * a + 1 / p * x0.rpow p = -(1 / q) * |a|.rpow q

Value of x*a + (1/p)*x^p at the candidate maximizer x0 = |a|^(q-1) in the a < 0 case.

theorem range_term_le_conjValue_neg_case {p q a x : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (hpq : 1 / p + 1 / q = 1) (ha : a < 0) (hx : 0 ≤ x) : x * a + 1 / p * x.rpow p ≤ -(1 / q) * |a|.rpow q

For a < 0, each finite range term in the Fenchel conjugate is bounded above by the optimal value -(1/q) * |a|^q.

theorem fenchelConjugate_neg_oneDiv_mul_rpow_top_case (p : ℝ) (hp0 : 0 < p) (xStar : Fin 1 → ℝ) (ha : 0 ≤ xStar 0) : fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => if 0 ≤ x 0 then ↑(-(1 / p) * (x 0).rpow p) else ⊤) xStar = ⊤

The xStar 0 ≥ 0 case: the conjugate is unbounded above, hence ⊤.

theorem fenchelConjugate_neg_oneDiv_mul_rpow (p q : ℝ) (hp0 : 0 < p) (hp1 : p < 1) (hpq : 1 / p + 1 / q = 1) (xStar : Fin 1 → ℝ) : fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => if 0 ≤ x 0 then ↑(-(1 / p) * (x 0).rpow p) else ⊤) xStar = if xStar 0 < 0 then ↑(-(1 / q) * |xStar 0|.rpow q) else ⊤

Text 12.2.6: Let 0 < p < 1. Consider the extended-real function on ℝ given by f(x) = -(1/p) * x^p for x ≥ 0 and f(x) = +∞ otherwise. Its conjugate has the piecewise formula f*(x*) = -(1/q) * |x*|^q for x* < 0 and f*(x*) = +∞ for x* ≥ 0, where 1/p + 1/q = 1 (in particular q < 0).