# mathlib3documentation

analysis.convex.body

# Convex bodies #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

convex_body V is a module over the nonnegative reals (nnreal) and a pseudo-metric space. If V is a normed space, convex_body 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 convex_body (V : Type u_2) [ 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.

Instances for convex_body
@[protected, instance]
def convex_body.set_like {V : Type u_1} [ V] :
V
Equations
@[protected]
theorem convex_body.convex {V : Type u_1} [ V] (K : convex_body V) :
K
@[protected]
theorem convex_body.is_compact {V : Type u_1} [ V] (K : convex_body V) :
@[protected]
theorem convex_body.nonempty {V : Type u_1} [ V] (K : convex_body V) :
@[protected, ext]
theorem convex_body.ext {V : Type u_1} [ V] {K L : convex_body V} (h : K = L) :
K = L
@[simp]
theorem convex_body.coe_mk {V : Type u_1} [ V] (s : set V) (h₁ : s) (h₂ : is_compact s) (h₃ : s.nonempty) :
{carrier := s, convex' := h₁, is_compact' := h₂, nonempty' := h₃} = s
@[protected, instance]
def convex_body.add_monoid {V : Type u_1} [ V]  :
Equations
@[simp]
theorem convex_body.coe_add {V : Type u_1} [ V] (K L : convex_body V) :
(K + L) = K + L
@[simp]
theorem convex_body.coe_zero {V : Type u_1} [ V]  :
0 = 0
@[protected, instance]
def convex_body.inhabited {V : Type u_1} [ V]  :
Equations
@[protected, instance]
def convex_body.add_comm_monoid {V : Type u_1} [ V]  :
Equations
@[protected, instance]
def convex_body.has_smul {V : Type u_1} [ V]  :
Equations
@[simp]
theorem convex_body.coe_smul {V : Type u_1} [ V] (c : ) (K : convex_body V) :
(c K) = c K
@[protected, instance]
def convex_body.distrib_mul_action {V : Type u_1} [ V]  :
Equations
@[simp]
theorem convex_body.coe_smul' {V : Type u_1} [ V] (c : nnreal) (K : convex_body V) :
(c K) = c K
@[protected, instance]
def convex_body.module {V : Type u_1} [ V]  :

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

Equations
@[protected]
theorem convex_body.bounded {V : Type u_1} [ V] (K : convex_body V) :
theorem convex_body.Hausdorff_edist_ne_top {V : Type u_1} [ V] {K L : convex_body V} :
@[protected, instance]
noncomputable def convex_body.pseudo_metric_space {V : Type u_1} [ V] :

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

Equations
@[simp, norm_cast]
theorem convex_body.Hausdorff_dist_coe {V : Type u_1} [ V] (K L : convex_body V) :
@[simp, norm_cast]
theorem convex_body.Hausdorff_edist_coe {V : Type u_1} [ V] (K L : convex_body V) :
@[protected, instance]
noncomputable def convex_body.metric_space {V : Type u_1} [ V] :

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

Equations