L4 L6

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

theorem CIV.lintegral_l4l6_le_of_l6_bound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {ρ C β : ℝ} (hC : 0 ≤ C) (hβ : 0 ≤ β ∧ 4 * β < 1) {tη : ℝ} (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) ^ (-β))) (r : ℝ) : 0 < r → r ≤ ρ → r ^ 2 ≤ -tη → ∫⁻ (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 (C ^ 4 * r ^ (2 * (1 - 4 * β)) / (1 - 4 * β))