`DiscreteModel`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.Discrete
domain: ClassicalBridge
line: 44 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.Discrete on GitHub at line 44.

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

  41deriving DecidableEq
  42
  43/-- A discrete dynamical model intended to approximate NS. -/
  44structure DiscreteModel where
  45  /-- State type (e.g. truncated Fourier coefficients). -/
  46  State : Type
  47  /-- Tag: Galerkin vs grid, etc. -/
  48  kind : DiscretizationKind
  49  /-- One (discrete) time step of the model. -/
  50  step : NSParams → TimeStep → State → State
  51
  52/-- Optional energy functional on the discrete state (used for a priori bounds). -/
  53structure EnergyFunctional (D : DiscreteModel) where
  54  E : D.State → ℝ
  55
  56end Fluids
  57end ClassicalBridge
  58end IndisputableMonolith

papers checked against this theorem

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