Pressure-side comparisons for the Tsai excess quantities.

theorem CKN.tsaiPressureExcess_le_two_three_halves_delta_cube {Ω : 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) : tsaiPressureExcess p z r ≤ 2 ^ (3 / 2) * delta p z r ^ 3

theorem CKN.tsaiPhi_le_two_gamma_add_two_delta_sq {Ω : 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) : tsaiPhi u p z r ≤ 2 * gamma u z r + 2 * delta p z r ^ 2

theorem CKN.tsaiPsi_le_C3_gamma {Ω : 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) : tsaiPsi u z r ≤ (4 * Real.pi / 3) ^ (-1 / 3) * gamma u z r