Smooth momentum pairings on the source cylinder #
The local momentum identity gives a time-integral formula for every smooth
spatial pairing with the all-time representative from lem:weak-cont-L3.
theorem
ESS.blowup_limit_source_pairing_formulas_with_trace
{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 → ℝ}
(hu :
MeasureTheory.AEStronglyMeasurable u
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hDu :
MeasureTheory.AEStronglyMeasurable Du
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(henergy :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤)
(hp :
MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hL3 :
essSup
(fun (t : ℝ) =>
∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3)
(MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤)
(hgrad :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (i : Fin 3),
CKN.HasWeakGradientOn (CKN.Foundation.Parabolic.vec3Ball 0 1) (fun (x : CKN.Vec 3) => u (x, t) i)
fun (x : CKN.Vec 3) => Du (x, t) i)
(hS3 :
∀ φ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3,
∑ j : Fin 3,
u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3,
∑ j : Fin 3,
Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, 0 z i * φ z i = 0)
:
∃ (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),
(∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)), ‖v t‖ ≤ weakContL3MomentBound.toReal) ∧ Measurable W ∧ (∀ (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)) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-(3 / 4) ^ 2) 0), ∃ (ht : t ∈ Set.Icc (-(3 / 4) ^ 2) 0),
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
W (x, ⟨t, ht⟩)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))]
fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) ∧ (∀
(w :
↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))))),
Continuous fun (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)) =>
∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4), inner ℝ (↑↑(v t) x) (↑↑w x)) ∧ ∀ (ψ : 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)),
(∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4), ∑ i : Fin 3, (↑↑(v t) x).ofLp i * ψ x i) - ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4), ∑ i : Fin 3, (↑↑(v s) x).ofLp i * ψ x i = ∫ (τ : ℝ) in ↑s..↑t, ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ∑ i : Fin 3,
∑ j : Fin 3,
u (x, τ) i * u (x, τ) j * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y i) j x - ∑ i : Fin 3,
∑ j : Fin 3,
Du (x, τ) i j * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y i) j x + p (x, τ) * ∑ i : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y i) i x
One measurable trace representative satisfies every smooth momentum
pairing formula on the closed time interval used in prop:blowup-limit.