Rescaled equations on the unit cylinder

Continuing the rescaling step of lem:pv-positive-bound: the divergence-free condition, the momentum identity with pressure, and the L^{3/2} pressure bound pass from the slab ℝ³ × (0, T) to the rescaled fields on the unit cylinder B₁ × (-1, 0), for cylinders ending at any time t₀ ≤ T.

theorem ESS.pv_unit_pressure_memLp {T t₀ R : ℝ} (x₀ : CKN.Foundation.Parabolic.Vec3) (hR : 0 < R) (hlow : R ^ 2 ≤ t₀) (hup : t₀ ≤ T) {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : MeasureTheory.MemLp (CKN.rescalePressure R (x₀, t₀) p) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))

The rescaled pressure lies in L^{3/2} of the unit cylinder.

theorem ESS.pv_unit_divergence {T t₀ R : ℝ} (x₀ : CKN.Foundation.Parabolic.Vec3) (hR : 0 < R) (hlow : R ^ 2 ≤ t₀) (hup : t₀ ≤ T) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hS2 : ∀ ψ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 T), MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, u z i * CKN.spatialPartial ψ i z) (tsupport ψ) MeasureTheory.volume ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ∑ i : Fin 3, u z i * CKN.spatialPartial ψ i z = 0) (ψ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : ψ ∈ 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, CKN.rescaleVelocity R (x₀, t₀) u z i * CKN.spatialPartial ψ i z = 0

The rescaled velocity is divergence free on the unit cylinder.

theorem ESS.pv_unit_momentum {T t₀ R : ℝ} (x₀ : CKN.Foundation.Parabolic.Vec3) (hR : 0 < R) (hlow : R ^ 2 ≤ t₀) (hup : t₀ ≤ T) {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 → ℝ} (hS3 : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 T), MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => -∑ i : Fin 3, u z i * CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ w i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ w i) i z - ∑ i : Fin 3, 0 z i * φ z i) (tsupport φ) MeasureTheory.volume ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ i : Fin 3, u z i * CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ w i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ w i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ w i) i z - ∑ i : Fin 3, 0 z i * φ z i = 0) (φ : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : φ ∈ 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, CKN.rescaleVelocity R (x₀, t₀) u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, CKN.rescaleVelocity R (x₀, t₀) u z i * CKN.rescaleVelocity R (x₀, t₀) u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, CKN.rescaleGradient R (x₀, t₀) Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - CKN.rescalePressure R (x₀, t₀) 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

The rescaled fields satisfy the momentum identity with the rescaled pressure on the unit cylinder.