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

PBMDeviceSpec

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)

 301structure PBMDeviceSpec where
 302  /-- Operating wavelength (meters) -/
 303  wavelength_m : ℝ
 304  /-- Window-neutral modulation pattern -/
 305  modulation_pattern : WindowNeutralPattern
 306  /-- Theta mode frequency (Hz) -/
 307  theta_freq_Hz : ℝ
 308  /-- Alpha mode frequency (Hz) -/
 309  alpha_freq_Hz : ℝ
 310  /-- Gamma mode frequency (Hz) -/
 311  gamma_freq_Hz : ℝ
 312  /-- Ticks per modulation cycle -/
 313  ticks_per_cycle : ℕ
 314
 315  wavelength_pos : 0 < wavelength_m
 316  wavelength_therapeutic : 750e-9 < wavelength_m ∧ wavelength_m < 780e-9
 317  ticks_is_eight : ticks_per_cycle = 8
 318  theta_in_band : 4 < theta_freq_Hz ∧ theta_freq_Hz < 8
 319  alpha_in_band : 8 < alpha_freq_Hz ∧ alpha_freq_Hz < 13
 320  gamma_in_band : 30 < gamma_freq_Hz ∧ gamma_freq_Hz < 100
 321  modes_ordered : theta_freq_Hz < alpha_freq_Hz ∧ alpha_freq_Hz < gamma_freq_Hz
 322
 323/-- The canonical RS-coherent PBM device.
 324    All parameters are derived from φ with zero free parameters. -/

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.