Interpolation

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

noncomputable def CKN.gagliardoConstant : ℝ

Positive coefficient for the scale-normalized velocity interpolation estimate.

Equations

• CKN.gagliardoConstant = 1 + (81 * ENNReal.ofReal √3 * Classical.choose CKN.interpolationBall_three_finite).toReal

theorem CKN.gamma_le_gagliardo_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I) : gamma u z r ≤ gagliardoConstant * alpha u z r ^ (1 / 2) * beta u Du z r ^ (1 / 2) + gagliardoConstant * alpha u z r