Interior spatial analyticity of classical solutions

The proof of thm:analytic:interior. On nested regions of depth τ ∈ (0, 1] inside a compactly contained cylinder, the weighted derivatives (τ d)^k |∂^α g| of the velocity components and the pressure are bounded by the majorant b_k ≤ M K^k k!, by induction on k: the one-step estimate on a backward window one geometric step deeper, the absorption of the provisional top-order bound, and the majorant arithmetic. At depth 1 this is the bound AnalyticBoundOn u R' [s₁, s₂] M (d / K).

theorem CIV.kahane_compact_order_bound {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hg : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) (CKN.spaceTimeSet Ω I)) {Kc : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hK : IsCompact Kc) (hKS : ∀ z ∈ Kc, z.1 ∈ Ω ∧ z.2 ∈ I) (k : ℕ) : ∃ (N : ℝ), 0 ≤ N ∧ ∀ z ∈ Kc, ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k → |multiPartial g γ z| ≤ N

Compactness gives a finite bound at each fixed derivative order.

theorem CIV.kahane_region_bound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hsol : IsClassicalSolutionOn u p f (CKN.spaceTimeSet Ω I)) {R' d s₁ s₂ : ℝ} (hreg : ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x ≤ R' + d → s₁ - d ^ 2 ≤ t → t ≤ s₂ → x ∈ Ω ∧ t ∈ I) (k : ℕ) : ∃ (N : ℝ), 0 ≤ N ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x ≤ R' + d → s₁ - d ^ 2 ≤ t → t ≤ s₂ → ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k → (∀ (i : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) γ (x, t)| ≤ N) ∧ |multiPartial p γ (x, t)| ≤ N

A finite bound at each fixed order for the velocity components and the pressure on the closed outer region.

theorem CIV.kahane_level_step : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Ω : Set CKN.Foundation.Parabolic.Vec3) (I : Set ℝ) (R' d s₁ s₂ M K Mf af : ℝ) (k : ℕ), IsOpen Ω → IsOpen I → IsClassicalSolutionOn u p f (CKN.spaceTimeSet Ω I) → 0 < d → d ≤ 1 → 1 ≤ M → 0 < af → 0 ≤ Mf → Mf * (1 + 3 / af) ≤ M → 12800 * C ^ 2 * (1 + M) ≤ K → 1 / af ≤ K → 1 ≤ K → 1 ≤ k → (∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x ≤ R' + d → s₁ - d ^ 2 ≤ t → t ≤ s₂ → x ∈ Ω ∧ t ∈ I) → (∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x ≤ R' + d → s₁ - d ^ 2 ≤ t → t ≤ s₂ → ∀ (γ : Fin 3 → ℕ) (i : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) γ (x, t)| ≤ Mf * af ^ (-↑(γ 0 + γ 1 + γ 2)) * ↑(γ 0 + γ 1 + γ 2).factorial) → (∀ j ≤ k, ∀ (τ : ℝ), 0 < τ → τ ≤ 1 → ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x < R' + (1 - τ) * d → s₁ - (1 - τ) * d ^ 2 ≤ t → t ≤ s₂ → ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = j → (∀ (i : Fin 3), (τ * d) ^ j * |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) γ (x, t)| ≤ kahaneMajorant M K j) ∧ (τ * d) ^ j * |multiPartial p γ (x, t)| ≤ kahaneMajorant M K j) → ∀ (τ : ℝ), 0 < τ → τ ≤ 1 → ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x < R' + (1 - τ) * d → s₁ - (1 - τ) * d ^ 2 ≤ t → t ≤ s₂ → ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k + 1 → (∀ (i : Fin 3), (τ * d) ^ (k + 1) * |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) γ (x, t)| ≤ kahaneMajorant M K (k + 1)) ∧ (τ * d) ^ (k + 1) * |multiPartial p γ (x, t)| ≤ kahaneMajorant M K (k + 1)

The weighted bound at order k + 1 from the weighted bounds at orders ≤ k, by absorbing the provisional bound (the compactness bound halves at each iteration).

theorem CIV.kahane_levels {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hsol : IsClassicalSolutionOn u p f (CKN.spaceTimeSet Ω I)) {R' d s₁ s₂ Mf af : ℝ} (hd : 0 < d) (hd1 : d ≤ 1) (haf : 0 < af) (hMf : 0 ≤ Mf) (hreg : ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x ≤ R' + d → s₁ - d ^ 2 ≤ t → t ≤ s₂ → x ∈ Ω ∧ t ∈ I) (hforce : ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x ≤ R' + d → s₁ - d ^ 2 ≤ t → t ≤ s₂ → ∀ (γ : Fin 3 → ℕ) (i : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) γ (x, t)| ≤ Mf * af ^ (-↑(γ 0 + γ 1 + γ 2)) * ↑(γ 0 + γ 1 + γ 2).factorial) : ∃ (M : ℝ) (K : ℝ), 1 ≤ M ∧ 1 ≤ K ∧ ∀ (k : ℕ) (τ : ℝ), 0 < τ → τ ≤ 1 → ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x < R' + (1 - τ) * d → s₁ - (1 - τ) * d ^ 2 ≤ t → t ≤ s₂ → ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k → (∀ (i : Fin 3), (τ * d) ^ k * |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) γ (x, t)| ≤ kahaneMajorant M K k) ∧ (τ * d) ^ k * |multiPartial p γ (x, t)| ≤ kahaneMajorant M K k

The weighted bounds (τ d)^k |∂^α g| ≤ b_k at every depth τ and every order k, by strong induction on the order.

theorem CIV.kahane_analyticBoundOn {R t₁ t₂ : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u p f (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo t₁ t₂))) (hf : LocallyUniformlyAnalyticOn f R t₁ t₂) {R' : ℝ} (hR' : R' < R) {s₁ s₂ : ℝ} (hs₁ : t₁ < s₁) (hs₂ : s₂ < t₂) : ∃ (M : ℝ) (a : ℝ), 0 < a ∧ AnalyticBoundOn u R' (Set.Icc s₁ s₂) M a

The analyticity bound of thm:analytic:interior on one compactly contained cylinder.

theorem CIV.kahane_interiorAnalyticity (R t₁ t₂ : ℝ) (hR : 0 < R) (ht : t₁ < t₂) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u p f (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo t₁ t₂))) (hf : LocallyUniformlyAnalyticOn f R t₁ t₂) : LocallyUniformlyAnalyticOn u R t₁ t₂

thm:analytic:interior: a classical solution of eq:nse:forced on B(R) × (t₁, t₂) with a locally uniformly spatially analytic force is locally uniformly spatially analytic.