# Ordered scalar product #

In this file we define

• OrderedSMul R M : an ordered additive commutative monoid M is an OrderedSMul over an OrderedSemiring R if the scalar product respects the order relation on the monoid and on the ring. There is a correspondence between this structure and convex cones, which is proven in Analysis/Convex/Cone.lean.

## Implementation notes #

• We choose to define OrderedSMul as a Prop-valued mixin, so that it can be used for actions, modules, and algebras (the axioms for an "ordered algebra" are exactly that the algebra is ordered as a module).
• To get ordered modules and ordered vector spaces, it suffices to replace the OrderedAddCommMonoid and the OrderedSemiring as desired.

## TODO #

This file is now mostly useless. We should try deleting OrderedSMul

## Tags #

ordered module, ordered scalar, ordered smul, ordered action, ordered vector space

class OrderedSMul (R : Type u_1) (M : Type u_2) [] [] :

The ordered scalar product property is when an ordered additive commutative monoid with a partial order has a scalar multiplication which is compatible with the order.

• smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, a < b0 < cc a < c b

Scalar multiplication by positive elements preserves the order.

• lt_of_smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, c a < c b0 < ca < b

If c • a < c • b for some positive c, then a < b.

Instances
theorem OrderedSMul.smul_lt_smul_of_pos {R : Type u_1} {M : Type u_2} [] [] [self : ] {a : M} {b : M} {c : R} :
a < b0 < cc a < c b

Scalar multiplication by positive elements preserves the order.

theorem OrderedSMul.lt_of_smul_lt_smul_of_pos {R : Type u_1} {M : Type u_2} [] [] [self : ] {a : M} {b : M} {c : R} :
c a < c b0 < ca < b

If c • a < c • b for some positive c, then a < b.

instance OrderedSMul.toPosSMulStrictMono {R : Type u_6} {M : Type u_7} [] [] [] :
Equations
• =
instance OrderedSMul.toPosSMulReflectLT {R : Type u_6} {M : Type u_7} [] [] [] :
Equations
• =
instance OrderDual.instOrderedSMul {R : Type u_6} {M : Type u_7} [] [] [] :
Equations
• =
theorem OrderedSMul.mk'' {𝕜 : Type u_5} {M : Type u_7} [] [] (h : ∀ ⦃c : 𝕜⦄, 0 < cStrictMono fun (a : M) => c a) :

To prove that a linear ordered monoid is an ordered module, it suffices to verify only the first axiom of OrderedSMul.

instance Nat.orderedSMul {M : Type u_7} :
Equations
• =
instance Int.orderedSMul {M : Type u_7} :
Equations
• =
Equations
• =
theorem OrderedSMul.mk' {𝕜 : Type u_5} {M : Type u_7} [] (h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b0 < cc a c b) :

To prove that a vector space over a linear ordered field is ordered, it suffices to verify only the first axiom of OrderedSMul.

instance instOrderedSMulProd {𝕜 : Type u_5} {M : Type u_7} {N : Type u_8} [] [] [] [] :
OrderedSMul 𝕜 (M × N)
Equations
• =
instance Pi.orderedSMul {ι : Type u_1} {𝕜 : Type u_5} {M : ιType u_9} [(i : ι) → OrderedAddCommMonoid (M i)] [(i : ι) → MulActionWithZero 𝕜 (M i)] [∀ (i : ι), OrderedSMul 𝕜 (M i)] :
OrderedSMul 𝕜 ((i : ι) → M i)
Equations
• =
theorem inf_eq_half_smul_add_sub_abs_sub (α : Type u_9) {β : Type u_10} [] [] [] [] [Module α β] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] (x : β) (y : β) :
x y = 2 (x + y - |y - x|)
theorem sup_eq_half_smul_add_add_abs_sub (α : Type u_9) {β : Type u_10} [] [] [] [] [Module α β] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] (x : β) (y : β) :
x y = 2 (x + y + |y - x|)
theorem inf_eq_half_smul_add_sub_abs_sub' (α : Type u_9) {β : Type u_10} [] [] [] [] [Module α β] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] (x : β) (y : β) :
x y = 2⁻¹ (x + y - |y - x|)
theorem sup_eq_half_smul_add_add_abs_sub' (α : Type u_9) {β : Type u_10} [] [] [] [] [Module α β] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] (x : β) (y : β) :
x y = 2⁻¹ (x + y + |y - x|)