Finite-word viscous energy for the actual lifted transport and projected-pressure equation.
noncomputable def
EulerCylinderViscousEnergy.heatEnergyConstant
(period : ℝ)
(K : EulerSpatialSobolevInverse.SmoothCoefficient period)
(c : ℝ)
:
The exact coefficient left after absorbing half the variable-metric heat dissipation.
Equations
- EulerCylinderViscousEnergy.heatEnergyConstant period K c = 2 * ↑K.firstBound ^ 2 / c ^ 2
Instances For
noncomputable def
EulerCylinderViscousEnergy.transportEnergyConstant
(period : ℝ)
(K : EulerSpatialSobolevInverse.SmoothCoefficient period)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(B : NNReal)
:
The actual transport metric correction for a bounded lifted velocity.
Equations
Instances For
theorem
EulerCylinderViscousEnergy.finite_cylinder_viscous_energy
(period : ℝ)
[Fact (0 < period)]
{ι : Type u_1}
[Fintype ι]
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(K : ℝ → EulerSpatialSobolevInverse.SmoothCoefficient period)
(G : EulerSpatialSobolevInverse.SmoothCoefficient period)
(e : ι → ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period))
(t δ c ν : ℝ)
(K' : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))
(e' p forcing : ι → ↥(EulerLiftedGradientSpace.LiftL2 period))
(z : ↥(EulerLiftedGradientSpace.LiftL2 period))
(J : (i : ι) → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 2 (e i t))
(g : ι → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3)
(hrep : ∀ (i : ι), ↑↑(e i t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g i)
(hg :
∀ (i : ι) (x : EulerLiftedGradientSpace.LiftDomain period),
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (g i) x))
(hDg :
∀ (i : ι),
MeasureTheory.MemLp
(fun (x : EulerLiftedGradientSpace.LiftDomain period) =>
fderiv ℝ (EulerMetricTransport.localFieldLift period (g i) x) 0)
2 (EulerLiftedGradientSpace.liftMeasure period))
(hδ : 0 < δ)
(hc : 0 < c)
(hν : 0 ≤ ν)
(hKt : HasDerivAt (fun (s : ℝ) => (K s).operator) K' t)
(het : ∀ (i : ι), HasDerivAt (e i) (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 : ι), e i t ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m)
(hp : ∀ (i : ι), p i ∈ EulerLiftedGradientSpace.gradientSpace period κ m)
(hz : z ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m)
(B : NNReal)
(hzB : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑z x‖ ≤ ↑B)
(heq :
∀ (i : ι),
e' i + EulerRepresentativeMetricEvolution.liftedTransport period κ m (g i) z ⋯ B hzB + G.operator (p i) = forcing i + ν • EulerMetricHeatEnergy.jetLaplacian period (J i))
:
deriv (fun (s : ℝ) => √((EulerFiniteMetricEnergy.familyEnergy (K s).operator fun (i : ι) => e i s) + δ ^ 2)) t ≤ (‖K'‖ + 2 * transportEnergyConstant period (K t) κ m B + 2 * ν * heatEnergyConstant period (K t) c) / (2 * c ^ 2) * √((EulerFiniteMetricEnergy.familyEnergy (K t).operator fun (i : ι) => e i t) + δ ^ 2) + ↑(K t).bound / c * EulerFiniteMetricEnergy.familyNorm forcing
The regularized root of a finite sum of actual cylinder word energies obeys the viscous estimate.