CoordinatePrimitive

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

A one-coordinate primitive for scalar forcing

This file constructs a scalar primitive by integrating along one coordinate. The fixed-interval formula makes its joint parameter regularity accessible to the parametric-integral calculus API. A change of variables recovers the ordinary oriented coordinate integral, from which the selected derivative and the sharp segment bound follow.

noncomputable def DivergenceFormProcess.coordinatePrimitive {d : ℕ} (f : HCPolySupport.Vec d → ℝ) (i : Fin d) (z : ℝ) (x : HCPolySupport.Vec d) : ℝ

The primitive of f along coordinate i, based at coordinate z, written as a fixed integral over [0, 1].

Equations

• DivergenceFormProcess.coordinatePrimitive f i z x = ∫ (t : ℝ) in Set.Icc 0 1, (x i - z) * f (Function.update x i (z + t * (x i - z)))

theorem DivergenceFormProcess.contDiff_one_coordinatePrimitive {d : ℕ} (f : HCPolySupport.Vec d → ℝ) (hf : ContDiff ℝ 1 f) (i : Fin d) (z : ℝ) : ContDiff ℝ 1 (coordinatePrimitive f i z)

A globally C¹ scalar field has a globally C¹ one-coordinate primitive.

theorem DivergenceFormProcess.coordinatePrimitive_eq_intervalIntegral {d : ℕ} (f : HCPolySupport.Vec d → ℝ) (hf : Continuous f) (i : Fin d) (z : ℝ) (x : HCPolySupport.Vec d) : coordinatePrimitive f i z x = ∫ (s : ℝ) in z..x i, f (Function.update x i s)

The fixed-interval definition equals the ordinary oriented coordinate integral.

theorem DivergenceFormProcess.coordinatePrimitive_hasDerivAt_update {d : ℕ} (f : HCPolySupport.Vec d → ℝ) (hf : Continuous f) (i : Fin d) (z : ℝ) (x : HCPolySupport.Vec d) : HasDerivAt (fun (s : ℝ) => coordinatePrimitive f i z (Function.update x i s)) (f x) (x i)

Varying the selected coordinate differentiates the primitive back to the original scalar field.