Mathlib.Algebra.Order.Module.OrderedSMul

Module docstring

{"# 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 Mathlib/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/Orderedvectorspace

Tags

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

OrderedSMul structure

(R M : Type*) [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M] [SMulWithZero R M]

Full source

/-- 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. Note that this
is different from `IsOrderedSMul`, which uses `≤`, has no semiring assumption, and has no positivity
constraint on the defining conditions.
-/
class OrderedSMul (R M : Type*) [Semiring R] [PartialOrder R]
    [AddCommMonoid M] [PartialOrder M] [SMulWithZero R M] :
  Prop where
  /-- Scalar multiplication by positive elements preserves the order. -/
  protected 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`. -/
  protected lt_of_smul_lt_smul_of_pos : ∀ {a b : M}, ∀ {c : R}, c • a < c • b → 0 < c → a < b

Ordered Scalar Product

Informal description

An ordered scalar product structure on a partially ordered additive commutative monoid $M$ over a partially ordered semiring $R$ with a zero-preserving scalar multiplication, where the scalar multiplication is compatible with the order relations on both $M$ and $R$.

OrderedSMul.toPosSMulStrictMono instance

: PosSMulStrictMono R M

Full source

instance OrderedSMul.toPosSMulStrictMono : PosSMulStrictMono R M where
  elim _a ha _b₁ _b₂ hb := OrderedSMul.smul_lt_smul_of_pos hb ha

Strict Monotonicity of Scalar Multiplication by Positive Elements

Informal description

For any ordered semiring $R$ and ordered additive commutative monoid $M$ with a scalar multiplication operation, if $M$ is an ordered scalar product over $R$, then the scalar multiplication by positive elements of $R$ is strictly monotone on $M$. That is, for any $r \in R$ with $0 < r$ and any $x, y \in M$ with $x < y$, we have $r \cdot x < r \cdot y$.

OrderedSMul.toPosSMulReflectLT instance

: PosSMulReflectLT R M

Full source

instance OrderedSMul.toPosSMulReflectLT : PosSMulReflectLT R M :=
  PosSMulReflectLT.of_pos fun _a ha _b₁ _b₂ h ↦ OrderedSMul.lt_of_smul_lt_smul_of_pos h ha

Reflection of Strict Order under Positive Scalar Multiplication

Informal description

For any ordered semiring $R$ and ordered additive commutative monoid $M$ with a scalar multiplication operation, if $M$ is an ordered scalar product over $R$, then the scalar multiplication by positive elements of $R$ reflects the strict order on $M$. That is, for any $r \in R$ with $0 < r$ and any $x, y \in M$, if $r \cdot x < r \cdot y$, then $x < y$.

OrderDual.instOrderedSMul instance

: OrderedSMul R Mᵒᵈ

Full source

instance OrderDual.instOrderedSMul : OrderedSMul R Mᵒᵈ where
  smul_lt_smul_of_pos := OrderedSMul.smul_lt_smul_of_pos (M := M)
  lt_of_smul_lt_smul_of_pos := OrderedSMul.lt_of_smul_lt_smul_of_pos (M := M)

Order Dual as Ordered Scalar Product

Informal description

For any ordered semiring $R$ and ordered additive commutative monoid $M$, the order dual $M^{\text{op}}$ is also an ordered scalar product over $R$.

OrderedSMul.mk'' theorem

 [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid M] [LinearOrder M] [SMulWithZero 𝕜 M]
  (h : ∀ ⦃c : 𝕜⦄, 0 < c → StrictMono fun a : M => c • a) : OrderedSMul 𝕜 M

Full source

/-- To prove that a linear ordered monoid is an ordered module, it suffices to verify only the first
axiom of `OrderedSMul`. -/
theorem OrderedSMul.mk'' [Semiring 𝕜] [PartialOrder 𝕜]
    [AddCommMonoid M] [LinearOrder M] [SMulWithZero 𝕜 M]
    (h : ∀ ⦃c : 𝕜⦄, 0 < c → StrictMono fun a : M => c • a) : OrderedSMul 𝕜 M :=
  { smul_lt_smul_of_pos := fun hab hc => h hc hab
    lt_of_smul_lt_smul_of_pos := fun hab hc => (h hc).lt_iff_lt.1 hab }

Sufficient Condition for Ordered Scalar Product via Strict Monotonicity

Informal description

Let $\mathbb{k}$ be a partially ordered semiring, $M$ be a linearly ordered additive commutative monoid with a zero-preserving scalar multiplication $\mathbb{k} \times M \to M$. If for every positive element $c \in \mathbb{k}$ the function $a \mapsto c \cdot a$ is strictly monotone on $M$, then $M$ is an ordered scalar product over $\mathbb{k}$.

Nat.orderedSMul instance

[AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] : OrderedSMul ℕ M

Full source

instance Nat.orderedSMul [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] :
    OrderedSMul ℕ M :=
  OrderedSMul.mk'' fun n hn a b hab => by
    cases n with
    | zero => cases hn
    | succ n =>
      induction n with
      | zero => dsimp; rwa [one_nsmul, one_nsmul]
      | succ n ih => simp only [succ_nsmul _ n.succ, _root_.add_lt_add (ih n.succ_pos) hab]

Ordered Scalar Product Structure by Natural Numbers

Informal description

For any linearly ordered additive commutative monoid $M$ that is also an ordered cancel additive monoid, the natural numbers $\mathbb{N}$ form an ordered scalar product structure on $M$. This means that the scalar multiplication by natural numbers preserves the order relation on $M$.

Int.orderedSMul instance

[AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : OrderedSMul ℤ M

Full source

instance Int.orderedSMul [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] :
    OrderedSMul ℤ M :=
  OrderedSMul.mk'' fun n hn => by
    cases n
    · simp only [Int.ofNat_eq_coe, Int.natCast_pos, natCast_zsmul] at hn ⊢
      exact strictMono_smul_left_of_pos hn
    · cases (Int.negSucc_not_pos _).1 hn

Ordered Scalar Product Structure by Integers

Informal description

For any linearly ordered additive commutative group $M$ that is also an ordered additive monoid, the integers $\mathbb{Z}$ form an ordered scalar product structure on $M$. This means that the scalar multiplication by integers preserves the order relation on $M$.

LinearOrderedSemiring.toOrderedSMul instance

: OrderedSMul R R

Full source

instance LinearOrderedSemiring.toOrderedSMul : OrderedSMul R R :=
  OrderedSMul.mk'' fun _ => strictMono_mul_left_of_pos

Linearly Ordered Semiring as Ordered Scalar Product over Itself

Informal description

Every linearly ordered semiring $R$ is an ordered scalar product over itself.

OrderedSMul.mk' theorem

(h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b) : OrderedSMul 𝕜 M

Full source

/-- To prove that a vector space over a linear ordered field is ordered, it suffices to verify only
the first axiom of `OrderedSMul`. -/
theorem OrderedSMul.mk' (h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b) :
    OrderedSMul 𝕜 M := by
  have hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b := by
    refine fun a b c hab hc => (h hab hc).lt_of_ne ?_
    rw [Ne, hc.ne'.isUnit.smul_left_cancel]
    exact hab.ne
  refine ⟨fun {a b c} => hlt' a b c, fun {a b c hab hc} => ?_⟩
  obtain ⟨c, rfl⟩ := hc.ne'.isUnit
  rw [← inv_smul_smul c a, ← inv_smul_smul c b]
  refine hlt' _ _ _ hab (pos_of_mul_pos_right ?_ hc.le)
  simp only [c.mul_inv, zero_lt_one]

Sufficient Condition for Ordered Scalar Product

Informal description

Let $M$ be a partially ordered additive commutative monoid and $\mathbb{K}$ be a partially ordered semiring with a zero-preserving scalar multiplication. If for all $a, b \in M$ and $c \in \mathbb{K}$, the condition $a < b$ and $0 < c$ implies $c \cdot a \leq c \cdot b$, then $M$ is an ordered scalar product over $\mathbb{K}$.

instOrderedSMulProd instance

[OrderedSMul 𝕜 M] [OrderedSMul 𝕜 N] : OrderedSMul 𝕜 (M × N)

Full source

instance [OrderedSMul 𝕜 M] [OrderedSMul 𝕜 N] : OrderedSMul 𝕜 (M × N) :=
  OrderedSMul.mk' fun _ _ _ h hc =>
    ⟨smul_le_smul_of_nonneg_left h.1.1 hc.le, smul_le_smul_of_nonneg_left h.1.2 hc.le⟩

Ordered Scalar Product on Product Spaces

Informal description

For any ordered semiring $\mathbb{K}$ and ordered additive commutative monoids $M$ and $N$ with scalar multiplication, if both $M$ and $N$ are ordered scalar products over $\mathbb{K}$, then the product space $M \times N$ is also an ordered scalar product over $\mathbb{K}$.

Pi.orderedSMul instance

 {M : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, PartialOrder (M i)] [∀ i, MulActionWithZero 𝕜 (M i)]
  [∀ i, OrderedSMul 𝕜 (M i)] : OrderedSMul 𝕜 (∀ i, M i)

Full source

instance Pi.orderedSMul {M : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, PartialOrder (M i)]
    [∀ i, MulActionWithZero 𝕜 (M i)] [∀ i, OrderedSMul 𝕜 (M i)] : OrderedSMul 𝕜 (∀ i, M i) :=
  OrderedSMul.mk' fun _ _ _ h hc i => smul_le_smul_of_nonneg_left (h.le i) hc.le

Ordered Scalar Product on Product Spaces

Informal description

For any family of partially ordered additive commutative monoids $(M_i)_{i \in \iota}$ with zero-preserving scalar multiplication over a partially ordered semiring $\mathbb{K}$, if each $M_i$ is an ordered scalar product over $\mathbb{K}$, then the product space $\prod_{i \in \iota} M_i$ is also an ordered scalar product over $\mathbb{K}$.

inf_eq_half_smul_add_sub_abs_sub theorem

(x y : β) : x ⊓ y = (⅟ 2 : α) • (x + y - |y - x|)

Full source

lemma inf_eq_half_smul_add_sub_abs_sub (x y : β) : x ⊓ y = (⅟2 : α) • (x + y - |y - x|) := by
  rw [← two_nsmul_inf_eq_add_sub_abs_sub x y, two_smul, ← two_smul α,
    smul_smul, invOf_mul_self, one_smul]

Infimum as Half of Sum Minus Absolute Difference

Informal description

For any elements $x$ and $y$ in a partially ordered vector space $\beta$ over a field $\alpha$ with an inverse operation, the infimum $x \sqcap y$ is equal to $\frac{1}{2} \cdot (x + y - |y - x|)$, where $|\cdot|$ denotes the absolute value and $\cdot$ denotes the scalar multiplication.

sup_eq_half_smul_add_add_abs_sub theorem

(x y : β) : x ⊔ y = (⅟ 2 : α) • (x + y + |y - x|)

Full source

lemma sup_eq_half_smul_add_add_abs_sub (x y : β) : x ⊔ y = (⅟2 : α) • (x + y + |y - x|) := by
  rw [← two_nsmul_sup_eq_add_add_abs_sub x y, two_smul, ← two_smul α,
    smul_smul, invOf_mul_self, one_smul]

Supremum as Half-Scaled Sum Plus Absolute Difference

Informal description

Let $\alpha$ be a type with an inverse operation for $2$ (denoted by $⅟ 2$) and $\beta$ be a type with addition, subtraction, and absolute value operations. For any elements $x, y \in \beta$, the supremum $x \sqcup y$ is equal to $(⅟ 2) \cdot (x + y + |y - x|)$.

inf_eq_half_smul_add_sub_abs_sub' theorem

(x y : β) : x ⊓ y = (2⁻¹ : α) • (x + y - |y - x|)

Full source

lemma inf_eq_half_smul_add_sub_abs_sub' (x y : β) : x ⊓ y = (2⁻¹ : α) • (x + y - |y - x|) := by
  letI := invertibleOfNonzero (two_ne_zero' α)
  exact inf_eq_half_smul_add_sub_abs_sub α x y

Infimum Formula via Half-Scaled Sum and Absolute Difference

Informal description

For any elements $x$ and $y$ in a partially ordered vector space $\beta$ over a field $\alpha$ with a multiplicative inverse of 2, the infimum $x \sqcap y$ is equal to $\frac{1}{2} \cdot (x + y - |y - x|)$, where $|\cdot|$ denotes the absolute value and $\cdot$ denotes the scalar multiplication.

sup_eq_half_smul_add_add_abs_sub' theorem

(x y : β) : x ⊔ y = (2⁻¹ : α) • (x + y + |y - x|)

Full source

lemma sup_eq_half_smul_add_add_abs_sub' (x y : β) : x ⊔ y = (2⁻¹ : α) • (x + y + |y - x|) := by
  letI := invertibleOfNonzero (two_ne_zero' α)
  exact sup_eq_half_smul_add_add_abs_sub α x y

Supremum Formula via Scaled Sum and Absolute Difference

Informal description

For any elements $x, y$ in a type $\beta$ with addition, subtraction, and absolute value operations, and given a type $\alpha$ with an inverse operation for $2$ (denoted by $2^{-1}$), the supremum $x \sqcup y$ is equal to $2^{-1} \cdot (x + y + |y - x|)$.