Real powers and logarithms with a specified base

Real powers use exp (log x * y) on strictly positive base intervals. Both the base and the exponent may vary. Logarithms with a specified base divide the argument's logarithm by the base's logarithm; the latter enclosure must exclude zero. All intermediate bounds are rational. PowersProof proves containment for every real member of the input intervals.

def FloatLib.Numerics.Interval.rpowBounds? (I J : Interval ℚ) (terms : ℕ) : Option (Interval ℚ)

Enclose real powers on a strictly positive base interval, with a possibly variable real exponent.

A nonpositive lower base endpoint is rejected, including zero: logarithmic reduction cannot enclose it. Negative and zero exponents are allowed when the base interval is positive.

def FloatLib.Numerics.Interval.logbBounds? (B I : Interval ℚ) (terms : ℕ) : Option (Interval ℚ)

Enclose logb b x when the base and argument intervals are positive and the base logarithm enclosure excludes zero. A base range containing one, or an insufficiently accurate logarithm enclosure, is rejected by the interval division.