The inverse-square field and its divergence

The gradient of the inverse-square potential, with its scalar factor written by squared norm.

The inverse-square potential has precisely the displayed gradient field.

noncomputable def LiebThirring.exteriorInverseSquareField (c x : Position) : Position

The gradient of the inverse-square potential, with its scalar factor written by squared norm.

Equations

• LiebThirring.exteriorInverseSquareField c x = (-2 * (‖x - c‖ ^ 2)⁻¹ ^ 2) • (x - c)

noncomputable def LiebThirring.positionDivergence (V : Position → Position) (x : Position) : ℝ

Coordinate trace of the derivative on physical Euclidean space.

Equations

• LiebThirring.positionDivergence V x = ∑ i : Fin 3, ((fderiv ℝ V x) ((EuclideanSpace.basisFun (Fin 3) ℝ) i)).ofLp i

theorem LiebThirring.hasFDerivAt_inverse_fourth_factor (c x : Position) (hx : x ≠ c) : HasFDerivAt (fun (y : Position) => -2 * (‖y - c‖ ^ 2)⁻¹ ^ 2) ((8 / ‖x - c‖ ^ 6) • (innerSL ℝ) (x - c)) x

Directional derivative of the scalar factor away from the nucleus.

theorem LiebThirring.fderiv_exteriorInverseSquareField_apply (c x v : Position) (hx : x ≠ c) : (fderiv ℝ (exteriorInverseSquareField c) x) v = (-2 / ‖x - c‖ ^ 4) • v + (8 / ‖x - c‖ ^ 6 * inner ℝ (x - c) v) • (x - c)

The vector field derivative evaluated in an arbitrary direction.

theorem LiebThirring.positionDivergence_exteriorInverseSquareField (c x : Position) (hx : x ≠ c) : positionDivergence (exteriorInverseSquareField c) x = 2 / ‖x - c‖ ^ 4

Exact divergence of the inverse-square gradient off the nucleus.

theorem LiebThirring.fderiv_exteriorFluxCutoff_radial (c x : Position) (T : ℝ) : (fderiv ℝ (exteriorFluxCutoff c T) x) (x - c) = exteriorFluxDefect (T⁻¹ • (x - c))

Applying the derivative of the scaled cutoff in the radial direction.

theorem LiebThirring.sum_position_rankOne (L : Position →L[ℝ] ℝ) (v : Position) : ∑ i : Fin 3, L ((EuclideanSpace.basisFun (Fin 3) ℝ) i) * v.ofLp i = L v

Trace of a rank-one map in the standard orthonormal frame.

theorem LiebThirring.positionDivergence_smul (f : Position → ℝ) (V : Position → Position) (x : Position) (hf : DifferentiableAt ℝ f x) (hV : DifferentiableAt ℝ V x) : positionDivergence (fun (y : Position) => f y • V y) x = f x * positionDivergence V x + (fderiv ℝ f x) (V x)

Divergence product rule for a scalar and a vector field at a differentiability point.

theorem LiebThirring.positionDivergence_cutoff_field (c x : Position) (T : ℝ) (hx : x ≠ c) : positionDivergence (fun (y : Position) => exteriorFluxCutoff c T y • exteriorInverseSquareField c y) x = exteriorFluxCutoff c T x * (2 / ‖x - c‖ ^ 4) - exteriorFluxDefect (T⁻¹ • (x - c)) * (2 / ‖x - c‖ ^ 4)

The exact pointwise cutoff divergence, including its gradient error.