`coeffBound`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D
domain: ClassicalBridge
line: 1400 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D on GitHub at line 1400.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

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
1420        simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1421      · intro t k
1422        exact ConvergenceHypothesis.divConstraint_eq_zero_of_forall (HC := HC) (t := t) (k := k)
1423          (hDF := fun N => hDF N t k) }
1424
1425/-- Identification constructor: coefficient bound + (linear) Stokes/heat mild identity.
1426
1427The bound part is proved from `UniformBoundsHypothesis` + convergence.
1428The mild Stokes identity is proved from the extra assumption that it holds for every approximant. -/
1429def stokesMildCoeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1430    (hMild :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.