The L⁶ bound from an order-0 annulus bound

This file assembles the L⁶(B(ρ)) bound eq:aniso:closure:elliptic (the Sobolev step of the closure lemma lem:aniso:closure) and the Gustafson–Kang–Tsai smallness hypothesis from a plain order-0 bound on a space–time annulus, instantiating the generic cutoff of l6_ball_bound_of_enstrophy_bound/closure_from_enstrophy_bound with the concrete CKN.canonicalBallCutoff. The last theorem uses the statement CIV.timeZeroSingularSetNull, an input of lem:aniso:annulus.

theorem CIV.gradVec_eq_zero_of_notMem_tsupport {φ : CKN.Foundation.Parabolic.Vec3 → ℝ} {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∉ tsupport φ) : gradVec φ x = 0

A gradient vanishes at a point outside the topological support of the function.

theorem CIV.gradVec_canonicalBallCutoff_eq_zero_of_mem_inner {ρ Rstar : ℝ} (hρ : 0 < ρ) (hρR : ρ < Rstar) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ) : gradVec (CKN.canonicalBallCutoff 0 ρ Rstar) x = 0

The gradient of the canonical ball cutoff vanishes inside the inner ball.

theorem CIV.hMu_canonicalBallCutoff_of_annulus_bound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {ρ Rstar Rlo Rhi tη Mu : ℝ} (hρ : 0 < ρ) (hρR : ρ < Rstar) (hRloρ : Rlo < ρ) (hRstarRhi : Rstar ≤ Rhi) (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rlo < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rhi → ∀ t ∈ Set.Ioo tη 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ Mu) (t : ℝ) : t ∈ Set.Ioo tη 0 → ∀ (x : CKN.Foundation.Parabolic.Vec3), gradVec (CKN.canonicalBallCutoff 0 ρ Rstar) x ≠ 0 → ∑ i : Fin 3, u (x, t) i ^ 2 ≤ Mu ^ 2

If u is bounded by Mu on an annulus {Rlo < |x| < Rhi} × (tη, 0), then the canonical ball cutoff's gradient bound implies the pointwise squared norm bound |u(·,t)|² ≤ Mu² wherever ∇χ ≠ 0.

theorem CIV.l6_ball_bound_of_annulus_bound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {ρ Rstar Rlo Rhi tη a C' : ℝ} (hρ : 0 < ρ) (hρR : ρ < Rstar) (hRloρ : Rlo < ρ) (hRstarRhi : Rstar ≤ Rhi) (hu : ∀ t ∈ Set.Ioo tη 0, ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) (CKN.Foundation.Parabolic.vec3Ball 0 Rstar)) (hdiv : ∀ t ∈ Set.Ioo tη 0, ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) j) x) (CKN.basisVec j) = 0) {Mu : ℝ} (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rlo < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rhi → ∀ t ∈ Set.Ioo tη 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ Mu) (hC' : 0 ≤ C') (hY : ∀ t ∈ Set.Ioo tη 0, (∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.canonicalBallCutoff 0 ρ Rstar x ^ 2 * ∑ i : Fin 3, curlVec (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t)) x i ^ 2) + 1 ≤ C' * (-t) ^ (-a)) : ∃ (C'' : ℝ), 0 ≤ C'' ∧ ∀ t ∈ Set.Ioo tη 0, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 ρ, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 6) ^ (1 / 6) ≤ ENNReal.ofReal (C'' * (-t) ^ (-(a / 2)))

The L⁶ bound on B(ρ) from an order-0 annulus bound: assembles the Sobolev step l6_ball_bound_of_enstrophy_bound with the canonical ball cutoff.

theorem CIV.closure_from_annulus_bound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {ρ Rstar Rlo Rhi tη Cstar η C' : ℝ} (hρ : 0 < ρ) (hρR : ρ < Rstar) (hRloρ : Rlo < ρ) (hRstarRhi : Rstar ≤ Rhi) (hu : ∀ t ∈ Set.Ioo tη 0, ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) (CKN.Foundation.Parabolic.vec3Ball 0 Rstar)) (hdiv : ∀ t ∈ Set.Ioo tη 0, ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) j) x) (CKN.basisVec j) = 0) {Mu : ℝ} (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rlo < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rhi → ∀ t ∈ Set.Ioo tη 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ Mu) (htη : tη < 0) (hCstar : 0 < Cstar) (hη : η = 1 / (16 * Cstar)) (hC' : 0 ≤ C') (hY : ∀ t ∈ Set.Ioo tη 0, (∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.canonicalBallCutoff 0 ρ Rstar x ^ 2 * ∑ i : Fin 3, curlVec (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t)) x i ^ 2) + 1 ≤ C' * (-t) ^ (-(Cstar * η))) (ε : ℝ) : 0 < ε → ∃ (r₀ : ℝ), 0 < r₀ ∧ ∀ (r : ℝ), 0 < r → r < r₀ → ∫⁻ (t : ℝ) in Set.Ioo (-r ^ 2) 0, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 r, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 6) ^ (2 / 3) ≤ ENNReal.ofReal ε

The closure step from an order-0 annulus bound: with η = 1/(16C_*) the annulus bound yields the parabolic smallness hypothesis of the Gustafson–Kang–Tsai criterion.

theorem CIV.closure_from_timeZeroSingularSetNull (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) (hMf : ForceC2Bounded f) (R₁ R₀ : ℝ) (hR₁ : 0 ≤ R₁) (hR₁R₀ : R₁ < R₀) (hR₀ : R₀ < 1) {Cstar : ℝ} (hCstar : 0 < Cstar) (hu : ∀ Rstar < 1, ∀ tη ∈ Set.Ioo (-1) 0, ∀ t ∈ Set.Ioo tη 0, ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) (CKN.Foundation.Parabolic.vec3Ball 0 Rstar)) (hdiv : ∀ Rstar < 1, ∀ tη ∈ Set.Ioo (-1) 0, ∀ t ∈ Set.Ioo tη 0, ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) j) x) (CKN.basisVec j) = 0) (hC' : ∀ (ρ Rstar tη : ℝ), tη ∈ Set.Ioo (-1) 0 → 0 < ρ → ρ < Rstar → Rstar < 1 → ∃ (C' : ℝ), 0 ≤ C' ∧ ∀ t ∈ Set.Ioo tη 0, (∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.canonicalBallCutoff 0 ρ Rstar x ^ 2 * ∑ i : Fin 3, curlVec (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t)) x i ^ 2) + 1 ≤ C' * (-t) ^ (-(Cstar * (1 / (16 * Cstar))))) (ε : ℝ) : 0 < ε → ∃ (r₀ : ℝ), 0 < r₀ ∧ ∀ (r : ℝ), 0 < r → r < r₀ → ∫⁻ (t : ℝ) in Set.Ioo (-r ^ 2) 0, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 r, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 6) ^ (2 / 3) ≤ ENNReal.ofReal ε

The time-zero singular set null implies the L⁶-smallness condition: from the statement CIV.timeZeroSingularSetNull and the order-0 annulus bound exists_annulus_bound_of_timeZeroSingularSetNull, the L⁶ bound on small balls declines to zero as the radius shrinks, which is the parabolic smallness hypothesis of the Gustafson–Kang–Tsai criterion.

The window parameter tη of hu, hdiv and hC' ranges over Ioo (-1) 0, the time interval of the unit cylinder on which the solution class is defined: the radius selection returns its t₀ there, and a tη ≤ -1 would ask for data at times where u is not given.