Higher Bounds

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

theorem CKN.Foundation.Heat.heatKernelSpaceThirdDerivative_abs_le_rho_inv_six {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) (i j k : Fin 3) : |heatKernelSpaceThirdDerivative x t i j k| ≤ 1000000000000 / rhoTwo x t ^ 6

theorem CKN.Foundation.Heat.heatKernelSpaceFourthDerivative_abs_le_rho_inv_seven {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) (i j k l : Fin 3) : |heatKernelSpaceFourthDerivative x t i j k l| ≤ 1000000000000000000000000000000 / rhoTwo x t ^ 7