The exterior energy estimate eq:reg-tails #
The compact-weight bound of CKN.Leray.RegTailsFinalCore is sent to the
initial time by the L² continuity of the slices, and the compact cutoffs
exhaust the exterior of the ball of radius (R2) (lem:reg-tails). Together with
the initial mollifier tail this is the hypothesis hregTails of
prop:leray-limit.
theorem
CKN.Leray.regTailsFinal_compact_weight_bound_initial
(ρ : RegMollifierProfile)
(uε :
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) →
IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(pε :
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → ℝ)
(hregularised :
∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε : ℝ) (hε : 0 < ε),
have u := uε a ha ε;
have p := pε a ha ε;
have D := fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) =>
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z;
have DD := fun (z : Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) =>
spatialPartial
(fun (y : Foundation.Parabolic.ParabolicPoint) =>
spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y)
k z;
have Dt := fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) z;
have Dp := fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z;
(∃ (hSlice :
∀ (t : ℝ),
0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume),
(Continuous fun (t : ↑(Set.Ici 0)) =>
realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑t)) ⋯) ∧ (fun (x : Foundation.Parabolic.Vec3) => u (x, 0)) =ᵐ[MeasureTheory.volume]
regUniformMollifiedInitial ρ ε hε a ∧ ∀ (t : ℝ), 0 ≤ t → IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ∧ (∀ (i : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i j : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => D z i j)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i j k : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => DD z i j k)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Dt z i)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ ContinuousOn p (spaceTimeSet Set.univ (Set.Ioi 0)) ∧ (∀ (i : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i : Fin 3),
ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0),
∀ (i j : Fin 3),
DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => D (x, z.2) i j) z.1) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0),
DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => p (x, z.2)) z.1) ∧ (∀ (δ T : ℝ),
0 < δ →
δ < T →
∃ (C : ℝ),
0 ≤ C ∧ ∀ z ∈ spaceTimeSet Set.univ (Set.Icc δ T),
Foundation.Parabolic.vec3EuclideanNorm (u z) ≤ C ∧ |p z| ≤ C ∧ (∀ (i j : Fin 3), |D z i j| ≤ C) ∧ (∀ (i j k : Fin 3), |DD z i j k| ≤ C) ∧ (∀ (i : Fin 3), |Dt z i| ≤ C) ∧ ∀ (i : Fin 3), |Dp z i| ≤ C) ∧ (∀ (δ T : ℝ),
0 < δ →
δ < T →
(∀ (i : Fin 3),
MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i j : Fin 3),
MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => D z i j) 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i j k : Fin 3),
MeasureTheory.MemLp
(fun (z : Foundation.Parabolic.ParabolicPoint) => DD z i j k) 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i : Fin 3),
MeasureTheory.MemLp
(fun (z : Foundation.Parabolic.ParabolicPoint) => Dt z i) 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ MeasureTheory.MemLp p 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (z : Foundation.Parabolic.ParabolicPoint),
0 < z.2 →
∀ (i : Fin 3),
Dt z i - ∑ j : Fin 3, DD z i j j + ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε u z j * D z i j + Dp z i = 0) ∧ (∀ (t : ℝ),
0 < t →
∃ (hF :
∀ (i j : Fin 3),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) =>
regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j)
(ENNReal.ofReal 2) MeasureTheory.volume),
((fun (x : Foundation.Parabolic.Vec3) => p (x, t)) =ᵐ[MeasureTheory.volume]
rieszPressureSliceRepresentative 2
regTailsFinal_compact_weight_bound_initial._proof_55 fun (i j : Fin 3) =>
MeasureTheory.MemLp.toLp
(fun (x : Foundation.Parabolic.Vec3) =>
regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j)
⋯) ∧ ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
∫ (x : Foundation.Parabolic.Vec3), p (x, t) * spatialLaplacian ψ x = -∑ i : Fin 3,
∑ j : Fin 3,
∫ (x : Foundation.Parabolic.Vec3), regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j * mixedSecond ψ i j x) ∧ ∀ (t : ℝ),
0 ≤ t →
MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation u D t = MeasureTheory.eLpNorm (regMollifyVector ρ ε hε (regUniformSpatialField a)) 2
MeasureTheory.volume ^ 2)
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(ha : IsInJ a)
(ε : ℝ)
(hε : 0 < ε)
(q : Foundation.Parabolic.Vec3 → ℝ)
(hq : ContDiff ℝ (↑⊤) q)
(hqc : HasCompactSupport q)
(hq0 : ∀ (x : Foundation.Parabolic.Vec3), 0 ≤ q x)
(hq1 : ∀ (x : Foundation.Parabolic.Vec3), q x ≤ 1)
{M : ℝ}
(hM : 0 ≤ M)
(hDq : ∀ (x : Foundation.Parabolic.Vec3) (j : Fin 3), |spatialDeriv q j x| ≤ M)
{t : ℝ}
(ht : 0 ≤ t)
:
regTailsEnergyWeight (uε a ha ε) q t ≤ regTailsEnergyWeight (uε a ha ε) q 0 + (18 * M * (MeasureTheory.eLpNorm (regUniformSpatialField a) 2 MeasureTheory.volume).toReal ^ 2 * t ^ (1 / 2) + regTailsFluxConstant * M * (MeasureTheory.eLpNorm (regUniformSpatialField a) 2 MeasureTheory.volume).toReal ^ 3 * t ^ (1 / 4))
The compact-weight bound of lem:reg-tails from the initial time: for
t ≥ 0 the localized energy at time t is at most the one at time 0 plus
18 M B² t^{1/2} + Q M B³ t^{1/4}.
theorem
CKN.Leray.regTailsFinal_exterior_bound
(ρ : RegMollifierProfile)
(uε :
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) →
IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(pε :
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → ℝ)
(hregularised :
∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε : ℝ) (hε : 0 < ε),
have u := uε a ha ε;
have p := pε a ha ε;
have D := fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) =>
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z;
have DD := fun (z : Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) =>
spatialPartial
(fun (y : Foundation.Parabolic.ParabolicPoint) =>
spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y)
k z;
have Dt := fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) z;
have Dp := fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z;
(∃ (hSlice :
∀ (t : ℝ),
0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume),
(Continuous fun (t : ↑(Set.Ici 0)) =>
realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑t)) ⋯) ∧ (fun (x : Foundation.Parabolic.Vec3) => u (x, 0)) =ᵐ[MeasureTheory.volume]
regUniformMollifiedInitial ρ ε hε a ∧ ∀ (t : ℝ), 0 ≤ t → IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ∧ (∀ (i : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i j : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => D z i j)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i j k : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => DD z i j k)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Dt z i)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ ContinuousOn p (spaceTimeSet Set.univ (Set.Ioi 0)) ∧ (∀ (i : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i : Fin 3),
ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0),
∀ (i j : Fin 3),
DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => D (x, z.2) i j) z.1) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0),
DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => p (x, z.2)) z.1) ∧ (∀ (δ T : ℝ),
0 < δ →
δ < T →
∃ (C : ℝ),
0 ≤ C ∧ ∀ z ∈ spaceTimeSet Set.univ (Set.Icc δ T),
Foundation.Parabolic.vec3EuclideanNorm (u z) ≤ C ∧ |p z| ≤ C ∧ (∀ (i j : Fin 3), |D z i j| ≤ C) ∧ (∀ (i j k : Fin 3), |DD z i j k| ≤ C) ∧ (∀ (i : Fin 3), |Dt z i| ≤ C) ∧ ∀ (i : Fin 3), |Dp z i| ≤ C) ∧ (∀ (δ T : ℝ),
0 < δ →
δ < T →
(∀ (i : Fin 3),
MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i j : Fin 3),
MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => D z i j) 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i j k : Fin 3),
MeasureTheory.MemLp
(fun (z : Foundation.Parabolic.ParabolicPoint) => DD z i j k) 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i : Fin 3),
MeasureTheory.MemLp
(fun (z : Foundation.Parabolic.ParabolicPoint) => Dt z i) 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ MeasureTheory.MemLp p 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (z : Foundation.Parabolic.ParabolicPoint),
0 < z.2 →
∀ (i : Fin 3),
Dt z i - ∑ j : Fin 3, DD z i j j + ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε u z j * D z i j + Dp z i = 0) ∧ (∀ (t : ℝ),
0 < t →
∃ (hF :
∀ (i j : Fin 3),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) =>
regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j)
(ENNReal.ofReal 2) MeasureTheory.volume),
((fun (x : Foundation.Parabolic.Vec3) => p (x, t)) =ᵐ[MeasureTheory.volume]
rieszPressureSliceRepresentative 2
regTailsFinal_compact_weight_bound_initial._proof_55 fun (i j : Fin 3) =>
MeasureTheory.MemLp.toLp
(fun (x : Foundation.Parabolic.Vec3) =>
regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j)
⋯) ∧ ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
∫ (x : Foundation.Parabolic.Vec3), p (x, t) * spatialLaplacian ψ x = -∑ i : Fin 3,
∑ j : Fin 3,
∫ (x : Foundation.Parabolic.Vec3), regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j * mixedSecond ψ i j x) ∧ ∀ (t : ℝ),
0 ≤ t →
MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation u D t = MeasureTheory.eLpNorm (regMollifyVector ρ ε hε (regUniformSpatialField a)) 2
MeasureTheory.volume ^ 2)
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(ha : IsInJ a)
(ε : ℝ)
(hε : 0 < ε)
{R1 R2 t : ℝ}
(hR1 : 0 < R1)
(hR12 : R1 < R2)
(ht : 0 ≤ t)
:
∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R2 < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (uε a ha ε (x, t)) ^ 2 ≤ (∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R1 < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (regUniformMollifiedInitial ρ ε hε a x) ^ 2) + 64 / (R2 - R1) * (18 * (MeasureTheory.eLpNorm (regUniformSpatialField a) 2 MeasureTheory.volume).toReal ^ 2 * t ^ (1 / 2) + regTailsFluxConstant * (MeasureTheory.eLpNorm (regUniformSpatialField a) 2 MeasureTheory.volume).toReal ^ 3 * t ^ (1 / 4))
The exterior energy estimate of lem:reg-tails for one regularized
solution, with the Euclidean L² norm B of the datum.
theorem
CKN.Leray.regTails_of_regularised
(ρ : RegMollifierProfile)
(uε :
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) →
IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(pε :
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → ℝ)
(hregularised :
∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε : ℝ) (hε : 0 < ε),
have u := uε a ha ε;
have p := pε a ha ε;
have D := fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) =>
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z;
have DD := fun (z : Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) =>
spatialPartial
(fun (y : Foundation.Parabolic.ParabolicPoint) =>
spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y)
k z;
have Dt := fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) z;
have Dp := fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z;
(∃ (hSlice :
∀ (t : ℝ),
0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume),
(Continuous fun (t : ↑(Set.Ici 0)) =>
realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑t)) ⋯) ∧ (fun (x : Foundation.Parabolic.Vec3) => u (x, 0)) =ᵐ[MeasureTheory.volume]
regUniformMollifiedInitial ρ ε hε a ∧ ∀ (t : ℝ), 0 ≤ t → IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ∧ (∀ (i : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i j : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => D z i j)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i j k : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => DD z i j k)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Dt z i)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ ContinuousOn p (spaceTimeSet Set.univ (Set.Ioi 0)) ∧ (∀ (i : Fin 3),
ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ (i : Fin 3),
ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i)
(spaceTimeSet Set.univ (Set.Ioi 0))) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0),
∀ (i j : Fin 3),
DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => D (x, z.2) i j) z.1) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0),
DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => p (x, z.2)) z.1) ∧ (∀ (δ T : ℝ),
0 < δ →
δ < T →
∃ (C : ℝ),
0 ≤ C ∧ ∀ z ∈ spaceTimeSet Set.univ (Set.Icc δ T),
Foundation.Parabolic.vec3EuclideanNorm (u z) ≤ C ∧ |p z| ≤ C ∧ (∀ (i j : Fin 3), |D z i j| ≤ C) ∧ (∀ (i j k : Fin 3), |DD z i j k| ≤ C) ∧ (∀ (i : Fin 3), |Dt z i| ≤ C) ∧ ∀ (i : Fin 3), |Dp z i| ≤ C) ∧ (∀ (δ T : ℝ),
0 < δ →
δ < T →
(∀ (i : Fin 3),
MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i j : Fin 3),
MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => D z i j) 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i j k : Fin 3),
MeasureTheory.MemLp
(fun (z : Foundation.Parabolic.ParabolicPoint) => DD z i j k) 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (i : Fin 3),
MeasureTheory.MemLp
(fun (z : Foundation.Parabolic.ParabolicPoint) => Dt z i) 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ MeasureTheory.MemLp p 2
(MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))) ∧ (∀ (z : Foundation.Parabolic.ParabolicPoint),
0 < z.2 →
∀ (i : Fin 3),
Dt z i - ∑ j : Fin 3, DD z i j j + ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε u z j * D z i j + Dp z i = 0) ∧ (∀ (t : ℝ),
0 < t →
∃ (hF :
∀ (i j : Fin 3),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) =>
regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j)
(ENNReal.ofReal 2) MeasureTheory.volume),
((fun (x : Foundation.Parabolic.Vec3) => p (x, t)) =ᵐ[MeasureTheory.volume]
rieszPressureSliceRepresentative 2
regTailsFinal_compact_weight_bound_initial._proof_55 fun (i j : Fin 3) =>
MeasureTheory.MemLp.toLp
(fun (x : Foundation.Parabolic.Vec3) =>
regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j)
⋯) ∧ ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
∫ (x : Foundation.Parabolic.Vec3), p (x, t) * spatialLaplacian ψ x = -∑ i : Fin 3,
∑ j : Fin 3,
∫ (x : Foundation.Parabolic.Vec3), regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j * mixedSecond ψ i j x) ∧ ∀ (t : ℝ),
0 ≤ t →
MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation u D t = MeasureTheory.eLpNorm (regMollifyVector ρ ε hε (regUniformSpatialField a)) 2
MeasureTheory.volume ^ 2)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε : ℝ) (hε : 0 < ε),
ε ≤ 1 →
(∀ (R1 R2 t : ℝ),
0 < R1 →
R1 < R2 →
0 ≤ t →
∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R2 < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (uε a ha ε (x, t)) ^ 2 ≤ (∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R1 < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (regUniformMollifiedInitial ρ ε hε a x) ^ 2) + C * ((MeasureTheory.eLpNorm a 2 MeasureTheory.volume).toReal ^ 2 * t ^ (1 / 2) + (MeasureTheory.eLpNorm a 2 MeasureTheory.volume).toReal ^ 3 * t ^ (1 / 4)) / (R2 - R1)) ∧ ∀ (R1 : ℝ),
0 < R1 →
∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R1 < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (regUniformMollifiedInitial ρ ε hε a x) ^ 2 ≤ ∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R1 - 1 < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (a x) ^ 2
The regularized exterior energy estimate eq:reg-tails together with the
initial mollifier tail (lem:reg-tails): this is the hypothesis hregTails of
prop:leray-limit, with one constant for every datum in J and every
ε ∈ (0, 1].