Finite-family viscous metric energy for actual finite Sobolev solutions.

theorem EulerSobolevViscousEnergy.finite_sobolev_viscous_energy (period : ℝ) [Fact (0 < period)] {ι : Type u_1} [Fintype ι] {q : ℕ} (hq : 3 ≤ q) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : ℝ → EulerSpatialSobolevInverse.SmoothCoefficient period) (G : EulerSpatialSobolevInverse.SmoothCoefficient period) (e : ι → ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)) (t δ c ν : ℝ) (K' : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (e' p forcing : ι → ↥(EulerLiftedGradientSpace.LiftL2 period)) (z : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hδ : 0 < δ) (hc : 0 < c) (hν : 0 ≤ ν) (hKt : HasDerivAt (fun (s : ℝ) => (K s).operator) K' t) (het : ∀ (i : ι), HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period (e i s)) (e' i) t) (hsym : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ (((K t).coefficient x) v) w = inner ℝ v (((K t).coefficient x) w)) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (((K t).coefficient x) v) v) (hKG : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), ((K t).coefficient x) ((G.coefficient x) v) = v) (hediv : ∀ (i : ι), EulerCylinderSobolevSpace.value period (e i t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hp : ∀ (i : ι), p i ∈ EulerLiftedGradientSpace.gradientSpace period κ m) (hz : EulerCylinderSobolevSpace.value period z ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (B : NNReal) (hzB : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑(EulerCylinderSobolevSpace.value period z) x‖ ≤ ↑B) (heq : ∀ (i : ι), e' i + (EulerSobolevMetricTransport.transportOperator period hq κ m z) ((EulerCylinderSobolevSpace.restrictOperator period finite_sobolev_viscous_energy._proof_1) (e i t)) + G.operator (p i) = forcing i + ν • EulerMetricHeatEnergy.jetLaplacian period (EulerCylinderSobolevSpace.toJet period (e i t))) : deriv (fun (s : ℝ) => √((EulerFiniteMetricEnergy.familyEnergy (K s).operator fun (i : ι) => EulerCylinderSobolevSpace.value period (e i s)) + δ ^ 2)) t ≤ (‖K'‖ + 2 * EulerCylinderViscousEnergy.transportEnergyConstant period (K t) κ m B + 2 * ν * EulerCylinderViscousEnergy.heatEnergyConstant period (K t) c) / (2 * c ^ 2) * √((EulerFiniteMetricEnergy.familyEnergy (K t).operator fun (i : ι) => EulerCylinderSobolevSpace.value period (e i t)) + δ ^ 2) + ↑(K t).bound / c * EulerFiniteMetricEnergy.familyNorm forcing

The genuine finite-word viscous metric estimate for H² fields and an Hq advecting velocity, q≥3. No classical smooth representative of the evolving fields is required.