Axisymmetry on a fixed ball from axisymmetry on a shrinking core

The reduction of Section sec:reduction:core: at a fixed time t at which the velocity slice u(·, t) is real analytic on B(1), axisymmetry on a core ball B(ρ) with ρ > 0 propagates to all of B(1).

The argument is the one printed after eq:interior:defect. For an angle φ the defect F_φ(x) = u(x, t) - Q_φ u(Q_φ^{-1} x, t) is real analytic on B(1), because the rotation Q_φ is a continuous linear automorphism of the space which preserves the ball. On the core ball F_φ vanishes, since there u agrees with its angular mean and the angular mean is fixed by every rotation. The identity theorem on the connected set B(1) then gives F_φ ≡ 0 on B(1); as φ is arbitrary, u is fixed by every rotation there, which is axisymmetry.

The time variable is a spectator throughout: the analyticity radius and the core radius may depend on t in any way, which is what eq:interior:global:symmetry needs.

Balls centred on the axis are connected

theorem CIV.vec3EuclideanNorm_add_le (x y : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.vec3EuclideanNorm (x + y) ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm x + CKN.Foundation.Parabolic.vec3EuclideanNorm y

The triangle inequality for the Euclidean norm of Vec3.

theorem CIV.convex_vec3Ball_zero (r : ℝ) : Convex ℝ (CKN.Foundation.Parabolic.vec3Ball 0 r)

A ball centred on the axis is convex.

theorem CIV.isPreconnected_vec3Ball_zero (r : ℝ) : IsPreconnected (CKN.Foundation.Parabolic.vec3Ball 0 r)

A ball centred on the axis is connected, so the identity theorem applies on it.

theorem CIV.zero_mem_vec3Ball_zero {r : ℝ} (hr : 0 < r) : 0 ∈ CKN.Foundation.Parabolic.vec3Ball 0 r

theorem CIV.rotZ_mem_spaceTimeSet_vec3Ball_zero (r : ℝ) (I : Set ℝ) (φ : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 r) I) : (rotZ φ z.1, z.2) ∈ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 r) I

A space-time slab over a ball centred on the axis is rotation invariant.

Analyticity of the rotated slice

theorem CIV.analyticOnNhd_rotField_slice {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {t r : ℝ} (hu : ∀ (i : Fin 3), AnalyticOnNhd ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) (CKN.Foundation.Parabolic.vec3Ball 0 r)) (φ : ℝ) : AnalyticOnNhd ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => rotField φ u (x, t)) (CKN.Foundation.Parabolic.vec3Ball 0 r)

If every component of the velocity slice u(·, t) is real analytic on a ball centred on the axis, then so is every component of the rotated slice (ℛ_φ u)(·, t): the rotation is a continuous linear automorphism preserving the ball.

The reduction

theorem CIV.isAxisymmetric_slice_of_analytic_of_core {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {t ρ : ℝ} (hu : ∀ (i : Fin 3), AnalyticOnNhd ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) (CKN.Foundation.Parabolic.vec3Ball 0 1)) (hρ : ρ ∈ Set.Ioc 0 1) (hcore : IsAxisymmetricOn u (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) {t})) : IsAxisymmetricOn u (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) {t})

Axisymmetry from an axisymmetric core. At a time t at which every component of u(·, t) is real analytic on B(1), axisymmetry on a core ball B(ρ) with 0 < ρ ≤ 1 forces axisymmetry on all of B(1); this is the step from eq:interior:core to eq:interior:global:symmetry in the proof of thm:main.

theorem CIV.isAxisymmetricOn_unitCylinder_of_analytic_of_core {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ∀ t ∈ Set.Ioo (-1) 0, ∀ (i : Fin 3), AnalyticOnNhd ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) (CKN.Foundation.Parabolic.vec3Ball 0 1)) (hcore : ∀ t ∈ Set.Ioo (-1) 0, ∃ ρ ∈ Set.Ioo 0 1, IsAxisymmetricOn u (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) {t})) : IsAxisymmetricOn u unitCylinder

The symmetry of eq:interior:global:symmetry. If at every time of (-1, 0) the velocity slice is real analytic on B(1) and axisymmetric on some core ball, then it is axisymmetric on the whole unit cylinder Q. The two radii are allowed to degenerate as t ↑ 0, at unrelated rates.

theorem CIV.isAxisymmetricOn_unitCylinder_of_iteratedFDeriv_bound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsmooth : ∀ t ∈ Set.Ioo (-1) 0, ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) (CKN.Foundation.Parabolic.vec3Ball 0 1)) (hbound : ∀ t ∈ Set.Ioo (-1) 0, ∀ (i : Fin 3), ∀ R' < 1, ∃ (C : ℝ) (K : ℝ), 0 < K ∧ ∀ (n : ℕ), ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 R', ‖iteratedFDeriv ℝ n (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) i) x‖ ≤ C * K ^ n * ↑n.factorial) (hcore : ∀ t ∈ Set.Ioo (-1) 0, ∃ ρ ∈ Set.Ioo 0 1, IsAxisymmetricOn u (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) {t})) : IsAxisymmetricOn u unitCylinder

The same conclusion from the quantitative form of the analyticity of the velocity: on each ball B(R') with R' < 1 the iterated spatial derivatives of every component obey a factorial bound, with constants that may degenerate as R' ↑ 1 and as t ↑ 0. This is the way eq:analytic:interior:velocity is used in the proof of thm:main.