# 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 element a can be decomposed into a⁺ - 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 element a of a multiplicative lattice ordered group
• a⁻ᵐ = a⁻¹ ⊔ 1: Negative component of an element a of a multiplicative lattice ordered group
• a⁺ = a ⊔ 0: Positive component of an element a of a lattice ordered group
• a⁻ = (-a) ⊔ 0: Negative component of an element a of a lattice ordered group

## References #

• [Birkhoff, Lattice-ordered Groups][birkhoff1942]
• [Bourbaki, Algebra II][bourbaki1981]
• [Fuchs, Partially Ordered Algebraic Systems][fuchs1963]
• [Zaanen, Lectures on "Riesz Spaces"][zaanen1966]
• [Banasiak, Banach Lattices in Applications][banasiak]

## Tags #

positive part, negative part

def posPart {α : Type u_1} [] [] (a : α) :
α

The positive part of an element a in a lattice ordered group is a ⊔ 0, denoted a⁺.

Equations
Instances For
def oneLePart {α : Type u_1} [] [] (a : α) :
α

The positive part of an element a in a lattice ordered group is a ⊔ 1, denoted a⁺ᵐ.

Equations
Instances For
def negPart {α : Type u_1} [] [] (a : α) :
α

The negative part of an element a in a lattice ordered group is (-a) ⊔ 0, denoted a⁻.

Equations
Instances For
def leOnePart {α : Type u_1} [] [] (a : α) :
α

The negative part of an element a in a lattice ordered group is a⁻¹ ⊔ 1, denoted a⁻ᵐ .

Equations
Instances For

The positive part of an element a in a lattice ordered group is a ⊔ 1, denoted a⁺ᵐ.

Equations
Instances For

The negative part of an element a in a lattice ordered group is a⁻¹ ⊔ 1, denoted a⁻ᵐ .

Equations
Instances For

The positive part of an element a in a lattice ordered group is a ⊔ 0, denoted a⁺.

Equations
Instances For

The negative part of an element a in a lattice ordered group is (-a) ⊔ 0, denoted a⁻.

Equations
Instances For
theorem posPart_mono {α : Type u_1} [] [] :
Monotone posPart
theorem oneLePart_mono {α : Type u_1} [] [] :
Monotone oneLePart
theorem negPart_anti {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :
Antitone negPart
theorem leOnePart_anti {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] :
Antitone leOnePart
@[simp]
theorem posPart_zero {α : Type u_1} [] [] :
0 = 0
@[simp]
theorem oneLePart_one {α : Type u_1} [] [] :
@[simp]
theorem negPart_zero {α : Type u_1} [] [] :
0 = 0
@[simp]
theorem leOnePart_one {α : Type u_1} [] [] :
theorem posPart_nonneg {α : Type u_1} [] [] (a : α) :
0 a
theorem one_le_oneLePart {α : Type u_1} [] [] (a : α) :
theorem negPart_nonneg {α : Type u_1} [] [] (a : α) :
0 a
theorem one_le_leOnePart {α : Type u_1} [] [] (a : α) :
theorem le_posPart {α : Type u_1} [] [] (a : α) :
a a
theorem le_oneLePart {α : Type u_1} [] [] (a : α) :
theorem neg_le_negPart {α : Type u_1} [] [] (a : α) :
theorem inv_le_leOnePart {α : Type u_1} [] [] (a : α) :
@[simp]
theorem posPart_eq_self {α : Type u_1} [] [] {a : α} :
a = a 0 a
@[simp]
theorem oneLePart_eq_self {α : Type u_1} [] [] {a : α} :
a⁺ᵐ = a 1 a
theorem posPart_eq_zero {α : Type u_1} [] [] {a : α} :
a = 0 a 0
theorem oneLePart_eq_one {α : Type u_1} [] [] {a : α} :
a⁺ᵐ = 1 a 1
theorem negPart_eq_neg' {α : Type u_1} [] [] {a : α} :
a = -a 0 -a

See also negPart_eq_neg.

theorem leOnePart_eq_inv' {α : Type u_1} [] [] {a : α} :

See also leOnePart_eq_inv.

@[simp]
theorem negPart_eq_neg {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} :
a = -a a 0
@[simp]
theorem leOnePart_eq_inv {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} :
theorem negPart_eq_zero' {α : Type u_1} [] [] {a : α} :
a = 0 -a 0

See also negPart_eq_zero.

theorem leOnePart_eq_one' {α : Type u_1} [] [] {a : α} :

See also leOnePart_eq_one.

@[simp]
theorem negPart_eq_zero {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} :
a = 0 0 a
@[simp]
theorem leOnePart_eq_one {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} :
a⁻ᵐ = 1 1 a
theorem posPart_nonpos {α : Type u_1} [] [] {a : α} :
a 0 a 0
theorem oneLePart_le_one {α : Type u_1} [] [] {a : α} :
a⁺ᵐ 1 a 1
theorem negPart_nonpos' {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} :
a 0 -a 0

See also negPart_nonpos.

theorem leOnePart_le_one' {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} :

See also leOnePart_le_one.

theorem negPart_nonpos {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} :
a 0 -a 0
theorem leOnePart_le_one {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} :
@[simp]
theorem posPart_pos {α : Type u_1} [] [] {a : α} (ha : 0 < a) :
0 < a
@[simp]
theorem one_lt_oneLePart {α : Type u_1} [] [] {a : α} (ha : 1 < a) :
@[simp]
theorem negPart_pos {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} (ha : a < 0) :
0 < a
@[simp]
theorem one_lt_ltOnePart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} (ha : a < 1) :
@[simp]
theorem posPart_neg {α : Type u_1} [] [] (a : α) :
(-a) = a
@[simp]
theorem oneLePart_inv {α : Type u_1} [] [] (a : α) :
@[simp]
theorem negPart_neg {α : Type u_1} [] [] (a : α) :
(-a) = a
@[simp]
theorem leOnePart_inv {α : Type u_1} [] [] (a : α) :
theorem negPart_eq_neg_inf_zero {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
a = -(a 0)
theorem leOnePart_eq_inv_inf_one {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
theorem posPart_add_negPart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
a + a = |a|
theorem oneLePart_mul_leOnePart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
theorem negPart_add_posPart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
a + a = |a|
theorem leOnePart_mul_oneLePart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
@[simp]
theorem posPart_sub_negPart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
a - a = a
@[simp]
theorem oneLePart_div_leOnePart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
@[simp]
theorem negPart_sub_posPart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
a - a = -a
@[simp]
theorem leOnePart_div_oneLePart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
theorem posPart_inf_negPart_eq_zero {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
a a = 0
theorem oneLePart_inf_leOnePart_eq_one {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
theorem sup_eq_add_posPart_sub {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
a b = b + (a - b)
theorem sup_eq_mul_oneLePart_div {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
a b = b * (a / b)⁺ᵐ
theorem inf_eq_sub_posPart_sub {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
a b = a - (a - b)
theorem inf_eq_div_oneLePart_div {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
a b = a / (a / b)⁺ᵐ
theorem le_iff_posPart_negPart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
theorem le_iff_oneLePart_leOnePart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
theorem abs_add_eq_two_nsmul_posPart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
|a| + a = 2 a
theorem mabs_mul_eq_oneLePart_sq {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
mabs a * a = a⁺ᵐ ^ 2
theorem add_abs_eq_two_nsmul_posPart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
a + |a| = 2 a
theorem mul_mabs_eq_oneLePart_sq {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
a * mabs a = a⁺ᵐ ^ 2
theorem abs_sub_eq_two_nsmul_negPart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
|a| - a = 2 a
theorem mabs_div_eq_leOnePart_sq {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
mabs a / a = a⁻ᵐ ^ 2
theorem sub_abs_eq_neg_two_nsmul_negPart {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
a - |a| = -(2 a)
theorem div_mabs_eq_inv_leOnePart_sq {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
a / mabs a = (a⁻ᵐ ^ 2)⁻¹
theorem posPart_eq_ite {α : Type u_1} [] [] {a : α} :
a = if 0 a then a else 0
theorem oneLePart_eq_ite {α : Type u_1} [] [] {a : α} :
a⁺ᵐ = if 1 a then a else 1
theorem negPart_eq_ite {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} :
a = if a 0 then -a else 0
theorem leOnePart_eq_ite {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} :
a⁻ᵐ = if a 1 then a⁻¹ else 1
@[simp]
theorem posPart_pos_iff {α : Type u_1} [] [] {a : α} :
0 < a 0 < a
@[simp]
theorem one_lt_oneLePart_iff {α : Type u_1} [] [] {a : α} :
1 < a⁺ᵐ 1 < a
@[simp]
theorem negPart_pos_iff {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} :
0 < a a < 0
@[simp]
theorem one_lt_ltOnePart_iff {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} :
1 < a⁻ᵐ a < 1
theorem posPart_eq_of_posPart_pos {α : Type u_1} [] [] {a : α} (ha : 0 < a) :
a = a
theorem oneLePart_of_one_lt_oneLePart {α : Type u_1} [] [] {a : α} (ha : 1 < a⁺ᵐ) :
@[simp]
theorem Pi.posPart_apply {ι : Type u_3} {α : ιType u_4} [(i : ι) → Lattice (α i)] [(i : ι) → AddCommGroup (α i)] (f : (i : ι) → α i) (i : ι) :
f i = (f i)
@[simp]
theorem Pi.oneLePart_apply {ι : Type u_3} {α : ιType u_4} [(i : ι) → Lattice (α i)] [(i : ι) → AddCommGroup (α i)] (f : (i : ι) → α i) (i : ι) :
f i = (f i)
@[simp]
theorem Pi.negPart_apply {ι : Type u_3} {α : ιType u_4} [(i : ι) → Lattice (α i)] [(i : ι) → AddCommGroup (α i)] (f : (i : ι) → α i) (i : ι) :
f i = (f i)
@[simp]
theorem Pi.leOnePart_apply {ι : Type u_3} {α : ιType u_4} [(i : ι) → Lattice (α i)] [(i : ι) → AddCommGroup (α i)] (f : (i : ι) → α i) (i : ι) :
f i = (f i)
theorem Pi.posPart_def {ι : Type u_3} {α : ιType u_4} [(i : ι) → Lattice (α i)] [(i : ι) → AddCommGroup (α i)] (f : (i : ι) → α i) :
f = fun (i : ι) => (f i)
theorem Pi.oneLePart_def {ι : Type u_3} {α : ιType u_4} [(i : ι) → Lattice (α i)] [(i : ι) → AddCommGroup (α i)] (f : (i : ι) → α i) :
f = fun (i : ι) => (f i)
theorem Pi.negPart_def {ι : Type u_3} {α : ιType u_4} [(i : ι) → Lattice (α i)] [(i : ι) → AddCommGroup (α i)] (f : (i : ι) → α i) :
f = fun (i : ι) => (f i)
theorem Pi.leOnePart_def {ι : Type u_3} {α : ιType u_4} [(i : ι) → Lattice (α i)] [(i : ι) → AddCommGroup (α i)] (f : (i : ι) → α i) :
f = fun (i : ι) => (f i)