The energy equality (R5) at every nonnegative time #
For a velocity whose nonnegative-time slices represent the global regularized
mild curve, whose first spatial partial derivatives are continuous and which
is jointly continuously differentiable at positive times, the interval energy
equality of thm:regularised (R5) holds at every nonnegative time.
@[instance_reducible]
The product normed additive group structure for the regularized R⁵ space-time argument.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[instance_reducible]
The real normed-space structure for the regularized R⁵ space-time argument.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.Leray.regR12_R5
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(ha : IsInJ a)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(hCurve :
∀ (t : ℝ),
0 ≤ t →
(fun (x : Foundation.Parabolic.Vec3) => u (x, t)) =ᵐ[MeasureTheory.volume]
realVectorL2Representative (regR12Curve ρ ε hε a ha t))
(hDprod :
∀ (i j : Fin 3),
ContinuousOn
(fun (z : Foundation.Parabolic.Vec3 × ℝ) =>
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j (z.1, z.2))
(Set.univ ×ˢ Set.Ioi 0))
(hC1 :
∀ (i : Fin 3),
ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0)))
(t : ℝ)
:
0 ≤ t →
MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation u
(fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) =>
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z)
t = MeasureTheory.eLpNorm (regMollifyVector ρ ε hε (regUniformSpatialField a)) 2 MeasureTheory.volume ^ 2
thm:regularised (R5) at every nonnegative time.