`State`

definition

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.DiscreteVorticity
domain: NavierStokes
line: 28 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NavierStokes.DiscreteVorticity on GitHub at line 28.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  25noncomputable section
  26
  27/-- A finite discrete vorticity field on a lattice window of `siteCount` sites. -/
  28structure State (siteCount : ℕ) where
  29  omega : Fin siteCount → ℝ
  30
  31/-- Sum of a scalar field over the finite lattice window. -/
  32def total {siteCount : ℕ} (f : Fin siteCount → ℝ) : ℝ :=
  33  ∑ i : Fin siteCount, f i
  34
  35/-- RMS square of a scalar field. -/
  36def rmsSq {siteCount : ℕ} (f : Fin siteCount → ℝ) : ℝ :=
  37  total (fun i => (f i) ^ 2) / siteCount
  38
  39/-- RMS amplitude of a scalar field. -/
  40def rms {siteCount : ℕ} (f : Fin siteCount → ℝ) : ℝ :=
  41  Real.sqrt (rmsSq f)
  42
  43/-- Pointwise normalized amplitude relative to the RMS scale. -/
  44def normalizedAmplitude {siteCount : ℕ} (f : Fin siteCount → ℝ) (i : Fin siteCount) : ℝ :=
  45  |f i| / rms f
  46
  47/-- The total J-cost of a discrete vorticity field relative to its RMS scale. -/
  48def totalJcost {siteCount : ℕ} (f : Fin siteCount → ℝ) : ℝ :=
  49  total (fun i => Jcost (normalizedAmplitude f i))
  50
  51/-- Contribution fields appearing in the J-cost derivative identity. -/
  52structure ContributionFields (siteCount : ℕ) where
  53  transport : Fin siteCount → ℝ
  54  viscous : Fin siteCount → ℝ
  55  stretching : Fin siteCount → ℝ
  56
  57/-- Total contributions of the three pieces. -/
  58def totalTransport {siteCount : ℕ} (c : ContributionFields siteCount) : ℝ :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.