Approximation in the squared-radius weighted norm #
Squared-radius weighted volume is finite on compact sets.
The squared-norm integral is the square of the extended L² seminorm.
theorem
LiebThirring.isFiniteMeasureOnCompacts_norm_sq_volume :
MeasureTheory.IsFiniteMeasureOnCompacts
(MeasureTheory.volume.withDensity fun (x : Position) => ENNReal.ofReal (‖x‖ ^ 2))
Squared-radius weighted volume is finite on compact sets.
theorem
LiebThirring.lintegral_norm_sq_eq_eLpNorm_sq
{E : Type u_1}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure Position}
{f : Position → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
The squared-norm integral is the square of the extended L² seminorm.
theorem
LiebThirring.memLp_two_of_lintegral_norm_sq_lt_top
{E : Type u_1}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure Position}
{f : Position → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(h : ∫⁻ (x : Position), ↑‖f x‖₊ ^ 2 ∂μ < ⊤)
:
MeasureTheory.MemLp f 2 μ
A finite squared-norm integral gives membership in L².
theorem
LiebThirring.tendsto_toLp_of_eLpNorm_sub_le
{E : Type u_1}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure Position}
{v : Position → E}
(hv : MeasureTheory.MemLp v 2 μ)
{f : ℕ → Position → E}
(hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) 2 μ)
(h : ∀ (n : ℕ), MeasureTheory.eLpNorm (v - f n) 2 μ ≤ ENNReal.ofReal (↑n + 1)⁻¹)
:
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.MemLp.toLp (f n) ⋯) Filter.atTop (nhds (MeasureTheory.MemLp.toLp v hv))
Vanishing L² approximation errors give convergence of the associated Lp elements.
theorem
LiebThirring.exists_schwartz_weighted_approximation
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(v : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume))
(hv : ∫⁻ (x : Position), ↑‖x‖₊ ^ 2 * ↑‖↑↑v x‖₊ ^ 2 < ⊤)
:
Schwartz approximation with both L² convergence and convergence of the radial quadratic integral.