Standard part function

Given a finite element in a non-archimedean field, the standard part function rounds it to the unique closest real number. That is, it chops off any infinitesimals.

Let K be a linearly ordered field. The subset of finite elements (i.e. those bounded by a natural number) is a ValuationSubring, which means we can construct its residue field FiniteResidueField, roughly corresponding to the finite elements quotiented by infinitesimals. This field inherits a LinearOrder instance, which makes it into an Archimedean linearly ordered field, meaning we can uniquely embed it in the reals.

Given a finite element of the field, the ArchimedeanClass.stdPart function returns the real number corresponding to this unique embedding. This function generalizes, among other things, the standard part function on Hyperreal.

TODO

Redefine Hyperreal.st in terms of ArchimedeanClass.stdPart.

References

• https://en.wikipedia.org/wiki/Standard_part_function

Finite residue field

noncomputable def ArchimedeanClass.FiniteElement (K : Type u_1) [LinearOrder K] [Field K] [IsOrderedRing K] : Type u_1

The valuation subring of elements in non-negative Archimedean classes, i.e. elements bounded by some natural number.

instance ArchimedeanClass.FiniteElement.instCommRing {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : CommRing (FiniteElement K)

instance ArchimedeanClass.FiniteElement.instIsDomain {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : IsDomain (FiniteElement K)

instance ArchimedeanClass.FiniteElement.instValuationRing {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : ValuationRing (FiniteElement K)

instance ArchimedeanClass.FiniteElement.instLinearOrder {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : LinearOrder (FiniteElement K)

instance ArchimedeanClass.FiniteElement.instIsStrictOrderedRing {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : IsStrictOrderedRing (FiniteElement K)

@[simp]

theorem ArchimedeanClass.FiniteElement.val_zero {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : ↑0 = 0

@[simp]

theorem ArchimedeanClass.FiniteElement.val_one {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : ↑1 = 1

@[simp]

theorem ArchimedeanClass.FiniteElement.val_add {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (x y : FiniteElement K) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem ArchimedeanClass.FiniteElement.val_sub {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (x y : FiniteElement K) : ↑(x - y) = ↑x - ↑y

@[simp]

theorem ArchimedeanClass.FiniteElement.val_mul {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (x y : FiniteElement K) : ↑(x * y) = ↑x * ↑y

theorem ArchimedeanClass.FiniteElement.ext {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : FiniteElement K} (h : ↑x = ↑y) : x = y

theorem ArchimedeanClass.FiniteElement.ext_iff {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : FiniteElement K} : x = y ↔ ↑x = ↑y

def ArchimedeanClass.FiniteElement.mk {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (x : K) (h : 0 ≤ mk x) : FiniteElement K

The constructor for FiniteElement.

@[simp]

theorem ArchimedeanClass.FiniteElement.mk_zero {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : FiniteElement.mk 0 ⋯ = 0

@[simp]

theorem ArchimedeanClass.FiniteElement.mk_one {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : FiniteElement.mk 1 ⋯ = 1

@[simp]

theorem ArchimedeanClass.FiniteElement.mk_natCast {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (n : ℕ) : FiniteElement.mk ↑n ⋯ = ↑n

@[simp]

theorem ArchimedeanClass.FiniteElement.mk_intCast {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (n : ℤ) : FiniteElement.mk ↑n ⋯ = ↑n

@[simp]

theorem ArchimedeanClass.FiniteElement.neg_mk {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} (h : 0 ≤ mk x) : -FiniteElement.mk x h = FiniteElement.mk (-x) ⋯

@[deprecated ArchimedeanClass.FiniteElement.neg_mk (since := "2025-12-24")]

theorem ArchimedeanClass.FiniteElement.mk_neg {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} (h : 0 ≤ mk x) : -FiniteElement.mk x h = FiniteElement.mk (-x) ⋯

Alias of ArchimedeanClass.FiniteElement.neg_mk.

@[simp]

theorem ArchimedeanClass.FiniteElement.mk_add_mk {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (x y : K) (hx : 0 ≤ mk x) (hy : 0 ≤ mk y) : FiniteElement.mk x hx + FiniteElement.mk y hy = FiniteElement.mk (x + y) ⋯

@[simp]

theorem ArchimedeanClass.FiniteElement.mk_sub_mk {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (x y : K) (hx : 0 ≤ mk x) (hy : 0 ≤ mk y) : FiniteElement.mk x hx - FiniteElement.mk y hy = FiniteElement.mk (x - y) ⋯

@[simp]

theorem ArchimedeanClass.FiniteElement.mk_mul_mk {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (x y : K) (hx : 0 ≤ mk x) (hy : 0 ≤ mk y) : FiniteElement.mk x hx * FiniteElement.mk y hy = FiniteElement.mk (x * y) ⋯

@[simp]

theorem ArchimedeanClass.FiniteElement.mk_le_mk {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (x y : K) (hx : 0 ≤ mk x) (hy : 0 ≤ mk y) : FiniteElement.mk x hx ≤ FiniteElement.mk y hy ↔ x ≤ y

@[simp]

theorem ArchimedeanClass.FiniteElement.mk_lt_mk {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (x y : K) (hx : 0 ≤ mk x) (hy : 0 ≤ mk y) : FiniteElement.mk x hx < FiniteElement.mk y hy ↔ x < y

theorem ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : FiniteElement K} : ¬IsUnit x ↔ 0 < mk ↑x

theorem ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : FiniteElement K} : IsUnit x ↔ mk ↑x = 0

instance ArchimedeanClass.FiniteElement.instRatCast {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : RatCast (FiniteElement K)

@[simp]

theorem ArchimedeanClass.FiniteElement.mk_ratCast {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (q : ℚ) : FiniteElement.mk ↑q ⋯ = ↑q

noncomputable instance ArchimedeanClass.FiniteElement.instFloorRing {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : FloorRing (FiniteElement K)

def ArchimedeanClass.FiniteResidueField (K : Type u_1) [LinearOrder K] [Field K] [IsOrderedRing K] : Type u_1

The residue field of FiniteElement. This quotient inherits an order from K, which makes it into a linearly ordered Archimedean field.

noncomputable instance ArchimedeanClass.FiniteResidueField.instField {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : Field (FiniteResidueField K)

noncomputable instance ArchimedeanClass.FiniteResidueField.instLinearOrder {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : LinearOrder (FiniteResidueField K)

def ArchimedeanClass.FiniteResidueField.mk {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : FiniteElement K →+*o FiniteResidueField K

The quotient map from finite elements on the field to the associated residue field.

theorem ArchimedeanClass.FiniteResidueField.ind {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {motive : FiniteResidueField K → Prop} (mk : ∀ (x : FiniteElement K), motive (mk x)) (x : FiniteResidueField K) : motive x

instance ArchimedeanClass.FiniteResidueField.ordConnected_preimage_mk {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (x : FiniteResidueField K) : (⇑mk ⁻¹' {x}).OrdConnected

theorem ArchimedeanClass.FiniteResidueField.mk_eq_mk {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : FiniteElement K} : mk x = mk y ↔ 0 < ArchimedeanClass.mk (↑x - ↑y)

theorem ArchimedeanClass.FiniteResidueField.mk_eq_zero {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : FiniteElement K} : mk x = 0 ↔ 0 < ArchimedeanClass.mk ↑x

theorem ArchimedeanClass.FiniteResidueField.mk_ne_zero {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : FiniteElement K} : mk x ≠ 0 ↔ ArchimedeanClass.mk ↑x = 0

theorem ArchimedeanClass.FiniteResidueField.mk_le_mk {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : FiniteElement K} : mk x ≤ mk y ↔ x ≤ y ∨ mk x = mk y

theorem ArchimedeanClass.FiniteResidueField.mk_lt_mk {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : FiniteElement K} : mk x < mk y ↔ x < y ∧ mk x ≠ mk y

theorem ArchimedeanClass.FiniteResidueField.lt_of_mk_lt_mk {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : FiniteElement K} (h : mk x < mk y) : x < y

instance ArchimedeanClass.FiniteResidueField.instIsOrderedRing {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : IsOrderedRing (FiniteResidueField K)

instance ArchimedeanClass.FiniteResidueField.instArchimedean {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : Archimedean (FiniteResidueField K)

@[simp]

theorem ArchimedeanClass.FiniteResidueField.mk_ratCast {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (q : ℚ) : mk ↑q = ↑q

def ArchimedeanClass.FiniteResidueField.ofArchimedean {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {R : Type u_2} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] [Archimedean R] (f : R →+*o K) : R →+*o FiniteResidueField K

An embedding from an Archimedean field into K induces an embedding into FiniteResidueField K.

theorem ArchimedeanClass.FiniteResidueField.ofArchimedean_apply {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {R : Type u_2} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] [Archimedean R] (f : R →+*o K) (r : R) : (ofArchimedean f) r = mk (FiniteElement.mk (f r) ⋯)

theorem ArchimedeanClass.FiniteResidueField.ofArchimedean_injective {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {R : Type u_2} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] [Archimedean R] (f : R →+*o K) : Function.Injective ⇑(ofArchimedean f)

@[simp]

theorem ArchimedeanClass.FiniteResidueField.ofArchimedean_inj {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {R : Type u_2} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] [Archimedean R] (f : R →+*o K) {x y : R} : (ofArchimedean f) x = (ofArchimedean f) y ↔ x = y

Standard part

noncomputable def ArchimedeanClass.stdPart {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (x : K) : ℝ

The standard part of a FiniteElement is the unique real number with an infinitesimal difference.

For any infinite inputs, this function outputs a junk value of 0.

theorem ArchimedeanClass.stdPart_of_mk_nonneg {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} (f : FiniteResidueField K →+*o ℝ) (h : 0 ≤ mk x) : stdPart x = f (FiniteResidueField.mk (FiniteElement.mk x h))

@[simp]

theorem ArchimedeanClass.stdPart_eq_zero {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} : stdPart x = 0 ↔ mk x ≠ 0

theorem ArchimedeanClass.stdPart_of_mk_ne_zero {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} : mk x ≠ 0 → stdPart x = 0

Alias of the reverse direction of ArchimedeanClass.stdPart_eq_zero.

theorem ArchimedeanClass.stdPart_monotoneOn {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : MonotoneOn stdPart {x : K | 0 ≤ mk x}

@[simp]

theorem ArchimedeanClass.stdPart_zero {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : stdPart 0 = 0

@[simp]

theorem ArchimedeanClass.stdPart_one {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] : stdPart 1 = 1

@[simp]

theorem ArchimedeanClass.stdPart_neg {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (x : K) : stdPart (-x) = -stdPart x

@[simp]

theorem ArchimedeanClass.stdPart_inv {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (x : K) : stdPart x⁻¹ = (stdPart x)⁻¹

theorem ArchimedeanClass.stdPart_add {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : K} (hx : 0 ≤ mk x) (hy : 0 ≤ mk y) : stdPart (x + y) = stdPart x + stdPart y

theorem ArchimedeanClass.stdPart_add_eq_right {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : K} (hx : 0 < mk x) : stdPart (x + y) = stdPart y

theorem ArchimedeanClass.stdPart_add_eq_left {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : K} (hy : 0 < mk y) : stdPart (x + y) = stdPart x

theorem ArchimedeanClass.stdPart_sub {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : K} (hx : 0 ≤ mk x) (hy : 0 ≤ mk y) : stdPart (x - y) = stdPart x - stdPart y

theorem ArchimedeanClass.stdPart_sub_eq_right {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : K} (hx : 0 < mk x) : stdPart (x - y) = -stdPart y

theorem ArchimedeanClass.stdPart_sub_eq_left {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : K} (hy : 0 < mk y) : stdPart (x - y) = stdPart x

theorem ArchimedeanClass.stdPart_mul {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : K} (hx : 0 ≤ mk x) (hy : 0 ≤ mk y) : stdPart (x * y) = stdPart x * stdPart y

theorem ArchimedeanClass.stdPart_div {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x y : K} (hx : 0 ≤ mk x) (hy : 0 ≤ -mk y) : stdPart (x / y) = stdPart x / stdPart y

@[simp]

theorem ArchimedeanClass.stdPart_ratCast {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (q : ℚ) : stdPart ↑q = ↑q

@[simp]

theorem ArchimedeanClass.stdPart_intCast {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (n : ℤ) : stdPart ↑n = ↑n

@[simp]

theorem ArchimedeanClass.stdPart_natCast {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (n : ℕ) : stdPart ↑n = ↑n

@[simp]

theorem ArchimedeanClass.stdPart_ofNat {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (n : ℕ) [n.AtLeastTwo] : stdPart (OfNat.ofNat n) = ↑n

@[simp]

theorem ArchimedeanClass.stdPart_map_real {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (f : ℝ →+*o K) (r : ℝ) : stdPart (f r) = r

@[simp]

theorem ArchimedeanClass.stdPart_real (r : ℝ) : stdPart r = r

theorem ArchimedeanClass.ofArchimedean_stdPart {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} (f : ℝ →+*o K) (hx : 0 ≤ mk x) : (FiniteResidueField.ofArchimedean f) (stdPart x) = FiniteResidueField.mk (FiniteElement.mk x hx)

theorem ArchimedeanClass.stdPart_nonneg {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} (h : 0 ≤ x) : 0 ≤ stdPart x

theorem ArchimedeanClass.stdPart_nonpos {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} (h : x ≤ 0) : stdPart x ≤ 0

theorem ArchimedeanClass.mk_sub_pos_iff {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} (f : ℝ →+*o K) {r : ℝ} (hx : 0 ≤ mk x) : 0 < mk (x - f r) ↔ stdPart x = r

The standard part of x is the unique real r such that x - r is infinitesimal.

theorem ArchimedeanClass.mk_sub_stdPart_pos {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} (f : ℝ →+*o K) (hx : 0 ≤ mk x) : 0 < mk (x - f (stdPart x))

theorem ArchimedeanClass.lt_of_lt_stdPart {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} (f : ℝ →+*o K) {r : ℝ} (hx : 0 ≤ mk x) (h : r < stdPart x) : f r < x

theorem ArchimedeanClass.lt_of_stdPart_lt {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} (f : ℝ →+*o K) {r : ℝ} (hx : 0 ≤ mk x) (h : stdPart x < r) : x < f r

theorem ArchimedeanClass.stdPart_le_of_le {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} (f : ℝ →+*o K) {r : ℝ} (hx : 0 ≤ mk x) (h : x ≤ f r) : stdPart x ≤ r

theorem ArchimedeanClass.le_stdPart_of_le {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} (f : ℝ →+*o K) {r : ℝ} (hx : 0 ≤ mk x) (h : f r ≤ x) : r ≤ stdPart x

theorem ArchimedeanClass.stdPart_eq {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] {x : K} (f : ℝ →+*o K) {r : ℝ} (hl : ∀ s < r, f s ≤ x) (hr : ∀ s > r, x ≤ f s) : stdPart x = r

theorem ArchimedeanClass.stdPart_eq_sInf {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (f : ℝ →+*o K) (x : K) : stdPart x = sInf {r : ℝ | x < f r}

theorem ArchimedeanClass.stdPart_eq_sSup {K : Type u_1} [LinearOrder K] [Field K] [IsOrderedRing K] (f : ℝ →+*o K) (x : K) : stdPart x = sSup {r : ℝ | f r < x}