Genuine norm, trace, and divergence constraints persist under actual uniform Sobolev limits.
@[instance_reducible]
The inherited normed group on the actual Sobolev path values.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerSobolevPathLimits.pathLimitSpace
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)
The inherited real normed space on the actual Sobolev path values.
Equations
Instances For
theorem
EulerSobolevPathLimits.restrict_path_norm
(period : ℝ)
[Fact (0 < period)]
{s q : ℕ}
(hq : q ≤ s)
(T : ℝ)
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s)))
:
‖(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period hq)) u‖ ≤ ‖u‖
Actual Sobolev restriction is contractive for the uniform time-path norm.
theorem
EulerSobolevPathLimits.limit_norm_bound
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(T R : ℝ)
(u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(h : Filter.Tendsto u Filter.atTop (nhds v))
(hu : ∀ (n : ℕ), ‖u n‖ ≤ R)
:
Uniform state bounds persist at the actual strong Sobolev limit.
theorem
EulerSobolevPathLimits.limit_zero_trace
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(T : ℝ)
(t : ↑(Set.Icc 0 T))
(u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(h : Filter.Tendsto u Filter.atTop (nhds v))
(hu : ∀ (n : ℕ), (u n) t = 0)
:
A fixed zero trace is preserved by actual uniform Sobolev convergence.
theorem
EulerSobolevPathLimits.limit_divergenceFree
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(T κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(h : Filter.Tendsto u Filter.atTop (nhds v))
(hu :
∀ (n : ℕ) (t : ↑(Set.Icc 0 T)),
EulerCylinderSobolevSpace.value period ((u n) t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m)
(t : ↑(Set.Icc 0 T))
:
EulerCylinderSobolevSpace.value period (v t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m
The genuine lifted divergence constraint is closed under actual uniform Sobolev convergence.