Locally Uniformly Analytic On

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

def CIV.LocallyUniformlyAnalyticOn (g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (R t₁ t₂ : ℝ) : Prop

Spatial analyticity of a field, locally uniformly on cylinders compactly contained in B(R) × (t₁, t₂): eq:analytic:interior:force / eq:analytic:interior:velocity.

Equations

• CIV.LocallyUniformlyAnalyticOn g R t₁ t₂ = ∀ R' < R, ∀ (s₁ s₂ : ℝ), t₁ < s₁ → s₂ < t₂ → ∃ (M : ℝ) (a : ℝ), 0 < a ∧ CIV.AnalyticBoundOn g R' (Set.Icc s₁ s₂) M a