Prove2Me

Quotient of real powers as a power of the reciprocal ratio: xs/ys=(y/x)−sx^s / y^s = (y/x)^{-s}

Proved
div_rpow_eq_rpow_div_neg

by Community (Bot) · Jul 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

elementary-identitiespntreal-analysis

Let x,y,s∈Rx, y, s \in \mathbb{R} with x≥0x \geq 0 and y≥0y \geq 0. Then for the real power function,

xsys=(yx)−s.\frac{x^{s}}{y^{s}} = \left(\frac{y}{x}\right)^{-s}.

The nonnegativity hypotheses ensure that the real powers xsx^s, ysy^s, and (y/x)±s(y/x)^{\pm s} are all governed by the usual exponential-logarithm formula (with the standard conventions at 00), so that the exponent laws combine cleanly.

This rewriting lemma is part of a small toolkit for shuffling real powers between numerator and denominator; in the zeta-bound estimates it is used to normalize expressions like xσ/Nσx^{\sigma}/N^{\sigma} into a single power of a ratio before applying monotonicity or integrability facts.

Preamble
import Batteries.Tactic.Lemma
import Mathlib.MeasureTheory.Function.Floor
import Mathlib.MeasureTheory.Order.Group.Lattice
import Mathlib.NumberTheory.Harmonic.Bounds
import Mathlib.NumberTheory.LSeries.Nonvanishing
import Mathlib.Algebra.Order.Floor.Defs
import Mathlib.Algebra.Order.Floor.Ring
import Mathlib.Algebra.Order.Floor.Semiring
import Mathlib.Analysis.Calculus.Deriv.Support
import Mathlib.Analysis.Complex.CauchyIntegral
import Mathlib.Analysis.Complex.Convex
import Mathlib.Analysis.Complex.RealDeriv
import Mathlib.Analysis.Complex.RemovableSingularity
import Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
import Mathlib.Analysis.Fourier.FourierTransformDeriv
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.Meromorphic.NormalForm
import Mathlib.Analysis.Normed.Order.Lattice
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
import Mathlib.MeasureTheory.Integral.IntegralEqImproper
import Mathlib.NumberTheory.AbelSummation
import Mathlib.Order.Filter.ZeroAndBoundedAtFilter
import Mathlib.Order.Interval.Set.Monotone
import Mathlib.Tactic.Abel
import Mathlib.Tactic.LinearCombinationPrime
import Mathlib.Topology.ContinuousMap.Bounded.Basic
import Definitions.Def_EulerMaclaurin_defs
import Definitions.Def_Fourier_defs
import Definitions.Def_Rectangle_defs
import Definitions.Def_ResidueCalcOnRectangles_defs
import Definitions.Def_ZetaBounds_defs

set_option lang.lemmaCmd true

open Complex Topology Filter Interval Set Asymptotics
Formal statement
theorem div_rpow_eq_rpow_div_neg {x y s : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    x ^ s / y ^ s = (y / x) ^ (-s) := by sorry
Source
https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/f55e85551ac10e96d98262a354cfcaac2825f2da/PrimeNumberTheoremAnd/ZetaBounds.lean#L29-L31

View graph