Compact smooth extension of the exterior cutoff field

A smooth inner cutoff eliminates the nucleus singularity inside the cell. The resulting field is globally smooth and compactly supported; outside radius a/2 it agrees with the original outer-cutoff field.

noncomputable def LiebThirring.exteriorFluxInnerBump (c : Position) (a : ℝ) (ha : 0 < a) : ContDiffBump c

A smooth inner bump whose transition is confined inside radius a/2.

Equations

• LiebThirring.exteriorFluxInnerBump c a ha = { rIn := a / 4, rOut := a / 2, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def LiebThirring.exteriorFluxExtendedField (c : Position) (a T : ℝ) (ha : 0 < a) (x : Position) : Position

Compact smooth extension of the outer-cutoff inverse-square field.

Equations

• LiebThirring.exteriorFluxExtendedField c a T ha x = (LiebThirring.exteriorFluxCutoff c T x * (1 - ↑(LiebThirring.exteriorFluxInnerBump c a ha) x)) • LiebThirring.exteriorInverseSquareField c x

theorem LiebThirring.contDiffAt_exteriorInverseSquareField (c x : Position) (hx : x ≠ c) : ContDiffAt ℝ (↑⊤) (exteriorInverseSquareField c) x

The inverse-square field is smooth off its singular centre.

theorem LiebThirring.contDiff_exteriorFluxExtendedField (c : Position) (a T : ℝ) (ha : 0 < a) : ContDiff ℝ (↑⊤) (exteriorFluxExtendedField c a T ha)

Global smoothness of the extended field.

theorem LiebThirring.exteriorFluxCutoff_eq_bump (c : Position) (T : ℝ) (hT : 0 < T) : exteriorFluxCutoff c T = ↑{ rIn := T, rOut := 2 * T, rIn_pos := hT, rIn_lt_rOut := ⋯ }

The scaled cutoff is a standard compactly supported bump at positive scale.

theorem LiebThirring.hasCompactSupport_exteriorFluxCutoff (c : Position) (T : ℝ) (hT : 0 < T) : HasCompactSupport (exteriorFluxCutoff c T)

Compact support of the expanding cutoff.

theorem LiebThirring.hasCompactSupport_exteriorFluxExtendedField (c : Position) (a T : ℝ) (ha : 0 < a) (hT : 0 < T) : HasCompactSupport (exteriorFluxExtendedField c a T ha)

Compact support of the extended smooth field.

theorem LiebThirring.exteriorFluxExtendedField_eq (c x : Position) (a T : ℝ) (ha : 0 < a) (hx : a / 2 ≤ ‖x - c‖) : exteriorFluxExtendedField c a T ha x = exteriorFluxCutoff c T x • exteriorInverseSquareField c x

The inner extension equals the original field outside its transition ball.

theorem LiebThirring.eventuallyEq_exteriorFluxExtendedField (c x : Position) (a T : ℝ) (ha : 0 < a) (hx : a / 2 < ‖x - c‖) : exteriorFluxExtendedField c a T ha =ᶠ[nhds x] fun (y : Position) => exteriorFluxCutoff c T y • exteriorInverseSquareField c y

The inner extension is locally invisible outside the transition ball.

theorem LiebThirring.positionDivergence_exteriorFluxExtendedField (c x : Position) (a T : ℝ) (ha : 0 < a) (hx : a / 2 < ‖x - c‖) : positionDivergence (exteriorFluxExtendedField c a T ha) x = exteriorFluxCutoff c T x * (2 / ‖x - c‖ ^ 4) - exteriorFluxDefect (T⁻¹ • (x - c)) * (2 / ‖x - c‖ ^ 4)

Exact divergence of the globally smooth extension outside its transition ball.