Documentation

Mathlib.Analysis.Convex.Body

Convex bodies #

This file contains the definition of the type ConvexBody V consisting of convex, compact, nonempty subsets of a real topological vector space V.

ConvexBody V is a module over the nonnegative reals (NNReal) and a pseudo-metric space. If V is a normed space, ConvexBody V is a metric space.

TODO #

Tags #

convex, convex body

structure ConvexBody (V : Type u_2) [TopologicalSpace V] [AddCommMonoid V] [SMul V] :
Type u_2

Let V be a real topological vector space. A subset of V is a convex body if and only if it is convex, compact, and nonempty.

  • carrier : Set V

    The carrier set underlying a convex body: the set of points contained in it

  • convex' : Convex self.carrier

    A convex body has convex carrier set

  • isCompact' : IsCompact self.carrier

    A convex body has compact carrier set

  • nonempty' : self.carrier.Nonempty

    A convex body has non-empty carrier set

Equations
theorem ConvexBody.ext {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] {K L : ConvexBody V} (h : K = L) :
K = L
theorem ConvexBody.ext_iff {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] {K L : ConvexBody V} :
K = L K = L
@[simp]
theorem ConvexBody.coe_mk {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] (s : Set V) (h₁ : Convex s) (h₂ : IsCompact s) (h₃ : s.Nonempty) :
{ carrier := s, convex' := h₁, isCompact' := h₂, nonempty' := h₃ } = s
theorem ConvexBody.zero_mem_of_symmetric {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] (K : ConvexBody V) (h_symm : xK, -x K) :
0 K

A convex body that is symmetric contains 0.

Equations
@[simp]
theorem ConvexBody.coe_zero {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] :
0 = 0
Equations
theorem ConvexBody.coe_nsmul {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] [ContinuousAdd V] (n : ) (K : ConvexBody V) :
↑(n K) = n K
@[simp]
theorem ConvexBody.coe_add {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] [ContinuousAdd V] (K L : ConvexBody V) :
↑(K + L) = K + L
Equations
@[simp]
theorem ConvexBody.coe_smul {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] [ContinuousSMul V] (c : ) (K : ConvexBody V) :
↑(c K) = c K
@[simp]
theorem ConvexBody.coe_smul' {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] [ContinuousSMul V] [ContinuousAdd V] (c : NNReal) (K : ConvexBody V) :
↑(c K) = c K

The convex bodies in a fixed space V form a module over the nonnegative reals.

Equations
theorem ConvexBody.smul_le_of_le {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] [ContinuousSMul V] [ContinuousAdd V] (K : ConvexBody V) (h_zero : 0 K) {a b : NNReal} (h : a b) :
a K b K

Convex bodies in a fixed seminormed space V form a pseudo-metric space under the Hausdorff metric.

Equations
  • One or more equations did not get rendered due to their size.
theorem ConvexBody.iInter_smul_eq_self {V : Type u_1} [SeminormedAddCommGroup V] [NormedSpace V] [T2Space V] {u : NNReal} (K : ConvexBody V) (h_zero : 0 K) (hu : Filter.Tendsto u Filter.atTop (nhds 0)) :
⋂ (n : ), (1 + (u n)) K = K

Let K be a convex body that contains 0 and let u n be a sequence of nonnegative real numbers that tends to 0. Then the intersection of the dilated bodies (1 + u n) • K is equal to K.

Convex bodies in a fixed normed space V form a metric space under the Hausdorff metric.

Equations