Positive & negative parts #
Mathematical structures possessing an absolute value often also possess a unique decomposition of elements into "positive" and "negative" parts which are in some sense "disjoint" (e.g. the Jordan decomposition of a measure).
This file defines posPart
and negPart
, the positive and negative parts of an element in a
lattice ordered group.
Main statements #
posPart_sub_negPart
: Every elementa
can be decomposed intoa⁺ - a⁻
, the difference of its positive and negative parts.posPart_inf_negPart_eq_zero
: The positive and negative parts are coprime.
Notations #
a⁺ᵐ = a ⊔ 1
: Positive component of an elementa
of a multiplicative lattice ordered groupa⁻ᵐ = a⁻¹ ⊔ 1
: Negative component of an elementa
of a multiplicative lattice ordered groupa⁺ = a ⊔ 0
: Positive component of an elementa
of a lattice ordered groupa⁻ = (-a) ⊔ 0
: Negative component of an elementa
of a lattice ordered group
References #
- Birkhoff, Lattice-ordered Groups
- Bourbaki, Algebra II
- Fuchs, Partially Ordered Algebraic Systems
- Zaanen, Lectures on "Riesz Spaces"
- Banasiak, Banach Lattices in Applications
Tags #
positive part, negative part
The positive part of an element a
in a lattice ordered group is a ⊔ 1
, denoted a⁺ᵐ
.
Equations
- «term_⁺ᵐ» = Lean.ParserDescr.trailingNode `term_⁺ᵐ 1024 1024 (Lean.ParserDescr.symbol "⁺ᵐ ")
Instances For
The negative part of an element a
in a lattice ordered group is a⁻¹ ⊔ 1
, denoted a⁻ᵐ
.
Equations
- «term_⁻ᵐ» = Lean.ParserDescr.trailingNode `term_⁻ᵐ 1024 1024 (Lean.ParserDescr.symbol "⁻ᵐ")
Instances For
The positive part of an element a
in a lattice ordered group is a ⊔ 0
, denoted a⁺
.
Equations
- «term_⁺» = Lean.ParserDescr.trailingNode `term_⁺ 1024 1024 (Lean.ParserDescr.symbol "⁺")
Instances For
The negative part of an element a
in a lattice ordered group is (-a) ⊔ 0
, denoted a⁻
.
Equations
- «term_⁻» = Lean.ParserDescr.trailingNode `term_⁻ 1024 1024 (Lean.ParserDescr.symbol "⁻")
Instances For
theorem
posPart_negPart_injective
{α : Type u_1}
[Lattice α]
[AddGroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
:
Function.Injective fun (a : α) => (a⁺, a⁻)
theorem
oneLePart_leOnePart_injective
{α : Type u_1}
[Lattice α]
[Group α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
:
Function.Injective fun (a : α) => (a⁺ᵐ , a⁻ᵐ)
theorem
negPart_anti
{α : Type u_1}
[Lattice α]
[AddGroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
:
Antitone negPart
theorem
leOnePart_anti
{α : Type u_1}
[Lattice α]
[Group α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
:
Antitone leOnePart
theorem
negPart_eq_neg_inf_zero
{α : Type u_1}
[Lattice α]
[AddGroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
leOnePart_eq_inv_inf_one
{α : Type u_1}
[Lattice α]
[Group α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
posPart_add_negPart
{α : Type u_1}
[Lattice α]
[AddGroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
oneLePart_mul_leOnePart
{α : Type u_1}
[Lattice α]
[Group α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
negPart_add_posPart
{α : Type u_1}
[Lattice α]
[AddGroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
leOnePart_mul_oneLePart
{α : Type u_1}
[Lattice α]
[Group α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
posPart_inf_negPart_eq_zero
{α : Type u_1}
[Lattice α]
[AddGroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
oneLePart_inf_leOnePart_eq_one
{α : Type u_1}
[Lattice α]
[Group α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
sup_eq_add_posPart_sub
{α : Type u_1}
[Lattice α]
[AddCommGroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
(b : α)
:
theorem
inf_eq_sub_posPart_sub
{α : Type u_1}
[Lattice α]
[AddCommGroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
(b : α)
:
theorem
abs_add_eq_two_nsmul_posPart
{α : Type u_1}
[Lattice α]
[AddCommGroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
add_abs_eq_two_nsmul_posPart
{α : Type u_1}
[Lattice α]
[AddCommGroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
abs_sub_eq_two_nsmul_negPart
{α : Type u_1}
[Lattice α]
[AddCommGroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
sub_abs_eq_neg_two_nsmul_negPart
{α : Type u_1}
[Lattice α]
[AddCommGroup α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
@[simp]
@[simp]
theorem
posPart_eq_of_posPart_pos
{α : Type u_1}
[LinearOrder α]
[AddGroup α]
{a : α}
(ha : 0 < a⁺)
:
theorem
oneLePart_of_one_lt_oneLePart
{α : Type u_1}
[LinearOrder α]
[Group α]
{a : α}
(ha : 1 < a⁺ᵐ)
:
theorem
negPart_eq_ite
{α : Type u_1}
[LinearOrder α]
[AddGroup α]
{a : α}
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
:
theorem
leOnePart_eq_ite
{α : Type u_1}
[LinearOrder α]
[Group α]
{a : α}
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
:
@[simp]
theorem
negPart_pos_iff
{α : Type u_1}
[LinearOrder α]
[AddGroup α]
{a : α}
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
:
@[simp]
theorem
one_lt_ltOnePart_iff
{α : Type u_1}
[LinearOrder α]
[Group α]
{a : α}
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
:
@[simp]
theorem
negPart_lt
{α : Type u_1}
[LinearOrder α]
[AddGroup α]
{a : α}
{b : α}
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
:
@[simp]
theorem
leOnePart_lt
{α : Type u_1}
[LinearOrder α]
[Group α]
{a : α}
{b : α}
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
: