Uniqueness of the actual finite-order inviscid correction equation.
@[instance_reducible]
noncomputable def
EulerInviscidCorrectionUniqueness.comparisonSobolevGroup
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
The existing Sobolev normed-group instance for the actual viscosity comparison.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerInviscidCorrectionUniqueness.comparisonSobolevSpace
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)
The existing real Sobolev module instance for the actual viscosity comparison.
Equations
Instances For
theorem
EulerInviscidCorrectionUniqueness.inviscid_correction_unique
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(T : ℝ)
(hT : 0 ≤ T)
(D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T))
(B : EulerCorrectionStabilityBudget.StabilityBudget period hT D)
(u v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(hi : u ⟨0, ⋯⟩ = v ⟨0, ⋯⟩)
(hu :
∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T),
HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT u r))
(EulerCylinderSobolevSpace.value period
((EulerCorrectionOperators.CorrectionData.coefficients period D hq).apply ⟨t, ⋯⟩ (u ⟨t, ⋯⟩)))
t)
(hv :
∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T),
HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT v r))
(EulerCylinderSobolevSpace.value period
((EulerCorrectionOperators.CorrectionData.coefficients period D hq).apply ⟨t, ⋯⟩ (v ⟨t, ⋯⟩)))
t)
(hz :
∀ (t : ↑(Set.Icc 0 T)),
EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
(hud :
∀ (t : ↑(Set.Icc 0 T)),
EulerCylinderSobolevSpace.value period (u t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
(hvd :
∀ (t : ↑(Set.Icc 0 T)),
EulerCylinderSobolevSpace.value period (v t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
:
Actual inviscid corrections with equal initial data and the concrete metric/coefficient bounds are unique. The squared energy inequality and the zero-difference conclusion are derived from their actual equations.