normalizedAmplitude

formal source

  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) : ℝ :=
  59  total c.transport
  60
  61def totalViscous {siteCount : ℕ} (c : ContributionFields siteCount) : ℝ :=
  62  total c.viscous
  63
  64def totalStretching {siteCount : ℕ} (c : ContributionFields siteCount) : ℝ :=
  65  total c.stretching
  66
  67/-- Data recording an exact J-cost derivative split. -/
  68structure EvolutionIdentity (siteCount : ℕ) where
  69  contributions : ContributionFields siteCount
  70  dJdt : ℝ
  71  split :
  72    dJdt = totalTransport contributions
  73      + totalViscous contributions
  74      + totalStretching contributions