The public statement CIV.Main.gktCriterion

This module proves the statement CIV.gktCriterion: smallness of the scale-invariant L⁴_t L⁶_x quantity of u on top-boundary cylinders at the origin gives boundedness near the origin. The proof is CIV.boundedNearOrigin_of_L4L6_small: Hölder turns the hypothesis into L³ smallness, the Lin pressure estimate is iterated over finitely many scales at base points below the top boundary, and CKN's Theorem A in its top-boundary form concludes. The smoothness of p and f on the open cylinder is not used.

theorem CIV.Main.gktCriterion (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) (hsmall : ∀ (ε : ℝ), 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 ε) : BoundedNearOrigin u

The public statement of the Gustafson–Kang–Tsai criterion, with the exponents p* = 6, q = 4: if the scale-invariant L⁴_t L⁶_x norm of u on the top-boundary cylinders B(r) × (−r², 0) tends to zero with r, then u is bounded near the origin.