Actual finite-order Sobolev time regularity of the inviscid cylinder correction.
@[instance_reducible]
noncomputable def
EulerInviscidSobolevEvolution.evolutionSobolevGroup
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
The inherited Sobolev group structure used for the stronger time equation.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerInviscidSobolevEvolution.evolutionSobolevSpace
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)
The inherited real Sobolev module used for the stronger time equation.
Equations
Instances For
theorem
EulerInviscidSobolevEvolution.sobolev_hasDerivAt
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(T : ℝ)
(hT : 0 ≤ T)
(A :
EulerQuadraticSource.Coefficients ↑(Set.Icc 0 T) ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))
↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(hd :
∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T),
HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT e r))
(EulerCylinderSobolevSpace.value period (A.apply ⟨t, ⋯⟩ (e ⟨t, ⋯⟩))) t)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 T)
:
HasDerivAt
(fun (r : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (EulerVolterraConvolution.extendPath T hT e r))
(A.apply ⟨t, ⋯⟩ (e ⟨t, ⋯⟩)) t
A genuine continuous quadratic Sobolev source upgrades the actual L² evolution to an Hq time derivative of the truncated H(q+1) path.
theorem
EulerInviscidSobolevEvolution.CorrectionData.source_sobolev
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : Type u_1}
[TopologicalSpace T]
(D : EulerCorrectionOperators.CorrectionData period q T)
(hq : 6 ≤ q)
(t : T)
(e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
(EulerCorrectionOperators.CorrectionData.coefficients period D hq).apply t e = -EulerCorrectionOperators.CorrectionData.rawSource period D hq t e - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (D.metric.jet t))
(EulerCorrectionOperators.CorrectionData.pressure period D hq t e)
The actual projected Sobolev source equals the literal non-pressure source and signed coercive pressure already before passing to L².
theorem
EulerInviscidSobolevEvolution.correction_sobolev_hasDerivAt
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(T : ℝ)
(hT : 0 ≤ T)
(D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(hd :
∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T),
HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT e r))
(EulerCylinderSobolevSpace.value period
((EulerCorrectionOperators.CorrectionData.coefficients period D hq).apply ⟨t, ⋯⟩ (e ⟨t, ⋯⟩)))
t)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 T)
:
HasDerivAt
(fun (r : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (EulerVolterraConvolution.extendPath T hT e r))
(-EulerCorrectionOperators.CorrectionData.rawSource period D hq ⟨t, ⋯⟩ (e ⟨t, ⋯⟩) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (D.metric.jet ⟨t, ⋯⟩))
(EulerCorrectionOperators.CorrectionData.pressure period D hq ⟨t, ⋯⟩ (e ⟨t, ⋯⟩)))
t
The actual correction equation has its literal signed-pressure time derivative in Hq whenever its continuous H(q+1) path satisfies the constructed L² equation.