Congruence of iterated derivatives for axisymmetric fields

If a vector field is axisymmetric on the unit cylinder, then its angular mean agrees with the field itself there, and consequently every iterated spatial partial derivative of each component of the angular mean agrees with the same derivative of the original field — and the anisotropic ℒ² bounds transfer from the angular mean to the field.

theorem CIV.spatialPartial_iterate_congr_of_eqOn {g h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (heq : Set.EqOn g h unitCylinder) (i : Fin 3) (n : ℕ) : Set.EqOn ((fun (k : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) => CKN.spatialPartial k i)^[n] g) ((fun (k : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) => CKN.spatialPartial k i)^[n] h) unitCylinder

Two scalar fields that agree on the unit cylinder have equal iterated spatial partial derivatives in a fixed direction, at every point of the unit cylinder.

theorem CIV.multiPartial_congr_of_isAxisymmetricOn {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (i : Fin 3) (α : Fin 3 → ℕ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) : multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => angularMean u w i) α z = multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α z

For an axisymmetric field, every multi-index spatial partial derivative of a component of its angular mean agrees with the same derivative of the field itself, at every point of the unit cylinder — the angular mean does not move a field that is already axisymmetric there.

theorem CIV.meridionalPartial_congr_of_isAxisymmetricOn {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (i : Fin 3) (a b : ℕ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) : meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => angularMean u w i) a b z = meridionalPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) a b z

The meridional-plane specialization of the previous theorem: for an axisymmetric field, iterated meridional partial derivatives of the angular mean of a component agree with the same derivatives of the component itself.

theorem CIV.anisotropicBounds_of_isAxisymmetricOn {C h : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hbounds : AnisotropicBounds C h (angularMean u)) : AnisotropicBounds C h u

The anisotropic ℒ² bounds transfer from the angular mean of an axisymmetric field to the field itself — used to convert thm:main's hypothesis AnisotropicBounds C h (angularMean u) into the hypothesis AnisotropicBounds C h u that thm:aniso:main needs, once u is known to be axisymmetric on the unit cylinder.