Eponyms

Named theorems of convex analysis, under the names people search for. Every declaration here is an alias: the library's primary names are descriptive (biconj_eq_clFn, convexHull_extremePoints), which is right for a library organised by subject but is not what a reader looks up first. Where the eponym is already the primary name — fenchel_duality, farkas, helly_finite — no alias appears.

perspective aliases a definition rather than a theorem: smulRight f a is Rockafellar's fa, the perspective function under its other name.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.

theorem Tdaf.ConvexAnalysis.fenchel_moreau {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {f : E → EReal} (hf : ConvexFn f) : biconj B f = clFn f

Fenchel–Moreau: a convex function's biconjugate is its closure.

theorem Tdaf.ConvexAnalysis.fenchel_inequality {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hp : Proper f) (x : E) (y : F) : ↑((B x) y) ≤ f x + conj B f y

Fenchel's inequality: ⟨x, y⟩ ≤ f x + f* y, for proper f.

theorem Tdaf.ConvexAnalysis.jensen {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {ι : Type u_2} (hf : ConvexFn f) (t : Finset ι) (u : ι → E) (m wt : ι → ℝ) (hm : ∀ j ∈ t, f (u j) ≤ ↑(m j)) (hw : ∀ j ∈ t, 0 ≤ wt j) (hw1 : ∑ j ∈ t, wt j = 1) : f (∑ j ∈ t, wt j • u j) ≤ ↑(∑ j ∈ t, wt j * m j)

Jensen's inequality for a finite convex combination.

theorem Tdaf.ConvexAnalysis.caratheodory {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {S : Set E} {x : E} : x ∈ (convexHull ℝ) S ↔ ∃ (w : Fin (Module.finrank ℝ E + 1) → ℝ) (z : Fin (Module.finrank ℝ E + 1) → E), (∀ (i : Fin (Module.finrank ℝ E + 1)), 0 ≤ w i) ∧ ∑ i : Fin (Module.finrank ℝ E + 1), w i = 1 ∧ (∀ (i : Fin (Module.finrank ℝ E + 1)), z i ∈ S) ∧ ∑ i : Fin (Module.finrank ℝ E + 1), w i • z i = x

Carathéodory's theorem: a point of conv S is a convex combination of at most dim E + 1 points of S.

theorem Tdaf.ConvexAnalysis.krein_milman {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hcomp : IsCompact C) (hconv : Convex ℝ C) : (convexHull ℝ) (Set.extremePoints ℝ C) = C

Krein–Milman, finite-dimensional form: a compact convex set is the convex hull of its extreme points.

theorem Tdaf.ConvexAnalysis.minkowski_weyl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} : PolyhedralCone K ↔ FinitelyGeneratedCone K

Minkowski–Weyl: a convex cone is polyhedral exactly when it is finitely generated.

theorem Tdaf.ConvexAnalysis.moreau_decomposition {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsContinuousInnerPairing B] [IsCompatiblePairing B] {f : E → EReal} (hf : ClosedProperConvexFn f) (z : E) : infConv f (quadFn B) z + infConv (conj B f) (quadFn B) z = quadFn B z

Moreau's decomposition: (f □ q) z + (f* □ q) z = q z, where q z = ½ B z z.

theorem Tdaf.ConvexAnalysis.subgradient_maximalMonotone {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {B : E →ₗ[ℝ] E →ₗ[ℝ] ℝ} [IsContinuousInnerPairing B] [IsCompatiblePairing B] {f : E → EReal} (hf : ClosedProperConvexFn f) : IsMaximalMonotoneRel B (subgradientRel B f)

Maximal monotonicity of the subdifferential of a closed proper convex function.

def Tdaf.ConvexAnalysis.perspective {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) (a : ℝ) : E → EReal

The perspective of a convex function, (f a) x = a · f (x / a) for a > 0, defined through the epigraph so that the a = 0 and improper cases come out right. Rockafellar's fa.

Equations

• @Tdaf.ConvexAnalysis.perspective = @Tdaf.ConvexAnalysis.smulRight