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 provides instances of 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.

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

instance instOneLePart {α : Type u_1} [Lattice α] [Group α] : OneLePart α

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

Equations

• instOneLePart = { oneLePart := fun (a : α) => a ⊔ 1 }

instance instPosPart {α : Type u_1} [Lattice α] [AddGroup α] : PosPart α

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

Equations

• instPosPart = { posPart := fun (a : α) => a ⊔ 0 }

instance instLeOnePart {α : Type u_1} [Lattice α] [Group α] : LeOnePart α

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

Equations

• instLeOnePart = { leOnePart := fun (a : α) => a⁻¹ ⊔ 1 }

instance instNegPart {α : Type u_1} [Lattice α] [AddGroup α] : NegPart α

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

Equations

• instNegPart = { negPart := fun (a : α) => -a ⊔ 0 }

theorem leOnePart_def {α : Type u_1} [Lattice α] [Group α] (a : α) : a⁻ᵐ = a⁻¹ ⊔ 1

theorem negPart_def {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : a⁻ = -a ⊔ 0

theorem oneLePart_def {α : Type u_1} [Lattice α] [Group α] (a : α) : a⁺ᵐ = a ⊔ 1

theorem posPart_def {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : a⁺ = a ⊔ 0

theorem oneLePart_mono {α : Type u_1} [Lattice α] [Group α] : Monotone fun (x : α) => x⁺ᵐ

theorem posPart_mono {α : Type u_1} [Lattice α] [AddGroup α] : Monotone fun (x : α) => x⁺

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Alias of the reverse direction of oneLePart_eq_self.

@[simp]

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

@[simp]

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

Alias of the reverse direction of oneLePart_eq_one.

@[simp]

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

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

See also leOnePart_eq_inv.

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

See also negPart_eq_neg.

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

See also leOnePart_eq_one.

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

See also negPart_eq_zero.

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

theorem posPart_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

See also leOnePart_le_one.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem leOnePart_of_le_one {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] : a ≤ 1 → a⁻ᵐ = a⁻¹

Alias of the reverse direction of leOnePart_eq_inv.

@[simp]

theorem negPart_of_nonpos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] : a ≤ 0 → a⁻ = -a

@[simp]

theorem leOnePart_of_one_le {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] : 1 ≤ a → a⁻ᵐ = 1

Alias of the reverse direction of leOnePart_eq_one.

@[simp]

theorem negPart_of_nonneg {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] : 0 ≤ a → a⁻ = 0

@[simp]

theorem one_lt_ltOnePart {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] (ha : a < 1) : 1 < a⁻ᵐ

@[simp]

theorem negPart_pos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] (ha : a < 0) : 0 < a⁻

@[simp]

theorem oneLePart_div_leOnePart {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] (a : α) : a⁺ᵐ / a⁻ᵐ = a

@[simp]

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

@[simp]

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

@[simp]

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

theorem oneLePart_leOnePart_injective {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] : Function.Injective fun (a : α) => (a⁺ᵐ , a⁻ᵐ)

theorem posPart_negPart_injective {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] : Function.Injective fun (a : α) => (a⁺, a⁻)

theorem oneLePart_leOnePart_inj {α : Type u_1} [Lattice α] [Group α] {a : α} {b : α} [MulLeftMono α] : a⁺ᵐ = b⁺ᵐ ∧ a⁻ᵐ = b⁻ᵐ ↔ a = b

theorem posPart_negPart_inj {α : Type u_1} [Lattice α] [AddGroup α] {a : α} {b : α} [AddLeftMono α] : a⁺ = b⁺ ∧ a⁻ = b⁻ ↔ a = b

theorem leOnePart_anti {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] : Antitone leOnePart

theorem negPart_anti {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] : Antitone negPart

theorem leOnePart_eq_inv_inf_one {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : a⁻ᵐ = (a ⊓ 1)⁻¹

theorem negPart_eq_neg_inf_zero {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : a⁻ = -(a ⊓ 0)

theorem oneLePart_mul_leOnePart {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : a⁺ᵐ * a⁻ᵐ = mabs a

theorem posPart_add_negPart {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : a⁺ + a⁻ = |a|

theorem leOnePart_mul_oneLePart {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : a⁻ᵐ * a⁺ᵐ = mabs a

theorem negPart_add_posPart {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : a⁻ + a⁺ = |a|

theorem oneLePart_inf_leOnePart_eq_one {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : a⁺ᵐ ⊓ a⁻ᵐ = 1

theorem posPart_inf_negPart_eq_zero {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : a⁺ ⊓ a⁻ = 0

theorem sup_eq_mul_oneLePart_div {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) (b : α) : a ⊔ b = b * (a / b)⁺ᵐ

theorem sup_eq_add_posPart_sub {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) (b : α) : a ⊔ b = b + (a - b)⁺

theorem inf_eq_div_oneLePart_div {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) (b : α) : a ⊓ b = a / (a / b)⁺ᵐ

theorem inf_eq_sub_posPart_sub {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) (b : α) : a ⊓ b = a - (a - b)⁺

theorem le_iff_oneLePart_leOnePart {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) (b : α) : a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ

theorem le_iff_posPart_negPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) (b : α) : a ≤ b ↔ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻

theorem mabs_mul_eq_oneLePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) : mabs a * a = a⁺ᵐ ^ 2

theorem abs_add_eq_two_nsmul_posPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) : |a| + a = 2 • a⁺

theorem mul_mabs_eq_oneLePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) : a * mabs a = a⁺ᵐ ^ 2

theorem add_abs_eq_two_nsmul_posPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) : a + |a| = 2 • a⁺

theorem mabs_div_eq_leOnePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) : mabs a / a = a⁻ᵐ ^ 2

theorem abs_sub_eq_two_nsmul_negPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) : |a| - a = 2 • a⁻

theorem div_mabs_eq_inv_leOnePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a : α) : a / mabs a = (a⁻ᵐ ^ 2)⁻¹

theorem sub_abs_eq_neg_two_nsmul_negPart {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a : α) : a - |a| = -(2 • a⁻)

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

theorem posPart_eq_ite {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} : a⁺ = if 0 ≤ a then a else 0

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem leOnePart_eq_ite {α : Type u_1} [LinearOrder α] [Group α] {a : α} [MulLeftMono α] : a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1

theorem negPart_eq_ite {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} [AddLeftMono α] : a⁻ = if a ≤ 0 then -a else 0

@[simp]

theorem one_lt_ltOnePart_iff {α : Type u_1} [LinearOrder α] [Group α] {a : α} [MulLeftMono α] : 1 < a⁻ᵐ ↔ a < 1

@[simp]

theorem negPart_pos_iff {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} [AddLeftMono α] : 0 < a⁻ ↔ a < 0

@[simp]

theorem leOnePart_lt {α : Type u_1} [LinearOrder α] [Group α] {a : α} {b : α} [MulLeftMono α] [MulRightMono α] : a⁻ᵐ < b ↔ b⁻¹ < a ∧ 1 < b

@[simp]

theorem negPart_lt {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} {b : α} [AddLeftMono α] [AddRightMono α] : a⁻ < b ↔ -b < a ∧ 0 < b

@[simp]

theorem Pi.oneLePart_apply {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → Group (α i)] (f : (i : ι) → α i) (i : ι) : f⁺ᵐ i = (f i)⁺ᵐ

@[simp]

theorem Pi.posPart_apply {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → AddGroup (α i)] (f : (i : ι) → α i) (i : ι) : f⁺ i = (f i)⁺

@[simp]

theorem Pi.leOnePart_apply {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → Group (α i)] (f : (i : ι) → α i) (i : ι) : f⁻ᵐ i = (f i)⁻ᵐ

@[simp]

theorem Pi.negPart_apply {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → AddGroup (α i)] (f : (i : ι) → α i) (i : ι) : f⁻ i = (f i)⁻

theorem Pi.oneLePart_def {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → Group (α i)] (f : (i : ι) → α i) : f⁺ᵐ = fun (i : ι) => (f i)⁺ᵐ

theorem Pi.posPart_def {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → AddGroup (α i)] (f : (i : ι) → α i) : f⁺ = fun (i : ι) => (f i)⁺

theorem Pi.leOnePart_def {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → Group (α i)] (f : (i : ι) → α i) : f⁻ᵐ = fun (i : ι) => (f i)⁻ᵐ

theorem Pi.negPart_def {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Lattice (α i)] [(i : ι) → AddGroup (α i)] (f : (i : ι) → α i) : f⁻ = fun (i : ι) => (f i)⁻