Containment for real powers and logarithms with a specified base

The proofs compose logarithm, multiplication, exponential, and division contracts. The real-power identity is used only after deriving positivity of every base value from the accepted interval.

theorem FloatLib.Numerics.Interval.containsReal_rpowBounds? {I J K : Interval ℚ} {terms : ℕ} (h : I.rpowBounds? J terms = some K) {x y : ℝ} (hx : ContainsReal some I x) (hy : ContainsReal some J y) : ContainsReal some K (x ^ y)

Successful real-power bounds contain the result for every real base and exponent member.

theorem FloatLib.Numerics.Interval.containsReal_logbBounds? {B I K : Interval ℚ} {terms : ℕ} (h : B.logbBounds? I terms = some K) {b x : ℝ} (hb : ContainsReal some B b) (hx : ContainsReal some I x) : ContainsReal some K (Real.logb b x)

Successful base-logarithm bounds contain the result at every pair of real input members.