Fixed constants for the initial gamma estimate

The gamma estimate uses its own numerical velocity constant. The force constant is the same explicit q-dependent constant as in Caccioppoli. Neither constant depends on the domain or the solution.

noncomputable def CKN.Core.Endgame.startGammaConstant : ℝ

A common constant for the three velocity/pressure terms of the gamma estimate.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Core.Endgame.caccioppoli_gamma_display_fixed {Ω : 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 ρ : ℝ} : 0 < ρ → 0 < r → r ≤ ρ / 2 → closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → alpha u z r + beta u Du z r ≤ startGammaConstant * (r / ρ * gamma u z ρ + (r / ρ) ^ (-1) * gamma u z ρ ^ (3 / 2) + (r / ρ) ^ (-1) * delta p z ρ * gamma u z ρ ^ (1 / 2)) + caccioppoliC₂₆ q * (r / ρ) ^ (-1 / 2) * gamma u z ρ ^ (1 / 2) * lambda q f z ρ ^ (1 / 2)

The initial gamma display with all numerical comparison premises discharged.