Ordered scalar product #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define
ordered_smul R M: an ordered additive commutative monoidMis anordered_smulover anordered_semiringRif 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 inanalysis/convex/cone.lean.
Implementation notes #
- We choose to define
ordered_smulas aProp-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
order_add_comm_monoidand theordered_semiringas desired.
References #
Tags #
ordered module, ordered scalar, ordered smul, ordered action, ordered vector space
@[class]
structure
ordered_smul
(R : Type u_1)
(M : Type u_2)
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M] :
Prop
- smul_lt_smul_of_pos : ∀ {a b : M} {c : R}, a < b → 0 < c → c • a < c • 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.
@[protected, instance]
def
order_dual.smul_with_zero
{R : Type u_3}
{M : Type u_4}
[has_zero R]
[add_zero_class M]
[h : smul_with_zero R M] :
smul_with_zero R Mᵒᵈ
Equations
- order_dual.smul_with_zero = {to_smul_zero_class := {to_has_smul := {smul := has_smul.smul order_dual.has_smul}, smul_zero := _}, zero_smul := _}
@[protected, instance]
def
order_dual.mul_action
{R : Type u_3}
{M : Type u_4}
[monoid R]
[mul_action R M] :
mul_action R Mᵒᵈ
Equations
- order_dual.mul_action = {to_has_smul := {smul := has_smul.smul order_dual.has_smul}, one_smul := _, mul_smul := _}
@[protected, instance]
def
order_dual.mul_action_with_zero
{R : Type u_3}
{M : Type u_4}
[monoid_with_zero R]
[add_monoid M]
[mul_action_with_zero R M] :
Equations
- order_dual.mul_action_with_zero = {to_mul_action := {to_has_smul := mul_action.to_has_smul order_dual.mul_action, one_smul := _, mul_smul := _}, smul_zero := _, zero_smul := _}
@[protected, instance]
def
order_dual.distrib_mul_action
{R : Type u_3}
{M : Type u_4}
[monoid_with_zero R]
[add_monoid M]
[distrib_mul_action R M] :
Equations
@[protected, instance]
def
order_dual.ordered_smul
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M] :
ordered_smul R Mᵒᵈ
theorem
smul_lt_smul_of_pos
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a b : M}
{c : R} :
theorem
smul_le_smul_of_nonneg
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a b : M}
{c : R}
(h₁ : a ≤ b)
(h₂ : 0 ≤ c) :
theorem
smul_nonneg
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a : M}
{c : R}
(hc : 0 ≤ c)
(ha : 0 ≤ a) :
theorem
smul_nonpos_of_nonneg_of_nonpos
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a : M}
{c : R}
(hc : 0 ≤ c)
(ha : a ≤ 0) :
theorem
eq_of_smul_eq_smul_of_pos_of_le
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a b : M}
{c : R}
(h₁ : c • a = c • b)
(hc : 0 < c)
(hle : a ≤ b) :
a = b
theorem
lt_of_smul_lt_smul_of_nonneg
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a b : M}
{c : R}
(h : c • a < c • b)
(hc : 0 ≤ c) :
a < b
theorem
smul_lt_smul_iff_of_pos
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a b : M}
{c : R}
(hc : 0 < c) :
theorem
smul_pos_iff_of_pos
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a : M}
{c : R}
(hc : 0 < c) :
theorem
smul_pos
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a : M}
{c : R}
(hc : 0 < c) :
Alias of the reverse direction of smul_pos_iff_of_pos.
theorem
monotone_smul_left
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{c : R}
(hc : 0 ≤ c) :
theorem
strict_mono_smul_left
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{c : R}
(hc : 0 < c) :
theorem
smul_lower_bounds_subset_lower_bounds_smul
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{s : set M}
{c : R}
(hc : 0 ≤ c) :
c • lower_bounds s ⊆ lower_bounds (c • s)
theorem
smul_upper_bounds_subset_upper_bounds_smul
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{s : set M}
{c : R}
(hc : 0 ≤ c) :
c • upper_bounds s ⊆ upper_bounds (c • s)
theorem
bdd_below.smul_of_nonneg
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{s : set M}
{c : R}
(hs : bdd_below s)
(hc : 0 ≤ c) :
theorem
bdd_above.smul_of_nonneg
{R : Type u_3}
{M : Type u_4}
[ordered_semiring R]
[ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{s : set M}
{c : R}
(hs : bdd_above s)
(hc : 0 ≤ c) :
theorem
ordered_smul.mk''
{𝕜 : Type u_2}
{M : Type u_4}
[ordered_semiring 𝕜]
[linear_ordered_add_comm_monoid M]
[smul_with_zero 𝕜 M]
(h : ∀ ⦃c : 𝕜⦄, 0 < c → strict_mono (λ (a : M), c • a)) :
ordered_smul 𝕜 M
To prove that a linear ordered monoid is an ordered module, it suffices to verify only the first
axiom of ordered_smul.
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
linear_ordered_semiring.to_ordered_smul
{R : Type u_3}
[linear_ordered_semiring R] :
ordered_smul R R
theorem
smul_max
{R : Type u_3}
{M : Type u_4}
[linear_ordered_semiring R]
[linear_ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a : R}
(ha : 0 ≤ a)
(b₁ b₂ : M) :
a • linear_order.max b₁ b₂ = linear_order.max (a • b₁) (a • b₂)
theorem
smul_min
{R : Type u_3}
{M : Type u_4}
[linear_ordered_semiring R]
[linear_ordered_add_comm_monoid M]
[smul_with_zero R M]
[ordered_smul R M]
{a : R}
(ha : 0 ≤ a)
(b₁ b₂ : M) :
a • linear_order.min b₁ b₂ = linear_order.min (a • b₁) (a • b₂)
theorem
ordered_smul.mk'
{𝕜 : Type u_2}
{M : Type u_4}
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
(h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b) :
ordered_smul 𝕜 M
To prove that a vector space over a linear ordered field is ordered, it suffices to verify only
the first axiom of ordered_smul.
@[protected, instance]
def
prod.ordered_smul
{𝕜 : Type u_2}
{M : Type u_4}
{N : Type u_5}
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[ordered_add_comm_monoid N]
[mul_action_with_zero 𝕜 M]
[mul_action_with_zero 𝕜 N]
[ordered_smul 𝕜 M]
[ordered_smul 𝕜 N] :
ordered_smul 𝕜 (M × N)
@[protected, instance]
def
pi.ordered_smul
{ι : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_semifield 𝕜]
{M : ι → Type u_3}
[Π (i : ι), ordered_add_comm_monoid (M i)]
[Π (i : ι), mul_action_with_zero 𝕜 (M i)]
[∀ (i : ι), ordered_smul 𝕜 (M i)] :
ordered_smul 𝕜 (Π (i : ι), M i)
@[protected, instance]
def
pi.ordered_smul'
{ι : Type u_1}
{𝕜 : Type u_2}
{M : Type u_4}
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
[ordered_smul 𝕜 M] :
ordered_smul 𝕜 (ι → M)
@[protected, instance]
def
pi.ordered_smul''
{ι : Type u_1}
{𝕜 : Type u_2}
[linear_ordered_semifield 𝕜] :
ordered_smul 𝕜 (ι → 𝕜)
theorem
smul_le_smul_iff_of_pos
{𝕜 : Type u_2}
{M : Type u_4}
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
[ordered_smul 𝕜 M]
{a b : M}
{c : 𝕜}
(hc : 0 < c) :
theorem
inv_smul_le_iff
{𝕜 : Type u_2}
{M : Type u_4}
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
[ordered_smul 𝕜 M]
{a b : M}
{c : 𝕜}
(h : 0 < c) :
theorem
inv_smul_lt_iff
{𝕜 : Type u_2}
{M : Type u_4}
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
[ordered_smul 𝕜 M]
{a b : M}
{c : 𝕜}
(h : 0 < c) :
theorem
le_inv_smul_iff
{𝕜 : Type u_2}
{M : Type u_4}
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
[ordered_smul 𝕜 M]
{a b : M}
{c : 𝕜}
(h : 0 < c) :
theorem
lt_inv_smul_iff
{𝕜 : Type u_2}
{M : Type u_4}
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
[ordered_smul 𝕜 M]
{a b : M}
{c : 𝕜}
(h : 0 < c) :
@[simp]
theorem
order_iso.smul_left_apply
{𝕜 : Type u_2}
(M : Type u_4)
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
[ordered_smul 𝕜 M]
{c : 𝕜}
(hc : 0 < c)
(b : M) :
⇑(order_iso.smul_left M hc) b = c • b
def
order_iso.smul_left
{𝕜 : Type u_2}
(M : Type u_4)
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
[ordered_smul 𝕜 M]
{c : 𝕜}
(hc : 0 < c) :
M ≃o M
Left scalar multiplication as an order isomorphism.
@[simp]
theorem
order_iso.smul_left_symm_apply
{𝕜 : Type u_2}
(M : Type u_4)
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
[ordered_smul 𝕜 M]
{c : 𝕜}
(hc : 0 < c)
(b : M) :
⇑(rel_iso.symm (order_iso.smul_left M hc)) b = c⁻¹ • b
@[simp]
theorem
lower_bounds_smul_of_pos
{𝕜 : Type u_2}
{M : Type u_4}
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
[ordered_smul 𝕜 M]
{s : set M}
{c : 𝕜}
(hc : 0 < c) :
lower_bounds (c • s) = c • lower_bounds s
@[simp]
theorem
upper_bounds_smul_of_pos
{𝕜 : Type u_2}
{M : Type u_4}
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
[ordered_smul 𝕜 M]
{s : set M}
{c : 𝕜}
(hc : 0 < c) :
upper_bounds (c • s) = c • upper_bounds s
@[simp]
theorem
bdd_below_smul_iff_of_pos
{𝕜 : Type u_2}
{M : Type u_4}
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
[ordered_smul 𝕜 M]
{s : set M}
{c : 𝕜}
(hc : 0 < c) :
@[simp]
theorem
bdd_above_smul_iff_of_pos
{𝕜 : Type u_2}
{M : Type u_4}
[linear_ordered_semifield 𝕜]
[ordered_add_comm_monoid M]
[mul_action_with_zero 𝕜 M]
[ordered_smul 𝕜 M]
{s : set M}
{c : 𝕜}
(hc : 0 < c) :