Standing data of the zoom argument of prop:aniso:small

Under the hypotheses of thm:aniso:main the proof of prop:aniso:small works with the angle-averaged pressure and force (Section sec:aniso:identities: "averaging over rotations ... we may take π and f axisymmetric"), and with the circulation bound eq:aniso:zoom:circulation on a window B(R_*) × (t_*, 0) with ρ < R_* < 1, which lem:aniso:annulus supplies. This module packages both.

The averaged pair enters only through its classical equations (CIV.isClassicalSolutionOn_angularMean); the regular annulus is obtained from the original suitable solution (CIV.exists_annulus_bound_of_timeZeroSingularSetNull), and the circulation bound from the maximum principle for the circulation equation of the averaged classical system (CIV.forall_Rstar_exists_circulation_bound_ball_of_annulus_bound), whose force is the axisymmetric angular mean.

theorem CIV.exists_zoom_standing_data (q : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p f) (henergy : GlobalEnergyClass u Du p) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hp : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder) (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (hMf : ForceC2Bounded f) {ρ : ℝ} (hρ : ρ ∈ Set.Ioo 0 1) : IsClassicalSolutionOn u (angularMeanScalar p) (angularMean f) unitCylinder ∧ IsAxisymmetricOn (angularMean f) unitCylinder ∧ ForceC2Bounded (angularMean f) ∧ ∃ (Rstar : ℝ) (tstar : ℝ) (CΓ : ℝ), ρ < Rstar ∧ Rstar < 1 ∧ tstar ∈ Set.Ioo (-1) 0 ∧ 0 ≤ CΓ ∧ ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, ∀ t ∈ Set.Ioo tstar 0, |circulation u (x, t)| ≤ CΓ

The standing data of the zoom argument in the proof of prop:aniso:small: the classical equations with the angle-averaged pressure and force, the axisymmetry and C² bound of the averaged force, and the circulation bound eq:aniso:zoom:circulation on B(R_*) × (t_*, 0) for some ρ < R_* < 1.