Morrey Decay Aux

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

theorem CKN.MorreyDecayAux.max_components_le_theta {κ : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hκ : 0 < κ) (hκle : κ ≤ 1) (hα : 0 ≤ alpha u z r) (hβ : 0 ≤ beta u Du z r) : max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ theta κ u Du p z r

theorem CKN.MorreyDecayAux.lambda_le_of_subset {Ω : 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 z' : Foundation.Parabolic.ParabolicPoint} {r R : ℝ} (hr : 0 < r) (hsub : Foundation.Parabolic.parabolicCylinder z.1 z.2 r ⊆ Foundation.Parabolic.parabolicCylinder z'.1 z'.2 R) (hI : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z'.1 z'.2 R, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q < ⊤) : lambda q f z r ≤ r ^ (3 - 5 / q) * (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z'.1 z'.2 R, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q).toReal ^ (1 / q)

theorem CKN.MorreyDecayAux.exists_small_normalized {T L : ℕ → ℝ} {ηd C₂₉ : ℝ} (hηd : 0 < ηd) (hrec : ∀ (n : ℕ), T (n + 1) ≤ 3 / 8 * T n + C₂₉ * L n) (hsource : ∀ (n : ℕ), C₂₉ * L n ≤ ηd / 16) : ∃ (n : ℕ), T n ≤ ηd / 4