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

• carrier : Set V
• convex' : Convex ℝ s.carrier
• isCompact' : IsCompact s.carrier
• nonempty' : Set.Nonempty s.carrier

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.

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

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) : Set.Nonempty ↑K

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₃ : Set.Nonempty s) : ↑{ carrier := s, convex' := h₁, isCompact' := h₂, nonempty' := h₃ } = s

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

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

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

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.instAddMonoidConvexBodyToAddCommMonoidToSMulRealToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassInstZeroRealToSMulWithZeroInstMonoidWithZeroRealToMulActionWithZeroSemiring {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [ContinuousAdd V] : AddMonoid (ConvexBody V)

@[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.instInhabitedConvexBodyToAddCommMonoidToSMulRealToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassInstZeroRealToSMulWithZeroInstMonoidWithZeroRealToMulActionWithZeroSemiring {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] : Inhabited (ConvexBody V)

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

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

@[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.instDistribMulActionRealConvexBodyToAddCommMonoidToSMulToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassInstZeroRealToSMulWithZeroInstMonoidWithZeroRealToMulActionWithZeroSemiringInstMonoidRealInstAddMonoidConvexBodyToAddCommMonoidToSMulRealToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassInstZeroRealToSMulWithZeroInstMonoidWithZeroRealToMulActionWithZeroSemiring {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [ContinuousSMul ℝ V] [ContinuousAdd V] : DistribMulAction ℝ (ConvexBody V)

@[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.instModuleNNRealConvexBodyToAddCommMonoidToSMulRealToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassInstZeroRealToSMulWithZeroInstMonoidWithZeroRealToMulActionWithZeroSemiringInstNNRealSemiringInstAddCommMonoidConvexBodyToAddCommMonoidToSMulRealToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassInstZeroRealToSMulWithZeroInstMonoidWithZeroRealToMulActionWithZeroSemiring {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.

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.instPseudoMetricSpaceConvexBodyToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToSMulRealToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassInstZeroRealToSMulWithZeroInstMonoidWithZeroRealToMulActionWithZeroSemiringToModuleNormedField {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.

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

noncomputable instance ConvexBody.instMetricSpaceConvexBodyToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToAddCommMonoidToAddCommGroupToSMulRealToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassInstZeroRealToSMulWithZeroInstMonoidWithZeroRealToMulActionWithZeroSemiringToModuleNormedField {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.