inductive
definition
DiscretizationKind
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.ClassicalBridge.Fluids.Discrete on GitHub at line 38.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
35def TimeStep.Valid (h : TimeStep) : Prop := 0 < h.Δt
36
37/-- High-level choice of discretization family. -/
38inductive DiscretizationKind where
39 | spectralGalerkin
40 | finiteDifference
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