pith. machine review for the scientific record. sign in
def definition def or abbrev

eegPredictions

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  62noncomputable def eegPredictions : List EEGPrediction :=

proof body

Definition body.

  63  [⟨-2, φ^(-2 : ℤ), 0.2, 0.5, 0.95⟩,   -- ~0.38 Hz (infra-slow)
  64   ⟨-1, φ^(-1 : ℤ), 0.2, 0.5, 0.95⟩,   -- ~0.62 Hz (delta-low)
  65   ⟨0, 1, 0.2, 1.0, 0.95⟩,              -- 1.00 Hz (delta-high)
  66   ⟨1, φ, 0.2, 1.0, 0.95⟩,              -- ~1.62 Hz (delta-theta)
  67   ⟨2, φ^(2 : ℤ), 0.2, 0.8, 0.95⟩,     -- ~2.62 Hz (theta-low)
  68   ⟨3, φ^(3 : ℤ), 0.2, 0.5, 0.95⟩]     -- ~4.24 Hz (theta)
  69
  70/-- FALSIFICATION: The EEG prediction is falsified if no φ-peaks found -/

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.