Imports
/-
Copyright (c) 2026 Gregory J. Loges. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gregory J. Loges
-/
module
public import Physlib.SpaceAndTime.Space.IsDistBounded
public import Physlib.SpaceAndTime.Space.Module
public import Mathlib.MeasureTheory.Constructions.HaarToSphere
public import Mathlib.Analysis.SpecialFunctions.ImproperIntegralsIntegrability of norm powers on subsets of Space
i. Overview
This module contains results on the integrability of x ↦ ‖x‖ᵖ for real exponents p on subsets of
Space d.
The integrability of x ↦ ‖x‖ᵖ on ball 0 b and (ball 0 b)ᶜ follows from the 1d results
integrableOn_Ioo_rpow_iff and integrableOn_Ioi_rpow_iff after changing to spherical coordinates.
ii. Key results
integrableOn_norm_rpow_iff_of_isBounded_nhds: Necessary and sufficient condition for
integrability on a set s which is a bounded neighborhood of the origin.
integrableOn_norm_rpow_of_isBounded_compl_nhds: Integrability for all bounded sets s
with 0 ∉ closure s.
integrableOn_norm_rpow_of_compl_nhds: A sufficient condition for integrability on s
with 0 ∉ closure s.
radial_norm_power_spherical_integral_eq_space_integral: The spherical-coordinate integral
identity for integer powers of the norm against a Schwartz map.
iii. Table of contents
iv. References
@[expose] public sectionprivate lemma npow_indicator_rpow_eq {n : ℕ} {s : Set ℝ} (hs : 0 ∉ s) (p : ℝ) :
(fun r ↦ r ^ n • s.indicator (fun r ↦ r ^ p) r) = s.indicator (fun r ↦ r ^ (n + p)) := n:ℕs:Set ℝhs:0 ∉ sp:ℝ⊢ (fun r => r ^ n • s.indicator (fun r => r ^ p) r) = s.indicator fun r => r ^ (↑n + p)
n:ℕs:Set ℝhs:0 ∉ sp:ℝr:ℝ⊢ r ^ n • s.indicator (fun r => r ^ p) r = s.indicator (fun r => r ^ (↑n + p)) r
n:ℕs:Set ℝhs:0 ∉ sp:ℝr:ℝhr:r ∈ s⊢ r ^ n • s.indicator (fun r => r ^ p) r = s.indicator (fun r => r ^ (↑n + p)) rn:ℕs:Set ℝhs:0 ∉ sp:ℝr:ℝhr:r ∉ s⊢ r ^ n • s.indicator (fun r => r ^ p) r = s.indicator (fun r => r ^ (↑n + p)) r
n:ℕs:Set ℝhs:0 ∉ sp:ℝr:ℝhr:r ∈ s⊢ r ^ n • s.indicator (fun r => r ^ p) r = s.indicator (fun r => r ^ (↑n + p)) r All goals completed! 🐙
n:ℕs:Set ℝhs:0 ∉ sp:ℝr:ℝhr:r ∉ s⊢ r ^ n • s.indicator (fun r => r ^ p) r = s.indicator (fun r => r ^ (↑n + p)) r All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙d:ℕp:ℕinst✝:NeZero dq:ℤhp_int:↑p = q + ↑dhp_pos:0 < pη:𝓢(Space d, ℝ)hf:Integrable (fun x => η x * ‖x‖ ^ q) volumen:↑(Metric.sphere 0 1)r:↑(Set.Ioi 0)hr:0 < ↑rhnorm:‖↑r • ↑n‖ = ↑r⊢ ↑r ^ (d - 1) * (η (↑r • ↑n) * ↑r ^ q) = ↑r ^ (d - 1) * ↑r ^ q * η (↑r • ↑n)
All goals completed! 🐙
The function x ↦ ‖x‖ᵖ is integrable on {x : Space d | 0 ≤ ‖x‖ < b} iff 0 < d + p.
d:ℕinst✝:NeZero db:ℝhb:0 < bp:ℝf:Space d → ENNReal := (Metric.ball 0 b).indicator fun x => ‖‖x‖ ^ p‖ₑg:ℝ → ℝ := (Set.Ioo 0 b).indicator fun r => r ^ phfg:f =ᵐ[volume] fun x => ‖g ‖x‖‖ₑ⊢ 0 < 1 + (↑d - 1 + p) ↔ 0 < ↑d + p
All goals completed! 🐙
The function x ↦ ‖x‖ᵖ is integrable on {x : Space d | 0 < a ≤ ‖x‖} iff d + p < 0.
d:ℕinst✝:NeZero da:ℝha:0 < ap:ℝf:Space d → ENNReal := (Metric.ball 0 a)ᶜ.indicator fun x => ‖‖x‖ ^ p‖ₑg:ℝ → ℝ := (Set.Ici a).indicator fun r => r ^ phfg:f = fun x => ‖g ‖x‖‖ₑ⊢ ↑d - 1 + p + 1 < 0 ↔ ↑d + p < 0
All goals completed! 🐙
The function x ↦ ‖x‖ᵖ is integrable on the shell {x : Space d | 0 < a ≤ ‖x‖ ∧ ‖x‖ < b}.
d:ℕa:ℝha:0 < ab:ℝp:ℝhab:¬a < bx:Space dthis:‖x‖ < b → ‖x‖ < a⊢ x ∈ Metric.ball 0 b ∩ (Metric.ball 0 a)ᶜ ↔ x ∈ ∅
All goals completed! 🐙
The function x ↦ ‖x‖ᵖ is integrable on a bounded neighborhood of the origin
iff 0 < d + p.
lemma integrableOn_norm_rpow_iff_of_isBounded_nhds {d : ℕ} [NeZero d] {s : Set (Space d)}
(hs : Bornology.IsBounded s) (hs' : s ∈ nhds 0) (p : ℝ) :
IntegrableOn (fun x : Space d ↦ ‖x‖ ^ p) s ↔ 0 < d + p := d:ℕinst✝:NeZero ds:Set (Space d)hs:Bornology.IsBounded shs':s ∈ nhds 0p:ℝ⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume ↔ 0 < ↑d + p
d:ℕinst✝:NeZero ds:Set (Space d)hs:Bornology.IsBounded shs':s ∈ nhds 0p:ℝa:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, s y⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume ↔ 0 < ↑d + p
d:ℕinst✝:NeZero ds:Set (Space d)hs:Bornology.IsBounded shs':s ∈ nhds 0p:ℝa:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, s yb:ℝhb:0 < bhb':s ⊆ Metric.ball 0 b⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume ↔ 0 < ↑d + p
d:ℕinst✝:NeZero ds:Set (Space d)hs:Bornology.IsBounded shs':s ∈ nhds 0p:ℝa:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, s yb:ℝhb:0 < bhb':s ⊆ Metric.ball 0 b⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume → 0 < ↑d + pd:ℕinst✝:NeZero ds:Set (Space d)hs:Bornology.IsBounded shs':s ∈ nhds 0p:ℝa:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, s yb:ℝhb:0 < bhb':s ⊆ Metric.ball 0 b⊢ 0 < ↑d + p → IntegrableOn (fun x => ‖x‖ ^ p) s volume d:ℕinst✝:NeZero ds:Set (Space d)hs:Bornology.IsBounded shs':s ∈ nhds 0p:ℝa:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, s yb:ℝhb:0 < bhb':s ⊆ Metric.ball 0 b⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume → 0 < ↑d + pd:ℕinst✝:NeZero ds:Set (Space d)hs:Bornology.IsBounded shs':s ∈ nhds 0p:ℝa:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, s yb:ℝhb:0 < bhb':s ⊆ Metric.ball 0 b⊢ 0 < ↑d + p → IntegrableOn (fun x => ‖x‖ ^ p) s volume d:ℕinst✝:NeZero ds:Set (Space d)hs:Bornology.IsBounded shs':s ∈ nhds 0p:ℝa:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, s yb:ℝhb:0 < bhb':s ⊆ Metric.ball 0 bh:0 < ↑d + p⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume
d:ℕinst✝:NeZero ds:Set (Space d)hs:Bornology.IsBounded shs':s ∈ nhds 0p:ℝa:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, s yb:ℝhb:0 < bhb':s ⊆ Metric.ball 0 bh:IntegrableOn (fun x => ‖x‖ ^ p) s volume⊢ 0 < ↑d + p All goals completed! 🐙
d:ℕinst✝:NeZero ds:Set (Space d)hs:Bornology.IsBounded shs':s ∈ nhds 0p:ℝa:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, s yb:ℝhb:0 < bhb':s ⊆ Metric.ball 0 bh:0 < ↑d + p⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume All goals completed! 🐙
The function x ↦ ‖x‖ᵖ is integrable on a bounded subset with the origin in its exterior.
lemma integrableOn_norm_rpow_of_isBounded_compl_nhds {d : ℕ} {s : Set (Space d)}
(hs : Bornology.IsBounded s) (hs' : sᶜ ∈ nhds 0) (p : ℝ) :
IntegrableOn (fun x : Space d ↦ ‖x‖ ^ p) s := d:ℕs:Set (Space d)hs:Bornology.IsBounded shs':sᶜ ∈ nhds 0p:ℝ⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume
d:ℕs:Set (Space d)hs:Bornology.IsBounded shs':sᶜ ∈ nhds 0p:ℝa:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, y ∉ s⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume
d:ℕs:Set (Space d)hs:Bornology.IsBounded shs':sᶜ ∈ nhds 0p:ℝa:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, y ∉ sb:ℝhb:0 < bhb':s ⊆ Metric.ball 0 b⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume
d:ℕs:Set (Space d)hs:Bornology.IsBounded shs':sᶜ ∈ nhds 0p:ℝa:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, y ∉ sb:ℝhb:0 < bhb':s ⊆ Metric.ball 0 bhsc:s ⊆ (Metric.ball 0 a)ᶜ⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume
All goals completed! 🐙
The function x ↦ ‖x‖ᵖ is integrable on a subset with the origin in its exterior provided
the decay at infinity is fast enough.
lemma integrableOn_norm_rpow_of_compl_nhds {d : ℕ} [NeZero d] {s : Set (Space d)}
(hs : sᶜ ∈ nhds 0) {p : ℝ} (h : d + p < 0) : IntegrableOn (fun x : Space d ↦ ‖x‖ ^ p) s := d:ℕinst✝:NeZero ds:Set (Space d)hs:sᶜ ∈ nhds 0p:ℝh:↑d + p < 0⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume
d:ℕinst✝:NeZero ds:Set (Space d)hs:sᶜ ∈ nhds 0p:ℝh:↑d + p < 0a:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, y ∉ s⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume
d:ℕinst✝:NeZero ds:Set (Space d)hs:sᶜ ∈ nhds 0p:ℝh:↑d + p < 0a:ℝha:a > 0ha':∀ y ∈ Metric.ball 0 a, y ∉ shs':s ⊆ (Metric.ball 0 a)ᶜ⊢ IntegrableOn (fun x => ‖x‖ ^ p) s volume
All goals completed! 🐙