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
- carrier : Set V
- 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.
Instances For
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)
:
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)
:
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)
:
@[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]
:
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)
:
instance
ConvexBody.instDistribMulActionRealConvexBodyToAddCommMonoidToSMulToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassInstZeroRealToSMulWithZeroInstMonoidWithZeroRealToMulActionWithZeroSemiringInstMonoidRealInstAddMonoidConvexBodyToAddCommMonoidToSMulRealToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassInstZeroRealToSMulWithZeroInstMonoidWithZeroRealToMulActionWithZeroSemiring
{V : Type u_1}
[TopologicalSpace V]
[AddCommGroup V]
[Module ℝ V]
[ContinuousSMul ℝ V]
[ContinuousAdd 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)
:
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)
:
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]
:
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]
:
Convex bodies in a fixed normed space V
form a metric space under the Hausdorff metric.