Real powers of the norm away from the origin

Mathlib computes the derivative of x ↦ ‖x‖ ^ p on the whole inner-product space when 1 < p. Negative powers, which occur in the Newtonian kernel, are smooth only away from the origin. This file supplies the corresponding local derivative, Hessian, and Laplacian formulas under the explicit hypothesis x ≠ 0, together with the Laplacian of the dipole-type product x ↦ ⟪a, x⟫ ‖x‖^p. The critical exponents give the functions ‖x‖^(2 - dim E) and ⟪a, x⟫ ‖x‖^(-dim E), harmonic away from the origin, from which the Poisson kernel of a ball is assembled.

The first derivative proof adapts Mathlib's hasFDerivAt_norm_rpow, retaining its norm-square chain-rule argument while replacing the global exponent hypothesis with the local condition x ≠ 0.

Main declarations

• norm_rpow_eq_norm_sq_rpow: a real power of the norm as a power of the squared norm.
• hasFDerivAt_norm_rpow_of_ne: the derivative of an arbitrary real power away from zero.
• iteratedFDeriv_two_norm_rpow_apply: the Hessian of an arbitrary real power away from zero.
• laplacian_norm_rpow_of_ne: the radial Laplacian formula Δ ‖x‖^p = p (p + dim E - 2) ‖x‖^(p-2) away from zero.
• laplacian_inner_mul_norm_rpow_of_ne: the dipole formula Δ (⟪a, x⟫ ‖x‖^p) = p (p + dim E) ⟪a, x⟫ ‖x‖^(p-2) away from zero.
• harmonicAt_norm_rpow_two_sub_finrank, harmonicAt_inner_mul_norm_rpow_neg_finrank: the harmonic radial and dipole powers.

theorem TauCeti.norm_rpow_eq_norm_sq_rpow {E : Type u_1} [NormedAddCommGroup E] (x : E) (p : ℝ) : ‖x‖ ^ p = (‖x‖ ^ 2) ^ (p / 2)

A real power of the norm, written as a power of the squared norm.

theorem TauCeti.hasFDerivAt_norm_rpow_of_ne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ℝ) {x : E} (hx : x ≠ 0) : HasFDerivAt (fun (y : E) => ‖y‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x

Away from the origin, the derivative of x ↦ ‖x‖ ^ p is p ‖x‖ ^ (p - 2) ⟨x, ·⟩. Unlike Mathlib's hasFDerivAt_norm_rpow, this local form allows every real exponent.

theorem TauCeti.fderiv_norm_rpow_of_ne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ℝ) {x : E} (hx : x ≠ 0) : fderiv ℝ (fun (y : E) => ‖y‖ ^ p) x = (p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x

The Fréchet derivative of an arbitrary real power of the norm away from the origin.

theorem TauCeti.iteratedFDeriv_two_norm_rpow_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ℝ) {x : E} (hx : x ≠ 0) (v w : E) : (iteratedFDeriv ℝ 2 (fun (y : E) => ‖y‖ ^ p) x) ![v, w] = p * (p - 2) * ‖x‖ ^ (p - 4) * inner ℝ x v * inner ℝ x w + p * ‖x‖ ^ (p - 2) * inner ℝ v w

The Hessian of x ↦ ‖x‖ ^ p away from the origin, evaluated on two directions.

theorem TauCeti.laplacian_norm_rpow_of_ne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (p : ℝ) {x : E} (hx : x ≠ 0) : Laplacian.laplacian (fun (y : E) => ‖y‖ ^ p) x = p * (p + ↑(Module.finrank ℝ E) - 2) * ‖x‖ ^ (p - 2)

The Laplacian of a real power of the norm away from the origin is p (p + dim E - 2) ‖x‖ ^ (p - 2).

theorem TauCeti.laplacian_inner_mul_norm_rpow_of_ne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (a : E) (p : ℝ) {x : E} (hx : x ≠ 0) : Laplacian.laplacian (fun (y : E) => inner ℝ a y * ‖y‖ ^ p) x = p * (p + ↑(Module.finrank ℝ E)) * inner ℝ a x * ‖x‖ ^ (p - 2)

The Laplacian of the dipole-type product x ↦ ⟪a, x⟫ ‖x‖ ^ p away from the origin is p (p + dim E) ⟪a, x⟫ ‖x‖ ^ (p - 2).

theorem TauCeti.harmonicAt_norm_rpow_two_sub_finrank {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {x : E} (hx : x ≠ 0) : InnerProductSpace.HarmonicAt (fun (y : E) => ‖y‖ ^ (2 - ↑(Module.finrank ℝ E))) x

Away from the origin, x ↦ ‖x‖ ^ (2 - dim E) is harmonic.

theorem TauCeti.harmonicAt_inner_mul_norm_rpow_neg_finrank {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (a : E) {x : E} (hx : x ≠ 0) : InnerProductSpace.HarmonicAt (fun (y : E) => inner ℝ a y * ‖y‖ ^ (-↑(Module.finrank ℝ E))) x

Away from the origin, the dipole x ↦ ⟪a, x⟫ ‖x‖ ^ (-dim E) is harmonic.