The real scalar dictionary

This module supplies the noncomputable Context ℝ instance and its compatibility laws with Mathlib's real field. Keeping these instances separate lets callers import the general Context interface without selecting the real scalar instance.

The instance also gives the exact meaning of the pointwise operators in Spec.PointwiseOp. At a pole or outside the real domain, such as a zero divisor or the reciprocal square root of a negative number, PyTorch returns an infinity or a NaN in every format and no real value is faithful to it, so the operator returns an error instead of Lean's junk value. Elsewhere the operator returns the real value, also where a binary format would round it to an infinity.

noncomputable def Context.truncReal (q : ℝ) : ℤ

The integer nearest to q in the direction of zero.

noncomputable def Context.realPointwise : Spec.PointwiseTable ℝ

Exact real meanings of the pointwise operators that depend on the scalar type.

Division requires a nonzero divisor and the reciprocal square root a positive argument. A power requires either a positive base, a zero base with a nonnegative exponent, or a negative base with an integral exponent; there it agrees with Real.rpow, and 0 ^ 0 = 1 as in PyTorch.

@[instance_reducible]

noncomputable instance instContextReal : Context ℝ

Full Context instance for ℝ (proof backend, noncomputable).

@[simp]

theorem Context.pointwise_real : pointwise = realPointwise

The real dictionary's pointwise operators are Context.realPointwise.

instance instLawfulContextReal : LawfulContext ℝ

The real dictionary uses Mathlib's field operations and has strictly positive tolerance.