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
• convex' : Convex ℝ self.carrier
• isCompact' : IsCompact self.carrier
• nonempty' : Set.Nonempty self.carrier

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.