The actual nonlinear viscosity-difference PDE implies a fixed squared metric energy inequality.
@[instance_reducible]
noncomputable def
EulerCorrectionDifferenceMetric.metricSobolevGroup
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
The existing Sobolev normed-group instance for the literal metric difference equation.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerCorrectionDifferenceMetric.metricSobolevSpace
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)
The existing real Sobolev module instance for the literal metric difference equation.
Equations
Instances For
theorem
EulerCorrectionDifferenceMetric.difference_metric_deriv_bound
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : Type u_1}
[TopologicalSpace T]
(D : EulerCorrectionOperators.CorrectionData period q T)
(hq : 6 ≤ q)
(τ : T)
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
(A : EulerSpatialSobolevInverse.SmoothCoefficient period)
(K : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))
(e : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period))
(t ν μ c Kb Kx Kt A0 A2 Z R : ℝ)
(K' : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))
(hc : 0 < c)
(hν : 0 ≤ ν)
(hν1 : ν ≤ 1)
(hKv : K t = A.operator)
(hev : e t = EulerCylinderSobolevSpace.value period (u - v))
(hK : HasDerivAt K K' t)
(he : HasDerivAt e (EulerCorrectionDifferencePDE.differenceRhs period D hq ν μ τ u v) t)
(hKb : ‖A.operator‖ ≤ Kb)
(hKx : ↑A.firstBound ≤ Kx)
(hKt : ‖K'‖ ≤ Kt)
(hA0 : ↑(D.linear.coefficient τ).bound ≤ A0)
(hA2 : ∑ i : Fin 3, ↑((D.quadratic i).coefficient τ).bound ≤ A2)
(hZ : ‖D.approximation τ‖ ≤ Z)
(hu : ‖u‖ ≤ R)
(hv : ‖v‖ ≤ R)
(hsym :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (a b : EulerLiftedGradientSpace.Vector3),
inner ℝ ((A.coefficient x) a) b = inner ℝ a ((A.coefficient x) b))
(hpos :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (a : EulerLiftedGradientSpace.Vector3),
c ^ 2 * ‖a‖ ^ 2 ≤ inner ℝ ((A.coefficient x) a) a)
(hinv :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (a : EulerLiftedGradientSpace.Vector3),
(A.coefficient x) (((D.metric.coefficient τ).coefficient x) a) = a)
(hz :
EulerCylinderSobolevSpace.value period (D.approximation τ) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
(hud : EulerCylinderSobolevSpace.value period u ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
(hvd : EulerCylinderSobolevSpace.value period v ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
:
deriv (fun (s : ℝ) => inner ℝ ((K s) (e s)) (e s)) t ≤ EulerCorrectionStabilityConstants.growthConstant c Kb Kx Kt
(EulerCorrectionStabilityConstants.velocityBound period q Z R)
(EulerCorrectionStabilityConstants.lowerConstant period q A0 A2 Z R) * inner ℝ ((K t) (e t)) (e t) + EulerCorrectionStabilityConstants.defectConstant Kb R * |ν - μ| ^ 2
The actual correction-difference PDE gives the quantitative squared L² metric bound, with no assumed energy inequality.