Integrability 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.

iii. Table of contents

iv. References

theorem Space.integrableOn_norm_rpow_ball_iff {d : ℕ} (hd : 0 < d) {b : ℝ} (hb : 0 < b) (p : ℝ) : MeasureTheory.IntegrableOn (fun (x : Space d) => ‖x‖ ^ p) (Metric.ball 0 b) MeasureTheory.volume ↔ 0 < ↑d + p

The function x ↦ ‖x‖ᵖ is integrable on {x : Space d | 0 ≤ ‖x‖ < b} iff 0 < d + p.

theorem Space.integrableOn_norm_rpow_ball_compl_iff {d : ℕ} (hd : 0 < d) {a : ℝ} (ha : 0 < a) (p : ℝ) : MeasureTheory.IntegrableOn (fun (x : Space d) => ‖x‖ ^ p) (Metric.ball 0 a)ᶜ MeasureTheory.volume ↔ ↑d + p < 0

The function x ↦ ‖x‖ᵖ is integrable on {x : Space d | 0 < a ≤ ‖x‖} iff d + p < 0.

theorem Space.integrableOn_norm_rpow_shell {d : ℕ} {a : ℝ} (ha : 0 < a) (b p : ℝ) : MeasureTheory.IntegrableOn (fun (x : Space d) => ‖x‖ ^ p) (Metric.ball 0 b ∩ (Metric.ball 0 a)ᶜ) MeasureTheory.volume

The function x ↦ ‖x‖ᵖ is integrable on the shell {x : Space d | 0 < a ≤ ‖x‖ ∧ ‖x‖ < b}.

theorem Space.integrableOn_norm_rpow_iff_of_isBounded_nhds {d : ℕ} (hd : 0 < d) {s : Set (Space d)} (hs : Bornology.IsBounded s) (hs' : s ∈ nhds 0) (p : ℝ) : MeasureTheory.IntegrableOn (fun (x : Space d) => ‖x‖ ^ p) s MeasureTheory.volume ↔ 0 < ↑d + p

The function x ↦ ‖x‖ᵖ is integrable on a bounded neighborhood of the origin iff 0 < d + p.

theorem Space.integrableOn_norm_rpow_of_isBounded_compl_nhds {d : ℕ} {s : Set (Space d)} (hs : Bornology.IsBounded s) (hs' : sᶜ ∈ nhds 0) (p : ℝ) : MeasureTheory.IntegrableOn (fun (x : Space d) => ‖x‖ ^ p) s MeasureTheory.volume

The function x ↦ ‖x‖ᵖ is integrable on a bounded subset with the origin in its exterior.

theorem Space.integrableOn_norm_rpow_of_compl_nhds {d : ℕ} (hd : 0 < d) {s : Set (Space d)} (hs : sᶜ ∈ nhds 0) {p : ℝ} (h : ↑d + p < 0) : MeasureTheory.IntegrableOn (fun (x : Space d) => ‖x‖ ^ p) s MeasureTheory.volume

The function x ↦ ‖x‖ᵖ is integrable on a subset with the origin in its exterior provided the decay at infinity is fast enough.