theorem
proved
continuum_limit_exists
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D on GitHub at line 1621.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
H -
coeff_bound_of_uniformBounds -
ConvergenceHypothesis -
extendByZero -
FourierState2D -
IdentificationHypothesis -
UniformBoundsHypothesis -
Mode2 -
H -
isSolution -
isSolution
used by
formal source
1618At this stage the theorem returns the packaged limit object together with its claimed properties.
1619-/
1620
1621theorem continuum_limit_exists
1622 (H : UniformBoundsHypothesis)
1623 (HC : ConvergenceHypothesis H)
1624 (HI : IdentificationHypothesis HC) :
1625 ∃ u : ℝ → FourierState2D,
1626 (∀ t : ℝ, ∀ k : Mode2, Tendsto (fun N : ℕ => (extendByZero (H.uN N t)) k) atTop (𝓝 ((u t) k)))
1627 ∧ HI.IsSolution u
1628 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) := by
1629 refine ⟨HC.u, HC.converges, ?_, ?_⟩
1630 · simpa using HI.isSolution
1631 · intro t ht k
1632 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1633
1634end ContinuumLimit2D
1635
1636end IndisputableMonolith.ClassicalBridge.Fluids