mathlib3 documentation

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 #

Tags #

convex, convex body

source
structure convex_body (V : Type u_2) [topological_space V] [add_comm_monoid V] [has_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.

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

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

Equations
source
@[protected]
theorem convex_body.bounded {V : Type u_1} [seminormed_add_comm_group V] [normed_space ℝ V] (K : convex_body V) :
metric.bounded ↑K
source
theorem convex_body.Hausdorff_edist_ne_top {V : Type u_1} [seminormed_add_comm_group V] [normed_space ℝ V] {K L : convex_body V} :
emetric.Hausdorff_edist ↑K ↑L ≠ ⊤
source
@[protected, instance]
noncomputable def convex_body.pseudo_metric_space {V : Type u_1} [seminormed_add_comm_group V] [normed_space ℝ V] :
pseudo_metric_space (convex_body V)

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

Equations
source
@[simp, norm_cast]
theorem convex_body.Hausdorff_dist_coe {V : Type u_1} [seminormed_add_comm_group V] [normed_space ℝ V] (K L : convex_body V) :
metric.Hausdorff_dist ↑K ↑L = has_dist.dist K L
source
@[simp, norm_cast]
theorem convex_body.Hausdorff_edist_coe {V : Type u_1} [seminormed_add_comm_group V] [normed_space ℝ V] (K L : convex_body V) :
emetric.Hausdorff_edist ↑K ↑L = has_edist.edist K L
source
@[protected, instance]
noncomputable def convex_body.metric_space {V : Type u_1} [normed_add_comm_group V] [normed_space ℝ V] :
metric_space (convex_body V)

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

Equations