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} [Lattice α] [AddGroup α] (a : α) : α

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

Equations

• a⁺ = a ⊔ 0

def oneLePart {α : Type u} [Lattice α] [Group α] (a : α) : α

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

Equations

• a⁺ᵐ = a ⊔ 1

def negPart {α : Type u} [Lattice α] [AddGroup α] (a : α) : α

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

Equations

• a⁻ = -a ⊔ 0

def leOnePart {α : Type u} [Lattice α] [Group α] (a : α) : α

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

Equations

• a⁻ᵐ = a⁻¹ ⊔ 1

def «term_⁺ᵐ» : Lean.TrailingParserDescr

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 "⁺ᵐ ")

def «term_⁻ᵐ» : Lean.TrailingParserDescr

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 "⁻ᵐ")

def «term_⁺» : Lean.TrailingParserDescr

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 "⁺")

def «term_⁻» : Lean.TrailingParserDescr

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 "⁻")

theorem posPart_mono {α : Type u} [Lattice α] [AddGroup α] : Monotone posPart

theorem oneLePart_mono {α : Type u} [Lattice α] [Group α] : Monotone oneLePart

theorem negPart_anti {α : Type u} [Lattice α] [AddGroup α] [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} [Lattice α] [Group α] [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} [Lattice α] [AddGroup α] : 0⁺ = 0

@[simp]

theorem oneLePart_one {α : Type u} [Lattice α] [Group α] : 1⁺ᵐ = 1

@[simp]

theorem negPart_zero {α : Type u} [Lattice α] [AddGroup α] : 0⁻ = 0

@[simp]

theorem leOnePart_one {α : Type u} [Lattice α] [Group α] : 1⁻ᵐ = 1

theorem posPart_nonneg {α : Type u} [Lattice α] [AddGroup α] (a : α) : 0 ≤ a⁺

theorem one_le_oneLePart {α : Type u} [Lattice α] [Group α] (a : α) : 1 ≤ a⁺ᵐ

theorem negPart_nonneg {α : Type u} [Lattice α] [AddGroup α] (a : α) : 0 ≤ a⁻

theorem one_le_leOnePart {α : Type u} [Lattice α] [Group α] (a : α) : 1 ≤ a⁻ᵐ

theorem le_posPart {α : Type u} [Lattice α] [AddGroup α] (a : α) : a ≤ a⁺

theorem le_oneLePart {α : Type u} [Lattice α] [Group α] (a : α) : a ≤ a⁺ᵐ

theorem neg_le_negPart {α : Type u} [Lattice α] [AddGroup α] (a : α) : -a ≤ a⁻

theorem inv_le_leOnePart {α : Type u} [Lattice α] [Group α] (a : α) : a⁻¹ ≤ a⁻ᵐ

theorem posPart_eq_self {α : Type u} [Lattice α] [AddGroup α] {a : α} : a⁺ = a ↔ 0 ≤ a

theorem oneLePart_eq_self {α : Type u} [Lattice α] [Group α] {a : α} : a⁺ᵐ = a ↔ 1 ≤ a

theorem posPart_eq_zero {α : Type u} [Lattice α] [AddGroup α] {a : α} : a⁺ = 0 ↔ a ≤ 0

theorem oneLePart_eq_one {α : Type u} [Lattice α] [Group α] {a : α} : a⁺ᵐ = 1 ↔ a ≤ 1

theorem negPart_eq_neg' {α : Type u} [Lattice α] [AddGroup α] {a : α} : a⁻ = -a ↔ 0 ≤ -a

theorem leOnePart_eq_inv' {α : Type u} [Lattice α] [Group α] {a : α} : a⁻ᵐ = a⁻¹ ↔ 1 ≤ a⁻¹

theorem negPart_eq_neg {α : Type u} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} : a⁻ = -a ↔ a ≤ 0

theorem leOnePart_eq_inv {α : Type u} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} : a⁻ᵐ = a⁻¹ ↔ a ≤ 1

theorem negPart_eq_zero' {α : Type u} [Lattice α] [AddGroup α] {a : α} : a⁻ = 0 ↔ -a ≤ 0

theorem leOnePart_eq_one' {α : Type u} [Lattice α] [Group α] {a : α} : a⁻ᵐ = 1 ↔ a⁻¹ ≤ 1

theorem negPart_eq_zero {α : Type u} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} : a⁻ = 0 ↔ 0 ≤ a

theorem leOnePart_eq_one {α : Type u} [Lattice α] [Group α] [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} [Lattice α] [AddGroup α] {a : α} : a⁺ ≤ 0 ↔ a ≤ 0

theorem oneLePart_le_one {α : Type u} [Lattice α] [Group α] {a : α} : a⁺ᵐ ≤ 1 ↔ a ≤ 1

theorem negPart_nonpos' {α : Type u} [Lattice α] [AddGroup α] [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} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} : a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1

@[simp]

theorem posPart_neg {α : Type u} [Lattice α] [AddGroup α] (a : α) : (-a)⁺ = a⁻

@[simp]

theorem oneLePart_inv {α : Type u} [Lattice α] [Group α] (a : α) : a⁻¹⁺ᵐ = a⁻ᵐ

@[simp]

theorem negPart_neg {α : Type u} [Lattice α] [AddGroup α] (a : α) : (-a)⁻ = a⁺

@[simp]

theorem leOnePart_inv {α : Type u} [Lattice α] [Group α] (a : α) : a⁻¹⁻ᵐ = a⁺ᵐ

theorem negPart_nonpos {α : Type u} [Lattice α] [AddGroup α] [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} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} : a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1

theorem negPart_eq_neg_inf_zero {α : Type u} [Lattice α] [AddGroup α] [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} [Lattice α] [Group α] [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 ⊓ 1)⁻¹

@[simp]

theorem posPart_sub_negPart {α : Type u} [Lattice α] [AddGroup α] [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} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) : a⁺ᵐ / a⁻ᵐ = a

theorem posPart_add_negPart {α : Type u} [Lattice α] [AddGroup α] [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} [Lattice α] [Group α] [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⁻ᵐ = mabs a

theorem posPart_inf_negPart_eq_zero {α : Type u} [Lattice α] [AddGroup α] [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} [Lattice α] [Group α] [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⁻ᵐ = 1

theorem sup_eq_add_posPart_sub {α : Type u} [Lattice α] [AddCommGroup α] [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} [Lattice α] [CommGroup α] [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} [Lattice α] [AddCommGroup α] [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} [Lattice α] [CommGroup α] [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} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : a ≤ b ↔ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻

theorem le_iff_oneLePart_leOnePart {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ

theorem posPart_eq_of_posPart_pos {α : Type u} [LinearOrder α] [AddCommGroup α] {a : α} (ha : 0 < a⁺) : a⁺ = a

theorem oneLePart_of_one_lt_oneLePart {α : Type u} [LinearOrder α] [CommGroup α] {a : α} (ha : 1 < a⁺ᵐ) : a⁺ᵐ = a