Strong lower-Sobolev compactness of an actual uniformly bounded correction family.
@[instance_reducible]
noncomputable def
EulerCorrectionFamilyCompactness.familySobolevGroup
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
The inherited Sobolev normed-group instance for family compactness.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerCorrectionFamilyCompactness.familySobolevSpace
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)
The inherited real Sobolev module instance for family compactness.
Equations
Instances For
theorem
EulerCorrectionFamilyCompactness.restrict_eq_truncate
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
The actual one-order restriction equals the original truncation map.
theorem
EulerCorrectionFamilyCompactness.exists_limit_with_constraints
(period : ℝ)
[Fact (0 < period)]
{s q : ℕ}
(hqs : q < s)
(T : ℝ)
(hT : 0 ≤ T)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s)))
(M : ℝ)
(huM : ∀ (n : ℕ), ‖u n‖ ≤ M)
(hu0 : ∀ (n : ℕ), (u n) ⟨0, ⋯⟩ = 0)
(hud :
∀ (n : ℕ) (t : ↑(Set.Icc 0 T)),
EulerCylinderSobolevSpace.value period ((u n) t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m)
(hCauchy :
CauchySeq fun (n : ℕ) =>
(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period s))
(u n))
:
∃ (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))),
Filter.Tendsto
(fun (n : ℕ) =>
(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T))
(EulerCylinderSobolevSpace.restrictOperator period ⋯))
(u n))
Filter.atTop (nhds e) ∧ e ⟨0, ⋯⟩ = 0 ∧ (∀ (t : ↑(Set.Icc 0 T)),
EulerCylinderSobolevSpace.value period (e t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) ∧ ‖e‖ ≤ M
Actual strong lower-order Sobolev compactness retains the trace, divergence constraint and common norm bound.
theorem
EulerCorrectionFamilyCompactness.exists_correction_family_limit
(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)
(ν : ℕ → ℝ)
(hν : ∀ (n : ℕ), 0 < ν n)
(hν1 : ∀ (n : ℕ), ν n ≤ 1)
(hνc : CauchySeq ν)
(u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(M : ℝ)
(huM : ∀ (n : ℕ), ‖u n‖ ≤ M)
(hu0 : ∀ (n : ℕ), (u n) ⟨0, ⋯⟩ = 0)
(hu :
∀ (n : ℕ) (t : ↑(Set.Icc 0 T)),
(u n) t = EulerQuadraticSource.quadraticDuhamel period (ν n) ⋯ hT ⋯
(EulerCorrectionOperators.CorrectionData.coefficients period D hq) 0 (u n) t)
(hz :
∀ (t : ↑(Set.Icc 0 T)),
EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
(hud :
∀ (n : ℕ) (t : ↑(Set.Icc 0 T)),
EulerCylinderSobolevSpace.value period ((u n) t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
:
∃ (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))),
Filter.Tendsto
(fun (n : ℕ) =>
(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T))
(EulerCylinderSobolevSpace.truncateOperator period q))
(u n))
Filter.atTop (nhds e) ∧ e ⟨0, ⋯⟩ = 0 ∧ (∀ (t : ↑(Set.Icc 0 T)),
EulerCylinderSobolevSpace.value period (e t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) ∧ ‖e‖ ≤ M
Genuine uniformly bounded correction solutions with Cauchy viscosities have an actual strong lower-Sobolev limit with the original trace and divergence constraint.