module
module
IndisputableMonolith.ClassicalBridge.Fluids.Regularity2D
show as:
view Lean formalization →
depends on (5)
declarations in this module (10)
-
structure
RSNS2DPipelineHypothesis -
theorem
rs_implies_global_regularity_2d -
theorem
rs_implies_global_regularity_2d_coeffBound -
theorem
rs_implies_global_regularity_2d_divFreeCoeffBound -
theorem
rs_implies_global_regularity_2d_stokesMildCoeffBound -
theorem
rs_implies_global_regularity_2d_stokesODECoeffBound -
theorem
rs_implies_global_regularity_2d_nsDuhamelCoeffBound -
theorem
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel -
theorem
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcing -
theorem
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp