Documentation

Mathlib.Algebra.Order.Group.PosPart

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 #

Notations #

References #

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
Instances For
    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
    Instances For
      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
      Instances For
        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
        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} [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 α] :
                  @[simp]
                  theorem negPart_zero {α : Type u_1} [Lattice α] [AddGroup α] :
                  0 = 0
                  @[simp]
                  theorem leOnePart_one {α : Type u_1} [Lattice α] [Group α] :
                  theorem posPart_nonneg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
                  0 a
                  theorem one_le_oneLePart {α : Type u_1} [Lattice α] [Group α] (a : α) :
                  theorem negPart_nonneg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
                  0 a
                  theorem one_le_leOnePart {α : Type u_1} [Lattice α] [Group α] (a : α) :
                  theorem le_posPart {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
                  a a
                  theorem le_oneLePart {α : Type u_1} [Lattice α] [Group α] (a : α) :
                  theorem neg_le_negPart {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
                  theorem inv_le_leOnePart {α : Type u_1} [Lattice α] [Group α] (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 : α} :

                  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 : α} :

                  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 : α} :

                  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 : α} :
                  @[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) :
                  @[simp]
                  theorem posPart_neg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
                  (-a) = a
                  @[simp]
                  theorem oneLePart_inv {α : Type u_1} [Lattice α] [Group α] (a : α) :
                  @[simp]
                  theorem negPart_neg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
                  (-a) = a
                  @[simp]
                  theorem leOnePart_inv {α : Type u_1} [Lattice α] [Group α] (a : α) :
                  @[simp]
                  theorem negPart_eq_neg {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
                  a = -a a 0
                  @[simp]
                  theorem leOnePart_eq_inv {α : Type u_1} [Lattice α] [Group α] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
                  @[simp]
                  theorem negPart_eq_zero {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
                  a = 0 0 a
                  @[simp]
                  theorem leOnePart_eq_one {α : Type u_1} [Lattice α] [Group α] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
                  a⁻ᵐ = 1 1 a
                  @[simp]
                  theorem negPart_pos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (ha : a < 0) :
                  0 < a
                  @[simp]
                  theorem one_lt_ltOnePart {α : Type u_1} [Lattice α] [Group α] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (ha : a < 1) :
                  @[simp]
                  theorem posPart_sub_negPart {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
                  a - a = a
                  @[simp]
                  theorem oneLePart_div_leOnePart {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) :
                  @[simp]
                  theorem negPart_sub_posPart {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
                  a - a = -a
                  @[simp]
                  theorem leOnePart_div_oneLePart {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) :
                  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 posPart_negPart_inj {α : Type u_1} [Lattice α] [AddGroup α] {a : α} {b : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
                  a = b a = b a = b
                  theorem oneLePart_leOnePart_inj {α : Type u_1} [Lattice α] [Group α] {a : α} {b : α} [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
                  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 : α) :
                  a = -(a 0)
                  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 : α) :
                  a + a = |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 : α) :
                  a + a = |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 : α) :
                  a a = 0
                  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 : α) :
                  a b = b + (a - b)
                  theorem sup_eq_mul_oneLePart_div {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
                  a b = b * (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 : α) :
                  a b = a - (a - b)
                  theorem inf_eq_div_oneLePart_div {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
                  a b = a / (a / b)⁺ᵐ
                  theorem le_iff_posPart_negPart {α : Type u_1} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
                  theorem le_iff_oneLePart_leOnePart {α : Type u_1} [Lattice α] [CommGroup α] [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 : α) :
                  |a| + a = 2 a
                  theorem mabs_mul_eq_oneLePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) :
                  mabs a * a = a⁺ᵐ ^ 2
                  theorem add_abs_eq_two_nsmul_posPart {α : Type u_1} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
                  a + |a| = 2 a
                  theorem mul_mabs_eq_oneLePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) :
                  a * mabs a = a⁺ᵐ ^ 2
                  theorem abs_sub_eq_two_nsmul_negPart {α : Type u_1} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
                  |a| - a = 2 a
                  theorem mabs_div_eq_leOnePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) :
                  mabs a / a = a⁻ᵐ ^ 2
                  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 : α) :
                  a - |a| = -(2 a)
                  theorem div_mabs_eq_inv_leOnePart_sq {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (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⁺ᵐ) :
                  @[simp]
                  theorem posPart_lt {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} {b : α} :
                  a < b a < b 0 < b
                  @[simp]
                  theorem oneLePart_lt {α : Type u_1} [LinearOrder α] [Group α] {a : α} {b : α} :
                  a⁺ᵐ < b a < b 1 < b
                  theorem negPart_eq_ite {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
                  a = if a 0 then -a else 0
                  theorem leOnePart_eq_ite {α : Type u_1} [LinearOrder α] [Group α] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
                  a⁻ᵐ = if a 1 then a⁻¹ else 1
                  @[simp]
                  theorem negPart_pos_iff {α : Type u_1} [LinearOrder α] [AddGroup α] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
                  0 < a a < 0
                  @[simp]
                  theorem one_lt_ltOnePart_iff {α : Type u_1} [LinearOrder α] [Group α] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
                  1 < a⁻ᵐ a < 1
                  @[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] :
                  a < b -b < a 0 < b
                  @[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] :
                  a⁻ᵐ < b b⁻¹ < a 1 < b
                  @[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)