module module

`IndisputableMonolith.NavierStokes.DiscreteMaximumPrinciple`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.NavierStokes.DiscreteNSOperator module_import
IndisputableMonolith.NavierStokes.VortexStretching module_import

declarations in this module (10)

structure OneStepData L45
theorem advection_dominated_by_viscosity L73
theorem one_step_factor_le_one L79
theorem gradient_nonincreasing L88
theorem subK_preserved L98
theorem subK_propagation L115
theorem unconditional_gradient_bound L131
theorem unconditional_Jcost_monotonicity L145
theorem Jcost_nonincreasing L151
theorem master_lattice_regularity L173