def definition def or abbrev

`corePairAmplitude`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 142def corePairAmplitude {siteCount : ℕ} (op : CoreNSOperator siteCount)
 143    (i : Fin siteCount) : ℝ :=

Definition body.

 144  |op.state.omega i| / op.omega_rms
 145

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

corePairAmplitude_pos in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
core_pair_budget_absorbed in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
corePairEvent in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
core_stretching_le_pair_budget in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
IncompressibleNSOperator in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use

Lean names referenced from this declaration's body.

CoreNSOperator in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use