`UniformBoundsHypothesis`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D
domain: ClassicalBridge
line: 938 · 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 938.

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

used by

formal source

 935- CPM coercivity/dispersion bounds, and
 936- compactness tools (Aubin–Lions / Banach–Alaoglu / etc.).
 937-/
 938structure UniformBoundsHypothesis where
 939  /-- Discrete Galerkin trajectories at each truncation level `N`. -/
 940  uN : (N : ℕ) → ℝ → GalerkinState N
 941  /-- A global (in time, and uniform in `N`) bound. -/
 942  B : ℝ
 943  B_nonneg : 0 ≤ B
 944  /-- Uniform bound: for all `N` and all `t ≥ 0`, `‖uN N t‖ ≤ B`. -/
 945  bound : ∀ N : ℕ, ∀ t ≥ 0, ‖uN N t‖ ≤ B
 946
 947/-- Build `UniformBoundsHypothesis` from the *viscous* Galerkin energy estimate, provided we have
 948an initial uniform bound `‖uN N 0‖ ≤ B` across all truncation levels.
 949-/
 950noncomputable def UniformBoundsHypothesis.ofViscous
 951    (ν : ℝ) (hν : 0 ≤ ν)
 952    (Bop : (N : ℕ) → ConvectionOp N)
 953    (HB : ∀ N : ℕ, EnergySkewHypothesis (Bop N))
 954    (u : (N : ℕ) → ℝ → GalerkinState N)
 955    (hu : ∀ N : ℕ, ∀ t : ℝ, HasDerivAt (u N) (galerkinNSRHS ν (Bop N) ((u N) t)) t)
 956    (B : ℝ) (B_nonneg : 0 ≤ B)
 957    (h0 : ∀ N : ℕ, ‖u N 0‖ ≤ B) :
 958    UniformBoundsHypothesis :=
 959  { uN := u
 960    B := B
 961    B_nonneg := B_nonneg
 962    bound := by
 963      intro N t ht
 964      have hNt : ‖u N t‖ ≤ ‖u N 0‖ :=
 965        viscous_norm_bound_from_initial (N := N) ν hν (Bop N) (HB N) (u N) (hu N) t ht
 966      exact le_trans hNt (h0 N) }
 967
 968/-- The (Galerkin) nonlinear forcing family in full Fourier variables:

papers checked against this theorem

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