Strong convergence of the actual nonlinear and viscous right-hand sides.
@[instance_reducible]
noncomputable def
EulerViscousSourcePathLimit.sourceLimitGroup
(period : ℝ)
[Fact (0 < period)]
(s : ℕ)
:
The inherited normed group on each actual Sobolev value space.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerViscousSourcePathLimit.sourceLimitSpace
(period : ℝ)
[Fact (0 < period)]
(s : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period s)
The inherited real normed space on each actual Sobolev value space.
Equations
Instances For
noncomputable def
EulerViscousSourcePathLimit.viscousSourcePath
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 2 ≤ q + 1 + 1)
(ν T : ℝ)
(C :
EulerQuadraticSource.Coefficients ↑(Set.Icc 0 T) ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))
↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))))
:
The literal continuous viscous right-hand side with the source evaluated one Sobolev order lower.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerViscousSourcePathLimit.viscousSourcePath_tendsto
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 2 ≤ q + 1 + 1)
(T : ℝ)
(C :
EulerQuadraticSource.Coefficients ↑(Set.Icc 0 T) ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))
↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(M : ℝ)
(huM : ∀ (n : ℕ), ‖u n‖ ≤ M)
(hconv :
Filter.Tendsto
(fun (n : ℕ) =>
(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T))
(EulerCylinderSobolevSpace.truncateOperator period (q + 1)))
(u n))
Filter.atTop (nhds e))
:
Filter.Tendsto (fun (n : ℕ) => viscousSourcePath period hq (EulerViscosityDefect.viscositySequence n) T C (u n))
Filter.atTop (nhds (EulerViscosityCauchy.valuePath period T (EulerQuadraticSourceLimit.sourcePath C e)))
Uniformly bounded strongly convergent states have convergent actual nonlinear-viscous right-hand sides.
theorem
EulerViscousSourcePathLimit.valuePath_tendsto_of_truncate
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(T : ℝ)
(u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(hconv :
Filter.Tendsto
(fun (n : ℕ) =>
(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period q))
(u n))
Filter.atTop (nhds e))
:
Filter.Tendsto (fun (n : ℕ) => EulerViscosityCauchy.valuePath period T (u n)) Filter.atTop
(nhds (EulerViscosityCauchy.valuePath period T e))
Strong convergence after restriction preserves the underlying continuous L² path.