Real powers in ℝ≥0∞

If X ^ r ≤ C * X ^ (r - 1) for a finite X, then X ≤ C: the factor X ^ (r - 1) cancels, since it is neither 0 nor ∞ unless X = 0, in which case the conclusion is trivial. This is the last step of every norming argument for Lᵖ norms, where X is a norm and X ^ r is its pairing with the extremal function. In the same way, m ≤ K * m ^ p for a finite m and an exponent p < 1 gives m ^ (1 - p) ≤ K, which turns an estimate μ(A) ≤ K μ(A) ^ (1/n) into the isoperimetric form μ(A) ^ (1 - 1/n) ≤ K.

The product x ^ y * x ^ z is at most x ^ (y + z) for all real exponents y and z, with no hypothesis on x; this combines the powers of a function at two exponents when one of them may be negative.

For 0 ≤ α ≤ 1, C = C₀ N / R ^ α / 2, M = D N and ρ = R / 2, the number max (2 C) (2 M / ρ ^ α) is at most max C₀ (4 D) * R ^ (-α) * N; this bounds a maximum of rescaled constants in a power-law scaling argument.

For an exponent p ∈ [0, 1] the powers x ^ p and x ^ (1 - p) multiply back to x, with no finiteness or positivity hypothesis on x. This is the case s = t of geometric interpolations t ^ p s ^ (1 - p), such as the distortion coefficient τ_{K,N}^{(t)}(θ) with p = 1 / N. Rescaling the factors of a weighted geometric mean a ^ p * b ^ q by finite F⁻¹ and G⁻¹ rescales it by (F ^ p * G ^ q)⁻¹; this normalizes suprema to one in Prékopa–Leindler. For distinct x and y such a weighted geometric mean x ^ (1 - p) * y ^ p still dominates min x y, which compares the hypotheses of the Prékopa–Leindler inequality and of its version for the minimum.

A nonpositive real power is antitone on ℝ≥0∞. Because 0 ^ z = ∞ for z < 0, no positivity hypothesis is needed, unlike its ℝ≥0 counterpart NNReal.rpow_le_rpow_of_nonpos; this is what makes ℝ≥0∞-valued bounds on weakly singular integrands such as |x - c| ^ (-1/2) hold everywhere, the pole included. In the same spirit, the inverse square root of a real x is at most ‖x‖ₑ ^ (-1/2), with equality for x > 0. Two bounds on kernels 1 / √d with d a product of three linear factors follow: at infinity the kernel decays like y ^ (-3/2), and near three distinct poles the product of the factors ‖z - eᵢ‖ₑ ^ (-1/2) is controlled by their sum, since at most one of them can be large.

A real power y ↦ y ^ d on ℝ≥0∞ is upper semicontinuous from the right uniformly on intervals: for ε ≠ 0, every y ∈ [x, z] satisfies y ^ d ≤ x ^ d + ε once z is close enough to x. For d ≥ 0 this is monotonicity and continuity; for d < 0 the power is antitone. Enlarging a set slightly thus changes its d-dimensional diameter sum by little, as in Hausdorff measure approximations by open covers. In the exponent, the roots c ^ (1 / p) of a finite nonzero c tend to 1 as p → ∞, which turns a lower or upper bound weighted by a power of a measure into the corresponding bound in the limit of the Lᵖ seminorms.

A real power of ENNReal.ofReal (a * r) with 0 ≤ a splits as ofReal a ^ d * ofReal r ^ d for every exponent d, since neither factor is ∞. This rescales the gauge (2 r) ^ d of densities and Hausdorff measures.

Marcinkiewicz interpolation at the height t / 2 produces the constant p * 2⁻¹ ^ (1 - p) / (p - 1) times twice the weak-type constant; this simplifies to 2 * p * 2 ^ (p - 1) / (p - 1) times that constant.

For a base in ℝ≥0 greater than one, power comparisons also express rational bounds and closed intervals for a reciprocal radius parameter α / r.

On a seminormed group, x ↦ c * ‖x‖₊ ^ a tends to 0 at 0 for every positive exponent a.

Main declarations

• ENNReal.le_of_rpow_le_mul_rpow_sub_one: X ^ r ≤ C * X ^ (r - 1) gives X ≤ C for a finite X.
• ENNReal.rpow_one_sub_le_of_le_mul_rpow: m ≤ K * m ^ p gives m ^ (1 - p) ≤ K for a finite m and p < 1.
• ENNReal.rpow_mul_rpow_one_sub: x ^ p * x ^ (1 - p) = x for p ∈ [0, 1].
• ENNReal.le_rpow_add: x ^ y * x ^ z ≤ x ^ (y + z) for all real y and z.
• ENNReal.inv_mul_rpow_mul_inv_mul_rpow: (F⁻¹ * a) ^ p * (G⁻¹ * b) ^ q = (F ^ p * G ^ q)⁻¹ * (a ^ p * b ^ q) for finite F, G.
• ENNReal.sq_rpow_one_half: (x ^ 2) ^ (1 / 2) = x, with no hypothesis on x.
• ENNReal.ofReal_mul_rpow: ofReal (a * r) ^ d = ofReal a ^ d * ofReal r ^ d for 0 ≤ a.
• ENNReal.min_le_rpow_one_sub_mul_rpow: min x y ≤ x ^ (1 - p) * y ^ p for p ∈ [0, 1].
• ENNReal.rpow_le_rpow_of_nonpos: x ≤ y gives y ^ z ≤ x ^ z for z ≤ 0.
• ENNReal.eventually_forall_mem_Icc_rpow_le_add: y ^ d ≤ x ^ d + ε for y ∈ [x, z] and z near x.
• ENNReal.exists_pos_forall_mem_Icc_rpow_le_add: for x < r, a radius η > 0 with x + η ≤ r and y ^ d ≤ x ^ d + ε for y ∈ [x, x + η].
• ENNReal.tendsto_rpow_one_div_atTop: c ^ (1 / p) → 1 as p → ∞ for c ∉ {0, ∞}.
• ENNReal.ofReal_inv_sqrt_le_enorm_rpow: ofReal (√x)⁻¹ ≤ ‖x‖ₑ ^ (-2⁻¹) for every real x.
• ENNReal.ofReal_inv_sqrt_le_of_pow_three_le: y³ ≤ 2 |d| gives 1 / √d ≤ √2 y^(-3/2).
• ENNReal.exists_enorm_sub_rpow_neg_half_mul_le: for three distinct points eᵢ, the product of the ‖z - eᵢ‖ₑ ^ (-1/2) is at most a constant times their sum.
• ENNReal.le_two_rpow_mul_inv_rpow_mul: a bound (s / 2) ^ q * a ≤ B gives a ≤ 2 ^ q * (s ^ q)⁻¹ * B for s ≠ 0, ∞.
• ENNReal.ofReal_mul_inv_two_rpow_div_mul_two_mul: the Marcinkiewicz constant at height t / 2, ofReal (p * 2⁻¹ ^ (1 - p) / (p - 1)) * (2 * A) = ofReal (2 * p * 2 ^ (p - 1) / (p - 1)) * A.
• NNReal.rpow_neg_mem_Icc_iff: an interval of negative powers is equivalent to an interval for the reciprocal parameter α / r.
• TauCeti.tendsto_const_mul_nnnorm_rpow_nhds_zero: c * ‖x‖₊ ^ a → 0 as x → 0 for 0 < a.

theorem ENNReal.le_of_rpow_le_mul_rpow_sub_one {X C : ENNReal} {r : ℝ} (hX : X ≠ ⊤) (h : X ^ r ≤ C * X ^ (r - 1)) : X ≤ C

If X ^ r ≤ C * X ^ (r - 1) for a finite X, then X ≤ C.

theorem ENNReal.rpow_one_sub_le_of_le_mul_rpow {m K : ENNReal} {p : ℝ} (hp : p < 1) (hm : m ≠ ⊤) (h : m ≤ K * m ^ p) : m ^ (1 - p) ≤ K

If m ≤ K * m ^ p for a finite m and an exponent p < 1, then m ^ (1 - p) ≤ K: the factor m ^ p cancels.

theorem ENNReal.rpow_mul_rpow_one_sub (x : ENNReal) {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) : x ^ p * x ^ (1 - p) = x

For p ∈ [0, 1], the powers x ^ p and x ^ (1 - p) multiply back to x.

theorem ENNReal.le_rpow_add (x : ENNReal) (y z : ℝ) : x ^ y * x ^ z ≤ x ^ (y + z)

The product x ^ y * x ^ z is at most x ^ (y + z), for every x and all real y and z; this is the ℝ≥0∞ form of Real.le_rpow_add. Away from 0 and ∞ it is an equality. At 0 and at ∞ either the right side is ∞, or one of the two factors on the left vanishes, or both exponents vanish.

theorem ENNReal.inv_mul_rpow_mul_inv_mul_rpow {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) {F G : ENNReal} (hF : F ≠ ⊤) (hG : G ≠ ⊤) (a b : ENNReal) : (F⁻¹ * a) ^ p * (G⁻¹ * b) ^ q = (F ^ p * G ^ q)⁻¹ * (a ^ p * b ^ q)

Scaling the factors of a ^ p * b ^ q by F⁻¹ and G⁻¹ scales it by (F ^ p * G ^ q)⁻¹, for finite F and G and nonnegative exponents.

theorem ENNReal.sq_rpow_one_half (x : ENNReal) : (x ^ 2) ^ (1 / 2) = x

The square root of a square in ℝ≥0∞, written as a real power: (x ^ 2) ^ (1 / 2) = x.

theorem ENNReal.ofReal_mul_rpow {a : ℝ} (ha : 0 ≤ a) (r d : ℝ) : ENNReal.ofReal (a * r) ^ d = ENNReal.ofReal a ^ d * ENNReal.ofReal r ^ d

A real power of ENNReal.ofReal (a * r) with 0 ≤ a splits as a product, for every exponent d.

theorem ENNReal.min_le_rpow_one_sub_mul_rpow (x y : ENNReal) {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) : min x y ≤ x ^ (1 - p) * y ^ p

For p ∈ [0, 1], the weighted geometric mean x ^ (1 - p) * y ^ p dominates min x y.

theorem ENNReal.rpow_le_rpow_of_nonpos {x y : ENNReal} {z : ℝ} (hxy : x ≤ y) (hz : z ≤ 0) : y ^ z ≤ x ^ z

A nonpositive real power is antitone on ℝ≥0∞: x ≤ y gives y ^ z ≤ x ^ z for z ≤ 0.

theorem ENNReal.eventually_forall_mem_Icc_rpow_le_add (x : ENNReal) {ε : ENNReal} (hε : ε ≠ 0) (d : ℝ) : ∀ᶠ (z : ENNReal) in nhds x, ∀ y ∈ Set.Icc x z, y ^ d ≤ x ^ d + ε

For ε ≠ 0, every y ∈ [x, z] satisfies y ^ d ≤ x ^ d + ε once z is close enough to x.

theorem ENNReal.exists_pos_forall_mem_Icc_rpow_le_add {x r ε : ENNReal} (hxr : x < r) (hε : ε ≠ 0) (d : ℝ) : ∃ (η : NNReal), 0 < η ∧ x + ↑η ≤ r ∧ ∀ y ∈ Set.Icc x (x + ↑η), y ^ d ≤ x ^ d + ε

For x < r and ε ≠ 0 there is η > 0 with x + η ≤ r such that every y ∈ [x, x + η] satisfies y ^ d ≤ x ^ d + ε.

theorem ENNReal.tendsto_rpow_one_div_atTop {c : ENNReal} (hc0 : c ≠ 0) (hc : c ≠ ⊤) : Filter.Tendsto (fun (p : ℝ) => c ^ (1 / p)) Filter.atTop (nhds 1)

For a finite nonzero c, the roots c ^ (1 / p) tend to 1 as the real exponent p tends to infinity.

theorem ENNReal.ofReal_inv_sqrt_le_enorm_rpow (x : ℝ) : ENNReal.ofReal (√x)⁻¹ ≤ ‖x‖ₑ ^ (-2⁻¹)

The inverse square root of a real x is at most ‖x‖ₑ ^ (-1/2), as a value in ℝ≥0∞. The two agree for x > 0; for x ≤ 0 the left side is 0.

theorem ENNReal.ofReal_inv_sqrt_le_of_pow_three_le {d y : ℝ} (hy : 0 < y) (h : y ^ 3 ≤ 2 * |d|) : ENNReal.ofReal (√d)⁻¹ ≤ ENNReal.ofReal √2 * ENNReal.ofReal (y ^ (-(3 / 2)))

If y > 0 and y³ ≤ 2 |d|, then 1 / √d ≤ √2 y^(-3/2), as values in ℝ≥0∞. This is the decay at infinity of a kernel 1 / √d(x) for a cubic d with leading coefficient 4, with y = 1 + |x|.

theorem ENNReal.exists_enorm_sub_rpow_neg_half_mul_le {E : Type u_1} [NormedAddGroup E] {e₁ e₂ e₃ : E} (h₁₂ : e₁ ≠ e₂) (h₁₃ : e₁ ≠ e₃) (h₂₃ : e₂ ≠ e₃) : ∃ (K : ENNReal), K ≠ ⊤ ∧ ∀ (z : E), ‖z - e₁‖ₑ ^ (-2⁻¹) * ‖z - e₂‖ₑ ^ (-2⁻¹) * ‖z - e₃‖ₑ ^ (-2⁻¹) ≤ K * (‖z - e₁‖ₑ ^ (-2⁻¹) + ‖z - e₂‖ₑ ^ (-2⁻¹) + ‖z - e₃‖ₑ ^ (-2⁻¹))

For three distinct points e₁, e₂, e₃ of a normed additive group, at most one of the factors ‖z - eᵢ‖ₑ ^ (-1/2) is large: the product of the three is at most a constant times their sum.

theorem ENNReal.le_two_rpow_mul_inv_rpow_mul {q : ℝ} {s a B : ENNReal} (hs : s ≠ 0) (hs' : s ≠ ⊤) (h : (s / 2) ^ q * a ≤ B) : a ≤ 2 ^ q * (s ^ q)⁻¹ * B

A bound on (s / 2) ^ q * a bounds a.

theorem ENNReal.ofReal_mul_inv_two_rpow_div_mul_two_mul (p : ℝ) (A : ENNReal) : ENNReal.ofReal (p * 2⁻¹ ^ (1 - p) / (p - 1)) * (2 * A) = ENNReal.ofReal (2 * p * 2 ^ (p - 1) / (p - 1)) * A

The constant that Marcinkiewicz interpolation at the height 2⁻¹ * t produces from a weak-type (1, 1) constant A and the L^∞ constant 1: the factor 2 of 2 * A and the power 2⁻¹ ^ (1 - p) = 2 ^ (p - 1) combine into 2 * p * 2 ^ (p - 1) / (p - 1).

theorem NNReal.rpow_le_rpow_iff_of_one_lt {b : NNReal} (hb : 1 < b) {x y : ℝ} : b ^ x ≤ b ^ y ↔ x ≤ y

For a base greater than one, real powers are ordered exactly by their exponents.

theorem NNReal.rpow_neg_mem_Icc_iff {c : NNReal} (hc : 1 < c) (α r a b : ℝ) (hr : 0 < r) (ha : 0 < a) (hb : 0 < b) : c ^ (-r) ∈ Set.Icc (c ^ (-α / a)) (c ^ (-α / b)) ↔ α / r ∈ Set.Icc a b

Reciprocal radius interval dictionary. For a base c > 1, the interval c ^ (-α/a) ≤ c ^ (-r) ≤ c ^ (-α/b) is equivalent to a ≤ α / r ≤ b when r, a, and b are positive.

theorem NNReal.rpow_num_den_le_iff {b : NNReal} (hb : 1 < b) (r : ℝ) (hr : 0 < r) (α : ℝ) (q : ℚ≥0) : (b ^ (-α)) ^ q.den ≤ (b ^ (-r)) ^ q.num ↔ ↑q ≤ α / r

A rational lower bound on the ratio α / r, expressed as a comparison of powers.

For r > 0, the inequality (b ^ (-α)) ^ q.den ≤ (b ^ (-r)) ^ q.num is equivalent to q ≤ α / r; the base is arbitrary above one.

theorem NNReal.rpow_den_num_le_iff {b : NNReal} (hb : 1 < b) (r : ℝ) (hr : 0 < r) (α : ℝ) (q : ℚ≥0) : (b ^ (-r)) ^ q.num ≤ (b ^ (-α)) ^ q.den ↔ α / r ≤ ↑q

A rational upper bound on the ratio α / r, expressed as a comparison of powers.

For r > 0, the inequality (b ^ (-r)) ^ q.num ≤ (b ^ (-α)) ^ q.den is equivalent to α / r ≤ q; the base is arbitrary above one.

theorem NNReal.max_two_mul_le_toNNReal {α C M ρ : NNReal} {C₀ D N R : ℝ} (hα1 : ↑α ≤ 1) (hR : 0 < R) (hC₀ : 0 ≤ C₀) (hD : 0 ≤ D) (hN : 0 ≤ N) (hC : ↑C = C₀ * N / R ^ ↑α / 2) (hM : ↑M = D * N) (hρ : ↑ρ = R / 2) : max (2 * C) (2 * M / ρ ^ ↑α) ≤ (max C₀ (4 * D) * R ^ (-↑α) * N).toNNReal

Bounding a maximum of rescaled constants: for 0 ≤ α ≤ 1, C = C₀ N / R ^ α / 2, M = D N and ρ = R / 2, the number max (2 C) (2 M / ρ ^ α) is at most max C₀ (4 D) * R ^ (-α) * N.

theorem TauCeti.tendsto_const_mul_nnnorm_rpow_nhds_zero {E : Type u_1} [SeminormedAddGroup E] (c : NNReal) {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (x : E) => c * ‖x‖₊ ^ a) (nhds 0) (nhds 0)

For a positive exponent a, the map x ↦ c * ‖x‖₊ ^ a on a seminormed group tends to 0 at 0.