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

EEGProtocol

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)

  36structure EEGProtocol where
  37  /-- Sample size for each group -/
  38  n_subjects : ℕ := 30

proof body

Definition body.

  39  /-- Recording duration in seconds -/
  40  duration_sec : ℕ := 600  -- 10 minutes
  41  /-- Sampling rate in Hz -/
  42  sampling_rate : ℕ := 256
  43  /-- Frequency resolution in Hz -/
  44  freq_resolution : ℝ := 0.1
  45  /-- Electrode positions (10-20 system) -/
  46  electrodes : List String := ["Fz", "Cz", "Pz", "O1", "O2"]
  47
  48/-- Predicted EEG peaks with confidence intervals -/

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.