structure
definition
def or abbrev
ConvergenceHypothesis
show as:
view Lean formalization →
formal statement (Lean)
1133structure ConvergenceHypothesis (H : UniformBoundsHypothesis) where
1134 /-- Candidate limit (time → full Fourier coefficients). -/
1135 u : ℝ → FourierState2D
1136 /-- Pointwise (mode-by-mode) convergence of the zero-extended Galerkin coefficients. -/
1137 converges : ∀ t : ℝ, ∀ k : Mode2,
1138 Tendsto (fun N : ℕ => (extendByZero (H.uN N t)) k) atTop (𝓝 ((u t) k))
1139
1140namespace ConvergenceHypothesis
1141
1142/-- Derived fact: if the approximants are uniformly bounded in the Galerkin norm for `t ≥ 0`,
1143then the limit coefficients inherit the same bound (by closedness of `closedBall`). -/
used by (28)
-
coeffBound -
coeff_bound_of_uniformBounds -
continuum_limit_exists -
divConstraint_eq_zero_of_forall -
divFreeCoeffBound -
divFree_of_forall -
IdentificationHypothesis -
nsDuhamelCoeffBound -
nsDuhamelCoeffBound_galerkinKernel -
nsDuhamelCoeffBound_galerkinKernel_of_forcing -
nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp -
nsDuhamelCoeffBound_kernelIntegral -
nsDuhamelCoeffBound_kernelIntegral_of_forcing -
nsDuhamel_of_forall -
nsDuhamel_of_forall_kernelIntegral -
nsDuhamel_of_forall_kernelIntegral_of_forcing -
stokesMildCoeffBound -
stokesMild_of_forall -
trivial -
rs_implies_global_regularity_2d_coeffBound -
rs_implies_global_regularity_2d_divFreeCoeffBound -
rs_implies_global_regularity_2d_nsDuhamelCoeffBound -
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel -
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcing -
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp -
rs_implies_global_regularity_2d_stokesMildCoeffBound -
rs_implies_global_regularity_2d_stokesODECoeffBound -
RSNS2DPipelineHypothesis