The Duhamel fixed point is a finite-energy weak solution #
This file proves the bundle clauses of prop:pv-local-solution: a fixed point
U = heatOrbit a + forcedHeat G, G = -(U ⊗ U + p I) cut off to the slab
ℝ³ × (0, σ) with the canonical Riesz pressure p, which lies in L⁵ ∩ L⁴ of
the slab and attains the datum at time zero, is a finite-energy weak solution
of the Navier–Stokes equations on ℝ³ × (0, σ) with pressure p and with the
sum of the gradients of the two parts as its weak gradient.
theorem
ESS.pvLocal_canonical_bundle
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(ha : CKN.IsInJ a)
{σ : ℝ}
(hσ : 0 < σ)
{U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hU5 :
MeasureTheory.MemLp U (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))))
(hU4 :
MeasureTheory.MemLp U (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))))
(hfix : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ≠ 0 → U z = pvLocalMap a σ U z)
(hinit : ∀ (x : CKN.Foundation.Parabolic.Vec3), U (x, 0) = a x)
:
∃ (DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3),
IsSerrinWeakSolution σ a U DU (pvSlabPressure σ U)
The Duhamel fixed point of prop:pv-local-solution is a finite-energy weak
solution with the canonical pressure. The L³ bound of the datum enters only
through the construction of the fixed point and is not used here.
theorem
ESS.pvLocal_bundle
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(ha : CKN.IsInJ a)
{σ : ℝ}
(hσ : 0 < σ)
{U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hU5 :
MeasureTheory.MemLp U (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))))
(hU4 :
MeasureTheory.MemLp U (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))))
(hfix : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ≠ 0 → U z = pvLocalMap a σ U z)
(hinit : ∀ (x : CKN.Foundation.Parabolic.Vec3), U (x, 0) = a x)
:
∃ (DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p :
CKN.Foundation.Parabolic.ParabolicPoint → ℝ), IsSerrinWeakSolution σ a U DU p
The local Duhamel fixed point has a finite-energy weak solution bundle.