structure definition def or abbrev

`EvolutionIdentity`

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

formal statement (Lean)

  68structure EvolutionIdentity (siteCount : ℕ) where
  69  contributions : ContributionFields siteCount
  70  dJdt : ℝ
  71  split :
  72    dJdt = totalTransport contributions
  73      + totalViscous contributions
  74      + totalStretching contributions
  75
  76/-- If the transport contribution has zero total, it cancels exactly. -/

used by (4)

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

CoreNSOperator in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
IncompressibleNSOperator in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
dJdt_eq_viscous_plus_stretching in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
dJdt_nonpos_of_transport_cancel_and_absorption in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use

depends on (8)

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
cancels in IndisputableMonolith.Masses.Ribbons decl_use
ContributionFields in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
total in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
totalStretching in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
totalTransport in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
totalViscous in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
total in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use