doc-next-gen

Mathlib.Algebra.Order.Nonneg.Field

Module docstring

{"# Semifield structure on the type of nonnegative elements

This file defines instances and prove some properties about the nonnegative elements {x : α // 0 ≤ x} of an arbitrary type α.

This is used to derive algebraic structures on ℝ≥0 and ℚ≥0 automatically.

Main declarations

  • {x : α // 0 ≤ x} is a CanonicallyLinearOrderedSemifield if α is a LinearOrderedField. "}
NNRat.cast_nonneg theorem
(q : ℚ≥0) : 0 ≤ (q : α)
Full source 
lemma NNRat.cast_nonneg (q : ℚ≥0) : 0 ≤ (q : α) := by
  rw [cast_def]; exact div_nonneg q.num.cast_nonneg q.den.cast_nonneg
Nonnegativity of Nonnegative Rational Number Cast in Ordered Semirings
Informal description
For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$ and any ordered semiring $\alpha$, the canonical embedding of $q$ into $\alpha$ is nonnegative, i.e., $0 \leq (q : \alpha)$.
nnqsmul_nonneg theorem
(q : ℚ≥0) (ha : 0 ≤ a) : 0 ≤ q • a
Full source 
lemma nnqsmul_nonneg (q : ℚ≥0) (ha : 0 ≤ a) : 0 ≤ q • a := by
  rw [NNRat.smul_def]; exact mul_nonneg q.cast_nonneg ha
Nonnegativity of Scalar Multiplication by Nonnegative Rational Numbers
Informal description
For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$ and any element $a$ in an ordered semiring $\alpha$ such that $0 \leq a$, the scalar multiplication $q \cdot a$ is nonnegative, i.e., $0 \leq q \cdot a$.
Nonneg.coe_inv theorem
(a : { x : α // 0 ≤ x }) : ((a⁻¹ : { x : α // 0 ≤ x }) : α) = (a : α)⁻¹
Full source 
@[simp, norm_cast]
protected theorem coe_inv (a : { x : α // 0 ≤ x }) : ((a⁻¹ : { x : α // 0 ≤ x }) : α) = (a : α)⁻¹ :=
  rfl
Coercion of Inverse for Nonnegative Elements: $(a^{-1})_{\alpha} = (a_{\alpha})^{-1}$
Informal description
For any nonnegative element $a$ in a type $\alpha$ (i.e., $a \in \{x : \alpha \mid 0 \leq x\}$), the canonical coercion of the inverse of $a$ in the subtype equals the inverse of $a$ in $\alpha$. In other words, if $a \geq 0$, then $(a^{-1})_{\alpha} = (a_{\alpha})^{-1}$.
Nonneg.inv_mk theorem
(hx : 0 ≤ x) : (⟨x, hx⟩ : { x : α // 0 ≤ x })⁻¹ = ⟨x⁻¹, inv_nonneg.2 hx⟩
Full source 
@[simp]
theorem inv_mk (hx : 0 ≤ x) :
    (⟨x, hx⟩ : { x : α // 0 ≤ x })⁻¹ = ⟨x⁻¹, inv_nonneg.2 hx⟩ :=
  rfl
Inverse of Nonnegative Element Construction: $\langle x, hx \rangle^{-1} = \langle x^{-1}, h \rangle$
Informal description
For any element $x$ of a type $\alpha$ with $0 \leq x$, the inverse of the nonnegative element $\langle x, hx \rangle$ (where $hx$ is the proof that $0 \leq x$) is equal to the nonnegative element $\langle x^{-1}, h \rangle$, where $h$ is the proof that $0 \leq x^{-1}$ obtained from the implication $0 \leq x \implies 0 \leq x^{-1}$.
Nonneg.coe_div theorem
(a b : { x : α // 0 ≤ x }) : ((a / b : { x : α // 0 ≤ x }) : α) = a / b
Full source 
@[simp, norm_cast]
protected theorem coe_div (a b : { x : α // 0 ≤ x }) : ((a / b : { x : α // 0 ≤ x }) : α) = a / b :=
  rfl
Canonical Map Preserves Division for Nonnegative Elements
Informal description
For any two nonnegative elements $a$ and $b$ of a type $\alpha$ (i.e., $a, b \in \{x : \alpha \mid 0 \leq x\}$), the canonical map from the nonnegative elements to $\alpha$ preserves division, meaning $(a / b) = a / b$ in $\alpha$.
Nonneg.mk_div_mk theorem
(hx : 0 ≤ x) (hy : 0 ≤ y) : (⟨x, hx⟩ : { x : α // 0 ≤ x }) / ⟨y, hy⟩ = ⟨x / y, div_nonneg hx hy⟩
Full source 
@[simp]
theorem mk_div_mk (hx : 0 ≤ x) (hy : 0 ≤ y) :
    (⟨x, hx⟩ : { x : α // 0 ≤ x }) / ⟨y, hy⟩ = ⟨x / y, div_nonneg hx hy⟩ :=
  rfl
Division of Nonnegative Elements in Subtype Preserves Nonnegativity
Informal description
For any elements $x$ and $y$ in a type $\alpha$ with $0 \leq x$ and $0 \leq y$, the division of the nonnegative elements $\langle x, hx \rangle$ and $\langle y, hy \rangle$ in the subtype $\{x : \alpha \mid 0 \leq x\}$ equals the nonnegative element $\langle x / y, \text{div\_nonneg } hx hy \rangle$, where $\text{div\_nonneg } hx hy$ is the proof that $0 \leq x / y$.
Nonneg.coe_zpow theorem
(a : { x : α // 0 ≤ x }) (n : ℤ) : ((a ^ n : { x : α // 0 ≤ x }) : α) = (a : α) ^ n
Full source 
@[simp, norm_cast]
protected theorem coe_zpow (a : { x : α // 0 ≤ x }) (n : ℤ) :
    ((a ^ n : { x : α // 0 ≤ x }) : α) = (a : α) ^ n :=
  rfl
Coercion of Integer Powers of Nonnegative Elements
Informal description
For any nonnegative element $a$ of a type $\alpha$ (i.e., $a \in \{x : \alpha \mid 0 \leq x\}$) and any integer exponent $n$, the canonical coercion of $a^n$ (computed in the nonnegative subtype) to $\alpha$ equals $a^n$ computed directly in $\alpha$. In other words, $(a^n : \alpha) = (a : \alpha)^n$.
Nonneg.mk_zpow theorem
(hx : 0 ≤ x) (n : ℤ) : (⟨x, hx⟩ : { x : α // 0 ≤ x }) ^ n = ⟨x ^ n, zpow_nonneg hx n⟩
Full source 
@[simp]
theorem mk_zpow (hx : 0 ≤ x) (n : ℤ) :
    (⟨x, hx⟩ : { x : α // 0 ≤ x }) ^ n = ⟨x ^ n, zpow_nonneg hx n⟩ :=
  rfl
Power of Nonnegative Element in Subtype Equals Power in Base Type
Informal description
For any element $x$ of a type $\alpha$ with $0 \leq x$ and any integer $n$, the $n$-th power of the nonnegative element $\langle x, hx \rangle$ (where $hx$ is the proof that $0 \leq x$) in the subtype $\{x : \alpha \mid 0 \leq x\}$ is equal to $\langle x^n, zpow\_nonneg\ hx\ n \rangle$, where $zpow\_nonneg\ hx\ n$ is the proof that $0 \leq x^n$.
Nonneg.instNNRatCast instance
: NNRatCast { x : α // 0 ≤ x }
Full source 
instance instNNRatCast : NNRatCast {x : α // 0 ≤ x} := ⟨fun q ↦ ⟨q, q.cast_nonneg⟩⟩
Canonical Homomorphism from Nonnegative Rationals to Nonnegative Elements
Informal description
For any type $\alpha$ with a nonnegative subset $\{x : \alpha \mid 0 \leq x\}$, there is a canonical homomorphism from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ to this subset. This homomorphism is defined by the natural embedding of $\mathbb{Q}_{\geq 0}$ into $\alpha$ restricted to the nonnegative elements.
Nonneg.coe_nnratCast theorem
(q : ℚ≥0) : (q : { x : α // 0 ≤ x }) = (q : α)
Full source 
@[simp, norm_cast] lemma coe_nnratCast (q : ℚ≥0) : (q : {x : α // 0 ≤ x}) = (q : α) := rfl
Canonical Embedding of Nonnegative Rationals into Nonnegative Elements
Informal description
For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the canonical embedding of $q$ into the nonnegative elements $\{x \in \alpha \mid 0 \leq x\}$ is equal to the canonical embedding of $q$ into $\alpha$.
Nonneg.mk_nnratCast theorem
(q : ℚ≥0) : (⟨q, q.cast_nonneg⟩ : { x : α // 0 ≤ x }) = q
Full source 
@[simp] lemma mk_nnratCast (q : ℚ≥0) : (⟨q, q.cast_nonneg⟩ : {x : α // 0 ≤ x}) = q := rfl
Canonical Embedding of Nonnegative Rationals into Nonnegative Elements Preserves Equality
Informal description
For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the element $\langle q, q.cast\_nonneg \rangle$ in the subtype $\{x : \alpha \mid 0 \leq x\}$ is equal to $q$ under the canonical embedding.
Nonneg.coe_nnqsmul theorem
(q : ℚ≥0) (a : { x : α // 0 ≤ x }) : ↑(q • a) = (q • a : α)
Full source 
@[simp, norm_cast] lemma coe_nnqsmul (q : ℚ≥0) (a : {x : α // 0 ≤ x}) :
    ↑(q • a) = (q • a : α) := rfl
Scalar Multiplication by Nonnegative Rationals Preserves Canonical Embedding
Informal description
For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$ and any nonnegative element $a \in \{x \in \alpha \mid 0 \leq x\}$, the scalar multiplication $q \cdot a$ in the subtype is equal to the scalar multiplication $q \cdot a$ in the original type $\alpha$ when viewed through the canonical embedding.
Nonneg.mk_nnqsmul theorem
(q : ℚ≥0) (a : α) (ha : 0 ≤ a) : (⟨q • a, by rw [NNRat.smul_def]; exact mul_nonneg q.cast_nonneg ha⟩ : { x : α // 0 ≤ x }) = q • a
Full source 
@[simp] lemma mk_nnqsmul (q : ℚ≥0) (a : α) (ha : 0 ≤ a) :
    (⟨q • a, by rw [NNRat.smul_def]; exact mul_nonneg q.cast_nonneg ha⟩ : {x : α // 0 ≤ x}) =
      q • a := rfl
Subtype Scalar Multiplication by Nonnegative Rationals Preserves Equality
Informal description
For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$ and any element $a \in \alpha$ with $0 \leq a$, the scalar multiplication $q \cdot a$ (interpreted in the subtype $\{x \in \alpha \mid 0 \leq x\}$) is equal to the scalar multiplication $q \cdot a$ in $\alpha$.
Nonneg.semifield instance
: Semifield { x : α // 0 ≤ x }
Full source 
instance semifield : Semifield { x : α // 0 ≤ x } := fast_instance%
  Subtype.coe_injective.semifield _ Nonneg.coe_zero Nonneg.coe_one Nonneg.coe_add
    Nonneg.coe_mul Nonneg.coe_inv Nonneg.coe_div (fun _ _ => rfl) coe_nnqsmul Nonneg.coe_pow
    Nonneg.coe_zpow Nonneg.coe_natCast coe_nnratCast
Semifield Structure on Nonnegative Elements of a Linearly Ordered Field
Informal description
For any type $\alpha$ with a linear order and field structure, the set of nonnegative elements $\{x : \alpha \mid 0 \leq x\}$ forms a semifield. This means it is a commutative semiring with multiplicative inverses for all nonzero elements, and the order is compatible with the algebraic operations.
Nonneg.linearOrderedCommGroupWithZero instance
[Field α] [LinearOrder α] [IsStrictOrderedRing α] : LinearOrderedCommGroupWithZero { x : α // 0 ≤ x }
Full source 
instance linearOrderedCommGroupWithZero [Field α] [LinearOrder α] [IsStrictOrderedRing α] :
    LinearOrderedCommGroupWithZero { x : α // 0 ≤ x } :=
  CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero
Nonnegative Elements of a Linearly Ordered Field Form a Linearly Ordered Commutative Group with Zero
Informal description
For any linearly ordered field $\alpha$ that is also a strict ordered ring, the set of nonnegative elements $\{x \in \alpha \mid 0 \leq x\}$ forms a linearly ordered commutative group with zero. This means it is a commutative monoid with zero, equipped with a linear order compatible with the algebraic operations, and every nonzero element has a multiplicative inverse.