structure
definition
EEGProtocol
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Experiments.Protocols on GitHub at line 36.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
33/-! ## EEG Frequency Predictions -/
34
35/-- A complete EEG experimental protocol -/
36structure EEGProtocol where
37 /-- Sample size for each group -/
38 n_subjects : ℕ := 30
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 -/
49structure EEGPrediction where
50 /-- The mode index n in φ^n -/
51 mode_index : ℤ
52 /-- Central frequency (φ^n Hz) -/
53 center_freq : ℝ
54 /-- Expected peak width (Hz) -/
55 bandwidth : ℝ := 0.2
56 /-- Minimum peak amplitude (μV²/Hz) -/
57 min_amplitude : ℝ
58 /-- Confidence level for detection -/
59 confidence : ℝ := 0.95
60
61/-- The set of predicted EEG frequencies -/
62noncomputable def eegPredictions : List EEGPrediction :=
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)