def
definition
def or abbrev
matchesPhiPeak
show as:
view Lean formalization →
formal statement (Lean)
80noncomputable def matchesPhiPeak (f : ℝ) (tolerance : ℝ) : Bool :=
proof body
Definition body.
81 (|f - φ^(-2 : ℤ)| < tolerance) ||
82 (|f - φ^(-1 : ℤ)| < tolerance) ||
83 (|f - 1| < tolerance) ||
84 (|f - φ| < tolerance) ||
85 (|f - φ^(2 : ℤ)| < tolerance) ||
86 (|f - φ^(3 : ℤ)| < tolerance)
87
88/-- The EEG prediction is falsified if too few peaks match -/