Relative cross identity for an endpoint Serrin solution #
The endpoint Serrin coefficient makes both oriented convection pairings
integrable; the slice cancellation at a fixed exponent then combines them into
the relative convection form (lem:lps-comparison).
theorem
ESS.lps_endpoint_velocity_convection_integrable
{T : ℝ}
{u w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{β : ℝ → ℝ}
{K : ENNReal}
(k : Fin 3)
(hu :
MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => u z k)
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hw : MeasureTheory.AEStronglyMeasurable w (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hDw : MeasureTheory.AEStronglyMeasurable Dw (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hβmeas : AEMeasurable (fun (τ : ℝ) => ENNReal.ofReal (β τ)) (MeasureTheory.volume.restrict (Set.Ioo 0 T)))
(hβ :
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), |u (x, τ) k| ≤ β τ)
(hβint : ∫⁻ (τ : ℝ) in Set.Ioo 0 T, ENNReal.ofReal (β τ) ^ 2 < ⊤)
(hK : K ≠ ⊤)
(hwK :
∀ (j : Fin 3),
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => w (x, τ) j) 2 MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => w (x, τ) j) 2 MeasureTheory.volume ≤ K)
(hDw2 :
∀ (j : Fin 3),
MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => Dw z k j) 2
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
:
MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => u z k * ∑ j : Fin 3, w z j * Dw z k j)
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))
Integrability of an essentially bounded velocity component against the
advective convection of an L∞_t L²_x ∩ L²_t H¹_x field.
theorem
ESS.lps_endpoint_energy_convection_integrable
{T : ℝ}
{z w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{β : ℝ → ℝ}
{K : ENNReal}
(k : Fin 3)
(hz :
MeasureTheory.AEStronglyMeasurable (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => z q k)
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hw : MeasureTheory.AEStronglyMeasurable w (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hDw : MeasureTheory.AEStronglyMeasurable Dw (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hβmeas : AEMeasurable (fun (τ : ℝ) => ENNReal.ofReal (β τ)) (MeasureTheory.volume.restrict (Set.Ioo 0 T)))
(hβ :
∀ (j : Fin 3),
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), |w (x, τ) j| ≤ β τ)
(hβint : ∫⁻ (τ : ℝ) in Set.Ioo 0 T, ENNReal.ofReal (β τ) ^ 2 < ⊤)
(hK : K ≠ ⊤)
(hzK :
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => z (x, τ) k) 2 MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => z (x, τ) k) 2 MeasureTheory.volume ≤ K)
(hDw2 :
∀ (j : Fin 3),
MeasureTheory.MemLp (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => Dw q k j) 2
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
:
MeasureTheory.Integrable (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => z q k * ∑ j : Fin 3, w q j * Dw q k j)
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))
Integrability of an L∞_t L²_x velocity component against the advective
convection of an essentially bounded L²_t L∞_x field.
theorem
ESS.lps_endpoint_relative_cross_identity
{T : ℝ}
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{pu pv : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hULH : CKN.IsLerayHopfSolution T a u Du)
(hVLH : CKN.IsLerayHopfSolution T a v Dv)
(hU : IsSerrinWeakSolution T a u Du pu)
(hV : IsSerrinWeakSolution T a v Dv pv)
(hEndpoint :
∫⁻ (t : ℝ) in Set.Ioo 0 T, essSup
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))))
MeasureTheory.volume ^ 2 < ⊤)
:
(∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, v (x, t) k * u (x, t) k) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, a x k * a x k = (-∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), lpsRelativeConvection u v Du Dv z) - 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du z k j * Dv z k j) ∧ MeasureTheory.Integrable (lpsRelativeConvection u v Du Dv)
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))
The endpoint Serrin cross-testings combine into the relative cross
identity. The two oriented densities are u · ((v · ∇)v) and v · ((u · ∇)u);
their cancellation uses only the integrable products in the slice lemma.