Uniform initial bounds from the three displayed inequalities #

The positive smallness threshold and all numerical norm bounds precede the domain and the solution. The proof consumes the actual start and iteration route on the wider cylinder needed for the first localization.

source

theorem CKN.Core.Endgame.theoremA_initial_uniform_of_displays (q C₂₅ C₂₆ C₂₇ C₂₈ C₃₂ : ℝ) (hq : 5 / 2 < q) (hC₂₇ : 0 < C₂₇) (hC₂₈ : 0 < C₂₈) (hC₂₅ : 0 ≤ C₂₅) (hC₂₆ : 0 ≤ C₂₆) (hC₃₂ : 0 ≤ C₃₂) (hCaccGamma : ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {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}, 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 ≤ C₂₅ * (r / ρ * gamma u z ρ + (r / ρ) ^ (-1) * gamma u z ρ ^ (3 / 2) + (r / ρ) ^ (-1) * delta p z ρ * gamma u z ρ ^ (1 / 2)) + C₂₆ * (r / ρ) ^ (-1 / 2) * gamma u z ρ ^ (1 / 2) * lambda q f z ρ ^ (1 / 2)) (hLin34 : ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {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}, 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 → pressureD p z r ≤ C₃₂ * ((ρ / r) ^ 2 * pressureChat u z ρ + r / ρ * pressureD p z ρ + (r / ρ) ^ (3 / 2) * lambda q f z ρ ^ (3 / 2))) (hThetaDecay : ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {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}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ {w : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ}, 0 < ρ → closure (Foundation.Parabolic.parabolicCylinder w.1 w.2 ρ) ⊆ spaceTimeSet Ω I → theta (iterationKappa C₂₇) u Du p w (iterationKappa C₂₇ * ρ) ≤ C₂₇ * iterationKappa C₂₇ ^ (2 / 3) * theta (iterationKappa C₂₇) u Du p w ρ + C₂₇ * iterationKappa C₂₇ ^ (-5) * (beta u Du w ρ ^ (1 / 2) + beta u Du w ρ) * theta (iterationKappa C₂₇) u Du p w ρ + C₂₈ * iterationKappa C₂₇ ^ (-1 / 2) * theta (iterationKappa C₂₇) u Du p w ρ ^ (1 / 2) * lambda q f w ρ ^ (1 / 2) + C₂₈ * iterationKappa C₂₇ ^ (-3) * lambda q f w ρ ∧ (theta (iterationKappa C₂₇) u Du p w ρ ≤ 1 → theta (iterationKappa C₂₇) u Du p w (iterationKappa C₂₇ * ρ) ≤ C₂₇ * iterationKappa C₂₇ ^ (2 / 3) * theta (iterationKappa C₂₇) u Du p w ρ + 2 * C₂₇ * iterationKappa C₂₇ ^ (-5) * theta (iterationKappa C₂₇) u Du p w ρ ^ (1 / 2) * theta (iterationKappa C₂₇) u Du p w ρ + C₂₈ * iterationKappa C₂₇ ^ (-1 / 2) * theta (iterationKappa C₂₇) u Du p w ρ ^ (1 / 2) * lambda q f w ρ ^ (1 / 2) + C₂₈ * iterationKappa C₂₇ ^ (-3) * lambda q f w ρ)) :

Uniform displayed estimates supply uniform initial velocity and gradient Morrey bounds on the cylinder of radius eleven sixteenths.

Documentation

LeanPool.CaffarelliKohnNirenberg.Core.Endgame.InitialUniform

Uniform initial bounds from the three displayed inequalities #