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} [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_1} [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_1} [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_1} [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_1} [Lattice α] [AddGroup α] : Monotone posPart

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

@[simp]

theorem posPart_zero {α : Type u_1} [Lattice α] [AddGroup α] : 0⁺ = 0

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

See also negPart_eq_neg.

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

See also leOnePart_eq_inv.

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

See also negPart_eq_zero.

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

See also leOnePart_eq_one.

theorem posPart_nonpos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} : a⁺ ≤ 0 ↔ a ≤ 0

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

theorem negPart_nonpos' {α : Type u_1} [Lattice α] [AddGroup α] {a : α} : a⁻ ≤ 0 ↔ -a ≤ 0

See also negPart_nonpos.

theorem leOnePart_le_one' {α : Type u_1} [Lattice α] [Group α] {a : α} : a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1

See also leOnePart_le_one.

theorem negPart_nonpos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} : a⁻ ≤ 0 ↔ -a ≤ 0

theorem leOnePart_le_one {α : Type u_1} [Lattice α] [Group α] {a : α} : a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1

@[simp]

theorem posPart_pos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} (ha : 0 < a) : 0 < a⁺

@[simp]

theorem one_lt_oneLePart {α : Type u_1} [Lattice α] [Group α] {a : α} (ha : 1 < a) : 1 < a⁺ᵐ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem negPart_pos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (ha : a < 0) : 0 < a⁻

@[simp]

theorem one_lt_ltOnePart {α : Type u_1} [Lattice α] [Group α] {a : α} [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (ha : a < 1) : 1 < a⁻ᵐ

@[simp]

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

@[simp]

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

theorem negPart_anti {α : Type u_1} [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_1} [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

theorem negPart_eq_neg_inf_zero {α : Type u_1} [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_1} [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 posPart_add_negPart {α : Type u_1} [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_1} [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 negPart_add_posPart {α : Type u_1} [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 leOnePart_mul_oneLePart {α : Type u_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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 abs_add_eq_two_nsmul_posPart {α : Type u_1} [Lattice α] [AddCommGroup α] [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} [Lattice α] [CommGroup α] [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} [Lattice α] [AddCommGroup α] [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} [Lattice α] [CommGroup α] [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} [Lattice α] [AddCommGroup α] [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} [Lattice α] [CommGroup α] [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} [Lattice α] [AddCommGroup α] [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} [Lattice α] [CommGroup α] [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} [LinearOrder α] [AddGroup α] {a : α} : a⁺ = if 0 ≤ a then a else 0

theorem oneLePart_eq_ite {α : Type u_1} [LinearOrder α] [Group α] {a : α} : a⁺ᵐ = if 1 ≤ a then a else 1

@[simp]

theorem posPart_pos_iff {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} : 0 < a⁺ ↔ 0 < a

@[simp]

theorem one_lt_oneLePart_iff {α : Type u_1} [LinearOrder α] [Group α] {a : α} : 1 < a⁺ᵐ ↔ 1 < a

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

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

theorem negPart_eq_ite {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : a⁻ = if a ≤ 0 then -a else 0

theorem leOnePart_eq_ite {α : Type u_1} [LinearOrder α] [Group α] {a : α} [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1

@[simp]

theorem negPart_pos_iff {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : 0 < a⁻ ↔ a < 0

@[simp]

theorem one_lt_ltOnePart_iff {α : Type u_1} [LinearOrder α] [Group α] {a : α} [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : 1 < a⁻ᵐ ↔ a < 1

@[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)⁻