# 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 #

• define positive convex bodies, requiring the interior to be nonempty
• introduce support sets
• Characterise the interaction of the distance with algebraic operations, eg dist (a • K) (a • L) = ‖a‖ * dist K L, dist (a +ᵥ K) (a +ᵥ L) = dist K L

## Tags #

convex, convex body

structure ConvexBody (V : Type u_2) [] [] [] :
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

Instances For
theorem ConvexBody.convex' {V : Type u_2} [] [] [] (self : ) :
Convex self.carrier

A convex body has convex carrier set

theorem ConvexBody.isCompact' {V : Type u_2} [] [] [] (self : ) :
IsCompact self.carrier

A convex body has compact carrier set

theorem ConvexBody.nonempty' {V : Type u_2} [] [] [] (self : ) :
self.carrier.Nonempty

A convex body has non-empty carrier set

instance ConvexBody.instSetLike {V : Type u_1} [] [] [] :
SetLike () V
Equations
• ConvexBody.instSetLike = { coe := ConvexBody.carrier, coe_injective' := }
theorem ConvexBody.convex {V : Type u_1} [] [] [] (K : ) :
Convex K
theorem ConvexBody.isCompact {V : Type u_1} [] [] [] (K : ) :
theorem ConvexBody.isClosed {V : Type u_1} [] [] [] [] (K : ) :
theorem ConvexBody.nonempty {V : Type u_1} [] [] [] (K : ) :
(K).Nonempty
theorem ConvexBody.ext {V : Type u_1} [] [] [] {K : } {L : } (h : K = L) :
K = L
@[simp]
theorem ConvexBody.coe_mk {V : Type u_1} [] [] [] (s : Set V) (h₁ : ) (h₂ : ) (h₃ : s.Nonempty) :
{ carrier := s, convex' := h₁, isCompact' := h₂, nonempty' := h₃ } = s
theorem ConvexBody.zero_mem_of_symmetric {V : Type u_1} [] [] [] (K : ) (h_symm : xK, -x K) :
0 K

A convex body that is symmetric contains 0.

instance ConvexBody.instAdd {V : Type u_1} [] [] [] [] :
Equations
• ConvexBody.instAdd = { add := fun (K L : ) => { carrier := K + L, convex' := , isCompact' := , nonempty' := } }
instance ConvexBody.instZero {V : Type u_1} [] [] [] :
Zero ()
Equations
• ConvexBody.instZero = { zero := { carrier := 0, convex' := , isCompact' := , nonempty' := } }
instance ConvexBody.instSMulNat {V : Type u_1} [] [] [] [] :
Equations
• ConvexBody.instSMulNat = { smul := nsmulRec }
theorem ConvexBody.coe_nsmul {V : Type u_1} [] [] [] [] (n : ) (K : ) :
(n K) = n K
instance ConvexBody.instAddMonoid {V : Type u_1} [] [] [] [] :
Equations
@[simp]
theorem ConvexBody.coe_add {V : Type u_1} [] [] [] [] (K : ) (L : ) :
(K + L) = K + L
@[simp]
theorem ConvexBody.coe_zero {V : Type u_1} [] [] [] :
0 = 0
instance ConvexBody.instInhabited {V : Type u_1} [] [] [] :
Equations
• ConvexBody.instInhabited = { default := 0 }
instance ConvexBody.instAddCommMonoid {V : Type u_1} [] [] [] [] :
Equations
instance ConvexBody.instSMulReal {V : Type u_1} [] [] [] [] :
Equations
• ConvexBody.instSMulReal = { smul := fun (c : ) (K : ) => { carrier := c K, convex' := , isCompact' := , nonempty' := } }
@[simp]
theorem ConvexBody.coe_smul {V : Type u_1} [] [] [] [] (c : ) (K : ) :
(c K) = c K
instance ConvexBody.instDistribMulActionReal {V : Type u_1} [] [] [] [] [] :
Equations
@[simp]
theorem ConvexBody.coe_smul' {V : Type u_1} [] [] [] [] [] (c : NNReal) (K : ) :
(c K) = c K
instance ConvexBody.instModuleNNReal {V : Type u_1} [] [] [] [] [] :

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

Equations
• ConvexBody.instModuleNNReal =
theorem ConvexBody.smul_le_of_le {V : Type u_1} [] [] [] [] [] (K : ) (h_zero : 0 K) {a : NNReal} {b : NNReal} (h : a b) :
a K b K
theorem ConvexBody.isBounded {V : Type u_1} [] (K : ) :
theorem ConvexBody.hausdorffEdist_ne_top {V : Type u_1} [] {K : } {L : } :
noncomputable instance ConvexBody.instPseudoMetricSpace {V : Type u_1} [] :

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.
@[simp]
theorem ConvexBody.hausdorffDist_coe {V : Type u_1} [] (K : ) (L : ) :
= dist K L
@[simp]
theorem ConvexBody.hausdorffEdist_coe {V : Type u_1} [] (K : ) (L : ) :
= edist K L
theorem ConvexBody.iInter_smul_eq_self {V : Type u_1} [] [] {u : } (K : ) (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.

noncomputable instance ConvexBody.instMetricSpace {V : Type u_1} [] :

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

Equations
• ConvexBody.instMetricSpace =