Radial reconstruction of a canonically normalized scalar potential.

noncomputable def EulerCanonicalGraphPotential.radialPotential (V : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (x : EulerLiftedGradientSpace.Vector3) : ℝ

The scalar radial integral of a spatial vector field, based at the origin.

Equations

• EulerCanonicalGraphPotential.radialPotential V x = ∫ (s : ℝ) in 0..1, inner ℝ (V (s • x)) x

theorem EulerCanonicalGraphPotential.radialPotential_zero (V : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) : radialPotential V 0 = 0

The radial integral is normalized to vanish at the origin.

theorem EulerCanonicalGraphPotential.radialPotential_eq_sub (V : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hV : Continuous V) (q : EulerLiftedGradientSpace.Vector3 → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hgrad : ∀ (x : EulerLiftedGradientSpace.Vector3), gradient q x = V x) (x : EulerLiftedGradientSpace.Vector3) : radialPotential V x = q x - q 0

The fundamental theorem of calculus identifies the radial integral with a normalized genuine potential.

theorem EulerCanonicalGraphPotential.radialPotential_smooth (V : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hV : Continuous V) (q : EulerLiftedGradientSpace.Vector3 → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hgrad : ∀ (x : EulerLiftedGradientSpace.Vector3), gradient q x = V x) : ContDiff ℝ (↑⊤) (radialPotential V)

A radial reconstruction of a genuine smooth gradient is itself spatially smooth.

theorem EulerCanonicalGraphPotential.radialPotential_gradient (V : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hV : Continuous V) (q : EulerLiftedGradientSpace.Vector3 → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hgrad : ∀ (x : EulerLiftedGradientSpace.Vector3), gradient q x = V x) (x : EulerLiftedGradientSpace.Vector3) : gradient (radialPotential V) x = V x

Radial normalization preserves the actual gradient.

theorem EulerCanonicalGraphPotential.radialPotential_joint_continuous {T : Type u_1} [TopologicalSpace T] [FirstCountableTopology T] [LocallyCompactSpace T] (V : T → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hV : Continuous (Function.uncurry V)) : Continuous fun (p : T × EulerLiftedGradientSpace.Vector3) => radialPotential (V p.1) p.2

A jointly continuous vector field has a jointly continuous radial scalar potential.