Small-data decay for Theorem A #
Steps 1 and 2 of the proof of thm:A. theoremA_morrey_decay_of_inputs is
Step 1: the start lemma lem:thmA-start at every centre of the one-sided
cylinder Q_{3/4}, followed by the scale iteration prop:iteration at the
fixed radius r₅ = κ/4, giving the decay eq:thmA-morrey with the constant
M = κ^{-4/3-ε} η r₅^{-ε} and ε = 2/5. The manuscript calls M absolute;
what is proved and used here is that it is fixed before the domain and the
solution.
theoremA_initial_morrey_wide_of_inputs is Step 2: the one-sided Morrey
transfer, giving the three memberships of eq:step2-morrey on the cylinder
of radius 11/16. The manuscript states them on Q₂^♯ of radius 5/8; the
larger radius is proved because the bootstrap round consumes the outer
cylinder and returns the inner one, and the transfer argument needs only
that the radius is below 3/4. The Hölder conclusion of thm:A is not
here: it additionally requires the causal localization and source estimates
of Step 3, through the top time face.
Scaling #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The rescaling identities used to move a centre to the unit cylinder.
theorem
CKN.thmA_scaling_data
(κ μ : ℝ)
(hμ : 0 < μ)
{Ω : 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 : ℝ)
(hr : 0 < r)
:
IsSuitableWeakSolutionIntegrable (rescaledSpace μ z₀.1 Ω) (rescaledTime μ z₀.2 I) q (rescaleVelocity μ z₀ u)
(rescaleGradient μ z₀ Du) (rescalePressure μ z₀ p) (rescaleForce μ z₀ f) ∧ theta κ (rescaleVelocity μ z₀ u) (rescaleGradient μ z₀ Du) (rescalePressure μ z₀ p) (0, 0) r = theta κ u Du p z₀ (μ * r) ∧ beta (rescaleVelocity μ z₀ u) (rescaleGradient μ z₀ Du) (0, 0) r = beta u Du z₀ (μ * r) ∧ gamma (rescaleVelocity μ z₀ u) (0, 0) r = gamma u z₀ (μ * r) ∧ delta (rescalePressure μ z₀ p) (0, 0) r = delta p z₀ (μ * r) ∧ lambda q (rescaleForce μ z₀ f) (0, 0) r = lambda q f z₀ (μ * r)
The parabolic rescaling preserves suitability and transports all four scale quantities to the original centre at the dilated radius.
theorem
CKN.thmA_scaling_step
(κ μ η Λ₀ : ℝ)
(hμ : 0 < μ)
{Ω : 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)
(hstart :
theta κ (rescaleVelocity μ z₀ u) (rescaleGradient μ z₀ Du) (rescalePressure μ z₀ p) (0, 0) (1 / 4) ≤ η ∧ lambda q (rescaleForce μ z₀ f) (0, 0) (1 / 4) ≤ Λ₀)
:
A start estimate at the rescaled unit centre transports to the original centre. The constants occur before the solution data, as in the paper.
theorem
CKN.theoremA_morrey_decay_of_inputs
(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₃₂)
:
∃ (ε₀ : ℝ),
0 < ε₀ ∧ ∀ {Ω : 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 →
∫⁻ (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 ε₀ →
(∀ {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)) →
(∀ {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))) →
(∀ {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 ρ)) →
∀ z ∈ Foundation.Parabolic.vec3Ball 0 (3 / 4) ×ˢ Set.Ioc (-(9 / 16)) 0,
∀ (r : ℝ),
0 < r →
r ≤ iterationKappa C₂₇ / 4 →
max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ iterationKappa C₂₇ ^ (-4 / 3 - iterationEpsilon) * iterationEta C₂₇ * (iterationKappa C₂₇ / 4) ^ (-iterationEpsilon) * r ^ (2 / 5)
A positive uniform small-data threshold yields the decay portion of
thm:A. It is chosen before the domain and the solution. No smallness
inequality for numerical parameters is left as a hypothesis.
theorem
CKN.theoremA_initial_morrey_wide_of_inputs
(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₃₂)
:
have M :=
iterationKappa C₂₇ ^ (-4 / 3 - iterationEpsilon) * iterationEta C₂₇ * (iterationKappa C₂₇ / 4) ^ (-iterationEpsilon);
∃ (ε₀ : ℝ),
0 < ε₀ ∧ ∃ (N : ℕ),
∀ {Ω : 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 →
∫⁻ (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 ε₀ →
(∀ {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)) →
(∀ {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))) →
(∀ {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 ρ)) →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 3)
((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ Core.Endgame.oneSidedVelocityMorreyBound M (iterationKappa C₂₇ / 4) ε₀) ∧ (∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ Core.Endgame.oneSidedGradientMorreyBound M (iterationKappa C₂₇ / 4) N) ∧ Foundation.Parabolic.Morrey.morreyNorm (3 / 2) (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator p) ≤ Core.Endgame.oneSidedPressureMorreyBound M (iterationKappa C₂₇ / 4) ε₀
The small-data start, iteration, and one-sided cylinder transfer give uniform initial Morrey bounds for velocity, gradient, and pressure on the cylinder of radius eleven sixteenths. The constants and positive threshold precede every solution.