theorem quadraticHalfLinear_translate_sub_of_dotProduct_symmetric {n : ℕ} (Q : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ) (hQsymm : ∀ (x y : Fin n → ℝ), Q x ⬝ᵥ y = x ⬝ᵥ Q y) (a x : Fin n → ℝ) : quadraticHalfLinear n Q (x - a) = quadraticHalfLinear n Q x + ↑(x ⬝ᵥ -Q a) + ↑(1 / 2 * a ⬝ᵥ Q a)

Translation identity for the shifted argument: rewrite quadraticHalfLinear n Q (x - a) in terms of quadraticHalfLinear n Q x, plus a linear term and a constant, assuming dot-product symmetry of Q.

theorem sq_segment_le (a b t : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : ((1 - t) * a + t * b) ^ 2 ≤ (1 - t) * a ^ 2 + t * b ^ 2

Convexity of the square function: t ↦ ((1 - t)a + t b)^2 lies below the chord between a^2 and b^2 for t ∈ [0,1].

theorem properConvexFunctionOn_diagonalQuadratic {n : ℕ} (d : Fin n → ℝ) (hd : ∀ (i : Fin n), 0 ≤ d i) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(1 / 2 * ∑ i : Fin n, d i * x i ^ 2)

A weighted diagonal quadratic function with nonnegative weights is a proper convex function on ℝ^n.

theorem properConvexFunctionOn_elementaryPartialQuadratic {n : ℕ} {h : (Fin n → ℝ) → EReal} (hElem : IsElementaryPartialQuadraticConvexFunction n h) : ProperConvexFunctionOn Set.univ h

Elementary partial quadratic convex functions are proper convex on Set.univ.

theorem properConvexFunctionOn_precomp_linearEquiv {n : ℕ} (A : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ) {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => f (A x)

Precomposition by a linear equivalence preserves proper convexity on Set.univ.

theorem properConvexFunctionOn_translate {n : ℕ} (a : Fin n → ℝ) {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => f (x - a)

Translating the input preserves proper convexity on Set.univ.

theorem properConvexFunctionOn_affine_dotProduct {n : ℕ} (v : Fin n → ℝ) (α : ℝ) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ v + α)

The affine function x ↦ ⟪x, v⟫ + α is a proper convex function on Set.univ.

theorem isPartialQuadraticConvexFunction_iff_exists_elementary_affine (n : ℕ) (f : (Fin n → ℝ) → EReal) : IsPartialQuadraticConvexFunction n f ↔ ∃ (h : (Fin n → ℝ) → EReal) (A : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ) (a : Fin n → ℝ) (aStar : Fin n → ℝ) (α : ℝ), IsElementaryPartialQuadraticConvexFunction n h ∧ f = fun (x : Fin n → ℝ) => h (A (x - a)) + ↑(x ⬝ᵥ aStar) + ↑α

Text 12.3.3: Characterization of partial quadratic convex functions by affine change of coordinates to an elementary partial quadratic convex function plus a linear term.

theorem ereal_iSup_neg_eq_neg_iInf {ι : Sort u_1} (g : ι → EReal) : ⨆ (i : ι), -g i = -⨅ (i : ι), g i

Negation turns iInf into iSup in EReal.

theorem fenchelConjugate_zero_eq_neg_iInf (n : ℕ) (f : (Fin n → ℝ) → EReal) : fenchelConjugate n f 0 = -⨅ (x : Fin n → ℝ), f x

The value of the Fenchel conjugate at 0 is the negative of the infimum of f.

theorem iInf_fenchelConjugate_eq_neg_eval_zero (n : ℕ) (f : (Fin n → ℝ) → EReal) (hf_closed : LowerSemicontinuous f) (hf_convex : ConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) : ⨅ (xStar : Fin n → ℝ), fenchelConjugate n f xStar = -f 0

For closed proper convex f, the infimum of the Fenchel conjugate is -f 0.

theorem inf_eq_at_zero_iff_conjugate_inf_eq_at_zero (n : ℕ) (f : (Fin n → ℝ) → EReal) (hf_closed : LowerSemicontinuous f) (hf_convex : ConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) : ⨅ (x : Fin n → ℝ), f x = f 0 ∧ f 0 = 0 ↔ ⨅ (xStar : Fin n → ℝ), fenchelConjugate n f xStar = fenchelConjugate n f 0 ∧ fenchelConjugate n f 0 = 0

Text 12.3.4: Let f be a closed proper convex function on ℝ^n. Then inf_x f x = f 0 = 0 if and only if inf_{x*} f* x* = f* 0 = 0, where f* is the Fenchel conjugate (here f* = fenchelConjugate n f).

@[reducible, inline]

abbrev IsSymmetricFunction {α : Type u_1} (n : ℕ) (f : (Fin n → ℝ) → α) : Prop

Defn 12.3: A function f on ℝ^n is symmetric (or even) if it satisfies f (-x) = f x for all x ∈ ℝ^n.

Equations

• IsSymmetricFunction n f = Function.Even f

theorem iSup_comp_neg {α : Type u_1} {β : Type u_2} [AddGroup α] [CompleteLattice β] (g : α → β) : ⨆ (x : α), g (-x) = iSup g

Reindex an iSup by the involution x ↦ -x.

theorem fenchelConjugate_even_of_even (n : ℕ) {f : (Fin n → ℝ) → EReal} (hf : Function.Even f) : Function.Even (fenchelConjugate n f)

If f is even, then its Fenchel conjugate f* is even.

theorem even_clConv_of_even_fenchelConjugate (n : ℕ) {f : (Fin n → ℝ) → EReal} (hf_convex : ConvexFunction f) (hEvenConj : Function.Even (fenchelConjugate n f)) : Function.Even (clConv n f)

If the Fenchel conjugate of f is even, then the closed convex envelope clConv n f is even.

theorem even_of_even_fenchelConjugate_of_closedProperConvex (n : ℕ) {f : (Fin n → ℝ) → EReal} (hf_closed : LowerSemicontinuous f) (hf_convex : ConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) (hEvenConj : Function.Even (fenchelConjugate n f)) : Function.Even f

For closed proper convex f, evenness of its Fenchel conjugate implies evenness of f.

theorem isSymmetricFunction_iff_isSymmetricFunction_fenchelConjugate (n : ℕ) (f : (Fin n → ℝ) → EReal) (hf_closed : LowerSemicontinuous f) (hf_convex : ConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) : IsSymmetricFunction n f ↔ IsSymmetricFunction n (fenchelConjugate n f)

Text 12.3.5: Let f be a closed proper convex function on ℝ^n. Then f is symmetric (i.e. f (-x) = f x for all x) if and only if its conjugate f* is symmetric (here f* = fenchelConjugate n f).

def IsRotationallySymmetric {α : Type u_1} (n : ℕ) (f : (Fin n → ℝ) → α) : Prop

Text 12.3.5: A function f on ℝ^n is symmetric with respect to all orthogonal transformations (rotationally symmetric) if and only if it has the form f x = g (‖x‖), for some function g on [0, +∞), where ‖·‖ is the Euclidean norm.

Furthermore, for such an f, it is a closed proper convex function on ℝ^n if and only if g satisfies:

1. g is convex on [0, +∞);
2. g is non-decreasing;
3. g is lower semicontinuous;
4. g 0 is finite.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def euclidNorm (n : ℕ) (x : Fin n → ℝ) : ℝ

The Euclidean norm on Fin n → ℝ, defined via the equivalence with EuclideanSpace.

Equations

• euclidNorm n x = ‖(EuclideanSpace.equiv (Fin n) ℝ).symm x‖

def nonnegRay : Set (Fin 1 → ℝ)

The nonnegative ray in Fin 1 → ℝ used to model [0, +∞).

Equations

• nonnegRay = {r : Fin 1 → ℝ | 0 ≤ r 0}

theorem convex_nonnegRay : Convex ℝ nonnegRay

The nonnegative ray nonnegRay is convex.

theorem exists_linearIsometryEquiv_euclideanSpace_apply_eq_of_norm_eq (n : ℕ) (x y : EuclideanSpace ℝ (Fin n)) (hxy : ‖x‖ = ‖y‖) : ∃ (O : EuclideanSpace ℝ (Fin n) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n)), O x = y

In Euclidean space, vectors of equal norm are related by some linear isometry.

theorem isRotationallySymmetric_iff_exists_norm_comp {α : Type u_1} (n : ℕ) (f : (Fin n → ℝ) → α) : IsRotationallySymmetric n f ↔ ∃ (g : (Fin 1 → ℝ) → α), ∀ (x : Fin n → ℝ), f x = g fun (x_1 : Fin 1) => euclidNorm n x

Text 12.3.5: Rotational symmetry is equivalent to depending only on the Euclidean norm.