The C² bound of the averaged force (sec:reduction:core)

CIV/Reduction/AveragedClassical.lean shows that averaging a classical solution's rotated triples over φ ∈ [0, 2π] again yields a classical solution (isClassicalSolutionOn_angularMean) with an axisymmetric force (isAxisymmetricOn_angularMean_force). This module proves the remaining piece design note R8 needs: if the original force is C²-bounded then so is its angular mean, forceC2Bounded_angularMean.

The C² bound of the averaged force

Elementary bounds

Second derivatives of the rotated field

Differentiation under the angular integral

Bounds on the rotated force and on the angular mean

The derivatives of the angular mean as angular averages

Reading the multi-index derivatives of order at most two

The C² bound

theorem CIV.forceC2Bounded_angularMean {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hMf : ForceC2Bounded f) : ForceC2Bounded (angularMean f)

The angular mean of a smooth, C²-bounded force is again C² bounded (eq:interior:force:c-two for the averaged force of design note R8). The spatial derivatives of the mean are the angular means of the corresponding derivatives of the rotated fields, and each of those is a bounded linear combination of the derivatives of the force at the rotated point, so the bound is inherited with an explicit numerical factor.