Smooth expanding cutoffs and the radial derivative defect

The fixed smooth cutoff, one on the unit ball and zero outside radius two.

Expanding smooth cutoff centred at the nucleus.

def LiebThirring.exteriorFluxBump : ContDiffBump 0

The fixed smooth cutoff, one on the unit ball and zero outside radius two.

Equations

• LiebThirring.exteriorFluxBump = { rIn := 1, rOut := 2, rIn_pos := LiebThirring.exteriorFluxBump._proof_2, rIn_lt_rOut := LiebThirring.exteriorFluxBump._proof_3 }

noncomputable def LiebThirring.exteriorFluxCutoff (c : Position) (T : ℝ) (x : Position) : ℝ

Expanding smooth cutoff centred at the nucleus.

Equations

• LiebThirring.exteriorFluxCutoff c T x = ↑LiebThirring.exteriorFluxBump (T⁻¹ • (x - c))

noncomputable def LiebThirring.exteriorFluxDefect (x : Position) : ℝ

The fixed radial derivative defect whose scaled form appears in the cutoff error.

Equations

• LiebThirring.exteriorFluxDefect x = (fderiv ℝ (↑LiebThirring.exteriorFluxBump) x) x

theorem LiebThirring.contDiff_exteriorFluxCutoff (c : Position) (T : ℝ) : ContDiff ℝ (↑⊤) (exteriorFluxCutoff c T)

The cutoff is smooth for every scale.

theorem LiebThirring.continuous_exteriorFluxDefect : Continuous exteriorFluxDefect

The radial derivative defect is continuous.

theorem LiebThirring.hasCompactSupport_exteriorFluxDefect : HasCompactSupport exteriorFluxDefect

Compact support of the radial derivative defect.

theorem LiebThirring.exteriorFluxDefect_bounded : ∃ (C : ℝ), ∀ (x : Position), ‖exteriorFluxDefect x‖ ≤ C

A global bound on the fixed radial derivative defect.

@[simp]

theorem LiebThirring.exteriorFluxDefect_zero : exteriorFluxDefect 0 = 0

The defect at the origin vanishes.

theorem LiebThirring.tendsto_exteriorFluxCutoff (c x : Position) : Filter.Tendsto (fun (T : ℝ) => exteriorFluxCutoff c T x) Filter.atTop (nhds 1)

Expanding cutoffs tend to one pointwise.

theorem LiebThirring.tendsto_exteriorFluxDefect (c x : Position) : Filter.Tendsto (fun (T : ℝ) => exteriorFluxDefect (T⁻¹ • (x - c))) Filter.atTop (nhds 0)

The scaled radial derivative defect tends to zero pointwise.

theorem LiebThirring.tendsto_integral_exteriorFluxCutoff (μ : MeasureTheory.Measure Position) (c : Position) (f : Position → ℝ) (hf : MeasureTheory.Integrable f μ) : Filter.Tendsto (fun (T : ℝ) => ∫ (x : Position), exteriorFluxCutoff c T x * f x ∂μ) Filter.atTop (nhds (∫ (x : Position), f x ∂μ))

Dominated convergence for a cutoff against any integrable real density.

theorem LiebThirring.tendsto_integral_exteriorFluxDefect (μ : MeasureTheory.Measure Position) (c : Position) (f : Position → ℝ) (hf : MeasureTheory.Integrable f μ) : Filter.Tendsto (fun (T : ℝ) => ∫ (x : Position), exteriorFluxDefect (T⁻¹ • (x - c)) * f x ∂μ) Filter.atTop (nhds 0)

The scaled radial cutoff derivative error vanishes under an integrable majorant.