Pointed cones

A pointed cone is defined to be a submodule of a module where the scalars are restricted to be nonnegative. This is equivalent to saying that as a set a pointed cone is convex cone which contains 0. This is a bundled version of ConvexCone.Pointed. We choose the submodule definition as it allows us to use the Module API to work with convex cones.

@[reducible, inline]

abbrev PointedCone (𝕜 : Type u_5) (E : Type u_6) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : Type u_6

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

Equations

• PointedCone 𝕜 E = Submodule { c : 𝕜 // 0 ≤ c } E

def PointedCone.toConvexCone {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (S : PointedCone 𝕜 E) : ConvexCone 𝕜 E

Every pointed cone is a convex cone.

Equations

• ↑S = { carrier := ↑S, smul_mem' := ⋯, add_mem' := ⋯ }

instance PointedCone.instCoeConvexCone {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : Coe (PointedCone 𝕜 E) (ConvexCone 𝕜 E)

Equations

• PointedCone.instCoeConvexCone = { coe := PointedCone.toConvexCone }

theorem PointedCone.toConvexCone_injective {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : Function.Injective PointedCone.toConvexCone

@[simp]

theorem PointedCone.toConvexCone_pointed {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (S : PointedCone 𝕜 E) : (↑S).Pointed

theorem PointedCone.ext {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {S : PointedCone 𝕜 E} {T : PointedCone 𝕜 E} (h : ∀ (x : E), x ∈ S ↔ x ∈ T) : S = T

instance PointedCone.instZero {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (S : PointedCone 𝕜 E) : Zero ↥S

Equations

• S.instZero = { zero := ⟨0, ⋯⟩ }

def ConvexCone.toPointedCone {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {S : ConvexCone 𝕜 E} (hS : S.Pointed) : PointedCone 𝕜 E

The PointedCone constructed from a pointed ConvexCone.

Equations

• ConvexCone.toPointedCone hS = { carrier := ↑S, add_mem' := ⋯, zero_mem' := hS, smul_mem' := ⋯ }

@[simp]

theorem ConvexCone.mem_toPointedCone {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {S : ConvexCone 𝕜 E} (hS : S.Pointed) (x : E) : x ∈ ConvexCone.toPointedCone hS ↔ x ∈ S

@[simp]

theorem ConvexCone.coe_toPointedCone {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {S : ConvexCone 𝕜 E} (hS : S.Pointed) : ↑(ConvexCone.toPointedCone hS) = S

instance PointedCone.canLift {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : CanLift (ConvexCone 𝕜 E) (PointedCone 𝕜 E) PointedCone.toConvexCone ConvexCone.Pointed

Equations

• ⋯ = ⋯

Maps between pointed cones

There is already a definition of maps between submodules, Submodule.map. In our case, these maps are induced from linear maps between the ambient modules that are linear over nonnegative scalars. Such maps are unlikely to be of any use in practice. So, we construct some API to define maps between pointed cones induced from linear maps between the ambient modules that are linear over all scalars.

def PointedCone.map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (f : E →ₗ[𝕜] F) (S : PointedCone 𝕜 E) : PointedCone 𝕜 F

The image of a pointed cone under a 𝕜-linear map is a pointed cone.

Equations

• PointedCone.map f S = Submodule.map (↑{ c : 𝕜 // 0 ≤ c } f) S

@[simp]

theorem PointedCone.toConvexCone_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (S : PointedCone 𝕜 E) (f : E →ₗ[𝕜] F) : ↑(PointedCone.map f S) = ConvexCone.map f ↑S

@[simp]

theorem PointedCone.coe_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (S : PointedCone 𝕜 E) (f : E →ₗ[𝕜] F) : ↑(PointedCone.map f S) = ⇑f '' ↑S

@[simp]

theorem PointedCone.mem_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] {f : E →ₗ[𝕜] F} {S : PointedCone 𝕜 E} {y : F} : y ∈ PointedCone.map f S ↔ ∃ x ∈ S, f x = y

theorem PointedCone.map_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [AddCommMonoid G] [Module 𝕜 G] (g : F →ₗ[𝕜] G) (f : E →ₗ[𝕜] F) (S : PointedCone 𝕜 E) : PointedCone.map g (PointedCone.map f S) = PointedCone.map (g ∘ₗ f) S

@[simp]

theorem PointedCone.map_id {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (S : PointedCone 𝕜 E) : PointedCone.map LinearMap.id S = S

def PointedCone.comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (f : E →ₗ[𝕜] F) (S : PointedCone 𝕜 F) : PointedCone 𝕜 E

The preimage of a convex cone under a 𝕜-linear map is a convex cone.

Equations

• PointedCone.comap f S = Submodule.comap (↑{ c : 𝕜 // 0 ≤ c } f) S

@[simp]

theorem PointedCone.coe_comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (f : E →ₗ[𝕜] F) (S : PointedCone 𝕜 F) : ↑(PointedCone.comap f S) = ⇑f ⁻¹' ↑S

@[simp]

theorem PointedCone.comap_id {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (S : PointedCone 𝕜 E) : PointedCone.comap LinearMap.id S = S

theorem PointedCone.comap_comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [AddCommMonoid G] [Module 𝕜 G] (g : F →ₗ[𝕜] G) (f : E →ₗ[𝕜] F) (S : PointedCone 𝕜 G) : PointedCone.comap f (PointedCone.comap g S) = PointedCone.comap (g ∘ₗ f) S

@[simp]

theorem PointedCone.mem_comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] {f : E →ₗ[𝕜] F} {S : PointedCone 𝕜 F} {x : E} : x ∈ PointedCone.comap f S ↔ f x ∈ S

def PointedCone.positive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] : PointedCone 𝕜 E

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

Equations

• PointedCone.positive 𝕜 E = ConvexCone.toPointedCone ⋯

@[simp]

theorem PointedCone.mem_positive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {x : E} : x ∈ PointedCone.positive 𝕜 E ↔ 0 ≤ x

@[simp]

theorem PointedCone.toConvexCone_positive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] : ↑(PointedCone.positive 𝕜 E) = ConvexCone.positive 𝕜 E

def PointedCone.dual {E : Type u_5} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : PointedCone ℝ E) : PointedCone ℝ E

The inner dual cone of a pointed cone is a pointed cone.

Equations

• S.dual = ConvexCone.toPointedCone ⋯

@[simp]

theorem PointedCone.toConvexCone_dual {E : Type u_5} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : PointedCone ℝ E) : ↑S.dual = (↑S).innerDualCone

@[simp]

theorem PointedCone.mem_dual {E : Type u_5} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S : PointedCone ℝ E} {y : E} : y ∈ S.dual ↔ ∀ ⦃x : E⦄, x ∈ S → 0 ≤ inner x y