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.

References

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

Finite residue field

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.

@[implicit_reducible]

noncomputable instance ArchimedeanClass.instCommRingFiniteElement (K : Type u_1) [LinearOrder K] [Field K] [IsOrderedRing K] : CommRing (FiniteElement K)

@[implicit_reducible]

noncomputable instance ArchimedeanClass.instIsDomainFiniteElement (K : Type u_1) [LinearOrder K] [Field K] [IsOrderedRing K] : IsDomain (FiniteElement K)

@[implicit_reducible]

noncomputable instance ArchimedeanClass.instValuationRingFiniteElement (K : Type u_1) [LinearOrder K] [Field K] [IsOrderedRing K] : ValuationRing (FiniteElement K)

@[implicit_reducible]

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

@[implicit_reducible]

noncomputable instance ArchimedeanClass.instIsStrictOrderedRingFiniteElement (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

@[implicit_reducible]

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

@[implicit_reducible]

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.

@[implicit_reducible]

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

@[implicit_reducible]

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

noncomputable 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

noncomputable 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}