def
definition
scaleFactor
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Chemistry.EnvPressure on GitHub at line 19.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
16open scoped Real
17
18/‑ Environment scale factor: φ^{β P}. -/
19def scaleFactor (beta P : ℝ) : ℝ :=
20 Real.rpow IndisputableMonolith.Constants.phi (beta * P)
21
22/‑ Display rescale: E' = E · φ^{β P}. -/
23def rescaleEnergy (E beta P : ℝ) : ℝ := E * scaleFactor beta P
24
25/‑ Eight-window neutrality diagnostic on a display observable stream x. -/
26def neutral8 (x : ℕ → ℝ) (t0 : ℕ) : ℝ :=
27 (Finset.range 8).sum (fun i => x (t0 + i))
28
29end EnvPressure
30end Chemistry
31end IndisputableMonolith