module module

`IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D`

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

used by (5)

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

IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D module_import
IndisputableMonolith.ClassicalBridge.Fluids.CPM2D module_import
IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics module_import
IndisputableMonolith.ClassicalBridge.Fluids.Regularity2D module_import
IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D module_import

declarations in this module (19)

abbrev Mode2 L34
def modeTrunc L37
def modes L41
lemma mem_modes_iff L44
abbrev VelCoeff L56
abbrev GalerkinState L59
def kSq L67
def laplacianCoeff L71
def ConvectionOp L77
def galerkinNSRHS L81
def discreteEnergy L90
structure EnergySkewHypothesis L95
theorem inviscid_energy_deriv_zero L103
lemma laplacianCoeff_inner_self_nonpos L133
theorem viscous_energy_deriv_le_zero L159
theorem viscous_energy_deriv_nonpos L183
theorem viscous_energy_antitone L193
theorem viscous_energy_bound_from_initial L208
theorem viscous_norm_bound_from_initial L220