Uniform one-sided gradient Morrey bounds

A finite geometric cover bounds the total gradient integral using only the small-cylinder decay constant. The cover is selected before the solution, so no solution-dependent large-scale integral enters the bound.

noncomputable def CKN.Core.Endgame.oneSidedGradientMorreyBound (M r₀ : ℝ) (N : ℕ) : ENNReal

Gradient Morrey constant associated with a finite geometric cover.

Equations

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

theorem CKN.Core.Endgame.oneSidedGradientMorreyBound_lt_top (M r₀ : ℝ) (N : ℕ) : oneSidedGradientMorreyBound M r₀ N < ⊤

Every finite cover gives a finite quantitative gradient bound.

theorem CKN.Core.Endgame.oneSided_gradient_morrey_of_decay (M r₀ : ℝ) (hM : 0 ≤ M) (hr₀ : 0 < r₀) (hrquarter : r₀ ≤ 1 / 4) : ∃ (N : ℕ), ∀ {Ω : 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}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → (∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4), ∀ (r : ℝ), 0 < r → r ≤ r₀ → max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ M * r ^ (2 / 5)) → ∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ oneSidedGradientMorreyBound M r₀ N

Uniform decay gives a quantitative gradient Morrey bound. The covering number is chosen before all domains and solutions.