Documentation

Mathlib.Analysis.Complex.Order

The partial order on the complex numbers #

This order is defined by z ≤ w ↔ z.re ≤ w.re ∧ z.im = w.im.

This is a natural order on ℂ because, as is well-known, there does not exist an order on ℂ making it into a linearly ordered field. However, the order described above is the canonical order stemming from the structure of ℂ as a ⋆-ring (i.e., it becomes a StarOrderedRing). Moreover, with this order ℂ satisfies IsStrictOrderedRing and the coercion (↑) : ℝ → ℂ is an order embedding.

This file only provides Complex.partialOrder and lemmas about it. Further structural classes are provided in Mathlib/Analysis/RCLike/Basic.lean as

These are all only available with open scoped ComplexOrder.

source
@[instance_reducible]
def Complex.partialOrder :
PartialOrder ℂ

We put a partial order on ℂ so that z ≤ w exactly if w - z is real and nonnegative. Complex numbers with different imaginary parts are incomparable.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complex.le_def {z w : ℂ} :
    z ≤ w ↔ z.re ≤ w.re ∧ z.im = w.im
    source
    theorem Complex.lt_def {z w : ℂ} :
    z < w ↔ z.re < w.re ∧ z.im = w.im
    source
    theorem Complex.nonneg_iff {z : ℂ} :
    0 ≤ z ↔ 0 ≤ z.re ∧ 0 = z.im
    source
    theorem Complex.pos_iff {z : ℂ} :
    0 < z ↔ 0 < z.re ∧ 0 = z.im
    source
    theorem Complex.nonpos_iff {z : ℂ} :
    z ≤ 0 ↔ z.re ≤ 0 ∧ z.im = 0
    source
    theorem Complex.neg_iff {z : ℂ} :
    z < 0 ↔ z.re < 0 ∧ z.im = 0
    source
    theorem Complex.sq_nonneg_iff {z : ℂ} :
    0 ≤ z ^ 2 ↔ z.im = 0
    source
    theorem Complex.sq_nonpos_iff {z : ℂ} :
    z ^ 2 ≤ 0 ↔ z.re = 0
    source
    @[simp]
    theorem Complex.real_le_real {x y : ℝ} :
    ↑x ≤ ↑y ↔ x ≤ y
    source
    @[simp]
    theorem Complex.real_lt_real {x y : ℝ} :
    ↑x < ↑y ↔ x < y
    source
    @[simp]
    theorem Complex.zero_le_real {x : ℝ} :
    0 ≤ ↑x ↔ 0 ≤ x
    source
    @[simp]
    theorem Complex.zero_lt_real {x : ℝ} :
    0 < ↑x ↔ 0 < x
    source
    theorem Complex.not_le_iff {z w : ℂ} :
    ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im
    source
    theorem Complex.not_lt_iff {z w : ℂ} :
    ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im
    source
    theorem Complex.not_le_zero_iff {z : ℂ} :
    ¬z ≤ 0 ↔ 0 < z.re ∨ z.im ≠ 0
    source
    theorem Complex.not_lt_zero_iff {z : ℂ} :
    ¬z < 0 ↔ 0 ≤ z.re ∨ z.im ≠ 0
    source
    theorem Complex.eq_re_of_ofReal_le {r : ℝ} {z : ℂ} (hz : ↑r ≤ z) :
    z = ↑z.re
    source
    @[simp]
    theorem Complex.re_eq_norm {z : ℂ} :
    z.re = ‖z‖ ↔ 0 ≤ z
    source
    @[simp]
    theorem Complex.neg_re_eq_norm {z : ℂ} :
    -z.re = ‖z‖ ↔ z ≤ 0
    source
    @[simp]
    theorem Complex.re_eq_neg_norm {z : ℂ} :
    z.re = -‖z‖ ↔ z ≤ 0
    source
    theorem Complex.monotone_ofReal :
    Monotone ofReal
    source
    theorem Mathlib.Meta.Positivity.ofReal_pos {x : ℝ} :
    0 < x → 0 < ↑x

    Alias of the reverse direction of Complex.zero_lt_real.

    source
    theorem Mathlib.Meta.Positivity.ofReal_nonneg {x : ℝ} :
    0 ≤ x → 0 ≤ ↑x

    Alias of the reverse direction of Complex.zero_le_real.

    source
    theorem Mathlib.Meta.Positivity.ofReal_ne_zero_of_ne_zero {z : ℝ} :
    z ≠ 0 → ↑z ≠ 0

    Alias of the reverse direction of Complex.ofReal_ne_zero.

    source
    def Mathlib.Meta.Positivity.evalComplexOfReal :
    PositivityExt

    Extension for the positivity tactic: Complex.ofReal is positive/nonnegative/nonzero if its input is.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For