Real powers

The inverse square root is the real power with exponent -1/2: (√x)⁻¹ = x ^ (-1 / 2). Like Mathlib's Real.sqrt_eq_rpow, this holds for every real x. For x < 0 both sides vanish: the square root is 0, and x ^ y = exp (log x * y) * cos (y * π) has the factor cos (-π / 2) = 0. This is the form in which a kernel 1 / √d is compared with the singular powers |x - c| ^ (-1/2). For 0 ≤ t, its natural powers are (√t)⁻¹ ^ n = t ^ (-n/2), the factor of a parabolic scaling. Splitting 1 - x² = (1 - x) (1 + x) gives (1 - x) (1 - x²)^(-1/2) = √(1 - x) / √(1 + x), again for every real x.

Eventually along a filter on which x is positive, the power x ^ q is exp (q * log x). This is the form in which power weights x ^ q are compared with exponential tilting weights.

The square root of a natural power of a nonnegative real is the real power with half the exponent: √(x ^ n) = x ^ (n / 2). This is the form in which a determinant det (c • G) = c ^ n det G of an n × n matrix contributes to a volume density √(det G).

A real power of a nonnegative base can also be written as a power of its square: (x ^ 2) ^ (s / 2) = x ^ s.

For i < d, comparing the (d - i)-th root x ^ (1 / (d - i)) with y is comparing x with the natural power y ^ (d - i), the form in which spectral values of polynomials are bounded.

For n ≠ 0, the n-th power of x ^ (1 - 1/n) is x ^ (n - 1) for nonnegative x, the form in which the volume factor V ^ (1 - 1/n) of an isoperimetric inequality is raised to the n-th power.

Rescaling a power law: if X ≤ N and C = C₀ N / R ^ α / 2, then C₀ (r / R) ^ α X ≤ 2 (C r ^ α) for r ≥ 0, R > 0 and C₀ ≥ 0.

A natural power b ^ n with 1 ≤ b and n ≤ δ r is at most (b ^ δ) ^ r, which turns a degree bound with a real factor δ into a bound by an r-th power.

For a positive base a, the real powers (a ^ (n + 1)) ^ B and (a ^ n) ^ C multiply to a ^ B * (a ^ (B + C)) ^ n, a geometric term in n. This is how dyadic annuli are summed against a geometric series.

A power x ^ y of a nonnegative real with exponent 0 ≤ y ≤ 1 is at most 1 + x, which bounds the fractional powers T ^ (α / 2) and √T of a time horizon uniformly by 1 + T.

A positive power x ↦ x ^ a maps the open unit interval onto itself, with inverse y ↦ y ^ a⁻¹. This is the image needed when a change of variables y = x ^ a is performed on (0, 1).

A real number whose natural powers grow at most polynomially, r ^ n ≤ C * (1 + n) ^ s for all n, is at most 1. This is how a spectral radius bound is read off from polynomially growing norms, as for the monomials of a weighted Sobolev algebra. Likewise, if n ^ b ≤ C * n ^ a for every natural number n, then b ≤ a; this is how a power-law exponent is read off from testing an inequality on n copies of one vector.

A two-sided real exponential with positive decay rate is little-o of every real power of |x| outside compact subsets of the real line.

A positive real raised to a finitely supported sum of exponents is the product of the powers: a ^ (∑ᶠ i, f i) = ∏ᶠ i, a ^ f i, the finsum form of Real.rpow_sum_of_pos.

An exponential upper bound on a nonnegative base passes to its nonnegative real powers: if 0 ≤ A ≤ e^{-t} and 0 ≤ c, then A ^ c ≤ e^{-c t}. This is how a bound |q| ≤ e^{-t} on a nome is turned into bounds on the fractional powers |q| ^ c in a product estimate.

A positive factor splits off a real power of any real number, including a negative one: (a t) ^ z = a ^ z t ^ z for 0 < a. For t < 0 both sides carry the factor cos (z π). This is the form in which a positive rescaling is pulled out of a power without a sign hypothesis.

For nonnegative a, C, I and q > 0, a bound a ≤ C * I ^ (1 / q) is equivalent to its q-th power a ^ q ≤ C ^ q * I. This is how a domination estimate by an L^q norm is compared with the corresponding integral of q-th powers.

Main results

• Real.inv_sqrt_eq_rpow: (√x)⁻¹ = x ^ (-1 / 2) for every real x.
• Real.inv_sqrt_pow_eq_rpow: (√t)⁻¹ ^ n = t ^ (-n/2) for 0 ≤ t.
• Real.one_sub_mul_one_sub_sq_rpow_neg_one_div_two: (1 - x) (1 - x²)^(-1/2) = √(1 - x) / √(1 + x) for every real x.
• Real.rpow_eventuallyEq_exp_mul_log: x ^ q = exp (q * log x) eventually along a filter on which x is eventually positive.
• Real.sqrt_pow_eq_rpow: √(x ^ n) = x ^ (n / 2) for 0 ≤ x.
• Real.pow_sqrt_eq_rpow: √x ^ n = x ^ (n / 2) for 0 ≤ x.
• Real.sq_rpow_div_two: (x ^ 2) ^ (s / 2) = x ^ s for 0 ≤ x.
• Real.rpow_one_div_natCast_sub_le_iff: x ^ (1 / (d - i)) ≤ y ↔ x ≤ y ^ (d - i) for i < d and nonnegative x, y.
• Real.rpow_one_sub_inv_natCast_pow: (x ^ (1 - 1/n)) ^ n = x ^ (n - 1) for 0 ≤ x and n ≠ 0.
• Real.pow_le_rpow_pow_of_le_mul: b ^ n ≤ (b ^ δ) ^ r when 1 ≤ b and n ≤ δ r.
• Real.pow_succ_rpow_mul_pow_rpow: (a ^ (n + 1)) ^ B * (a ^ n) ^ C = a ^ B * (a ^ (B + C)) ^ n for 0 < a.
• Real.rpow_le_one_add: x ^ y ≤ 1 + x for 0 ≤ x and 0 ≤ y ≤ 1.
• Real.image_rpow_Ioo_zero_one: a positive power maps the open unit interval onto itself.
• Real.tendsto_pow_div_mul_sub_pow_atTop: D ^ n / (n ω (D ^ n - ρ ^ n)) → (n ω)⁻¹ as D → ∞.
• Real.le_one_of_forall_pow_le_mul_rpow: r ≤ 1 when r ^ n ≤ C * (1 + n) ^ s for all n.
• Real.le_of_forall_natCast_rpow_le_mul_rpow: b ≤ a when n ^ b ≤ C * n ^ a for all n.
• TauCeti.exp_neg_mul_abs_isLittleO_abs_rpow_cocompact: a positive-rate exponential beats every real power at both ends of the real line.
• Real.rpow_le_exp_neg_mul: A ^ c ≤ e^{-c t} when 0 ≤ A ≤ e^{-t} and 0 ≤ c.
• Real.mul_rpow_of_pos_left: (a t) ^ z = a ^ z t ^ z for 0 < a and every real t.
• Real.rpow_le_mul_of_mul_le_of_inv_le: from a * b ≤ K and t⁻¹ ≤ c * b ^ q, deduce a ^ q ≤ K ^ q * c * t.
• Real.le_mul_rpow_one_div_iff: a ≤ C * I ^ (1 / q) ↔ a ^ q ≤ C ^ q * I for nonnegative a, C, I and 0 < q.
• Real.exists_le_mul_rpow_lt_of_neg: for 0 < ε and p < 0, arbitrarily large R' satisfy M * R' ^ p < ε.
• Real.rpow_mul_le_rpow_add_one: T ^ S * x ≤ R' ^ (S + 1) for 0 < R' ≤ T, x ≤ T and S + 1 ≤ 0.
• Function.HasFiniteSupport.hasFiniteMulSupport_fun_rpow: real powers with finitely supported exponents have finite multiplicative support.
• Real.rpow_finsum_of_pos: a ^ (∑ᶠ i, f i) = ∏ᶠ i, a ^ f i for 0 < a and finitely supported f.
• Real.le_sqrt_mul_rpow_sub_one_of_sq_le: x ≤ √B * d ^ (β - 1) when d ^ 2 * x ^ 2 ≤ B * d ^ (2 * β) with d > 0, the step turning a mean-value bound on d ^ 2 * x ^ 2 into a pointwise power bound on x.

theorem Real.inv_sqrt_eq_rpow (x : ℝ) : (√x)⁻¹ = x ^ (-1 / 2)

The inverse square root is the real power with exponent -1 / 2: (√x)⁻¹ = x ^ (-1 / 2), for every real x.

theorem Real.inv_sqrt_pow_eq_rpow {t : ℝ} (ht : 0 ≤ t) (n : ℕ) : (√t)⁻¹ ^ n = t ^ (-↑n / 2)

A natural power of the inverse square root is a real power: (√t)⁻¹ ^ n = t ^ (-n/2) for 0 ≤ t. This is the factor of a parabolic scaling x ↦ (√t)⁻¹ • x in dimension n.

theorem Real.one_sub_mul_one_sub_sq_rpow_neg_one_div_two (x : ℝ) : (1 - x) * (1 - x ^ 2) ^ (-1 / 2) = √(1 - x) / √(1 + x)

For every real x, (1 - x) (1 - x²)^(-1/2) = √(1 - x) / √(1 + x). For |x| > 1 both sides vanish, and at x = -1 both are 0 by the conventions 0 ^ y = 0 for y ≠ 0 and a / 0 = 0. This is the form in which the integrand (1 - k sin θ) (1 - k² sin² θ)^(-1/2) of a complete elliptic integral is bounded.

theorem Real.rpow_eventuallyEq_exp_mul_log {l : Filter ℝ} (hpos : ∀ᶠ (x : ℝ) in l, 0 < x) (q : ℝ) : (fun (x : ℝ) => x ^ q) =ᶠ[l] fun (x : ℝ) => exp (q * log x)

Along a filter on which x is eventually positive, x ^ q is eventually exp (q * log x).

theorem Real.sqrt_pow_eq_rpow {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : √(x ^ n) = x ^ (↑n / 2)

The square root of a natural power of a nonnegative real is the real power with half the exponent: √(x ^ n) = x ^ (n / 2).

theorem Real.pow_sqrt_eq_rpow {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : √x ^ n = x ^ (↑n / 2)

A natural power of the square root of a nonnegative real is the real power with half the exponent: √x ^ n = x ^ (n / 2).

@[simp]

theorem Real.sq_rpow_div_two {a : ℝ} (ha : 0 ≤ a) (s : ℝ) : (a ^ 2) ^ (s / 2) = a ^ s

For a nonnegative real number a, taking the real power s / 2 of a ^ 2 gives a ^ s.

theorem Real.rpow_one_div_natCast_sub_le_iff {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) {d i : ℕ} (h : i < d) : x ^ (1 / (↑d - ↑i)) ≤ y ↔ x ≤ y ^ (d - i)

For i < d, the (d - i)-th root of a nonnegative x is at most a nonnegative y exactly when x ≤ y ^ (d - i).

theorem Real.rpow_one_sub_inv_natCast_pow {x : ℝ} (hx : 0 ≤ x) {n : ℕ} (hn : n ≠ 0) : (x ^ (1 - (↑n)⁻¹)) ^ n = x ^ (n - 1)

For n ≠ 0 and nonnegative x, the n-th power of x ^ (1 - 1/n) is x ^ (n - 1).

theorem Real.pow_le_rpow_pow_of_le_mul {b δ : ℝ} (hb : 1 ≤ b) {n r : ℕ} (hn : ↑n ≤ δ * ↑r) : b ^ n ≤ (b ^ δ) ^ r

A natural power b ^ n with 1 ≤ b and n ≤ δ r is at most (b ^ δ) ^ r. This converts a degree bound n ≤ δ r with a real factor δ into a bound by an r-th power.

theorem Real.pow_succ_rpow_mul_pow_rpow {a : ℝ} (ha : 0 < a) (B C : ℝ) (n : ℕ) : (a ^ (n + 1)) ^ B * (a ^ n) ^ C = a ^ B * (a ^ (B + C)) ^ n

Real powers of consecutive natural powers of a positive base combine into a geometric term: (a ^ (n + 1)) ^ B * (a ^ n) ^ C = a ^ B * (a ^ (B + C)) ^ n. This is the form in which the contributions of the annuli a ^ n ≤ r < a ^ (n + 1) are compared with a geometric series.

theorem Real.rpow_le_one_add {x y : ℝ} (hx : 0 ≤ x) (hy₀ : 0 ≤ y) (hy₁ : y ≤ 1) : x ^ y ≤ 1 + x

A power of a nonnegative real with exponent in [0, 1] is at most 1 + x: x ^ y ≤ 1 for x ≤ 1 and x ^ y ≤ x for 1 ≤ x.

theorem Real.image_rpow_Ioo_zero_one {a : ℝ} (ha : 0 < a) : (fun (x : ℝ) => x ^ a) '' Set.Ioo 0 1 = Set.Ioo 0 1

A positive power x ↦ x ^ a maps the open unit interval onto itself.

theorem Real.le_one_of_forall_pow_le_mul_rpow {r C s : ℝ} (h : ∀ (n : ℕ), r ^ n ≤ C * (1 + ↑n) ^ s) : r ≤ 1

A real number whose natural powers grow at most polynomially is at most 1: otherwise r ^ x = exp (log r * x) with log r > 0 outgrows every power of 1 + x.

theorem Real.le_of_forall_natCast_rpow_le_mul_rpow {a b C : ℝ} (h : ∀ (n : ℕ), ↑n ^ b ≤ C * ↑n ^ a) : b ≤ a

If n ^ b ≤ C * n ^ a for every natural number n, then b ≤ a: otherwise n ^ (b - a) eventually exceeds C.

theorem Real.rpow_le_exp_neg_mul {A t c : ℝ} (hA : 0 ≤ A) (hAt : A ≤ exp (-t)) (hc : 0 ≤ c) : A ^ c ≤ exp (-(c * t))

If 0 ≤ A ≤ e^{-t} and 0 ≤ c, then A ^ c ≤ e^{-c t}.

theorem Real.mul_rpow_of_pos_left {a : ℝ} (ha : 0 < a) (t z : ℝ) : (a * t) ^ z = a ^ z * t ^ z

(a t) ^ z = a ^ z t ^ z for a > 0 and every real t, including t < 0, where both sides carry the same factor cos (z π).

theorem Real.le_mul_rpow_one_div_iff {a C I q : ℝ} (ha : 0 ≤ a) (hC : 0 ≤ C) (hI : 0 ≤ I) (hq : 0 < q) : a ≤ C * I ^ (1 / q) ↔ a ^ q ≤ C ^ q * I

For a, C, I ≥ 0 and q > 0, a ≤ C * I ^ (1 / q) if and only if a ^ q ≤ C ^ q * I.

theorem Real.exists_le_mul_rpow_lt_of_neg {M ε p : ℝ} (R : ℝ) (hε : 0 < ε) (hp : p < 0) : ∃ (R' : ℝ), R ≤ R' ∧ M * R' ^ p < ε

For 0 < ε and p < 0, arbitrarily large R' satisfy M * R' ^ p < ε.

theorem Real.rpow_mul_le_rpow_add_one {T S R' x : ℝ} (hR' : 0 < R') (hTR' : R' ≤ T) (hS1 : S + 1 ≤ 0) (hx : x ≤ T) : T ^ S * x ≤ R' ^ (S + 1)

If 0 < R' ≤ T, x ≤ T and S + 1 ≤ 0, then T ^ S * x ≤ R' ^ (S + 1): the bound T ^ S * x ≤ T ^ (S + 1) followed by antitonicity of r ↦ r ^ (S + 1) for a nonpositive exponent.

theorem Real.tendsto_pow_div_mul_sub_pow_atTop {n : ℕ} {ω : ℝ} (hn0 : n ≠ 0) (ρ : ℝ) : Filter.Tendsto (fun (D : ℝ) => D ^ n / (↑n * ω * (D ^ n - ρ ^ n))) Filter.atTop (nhds (↑n * ω)⁻¹)

The limit of the ratio D ^ n / (n ω (D ^ n - ρ ^ n)) as D → ∞ is (n ω)⁻¹, for every real ρ and n ≠ 0.

theorem Real.rpow_le_rpow_sub_mul_rpow {ρ R₁ β γ : ℝ} (hρ : 0 < ρ) (hρR : ρ ≤ R₁) (hβγ : β ≤ γ) : ρ ^ γ ≤ R₁ ^ (γ - β) * ρ ^ β

ρ ^ γ ≤ R₁ ^ (γ - β) ρ ^ β for 0 < ρ ≤ R₁ and β ≤ γ.

theorem Real.rpow_le_mul_of_mul_le_of_inv_le {a b K c t q : ℝ} (hq : 0 ≤ q) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : a * b ≤ K) (hx : t⁻¹ ≤ c * b ^ q) (ht : 0 < t) : a ^ q ≤ K ^ q * c * t

If a * b ≤ K and t⁻¹ ≤ c * b ^ q with a, b ≥ 0, t > 0 and q ≥ 0, then a ^ q ≤ K ^ q * c * t.

theorem Real.div_rpow_of_pos_right {c : ℝ} (hc : 0 < c) (r a : ℝ) : (r / c) ^ a = r ^ a / c ^ a

Dividing the base of a real power by a positive number divides the power by the same power of that number, whatever the sign of the base. Mathlib's Real.div_rpow needs a nonnegative base.

theorem Real.mul_rpow_div_mul_le_two_mul {α C₀ N R r X C : ℝ} (hC₀ : 0 ≤ C₀) (hr : 0 ≤ r) (hR : 0 < R) (hX : X ≤ N) (hC : C = C₀ * N / R ^ α / 2) : C₀ * (r / R) ^ α * X ≤ 2 * (C * r ^ α)

Rescaling a power law: if X ≤ N and C = C₀ N / R ^ α / 2, then C₀ (r / R) ^ α X ≤ 2 (C r ^ α) for r ≥ 0, R > 0 and C₀ ≥ 0.

theorem Real.le_sqrt_mul_rpow_sub_one_of_sq_le {x d B β : ℝ} (hd : 0 < d) (h : d ^ 2 * x ^ 2 ≤ B * d ^ (2 * β)) : x ≤ √B * d ^ (β - 1)

If d ^ 2 * x ^ 2 ≤ B * d ^ (2 * β) with d > 0, then x ≤ √B * d ^ (β - 1).

theorem Function.HasFiniteSupport.hasFiniteMulSupport_fun_rpow {α : Type u_1} (g : α → ℝ) {f : α → ℝ} (hf : HasFiniteSupport f) : HasFiniteMulSupport fun (i : α) => g i ^ f i

Real powers g i ^ f i with finitely supported exponents f have finite multiplicative support.

theorem Real.rpow_finsum_of_pos {α : Type u_1} {a : ℝ} (ha : 0 < a) {f : α → ℝ} (hf : Function.HasFiniteSupport f) : a ^ ∑ᶠ (i : α), f i = ∏ᶠ (i : α), a ^ f i

A positive real raised to a finitely supported sum is the product of the powers.

Two-sided exponential decay

theorem TauCeti.exp_neg_mul_abs_isLittleO_abs_rpow_cocompact {a : ℝ} (ha : 0 < a) (s : ℝ) : (fun (x : ℝ) => Real.exp (-(a * |x|))) =o[Filter.cocompact ℝ] fun (x : ℝ) => |x| ^ s

Rapid decay of the two-sided real exponential. For any positive real rate a, exp (-(a * |x|)) is little-o of |x| ^ s at cocompact ℝ, for every real exponent s.

Adapted from ForTauCeti/Analysis/Fourier/ExponentialAbs.lean in AIQ-Kitware/aiq-dkps-formalization (Apache-2.0; copyright 2026 Kitware, Inc.; authors Jon Crall and GPT 5.6 High).