Quantitative small-data regularity from the displayed analytic estimates #

The start and iteration produce uniform initial norms. Two pressure-gradient estimates and the literal localized equation supply the velocity improvement and the final closed-cylinder estimate. Every remaining analytic input is displayed explicitly; no regularity conclusion is assumed.

source

theorem CKN.epsilonRegularityL3_provider_of_producers (q C₁₂_p1 C₃₂ C_CZ : ℝ) (hq : 5 / 2 < q) (hC₃₂ : 0 ≤ C₃₂) (hC : 0 ≤ C_CZ) (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))) (hCZ_p1 : ∀ (Ω : 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 : ℝ} (hρ : 0 < ρ), 0 < r → r ≤ ρ / 2 → closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → ENNReal.ofReal (r ^ (-4 / 3)) * MeasureTheory.eLpNorm' (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP1 (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f w.2 w.1) (3 / 2) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 r)) ≤ ENNReal.ofReal (C₁₂_p1 * (r / ρ)⁻¹ * alpha u z ρ * beta u Du z ρ)) (hGA : ∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal), 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → 0 ≤ C_CZ → 0 < R₁ → R₁ < R₀ → R₀ < 3 / 4 → 0 ≤ ε → KU < ⊤ → KD < ⊤ → ∃ KP < ⊤, ∀ {Ω : 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 → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → (∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) → (∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε → ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I U J → U ⊆ Foundation.Parabolic.vec3Ball 0 R₁ → ∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I → ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ≤ KP) (hL : ∀ {Ω : 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 → ∀ {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ}, φ ∈ spaceTimeTestFunction Ω I → ∀ {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ}, localBox Ω I Ω' J → tsupport φ ⊆ Ω' ×ˢ J → ∀ {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, (∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) → (∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, tsupport ψ ⊆ Ω' ×ˢ J → ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) → Core.Step3.localizedVelocity φ u =ᵐ[MeasureTheory.volume] fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Core.HeatPotential.heatPotential (fun (w : Foundation.Parabolic.ParabolicPoint) => Core.Step4.localizedGradientSourceG φ u Du f Dp w i) (fun (j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint) => Core.Step4.localizedGradientSourceH φ u j w i) z) :

The quantitative small-data conclusion follows from the displayed start and theta inequalities, uniform one-sided pressure-gradient estimates, and the literal localized heat representation.

Documentation

LeanPool.CaffarelliKohnNirenberg.Main.TheoremAProvider

Quantitative small-data regularity from the displayed analytic estimates #