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) [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

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

instance ConvexBody.instSetLike {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] : SetLike (ConvexBody V) V

Equations

• ConvexBody.instSetLike = { coe := ConvexBody.carrier, coe_injective' := ⋯ }

theorem ConvexBody.convex {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] (K : ConvexBody V) : Convex ℝ ↑K

theorem ConvexBody.isCompact {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] (K : ConvexBody V) : IsCompact ↑K

theorem ConvexBody.isClosed {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [T2Space V] (K : ConvexBody V) : IsClosed ↑K

theorem ConvexBody.nonempty {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] (K : ConvexBody V) : (↑K).Nonempty

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 : ∀ x ∈ K, -x ∈ K) : 0 ∈ K

A convex body that is symmetric contains 0.

instance ConvexBody.instAdd {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [ContinuousAdd V] : Add (ConvexBody V)

Equations

• ConvexBody.instAdd = { add := fun (K L : ConvexBody V) => { carrier := ↑K + ↑L, convex' := ⋯, isCompact' := ⋯, nonempty' := ⋯ } }

instance ConvexBody.instZero {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] : Zero (ConvexBody V)

Equations

• ConvexBody.instZero = { zero := { carrier := 0, convex' := ⋯, isCompact' := ⋯, nonempty' := ⋯ } }

instance ConvexBody.instSMulNat {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [ContinuousAdd V] : SMul ℕ (ConvexBody V)

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

instance ConvexBody.instAddMonoid {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [ContinuousAdd V] : AddMonoid (ConvexBody V)

Equations

• ConvexBody.instAddMonoid = Function.Injective.addMonoid SetLike.coe ⋯ ⋯ ⋯ ⋯

@[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

@[simp]

theorem ConvexBody.coe_zero {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] : ↑0 = 0

instance ConvexBody.instInhabited {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] : Inhabited (ConvexBody V)

Equations

• ConvexBody.instInhabited = { default := 0 }

instance ConvexBody.instAddCommMonoid {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [ContinuousAdd V] : AddCommMonoid (ConvexBody V)

Equations

• ConvexBody.instAddCommMonoid = Function.Injective.addCommMonoid SetLike.coe ⋯ ⋯ ⋯ ⋯

instance ConvexBody.instSMulReal {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [ContinuousSMul ℝ V] : SMul ℝ (ConvexBody V)

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

instance ConvexBody.instDistribMulActionReal {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [ContinuousSMul ℝ V] [ContinuousAdd V] : DistribMulAction ℝ (ConvexBody V)

Equations

• ConvexBody.instDistribMulActionReal = Function.Injective.distribMulAction { toFun := SetLike.coe, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[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

instance ConvexBody.instModuleNNReal {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [ContinuousSMul ℝ V] [ContinuousAdd V] : Module NNReal (ConvexBody V)

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

Equations

• ConvexBody.instModuleNNReal = Module.mk ⋯ ⋯

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

theorem ConvexBody.isBounded {V : Type u_1} [SeminormedAddCommGroup V] [NormedSpace ℝ V] (K : ConvexBody V) : Bornology.IsBounded ↑K

theorem ConvexBody.hausdorffEdist_ne_top {V : Type u_1} [SeminormedAddCommGroup V] [NormedSpace ℝ V] {K : ConvexBody V} {L : ConvexBody V} : EMetric.hausdorffEdist ↑K ↑L ≠ ⊤

noncomputable instance ConvexBody.instPseudoMetricSpace {V : Type u_1} [SeminormedAddCommGroup V] [NormedSpace ℝ V] : PseudoMetricSpace (ConvexBody V)

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} [SeminormedAddCommGroup V] [NormedSpace ℝ V] (K : ConvexBody V) (L : ConvexBody V) : Metric.hausdorffDist ↑K ↑L = dist K L

@[simp]

theorem ConvexBody.hausdorffEdist_coe {V : Type u_1} [SeminormedAddCommGroup V] [NormedSpace ℝ V] (K : ConvexBody V) (L : ConvexBody V) : EMetric.hausdorffEdist ↑K ↑L = edist K L

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.

noncomputable instance ConvexBody.instMetricSpace {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : MetricSpace (ConvexBody V)

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

Equations

• ConvexBody.instMetricSpace = MetricSpace.mk ⋯