structure definition def or abbrev

`FiniteVolumeProfile`

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

formal statement (Lean)

  39structure FiniteVolumeProfile where
  40  siteCount : ℕ
  41  siteCount_pos : 0 < siteCount
  42  omegaMax : ℝ
  43  omegaRms : ℝ
  44  omegaRms_pos : 0 < omegaRms
  45  omegaRms_le_max : omegaRms ≤ omegaMax
  46  finiteVolumeControl : omegaMax ≤ Real.sqrt siteCount * omegaRms
  47
  48/-- The normalized ratio used by the lattice FRC bridge. -/

used by (12)

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

finiteVolume_Jcost_bound in IndisputableMonolith.NavierStokes.FRCBridge decl_use
FRCBridgeCert in IndisputableMonolith.NavierStokes.FRCBridge decl_use
frc_holds_on_RS_lattice in IndisputableMonolith.NavierStokes.FRCBridge decl_use
frc_holds_on_RS_lattice_exists in IndisputableMonolith.NavierStokes.FRCBridge decl_use
LatticeFRC in IndisputableMonolith.NavierStokes.FRCBridge decl_use
LatticeRegularityCertificate in IndisputableMonolith.NavierStokes.FRCBridge decl_use
lattice_regular_via_direction_constancy in IndisputableMonolith.NavierStokes.FRCBridge decl_use
normalizedRatio in IndisputableMonolith.NavierStokes.FRCBridge decl_use
normalizedRatio_ge_one in IndisputableMonolith.NavierStokes.FRCBridge decl_use
normalizedRatio_le_sqrt_siteCount in IndisputableMonolith.NavierStokes.FRCBridge decl_use
normalizedRatio_pos in IndisputableMonolith.NavierStokes.FRCBridge decl_use
RSLatticeFRC in IndisputableMonolith.NavierStokes.FRCBridge decl_use

depends on (2)

Lean names referenced from this declaration's body.

bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
normalized in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use