Convexity

DefinitionConvex function#

Convexity of functions

ConvexOn.{u_1, u_2, u_5} (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [Semiring 𝕜] [PartialOrder 𝕜]
  [AddCommMonoid E] [AddCommMonoid β] [PartialOrder β] [SMul 𝕜 E] [SMul 𝕜 β] (s : Set E)
  (f : E → β) : Prop
Sources
MathlibConvexOn
Uses 1 · Used by 5
Statement usesConvex subsets
Used byBertrand’s Postulate · Characterization of convexity · Jensen's inequality (finite sum version) · Jensen's inequality (integral version) · Continuity (continuity and differentiability of convex functions)

TheoremCharacterization of convexity#

If a function f is continuous on a convex set D ⊆ ℝ, is twice differentiable on its interior, and f'' is nonnegative on the interior, then f is convex on D.

convexOn_of_deriv2_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
  (hf' : DifferentiableOn ℝ f (interior D)) (hf'' : DifferentiableOn ℝ (deriv f) (interior D))
  (hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x) : ConvexOn ℝ D f
Sources
MathlibconvexOn_of_deriv2_nonneg
Uses 4
Statement usesConvex function · Differentials (linear tangent functions) · Holomorphic functions
Proof usesThe Mean Value Theorem (Freek Wiedijk's 100 theorems)

TheoremJensen's inequality (finite sum version)#

Convex Jensen's inequality, Finset.sum version.

ConvexOn.map_sum_le.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} {ι : Type u_4}
  [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [AddCommGroup β]
  [PartialOrder β] [IsOrderedAddMonoid β] [_root_.Module 𝕜 E] [_root_.Module 𝕜 β]
  [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}
  (hf : ConvexOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) :
  f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)
Sources
MathlibConvexOn.map_sum_le
Uses 7 · Used by 1
Statement usesConvex function · Field · Finite set · Module · Rational number
Proof usesCharacteristic zero · Product of vector spaces
Used byArithmetic Mean/Geometric Mean

TheoremJensen's inequality (integral version)#

Jensen's inequality: if a function g : E → ℝ is convex and continuous on a convex closed set s, μ is a probability measure on α, and f : α → E is a function sending μ-a.e. points to s, then the value of g at the expected value of f is less than or equal to the expected value of g ∘ f provided that both f and g ∘ f are integrable. See also ConvexOn.map_centerMass_le for a finite sum version of this lemma.

ConvexOn.map_integral_le.{u_1, u_2} {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α}
  {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hg : ConvexOn ℝ s g)
  (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s)
  (hfi : MeasureTheory.Integrable f μ) (hgi : MeasureTheory.Integrable (g ∘ f) μ) :
  g (∫ (x : α), f x ∂μ) ≤ ∫ (x : α), g (f x) ∂μ
Sources
MathlibConvexOn.map_integral_le
Uses 9
Statement usesBochner integral · Convex function · Inner product space, over \(R\) or \(C\) · Probability measure
Proof usesBorel sigma-algebra · Completeness of R · Measurable function · Order topology · Pointwise convergence

TheoremConvexity inequalities#

In this file we prove several inequalities for finite sums, including AM-GM inequality, HM-GM inequality, Young's inequality, Hölder inequality, and Minkowski inequality. Versions for integrals of some of these inequalities are available in Mathlib/MeasureTheory/Integral/MeanInequalities.lean.

Mathlib covers this with the module Mathlib.Analysis.MeanInequalities rather than a single declaration.

Its 58 documented declarations include Real.geom_mean_le_arith_mean, Real.geom_mean_eq_arith_mean_weighted_iff_of_pos', Real.geom_mean_eq_arith_mean_weighted_iff_of_nonneg', Real.geom_mean_eq_arith_mean_weighted_iff_of_pos, Real.geom_mean_eq_arith_mean_weighted_iff_of_nonneg, Real.geom_mean_lt_arith_mean_weighted_iff_of_pos', Real.geom_mean_lt_arith_mean_weighted_iff_of_nonneg', Real.geom_mean_lt_arith_mean_weighted_iff_of_pos, Real.geom_mean_lt_arith_mean_weighted_iff_of_nonneg, NNReal.geom_mean_le_arith_mean_weighted, NNReal.geom_mean_le_arith_mean2_weighted, ENNReal.geom_mean_le_arith_mean_weighted, and 46 more.

Sources
MathlibReal.geom_mean_le_arith_mean · Real.geom_mean_eq_arith_mean_weighted_iff_of_pos' · Real.geom_mean_eq_arith_mean_weighted_iff_of_nonneg' · Real.geom_mean_eq_arith_mean_weighted_iff_of_pos · Real.geom_mean_eq_arith_mean_weighted_iff_of_nonneg · Real.geom_mean_lt_arith_mean_weighted_iff_of_pos' · Real.geom_mean_lt_arith_mean_weighted_iff_of_nonneg' · Real.geom_mean_lt_arith_mean_weighted_iff_of_pos · Real.geom_mean_lt_arith_mean_weighted_iff_of_nonneg · NNReal.geom_mean_le_arith_mean_weighted · NNReal.geom_mean_le_arith_mean2_weighted · ENNReal.geom_mean_le_arith_mean_weighted

TheoremCarathéodory's theorem#

Carathéodory's convexity theorem

convexHull_eq_union.{u, u_1} {𝕜 : Type u_1} {E : Type u} [Field 𝕜] [LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [AddCommGroup E] [_root_.Module 𝕜 E] {s : Set E} :
  (convexHull 𝕜) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t
Sources
MathlibconvexHull_eq_union
Uses 7
Statement usesAffine space · Convex hull of a subset of an affine real space · Field · Finite set · Linear map · Rational number
Proof usesOrdered ring

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.