Integrals of a weakly singular norm power

Let E be a finite-dimensional real normed space of dimension d. This file computes the integral of the kernel x ↦ ‖x‖ ^ s on a ball centred at the origin, for every exponent s > -d. The singularity is locally integrable because the radial Jacobian is r ^ (d - 1). For an additive Haar measure μ and R ≥ 0,

\int x in ball 0 R, ‖x‖ ^ s ∂μ = d * μ.real (ball 0 1) * (R ^ (d + s) / (d + s)).

The weakly singular exponent s = 1 - d gives the value d * μ.real (ball 0 1) * R; this is the kernel bound used when the straight-segment estimate is averaged over a ball in the proof of the Poincaré--Wirtinger inequality. When d > 1, the exponents s = (1 - d) q with q < d / (d - 1) are the ones met in Hölder's inequality against the Riesz potential in Morrey's inequality. When d = 1, the kernel is constant and imposes no upper bound on q.

Main declarations

• TauCeti.integrableOn_norm_rpow_ball: integrability on a centred ball.
• TauCeti.integral_norm_rpow_ball: the exact radial integral.
• TauCeti.integrableOn_norm_sub_rpow_ball: integrability after translation.
• TauCeti.integral_norm_sub_rpow_ball: the exact integral with any centre.
• TauCeti.locallyIntegrable_norm_sub_rpow: local integrability after translation.
• TauCeti.setLIntegral_closedBall_enorm_sub_rpow: the lower integral with any centre, over a closed ball.
• TauCeti.integral_norm_sub_rpow_one_sub_finrank_le: the translated-ball bound, for s = 1 - d.

References

The statements and radial proof are adapted from Scott Armstrong and Julia Kempe's Apache-2.0 scottnarmstrong/DeGiorgi/DeGiorgi/Poincare.lean, commit 4c1b3077d3782b24065184df4ba59501b2e56fc7, lines 750--870. The formulation here uses an arbitrary additive Haar measure and Mathlib's MeasureTheory.integral_fun_norm_addHaar.

theorem TauCeti.integrableOn_norm_rpow_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {s : ℝ} (hs : -↑(Module.finrank ℝ E) < s) {R : ℝ} : MeasureTheory.IntegrableOn (fun (x : E) => ‖x‖ ^ s) (Metric.ball 0 R) mu

The kernel x ↦ ‖x‖ ^ s is integrable on every ball centred at the origin when -dim E < s.

theorem TauCeti.integral_norm_rpow_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {s : ℝ} (hs : -↑(Module.finrank ℝ E) < s) {R : ℝ} (hR : 0 ≤ R) : ∫ (x : E) in Metric.ball 0 R, ‖x‖ ^ s ∂mu = ↑(Module.finrank ℝ E) * mu.real (Metric.ball 0 1) * (R ^ (↑(Module.finrank ℝ E) + s) / (↑(Module.finrank ℝ E) + s))

The exact integral of the kernel x ↦ ‖x‖ ^ s on a ball centred at the origin, for -dim E < s. The coefficient is stated using the chosen additive Haar measure, so the result applies to both Lebesgue volume and its scalar multiples.

theorem TauCeti.integrableOn_norm_sub_rpow_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {s : ℝ} (hs : -↑(Module.finrank ℝ E) < s) (x : E) {R : ℝ} : MeasureTheory.IntegrableOn (fun (y : E) => ‖x - y‖ ^ s) (Metric.ball x R) mu

The kernel with pole x and exponent s > -dim E is integrable on every ball centred at x.

theorem TauCeti.locallyIntegrable_norm_sub_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {s : ℝ} (hs : -↑(Module.finrank ℝ E) < s) (x : E) : MeasureTheory.LocallyIntegrable (fun (y : E) => ‖x - y‖ ^ s) mu

The kernel with pole x and exponent s > -dim E is locally integrable.

theorem TauCeti.integral_norm_sub_rpow_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {s : ℝ} (hs : -↑(Module.finrank ℝ E) < s) {R : ℝ} (hR : 0 ≤ R) (x : E) : ∫ (y : E) in Metric.ball x R, ‖x - y‖ ^ s ∂mu = ↑(Module.finrank ℝ E) * mu.real (Metric.ball 0 1) * (R ^ (↑(Module.finrank ℝ E) + s) / (↑(Module.finrank ℝ E) + s))

The integral of the kernel with pole x and exponent s > -dim E over a ball centred at x does not depend on the centre and has the same exact value as the radial integral at the origin.

theorem TauCeti.integral_norm_sub_rpow_one_sub_finrank_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {R : ℝ} (x : E) {z : E} (hx : x ∈ Metric.closedBall z R) : ∫ (y : E) in Metric.ball z R, ‖x - y‖ ^ (1 - ↑(Module.finrank ℝ E)) ∂mu ≤ ↑(Module.finrank ℝ E) * mu.real (Metric.ball 0 1) * (2 * R)

If x lies in closedBall z R, then the integral over ball z R of the kernel with pole x is bounded by the exact integral on ball 0 (2R).

theorem TauCeti.setLIntegral_closedBall_enorm_sub_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {s : ℝ} (hs : -↑(Module.finrank ℝ E) < s) {R : ℝ} (hR : 0 ≤ R) (x : E) : ∫⁻ (y : E) in Metric.closedBall x R, ‖x - y‖ₑ ^ s ∂mu = ENNReal.ofReal (↑(Module.finrank ℝ E) * mu.real (Metric.ball 0 1) * (R ^ (↑(Module.finrank ℝ E) + s) / (↑(Module.finrank ℝ E) + s)))

The lower integral of the kernel with pole x and exponent s > -dim E over the closed ball of radius R about x. Unlike its Bochner counterpart TauCeti.integral_norm_sub_rpow_ball, the kernel takes the value ∞ at the pole when s < 0; this does not change the integral, since the pole is a null set.