Elementary scalar capabilities

MathFunctions supplies elementary functions, absolute value, and π for a scalar domain. The interface is independent of encoded formats, storage layouts, and execution backends.

class FloatLib.Numerics.MathFunctions (α : Type) : Type

Scalar functions and π shared by numerical and model code.

This class records which operations a scalar domain can evaluate; it does not by itself promise exactness, an error bound, correct rounding, a selectable rounding mode, or IEEE status flags. Those guarantees belong to separate contracts supplied by each implementation.

• exp : α → α

  Exponential function.

• tanh : α → α

  Hyperbolic tangent.

• cosh : α → α

  Hyperbolic cosine.

• sqrt : α → α

  Principal square root.

• abs : α → α

  Absolute value.

• log : α → α

  Natural logarithm.

• pi : α

  Circular constant π.

• cos : α → α

  Cosine.

• sin : α → α

  Sine.

• sinh : α → α

  Hyperbolic sine.

@[instance_reducible]

instance FloatLib.Numerics.instMathFunctionsFloat : MathFunctions Float

Host floating-point implementations of the scalar functions and π.

@[instance_reducible]

noncomputable instance FloatLib.Numerics.instMathFunctionsReal : MathFunctions ℝ

Real interpretations of the scalar functions and π.