TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.DirectedSemantics.Power

Real binary-power semantics #

Rational and directed rounding share this low-level real binary-power API. The file deliberately does not import executable arithmetic, allowing native kernels to reuse the logarithm proofs without an import cycle through Model.Arithmetic.

source
@[reducible, inline]
noncomputable abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.bpow (exponent : ℤ) :
ℝ

Binary power as a real number.

Instances For
    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bpow_pos (exponent : ℤ) :
    0 < bpow exponent

    Every real binary power is positive.

    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bpow_nonneg (exponent : ℤ) :
    0 ≤ bpow exponent

    Every real binary power is nonnegative.

    source
    @[simp]
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bpow_zero :
    bpow 0 = 1

    The binary power at exponent zero is one.

    source
    @[simp]
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bpow_one :
    bpow 1 = 2

    The binary power at exponent one is two.

    source
    @[simp]
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bpow_neg_one :
    bpow (-1) = 2⁻¹

    The binary power at exponent minus one is one half.

    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bpow_add (left right : ℤ) :
    bpow (left + right) = bpow left * bpow right

    Binary powers turn addition of exponents into multiplication.

    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bpow_le_bpow_of_le {left right : ℤ} (h : left ≤ right) :
    bpow left ≤ bpow right

    Binary powers are monotone in the exponent.

    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bpow_ofNat (exponent : ℕ) :
    bpow (Int.ofNat exponent) = ↑(pow2 exponent)

    A binary power at a natural exponent is the corresponding natural power of two.

    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bpow_natCast (exponent : ℕ) :
    bpow ↑exponent = 2 ^ exponent

    A natural exponent coerced to an integer denotes the corresponding real power of two.

    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bpow_negSucc (exponent : ℕ) :
    bpow (Int.negSucc exponent) = (↑(pow2 (exponent + 1)))⁻¹

    A binary power at a negative successor is the inverse natural power of two.