module module

`IndisputableMonolith.NavierStokes.StretchingPairs`

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

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

IndisputableMonolith.NavierStokes.DiscreteNSOperator 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.PhiLadderCutoff module_import

declarations in this module (11)

def pairwiseStretchingChange L29
theorem pairwise_RCL_balance L33
theorem pairwise_RCL_balance_factored L43
theorem pairwiseStretching_nonneg L51
structure PairEvent L59
def pairEventBudget L66
theorem pairEventBudget_nonneg L69
def totalPairBudget L73
theorem totalPairBudget_nonneg L76
def indexedPairBudget L85
theorem indexedPairBudget_nonneg L88