Gkt Smallness

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

theorem CIV.gkt_smallness_of_l6_bound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {ρ C β tη : ℝ} (hρ : 0 < ρ) (hC : 0 ≤ C) (hβ : 0 ≤ β ∧ 4 * β < 1) (htη : tη < 0) (hbound : ∀ 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) ^ (-β))) (ε : ℝ) : 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 ε

Smallness of the (2/3)-power of the L^6 spatial integral follows from the L^6 bound over B(0,ρ): lemma lem:aniso:closure in arXiv:2609.20803.