def
definition
trivial
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D on GitHub at line 1389.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1386namespace IdentificationHypothesis
1387
1388/-- Trivial identification constructor: choose `IsSolution := True`. -/
1389def trivial {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) :
1390 IdentificationHypothesis HC :=
1391 { IsSolution := fun _ => True
1392 isSolution := by trivial }
1393
1394/-- Concrete (but still minimal) identification: define `IsSolution u` to mean the limit coefficients
1395are uniformly bounded by the Galerkin bound `H.B` for `t ≥ 0`.
1396
1397This is **provable** from `UniformBoundsHypothesis` + modewise convergence (no extra analytic input),
1398via `ConvergenceHypothesis.coeff_bound_of_uniformBounds`.
1399-/
1400def coeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) :
1401 IdentificationHypothesis HC :=
1402 { IsSolution := fun u => ∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B
1403 isSolution := by
1404 intro t ht k
1405 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k) }
1406
1407/-- Identification constructor: coefficient bound + divergence-free (Fourier-side).
1408
1409The coefficient bound part is proved from `UniformBoundsHypothesis` + convergence.
1410The divergence-free part is proved from the extra assumption that *each approximant* is divergence-free.
1411-/
1412def divFreeCoeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1413 (hDF : ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2, divConstraint k ((extendByZero (H.uN N t)) k) = 0) :
1414 IdentificationHypothesis HC :=
1415 { IsSolution := fun u =>
1416 (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsDivergenceFreeTraj u
1417 isSolution := by
1418 refine ⟨?_, ?_⟩
1419 · intro t ht k