module module

`IndisputableMonolith.NavierStokes.DiscreteNSOperator`

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 (3)

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

IndisputableMonolith.NavierStokes.DiscreteMaximumPrinciple module_import
IndisputableMonolith.NavierStokes.JcostMonotonicity module_import
IndisputableMonolith.NavierStokes.VortexStretching module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.NavierStokes.DiscreteVorticity module_import
IndisputableMonolith.NavierStokes.StretchingPairs module_import

declarations in this module (33)

abbrev Axis L34
abbrev ScalarField L36
abbrev VectorField L38
structure LatticeTopology L40
def forwardDiff L44
def backwardDiff L48
def scalarLaplacian L52
def vectorLaplacian L56
def divergence L60
def advection L64
def conservativeTransportField L68
theorem total_conservativeTransportField_zero L73
def velocityGradientMag L86
structure CoreNSOperator L96
theorem core_transport_zero L132
def corePairAmplitude L142
theorem corePairAmplitude_pos L146
def corePairStretchFactor L151
theorem corePairStretchFactor_pos L155
def corePairEvent L161
theorem core_stretching_le_pair_budget L170
def coreOperatorPairBudget L178
theorem coreOperatorPairBudget_nonneg L181
theorem core_pair_budget_absorbed L187
theorem core_stretching_absorbed L195
theorem core_dJdt_nonpos L205
structure IncompressibleNSOperator L215
def pairEventAt L270
def operatorPairBudget L277
theorem operator_transport_zero L280
theorem operatorPairBudget_nonneg L287
theorem totalStretching_le_operatorPairBudget L293
theorem operatorPairBudget_absorbed_by_viscosity L301