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.

References #

https://en.wikipedia.org/wiki/Ordered_module

Tags #

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

source

ink

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

Prop

Scalar multiplication by positive elements preserves the order.
smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, a < b → 0 < c → c • a < c • b
If c • a < c • b for some positive c, then a < b.
lt_of_smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, c • a < c • b → 0 < c → a < b

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.

Instances

source

ink

instance OrderDual.instSMulWithZeroOrderDualInstZeroOrderDualToZero {R : Type u_1} {M : Type u_2} [inst : Zero R] [inst : AddZeroClass M] [inst : SMulWithZero R M] :

SMulWithZero R Mᵒᵈ

Equations

OrderDual.instSMulWithZeroOrderDualInstZeroOrderDualToZero = let src := instSMulOrderDual; SMulWithZero.mk (_ : ∀ (m : Mᵒᵈ), 0 • m = 0)

source

ink

instance OrderDual.instMulActionOrderDual {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst : MulAction R M] :

MulAction R Mᵒᵈ

Equations

OrderDual.instMulActionOrderDual = let src := instSMulOrderDual; MulAction.mk (_ : ∀ (m : Mᵒᵈ), 1 • m = m) (_ : ∀ (r y : R) (b : Mᵒᵈ), (r * y) • b = r • y • b)

source

ink

instance OrderDual.instMulActionWithZeroOrderDualInstZeroOrderDualToZero {R : Type u_1} {M : Type u_2} [inst : MonoidWithZero R] [inst : AddMonoid M] [inst : MulActionWithZero R M] :

MulActionWithZero R Mᵒᵈ

Equations

One or more equations did not get rendered due to their size.

source

ink

instance OrderDual.instDistribMulActionOrderDualToMonoidInstAddMonoidOrderDual {R : Type u_1} {M : Type u_2} [inst : MonoidWithZero R] [inst : AddMonoid M] [inst : DistribMulAction R M] :

DistribMulAction R Mᵒᵈ

Equations

OrderDual.instDistribMulActionOrderDualToMonoidInstAddMonoidOrderDual = DistribMulAction.mk (_ : ∀ (r : R), r • 0 = 0) (_ : ∀ (x : R) (a y : Mᵒᵈ), x • (a + y) = x • a + x • y)

source

ink

instance OrderDual.instOrderedSMulOrderDualOrderedAddCommMonoidInstSMulWithZeroOrderDualInstZeroOrderDualToZeroToZeroToMonoidWithZeroToSemiringToAddZeroClassToAddMonoidToAddCommMonoid {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] :

OrderedSMul R Mᵒᵈ

Equations

One or more equations did not get rendered due to their size.

source

ink

theorem smul_lt_smul_of_pos {R : Type u_2} {M : Type u_1} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {b : M} {c : R} :

a < b → 0 < c → c • a < c • b

source

ink

theorem smul_le_smul_of_nonneg {R : Type u_2} {M : Type u_1} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {b : M} {c : R} (h₁ : a ≤ b) (h₂ : 0 ≤ c) :

c • a ≤ c • b

source

ink

theorem smul_nonneg {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {c : R} (hc : 0 ≤ c) (ha : 0 ≤ a) :

0 ≤ c • a

source

ink

theorem smul_nonpos_of_nonneg_of_nonpos {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {c : R} (hc : 0 ≤ c) (ha : a ≤ 0) :

c • a ≤ 0

source

ink

theorem eq_of_smul_eq_smul_of_pos_of_le {R : Type u_2} {M : Type u_1} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {b : M} {c : R} (h₁ : c • a = c • b) (hc : 0 < c) (hle : a ≤ b) :

a = b

source

ink

theorem lt_of_smul_lt_smul_of_nonneg {R : Type u_2} {M : Type u_1} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {b : M} {c : R} (h : c • a < c • b) (hc : 0 ≤ c) :

a < b

source

ink

theorem smul_lt_smul_iff_of_pos {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {b : M} {c : R} (hc : 0 < c) :

c • a < c • b ↔ a < b

source

ink

theorem smul_pos_iff_of_pos {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {c : R} (hc : 0 < c) :

0 < c • a ↔ 0 < a

source

ink

theorem smul_pos {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {a : M} {c : R} (hc : 0 < c) :

0 < a → 0 < c • a

Alias of the reverse direction of smul_pos_iff_of_pos.

source

ink

theorem monotone_smul_left {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {c : R} (hc : 0 ≤ c) :

Monotone (SMul.smul c)

source

ink

theorem strictMono_smul_left {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {c : R} (hc : 0 < c) :

StrictMono (SMul.smul c)

source

ink

theorem smul_lowerBounds_subset_lowerBounds_smul {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {s : Set M} {c : R} (hc : 0 ≤ c) :

c • lowerBounds s ⊆ lowerBounds (c • s)

source

ink

theorem smul_upperBounds_subset_upperBounds_smul {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {s : Set M} {c : R} (hc : 0 ≤ c) :

c • upperBounds s ⊆ upperBounds (c • s)

source

ink

theorem BddBelow.smul_of_nonneg {R : Type u_2} {M : Type u_1} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {s : Set M} {c : R} (hs : BddBelow s) (hc : 0 ≤ c) :

BddBelow (c • s)

source

ink

theorem BddAbove.smul_of_nonneg {R : Type u_2} {M : Type u_1} [inst : OrderedSemiring R] [inst : OrderedAddCommMonoid M] [inst : SMulWithZero R M] [inst : OrderedSMul R M] {s : Set M} {c : R} (hs : BddAbove s) (hc : 0 ≤ c) :

BddAbove (c • s)

source

ink

theorem OrderedSMul.mk'' {𝕜 : Type u_1} {M : Type u_2} [inst : OrderedSemiring 𝕜] [inst : LinearOrderedAddCommMonoid M] [inst : SMulWithZero 𝕜 M] (h : ∀ ⦃c : 𝕜⦄, 0 < c → StrictMono fun a => 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.

source

ink

instance Nat.orderedSMul {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] :

OrderedSMul ℕ M

Equations

@Nat.orderedSMul = @Nat.orderedSMul.proof_1

source

ink

instance Int.orderedSMul {M : Type u_1} [inst : LinearOrderedAddCommGroup M] :

OrderedSMul ℤ M

Equations

@Int.orderedSMul = @Int.orderedSMul.proof_1

source

ink

instance LinearOrderedSemiring.toOrderedSMul {R : Type u_1} [inst : LinearOrderedSemiring R] :

OrderedSMul R R

Equations

@LinearOrderedSemiring.toOrderedSMul = @LinearOrderedSemiring.toOrderedSMul.proof_1

source

ink

theorem OrderedSMul.mk' {𝕜 : Type u_2} {M : Type u_1} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : 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.

source

ink

instance instOrderedSMulProdToOrderedSemiringToOrderedCommSemiringToStrictOrderedCommSemiringToLinearOrderedCommSemiringInstOrderedAddCommMonoidSumSmulWithZeroToZeroToMonoidWithZeroToSemiringToZeroToAddMonoidToAddCommMonoidToZeroToAddMonoidToAddCommMonoidToSMulWithZeroToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToSMulWithZero {𝕜 : Type u_1} {M : Type u_2} {N : Type u_3} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : OrderedAddCommMonoid N] [inst : MulActionWithZero 𝕜 M] [inst : MulActionWithZero 𝕜 N] [inst : OrderedSMul 𝕜 M] [inst : OrderedSMul 𝕜 N] :

OrderedSMul 𝕜 (M × N)

Equations

One or more equations did not get rendered due to their size.

source

ink

instance Pi.orderedSMul {ι : Type u_1} {𝕜 : Type u_2} [inst : LinearOrderedSemifield 𝕜] {M : ι → Type u_3} [inst : (i : ι) → OrderedAddCommMonoid (M i)] [inst : (i : ι) → MulActionWithZero 𝕜 (M i)] [inst : ∀ (i : ι), OrderedSMul 𝕜 (M i)] :

OrderedSMul 𝕜 ((i : ι) → M i)

Equations

@Pi.orderedSMul = @Pi.orderedSMul.proof_1

source

ink

instance Pi.orderedSMul' {ι : Type u_1} {𝕜 : Type u_2} {M : Type u_3} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] :

OrderedSMul 𝕜 (ι → M)

Equations

@Pi.orderedSMul' = @Pi.orderedSMul'.proof_1

source

ink

instance Pi.orderedSMul'' {ι : Type u_1} {𝕜 : Type u_2} [inst : LinearOrderedSemifield 𝕜] :

OrderedSMul 𝕜 (ι → 𝕜)

Equations

@Pi.orderedSMul'' = @Pi.orderedSMul''.proof_1

source

ink

theorem smul_le_smul_iff_of_pos {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {a : M} {b : M} {c : 𝕜} (hc : 0 < c) :

c • a ≤ c • b ↔ a ≤ b

source

ink

theorem inv_smul_le_iff {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {a : M} {b : M} {c : 𝕜} (h : 0 < c) :

c⁻¹ • a ≤ b ↔ a ≤ c • b

source

ink

theorem inv_smul_lt_iff {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {a : M} {b : M} {c : 𝕜} (h : 0 < c) :

c⁻¹ • a < b ↔ a < c • b

source

ink

theorem le_inv_smul_iff {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {a : M} {b : M} {c : 𝕜} (h : 0 < c) :

a ≤ c⁻¹ • b ↔ c • a ≤ b

source

ink

theorem lt_inv_smul_iff {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {a : M} {b : M} {c : 𝕜} (h : 0 < c) :

a < c⁻¹ • b ↔ c • a < b

source

ink

@[simp]

theorem OrderIso.smulLeft_symm_apply {𝕜 : Type u_1} (M : Type u_2) [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {c : 𝕜} (hc : 0 < c) (b : M) :

↑(RelIso.toRelEmbedding (RelIso.symm (OrderIso.smulLeft M hc))).toEmbedding b = c⁻¹ • b

source

ink

@[simp]

theorem OrderIso.smulLeft_apply {𝕜 : Type u_1} (M : Type u_2) [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {c : 𝕜} (hc : 0 < c) (b : M) :

↑(RelIso.toRelEmbedding (OrderIso.smulLeft M hc)).toEmbedding b = c • b

source

ink

def OrderIso.smulLeft {𝕜 : Type u_1} (M : Type u_2) [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {c : 𝕜} (hc : 0 < c) :

M ≃o M

Left scalar multiplication as an order isomorphism.

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem lowerBounds_smul_of_pos {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {s : Set M} {c : 𝕜} (hc : 0 < c) :

lowerBounds (c • s) = c • lowerBounds s

source

ink

@[simp]

theorem upperBounds_smul_of_pos {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {s : Set M} {c : 𝕜} (hc : 0 < c) :

upperBounds (c • s) = c • upperBounds s

source

ink

@[simp]

theorem bddBelow_smul_iff_of_pos {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {s : Set M} {c : 𝕜} (hc : 0 < c) :

BddBelow (c • s) ↔ BddBelow s

source

ink

@[simp]

theorem bddAbove_smul_iff_of_pos {𝕜 : Type u_1} {M : Type u_2} [inst : LinearOrderedSemifield 𝕜] [inst : OrderedAddCommMonoid M] [inst : MulActionWithZero 𝕜 M] [inst : OrderedSMul 𝕜 M] {s : Set M} {c : 𝕜} (hc : 0 < c) :

BddAbove (c • s) ↔ BddAbove s