Endpoint pairing moduli from the source momentum equation #
The all-time source trace formula, affine spatial change, and local momentum flux bounds give the time modulus on every closed rescaled interval.
theorem
ESS.blowup_limit_rescaled_trace_pairing_modulus_of_source_flux
(v :
↑(Set.Icc (-(3 / 4) ^ 2) 0) →
↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 3
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)))))
(W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3)
(hW :
∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)),
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
W (x, t)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))]
fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.weakContL3OfLp (↑↑(v t) x))
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{x₀ : CKN.Foundation.Parabolic.Vec3}
(hsourceFormula :
∀ (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4) →
∀ (s t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)),
(∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4), ∑ i : Fin 3, (↑↑(v t) y).ofLp i * ψ y i) - ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4), ∑ i : Fin 3, (↑↑(v s) y).ofLp i * ψ y i = ∫ (τ : ℝ) in ↑s..↑t, ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ∑ i : Fin 3,
∑ j : Fin 3,
u (y, τ) i * u (y, τ) j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => ψ z i) j y - ∑ i : Fin 3,
∑ j : Fin 3,
Du (y, τ) i j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => ψ z i) j y + p (y, τ) * ∑ i : Fin 3, CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => ψ z i) i y)
{C : Set CKN.Foundation.Parabolic.Vec3}
(hC : IsCompact C)
(a b : ℝ)
(hb : b ≤ 0)
(r : ℕ → ℝ)
(hr : ∀ (n : ℕ), 0 < r n)
(himage :
∀ (n : ℕ),
(fun (x : CKN.Foundation.Parabolic.Vec3) => x₀ + r n • x) '' C ⊆ CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))
(t₀ : ℝ)
(ht₀ : t₀ ≤ 0)
(htime : ∀ (n : ℕ), ∀ τ ∈ Set.Icc a b, t₀ + r n ^ 2 * τ ∈ Set.Icc (-(3 / 4) ^ 2) 0)
(Mvel Mgrad Mpress Mtest Mdiv : ENNReal)
(hMvel : Mvel < ⊤)
(hMgrad : Mgrad < ⊤)
(hMpress : Mpress < ⊤)
(hMtest : Mtest < ⊤)
(hMdiv : Mdiv < ⊤)
(hU :
∀ (n : ℕ) (i : Fin 3),
MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => blowupVelocity x₀ t₀ (r n) u z i) 3
(MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => blowupVelocity x₀ t₀ (r n) u z i) 3
(MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ≤ Mvel)
(hDU :
∀ (n : ℕ) (i j : Fin 3),
MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => blowupGradient x₀ t₀ (r n) Du z i j) 2
(MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => blowupGradient x₀ t₀ (r n) Du z i j) 2
(MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ≤ Mgrad)
(hP :
∀ (n : ℕ),
MeasureTheory.MemLp (blowupPressure x₀ t₀ (r n) p) (3 / 2) (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ∧ MeasureTheory.eLpNorm (blowupPressure x₀ t₀ (r n) p) (3 / 2) (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ≤ Mpress)
(w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3)
(hw : ContDiff ℝ (↑⊤) w)
(hwsupport : tsupport w ⊆ C)
(hDw :
∀ (i j : Fin 3),
MeasureTheory.MemLp
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => (w x).ofLp i) j z.1)
⊤ (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ∧ MeasureTheory.eLpNorm
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => (w x).ofLp i) j z.1)
⊤ (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ≤ Mtest)
(hdivw :
MeasureTheory.MemLp
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
∑ i : Fin 3, CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => (w x).ofLp i) i z.1)
⊤ (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ∧ MeasureTheory.eLpNorm
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
∑ i : Fin 3, CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => (w x).ofLp i) i z.1)
⊤ (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ≤ Mdiv)
:
∃ (A : ℝ) (B : ℝ) (θ : ℝ),
0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : ℝ),
s ∈ Set.Icc a b →
t ∈ Set.Icc a b →
|(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, blowupLimitTraceRescaling W x₀ t₀ (r n) (x, t) i * (w x).ofLp i) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, blowupLimitTraceRescaling W x₀ t₀ (r n) (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ
Uniform local flux bounds and the source momentum formula control all rescaled trace pairings, including pairings at time zero.