def LipschitzCondition {n : ℕ} (f : (Fin n → ℝ) → EReal) (α : ℝ) : Prop

Auxiliary definition: the global Lipschitz condition |f(z) - f(x)| ≤ α * ‖z - x‖, expressed via toReal for an EReal-valued function.

Equations

• LipschitzCondition f α = ∀ (z x : Fin n → ℝ), |(f z).toReal - (f x).toReal| ≤ α * ‖z - x‖

noncomputable def l1Norm {n : ℕ} (x : Fin n → ℝ) : ℝ

Auxiliary definition: the ℓ¹-norm on ℝ^n (with ℝ^n represented as Fin n → ℝ).

Equations

• l1Norm x = ∑ i : Fin n, ‖x i‖

noncomputable def conjugateDomainRadius {n : ℕ} (f : (Fin n → ℝ) → EReal) : ℝ

Auxiliary definition: the quantity sup { ‖xStar‖₁ | xStar ∈ dom f^* }, where dom f^* is the effective domain of the Fenchel conjugate f^*.

Equations

• conjugateDomainRadius f = sSup ((fun (xStar : Fin n → ℝ) => l1Norm xStar) '' effectiveDomain Set.univ (fenchelConjugate n f))

theorem section13_recessionFunction_le_mul_norm_of_LipschitzCondition {n : ℕ} {f : (Fin n → ℝ) → EReal} {α : ℝ} (hfinite : ∀ (z : Fin n → ℝ), f z ≠ ⊤ ∧ f z ≠ ⊥) (hLip : LipschitzCondition f α) (y : Fin n → ℝ) : recessionFunction f y ≤ ↑(α * ‖y‖)

If f is finite everywhere and satisfies LipschitzCondition f α, then its recession function is bounded above by α‖y‖.

theorem section13_set_eq_univ_of_supportFunctionEReal_eq_top {n : ℕ} (C : Set (Fin n → ℝ)) (hconv : Convex ℝ C) (hne : C.Nonempty) (htop : ∀ (y : Fin n → ℝ), y ≠ 0 → supportFunctionEReal C y = ⊤) : C = Set.univ

If a nonempty convex set has support function ⊤ in every nonzero direction, then the set is all of ℝ^n.

theorem section13_finite_everywhere_of_isBounded_effectiveDomain_fenchelConjugate {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) (hbounded : Bornology.IsBounded (effectiveDomain Set.univ (fenchelConjugate n f))) (z : Fin n → ℝ) : f z ≠ ⊤ ∧ f z ≠ ⊥

If f is proper convex and dom f* is bounded, then f is finite everywhere.

theorem section13_supportFunctionEReal_le_mul_norm_of_isBounded {n : ℕ} (C : Set (Fin n → ℝ)) (hbounded : Bornology.IsBounded C) : ∃ R ≥ 0, ∀ (y : Fin n → ℝ), supportFunctionEReal C y ≤ ↑(R * ‖y‖)

If C is bounded, then its support function is dominated by R‖y‖ for some R ≥ 0 with respect to the sup norm on ℝ^n.

theorem section13_lipschitzCondition_of_recessionFunction_le_mul_norm {n : ℕ} {f : (Fin n → ℝ) → EReal} {α : ℝ} (hfinite : ∀ (z : Fin n → ℝ), f z ≠ ⊤ ∧ f z ≠ ⊥) (hrec : ∀ (y : Fin n → ℝ), recessionFunction f y ≤ ↑(α * ‖y‖)) : LipschitzCondition f α

If f is finite everywhere and f₀⁺(y) ≤ α‖y‖ for all y, then f satisfies the global Lipschitz condition with constant α.

theorem section13_lipschitzCondition_of_isBounded_effectiveDomain_fenchelConjugate {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) (hbounded : Bornology.IsBounded (effectiveDomain Set.univ (fenchelConjugate n f))) (hfinite : ∀ (z : Fin n → ℝ), f z ≠ ⊤ ∧ f z ≠ ⊥) : ∃ (α : ℝ), 0 ≤ α ∧ LipschitzCondition f α

If f is proper convex and dom f* is bounded, then f satisfies a global Lipschitz condition for some α ≥ 0.

theorem isBounded_effectiveDomain_fenchelConjugate_iff_finite_and_exists_lipschitz {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) : Bornology.IsBounded (effectiveDomain Set.univ (fenchelConjugate n f)) ↔ (∀ (z : Fin n → ℝ), f z ≠ ⊤ ∧ f z ≠ ⊥) ∧ ∃ (α : ℝ), 0 ≤ α ∧ LipschitzCondition f α

Corollary 13.3.3. Let f be a proper convex function. The effective domain dom f^* is bounded if and only if f is finite everywhere and there exists α ≥ 0 such that |f(z) - f(x)| ≤ α * ‖z - x‖ for all z and x (a global Lipschitz condition).

theorem section13_dotProduct_le_l1Norm_mul_norm {n : ℕ} (x y : Fin n → ℝ) : x ⬝ᵥ y ≤ l1Norm x * ‖y‖

Hölder-style estimate for the sup-norm: ⟪x,y⟫ ≤ ‖x‖₁‖y‖.

theorem section13_bddAbove_image_l1Norm_of_isBounded {n : ℕ} (C : Set (Fin n → ℝ)) (hbounded : Bornology.IsBounded C) : BddAbove ((fun (x : Fin n → ℝ) => l1Norm x) '' C)

l1Norm is bounded above on a bounded set.

theorem section13_l1Norm_le_conjugateDomainRadius_of_mem_dom {n : ℕ} (f : (Fin n → ℝ) → EReal) (hbounded : Bornology.IsBounded (effectiveDomain Set.univ (fenchelConjugate n f))) (xStar : Fin n → ℝ) : xStar ∈ effectiveDomain Set.univ (fenchelConjugate n f) → l1Norm xStar ≤ conjugateDomainRadius f

If xStar ∈ dom f*, then ‖xStar‖₁ ≤ conjugateDomainRadius f.

theorem section13_supportFunctionEReal_le_mul_norm_conjugateDomainRadius {n : ℕ} (f : (Fin n → ℝ) → EReal) (hbounded : Bornology.IsBounded (effectiveDomain Set.univ (fenchelConjugate n f))) (y : Fin n → ℝ) : supportFunctionEReal (effectiveDomain Set.univ (fenchelConjugate n f)) y ≤ ↑(conjugateDomainRadius f * ‖y‖)

The support function of dom f* is bounded by conjugateDomainRadius f * ‖y‖.

theorem section13_fenchelConjugate_eq_top_of_LipschitzCondition_lt_l1Norm {n : ℕ} {f : (Fin n → ℝ) → EReal} {α : ℝ} (hfinite : ∀ (z : Fin n → ℝ), f z ≠ ⊤ ∧ f z ≠ ⊥) (hα0 : 0 ≤ α) (hLip : LipschitzCondition f α) (xStar : Fin n → ℝ) : α < l1Norm xStar → fenchelConjugate n f xStar = ⊤

If f is finite everywhere and satisfies a global Lipschitz condition with constant α, then any xStar with α < ‖xStar‖₁ lies outside dom f* (equivalently, f* xStar = ⊤).

theorem lipschitzCondition_conjugateDomainRadius_and_minimal {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) (hbounded : Bornology.IsBounded (effectiveDomain Set.univ (fenchelConjugate n f))) (hfinite : ∀ (z : Fin n → ℝ), f z ≠ ⊤ ∧ f z ≠ ⊥) : LipschitzCondition f (conjugateDomainRadius f) ∧ ∀ (α : ℝ), 0 ≤ α → LipschitzCondition f α → conjugateDomainRadius f ≤ α

Corollary 13.3.3 (optimal Lipschitz constant): assuming f is finite everywhere and dom f^* is bounded, the smallest α for which the global Lipschitz condition holds is α = sup { ‖xStar‖ | xStar ∈ dom f^* } (here conjugateDomainRadius f).

theorem section13_properConvexFunctionOn_dotProduct {n : ℕ} (a : Fin n → ℝ) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ a)

The EReal-valued affine functional x ↦ ⟪x, a⟫ is proper convex on univ.

theorem section13_fenchelConjugate_sub_dotProduct {n : ℕ} (f : (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) : have g := fun (x : Fin n → ℝ) => f x - ↑(x ⬝ᵥ xStar); fenchelConjugate n g = fun (yStar : Fin n → ℝ) => fenchelConjugate n f (yStar + xStar)

Theorem 12.3 specialization: conjugating x ↦ f x - ⟪x, xStar⟫ translates the conjugate.

theorem section13_effectiveDomain_fenchelConjugate_sub_dotProduct {n : ℕ} (f : (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) : have domFstar := effectiveDomain Set.univ (fenchelConjugate n f); have g := fun (x : Fin n → ℝ) => f x - ↑(x ⬝ᵥ xStar); effectiveDomain Set.univ (fenchelConjugate n g) = domFstar - {xStar}

The effective domain of (f - ⟪·, xStar⟫)^* is the translate dom f^* - xStar.

theorem section13_translate_mem_closure_iff {n : ℕ} (S : Set (Fin n → ℝ)) (a : Fin n → ℝ) : a ∈ closure S ↔ 0 ∈ closure (S - {a})

Translating a set preserves membership in closure (specialized to translation by -a).

theorem section13_translate_mem_interior_iff {n : ℕ} (S : Set (Fin n → ℝ)) (a : Fin n → ℝ) : a ∈ interior S ↔ 0 ∈ interior (S - {a})

Translating a set preserves membership in interior (specialized to translation by -a).

theorem section13_translate_mem_intrinsicInterior_iff {n : ℕ} (S : Set (Fin n → ℝ)) (a : Fin n → ℝ) : a ∈ intrinsicInterior ℝ S ↔ 0 ∈ intrinsicInterior ℝ (S - {a})

Translating a set preserves membership in intrinsicInterior.

theorem section13_translate_mem_affineSpan_iff {n : ℕ} (S : Set (Fin n → ℝ)) (a : Fin n → ℝ) : a ∈ ↑(affineSpan ℝ S) ↔ 0 ∈ ↑(affineSpan ℝ (S - {a}))

Translating a set preserves membership in its affineSpan.

theorem section13_translate_mem_closure_ri_interior_affineSpan_iff_zero {n : ℕ} (S : Set (Fin n → ℝ)) (a : Fin n → ℝ) : (a ∈ closure S ↔ 0 ∈ closure (S - {a})) ∧ (a ∈ intrinsicInterior ℝ S ↔ 0 ∈ intrinsicInterior ℝ (S - {a})) ∧ (a ∈ interior S ↔ 0 ∈ interior (S - {a})) ∧ (a ∈ ↑(affineSpan ℝ S) ↔ 0 ∈ ↑(affineSpan ℝ (S - {a})))

Translation invariance of closure, intrinsic interior, interior and affine span at the origin.

theorem section13_zero_mem_closure_iff_forall_zero_le_supportFunctionEReal {n : ℕ} (C : Set (Fin n → ℝ)) (hCconv : Convex ℝ C) (hCne : C.Nonempty) : 0 ∈ closure C ↔ ∀ (y : Fin n → ℝ), 0 ≤ supportFunctionEReal C y

Support-function characterization of (0 : ℝ^n) ∈ cl C for convex nonempty C.

theorem section13_zero_mem_interior_iff_forall_supportFunctionEReal_pos {n : ℕ} (C : Set (Fin n → ℝ)) (hCconv : Convex ℝ C) (hCne : C.Nonempty) : 0 ∈ interior C ↔ ∀ (y : Fin n → ℝ), y ≠ 0 → supportFunctionEReal C y > 0

Support-function characterization of (0 : ℝ^n) ∈ int C for convex nonempty C.