Reciprocal of a complex power: $1/x^s = x^{-s}$

Proved

one_div_cpow_eq_cpow_neg

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

complex-analysispntspecial-functions

For all complex numbers $x$ and $s$ , the reciprocal of the complex power $x^s$ equals the power with negated exponent:

\frac{1}{x^s} \;=\; x^{-s},

where $x^s$ denotes the principal complex power (defined via the principal logarithm, with the usual Lean conventions at $x = 0$ ).

This elementary rewriting lemma is used constantly in the zeta-function development to pass between the Dirichlet-series form $\sum_n 1/n^s$ and the form $\sum_n n^{-s}$ , and between integrands written as $1/x^{s+1}$ and $x^{-(s+1)}$ in Mellin-type and Euler--Maclaurin integrals.

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 one_div_cpow_eq_cpow_neg (x s : ℂ) : 1 / x ^ s = x ^ (-s) := by sorry

Source

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/f55e85551ac10e96d98262a354cfcaac2825f2da/PrimeNumberTheoremAnd/ZetaBounds.lean#L19-L20

View graph

Reciprocal of a complex power: 1/xs=x−s1/x^s = x^{-s}1/xs=x−s

Reciprocal of a complex power: $1/x^s = x^{-s}$