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

References

• https://en.wikipedia.org/wiki/Ordered_vector_space

Tags

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

class OrderedSMul (R : Type u_1) (M : Type u_2) [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M] : Prop

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 < b → 0 < c → c • 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 • b → 0 < c → a < b

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

theorem OrderedSMul.smul_lt_smul_of_pos {R : Type u_1} {M : Type u_2} [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M] [self : OrderedSMul R M] {a : M} {b : M} {c : R} : a < b → 0 < c → c • 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} [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M] [self : OrderedSMul R M] {a : M} {b : M} {c : R} : c • a < c • b → 0 < c → a < b

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

instance OrderedSMul.toPosSMulStrictMono {R : Type u_6} {M : Type u_7} [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M] [OrderedSMul R M] : PosSMulStrictMono R M

Equations

• ⋯ = ⋯

instance OrderedSMul.toPosSMulReflectLT {R : Type u_6} {M : Type u_7} [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M] [OrderedSMul R M] : PosSMulReflectLT R M

Equations

• ⋯ = ⋯

instance OrderDual.instOrderedSMul {R : Type u_6} {M : Type u_7} [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M] [OrderedSMul R M] : OrderedSMul R Mᵒᵈ

Equations

• ⋯ = ⋯

theorem OrderedSMul.mk'' {𝕜 : Type u_5} {M : Type u_7} [OrderedSemiring 𝕜] [LinearOrderedAddCommMonoid M] [SMulWithZero 𝕜 M] (h : ∀ ⦃c : 𝕜⦄, 0 < c → StrictMono fun (a : M) => c • a) : OrderedSMul 𝕜 M

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} [LinearOrderedCancelAddCommMonoid M] : OrderedSMul ℕ M

Equations

• ⋯ = ⋯

instance Int.orderedSMul {M : Type u_7} [LinearOrderedAddCommGroup M] : OrderedSMul ℤ M

Equations

• ⋯ = ⋯

instance LinearOrderedSemiring.toOrderedSMul {R : Type u_6} [LinearOrderedSemiring R] : OrderedSMul R R

Equations

• ⋯ = ⋯

theorem OrderedSMul.mk' {𝕜 : Type u_5} {M : Type u_7} [LinearOrderedSemifield 𝕜] [OrderedAddCommMonoid M] [MulActionWithZero 𝕜 M] (h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b) : OrderedSMul 𝕜 M

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} [LinearOrderedSemifield 𝕜] [OrderedAddCommMonoid M] [OrderedAddCommMonoid N] [MulActionWithZero 𝕜 M] [MulActionWithZero 𝕜 N] [OrderedSMul 𝕜 M] [OrderedSMul 𝕜 N] : OrderedSMul 𝕜 (M × N)

Equations

• ⋯ = ⋯

instance Pi.orderedSMul {ι : Type u_1} {𝕜 : Type u_5} [LinearOrderedSemifield 𝕜] {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} [Semiring α] [Invertible 2] [Lattice β] [AddCommGroup β] [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} [Semiring α] [Invertible 2] [Lattice β] [AddCommGroup β] [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} [DivisionSemiring α] [NeZero 2] [Lattice β] [AddCommGroup β] [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} [DivisionSemiring α] [NeZero 2] [Lattice β] [AddCommGroup β] [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|)