pith. machine review for the scientific record. sign in
structure definition def or abbrev

UniformBoundsHypothesis

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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 :=

proof body

Definition body.

 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:
 969
 970`F_N(N,s) := extendByZero (Bop N (uN N s) (uN N s))`. -/

used by (36)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 6 more

depends on (19)

Lean names referenced from this declaration's body.