structure definition def or abbrev

`PowerSpectrum`

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

formal statement (Lean)

  62structure PowerSpectrum where
  63  amplitude : ℝ
  64  spectral_index : ℝ
  65  pivot_scale : ℝ
  66  amplitude_pos : amplitude > 0
  67  pivot_pos : pivot_scale > 0
  68
  69/-- Power at wavenumber k. -/

used by (2)

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

observedSpectrum in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use
power in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use

depends on (4)

Lean names referenced from this declaration's body.

spectral_index in IndisputableMonolith.Gravity.Inflation decl_use
amplitude in IndisputableMonolith.QFT.SMatrixUnitarity decl_use
amplitude in IndisputableMonolith.Quantum.DoubleSlit decl_use
Power in IndisputableMonolith.Superhuman.Core decl_use