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

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

    A convex body has convex carrier set

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

    A convex body has compact carrier set

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

    A convex body has non-empty carrier set

    Equations
    • ConvexBody.instSetLike = { coe := ConvexBody.carrier, coe_injective' := }
    theorem ConvexBody.nonempty {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] (K : ConvexBody V) :
    (↑K).Nonempty
    theorem ConvexBody.ext_iff {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] {K : ConvexBody V} {L : ConvexBody V} :
    K = L K = L
    theorem ConvexBody.ext {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] {K : ConvexBody V} {L : ConvexBody V} (h : 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
    • ConvexBody.instZero = { zero := { carrier := 0, convex' := , isCompact' := , nonempty' := } }
    @[simp]
    theorem ConvexBody.coe_zero {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] :
    0 = 0
    Equations
    • ConvexBody.instInhabited = { default := 0 }
    Equations
    • ConvexBody.instAdd = { add := fun (K L : ConvexBody V) => { carrier := K + L, convex' := , isCompact' := , nonempty' := } }
    Equations
    • ConvexBody.instSMulNat = { smul := nsmulRec }
    theorem ConvexBody.coe_nsmul {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] [ContinuousAdd V] (n : ) (K : ConvexBody V) :
    (n K) = n K
    Equations
    @[simp]
    theorem ConvexBody.coe_add {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module V] [ContinuousAdd V] (K : ConvexBody V) (L : ConvexBody V) :
    (K + L) = K + L
    Equations
    Equations
    • ConvexBody.instSMulReal = { smul := fun (c : ) (K : ConvexBody V) => { carrier := c K, convex' := , isCompact' := , nonempty' := } }
    @[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
    Equations
    @[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 : NNReal} {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