Convex geometry

StructureConvex cone#

A convex cone is a subset s of an R-module such that a • x + b • y ∈ s whenever a, b > 0 and x, y ∈ s.

ConvexCone.{u_2, u_4} (R : Type u_2) (M : Type u_4) [Semiring R] [PartialOrder R] [AddCommMonoid M]
  [SMul R M] : Type u_4

Sources

• Mathlib documentation: ConvexCone
• Source of ConvexCone in Mathlib/Geometry/Convex/Cone/Basic.lean
• Mathlib overview: Geometry › Convex geometry

MathlibConvexCone

Uses 1 · Used by 2

Statement usesNatural number

Used byPositive cone · Salient cone

DefinitionSalient cone#

A convex cone is salient if it doesn't include x and -x for any nonzero x.

ConvexCone.Salient.{u_2, u_3} {R : Type u_2} {G : Type u_3} [Semiring R] [PartialOrder R]
  [AddCommGroup G] [SMul R G] (C : ConvexCone R G) : Prop

Sources

• Mathlib documentation: ConvexCone.Salient
• Source of ConvexCone.Salient in Mathlib/Geometry/Convex/Cone/Basic.lean
• Mathlib overview: Geometry › Convex geometry

MathlibConvexCone.Salient

Uses 2

Statement usesConvex cone · Integer

DefinitionPositive cone#

The positive cone is the convex cone formed by the set of nonnegative elements in an ordered module.

ConvexCone.positive.{u_2, u_4} (R : Type u_2) (M : Type u_4) [Semiring R] [PartialOrder R]
  [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [_root_.Module R M] [PosSMulMono R M] :
  ConvexCone R M

Sources

• Mathlib documentation: ConvexCone.positive
• Source of ConvexCone.positive in Mathlib/Geometry/Convex/Cone/Basic.lean
• Mathlib overview: Geometry › Convex geometry

MathlibConvexCone.positive

Uses 2

Statement usesConvex cone · Module

AbbreviationPointed cone#

A pointed cone is a submodule of a module with scalars restricted to being nonnegative.

PointedCone.{u_5, u_6} (R : Type u_5) (E : Type u_6) [Semiring R] [PartialOrder R] [IsOrderedRing R]
  [AddCommMonoid E] [_root_.Module R E] : Type u_6

Sources

• Mathlib documentation: PointedCone
• Source of PointedCone in Mathlib/Geometry/Convex/Cone/Pointed.lean
• Mathlib overview: Geometry › Convex geometry

MathlibPointedCone

Uses 2 · Used by 3

Statement usesModule · Ordered ring

Used byDual cone · Minimal tensor product · M. Riesz extension theorem

DefinitionDual cone#

The dual cone of a set s with respect to a bilinear pairing p is the cone consisting of all points y such that for all points x ∈ s we have 0 ≤ p x y.

PointedCone.dual.{u_1, u_2, u_3} {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsOrderedRing R]
  {M : Type u_2} [AddCommMonoid M] [_root_.Module R M] {N : Type u_3} [AddCommMonoid N]
  [_root_.Module R N] (p : M →ₗ[R] N →ₗ[R] R) (s : Set M) : PointedCone R N

Sources

• Mathlib documentation: PointedCone.dual
• Source of PointedCone.dual in Mathlib/Geometry/Convex/Cone/Dual.lean
• Mathlib overview: Geometry › Convex geometry

MathlibPointedCone.dual

Uses 3 · Used by 1

Statement usesAssociative algebra over a commutative ring · Linear map · Pointed cone

Used byMaximal tensor product

DefinitionMinimal tensor product#

The minimal tensor product of two cones is given by all conical combinations of elementary tensor products x ⊗ₜ y with x ∈ C₁ and y ∈ C₂.

PointedCone.minTensorProduct.{u_1, u_2, u_3} {R : Type u_1} [CommRing R] [LinearOrder R]
  [IsStrictOrderedRing R] {G : Type u_2} [AddCommGroup G] [_root_.Module R G] {H : Type u_3}
  [AddCommGroup H] [_root_.Module R H] (C₁ : PointedCone R G) (C₂ : PointedCone R H) :
  PointedCone R (TensorProduct R G H)

Sources

• Mathlib documentation: PointedCone.minTensorProduct
• Source of PointedCone.minTensorProduct in Mathlib/Geometry/Convex/Cone/TensorProduct.lean
• Mathlib overview: Geometry › Convex geometry

MathlibPointedCone.minTensorProduct

Uses 4 · Used by 1

Statement usesGenerating sets · Integer · Pointed cone · Tensor product

Used byMaximal tensor product

DefinitionMaximal tensor product#

The maximal tensor product of two cones is the dual (pointed cone) of the minimal tensor product of the dual cones.

PointedCone.maxTensorProduct.{u_1, u_2, u_3} {R : Type u_1} [CommRing R] [LinearOrder R]
  [IsStrictOrderedRing R] {G : Type u_2} [AddCommGroup G] [_root_.Module R G] {H : Type u_3}
  [AddCommGroup H] [_root_.Module R H] (C₁ : PointedCone R G) (C₂ : PointedCone R H) :
  PointedCone R (TensorProduct R G H)

Sources

• Mathlib documentation: PointedCone.maxTensorProduct
• Source of PointedCone.maxTensorProduct in Mathlib/Geometry/Convex/Cone/TensorProduct.lean
• Mathlib overview: Geometry › Convex geometry

MathlibPointedCone.maxTensorProduct

Uses 3

Statement usesDual cone · Dual vector space · Minimal tensor product

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.