theorem
proved
dftMode_count
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum on GitHub at line 31.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
28/-- The DFT mode index. -/
29abbrev DFTMode : Type := Fin 8
30
31theorem dftMode_count : Fintype.card DFTMode = 8 := by decide
32
33/-- The k-th harmonic frequency of the RS comb: ν_k = k · 5φ / 8 Hz. -/
34noncomputable def harmonicFrequency (k : DFTMode) : ℝ :=
35 (k.val : ℝ) * 5 * phi / 8
36
37/-- Carrier frequency: 5φ ≈ 8.09 Hz (theta band). -/
38noncomputable def carrierFreq : ℝ := 5 * phi
39
40theorem carrierFreq_pos : 0 < carrierFreq := by
41 unfold carrierFreq
42 exact mul_pos (by norm_num) phi_pos
43
44/-- Theta-band lower bound: 5φ > 5 · 1.6 = 8. -/
45theorem carrier_gt_8 : carrierFreq > 8 := by
46 unfold carrierFreq
47 have := phi_gt_onePointSixOne
48 linarith
49
50/-- Theta-band upper bound: 5φ < 5 · 1.62 = 8.1. -/
51theorem carrier_lt_8point1 : carrierFreq < 8.1 := by
52 unfold carrierFreq
53 have := phi_lt_onePointSixTwo
54 linarith
55
56/-- All harmonics are non-negative. -/
57theorem harmonics_nonneg (k : DFTMode) : 0 ≤ harmonicFrequency k := by
58 unfold harmonicFrequency
59 apply div_nonneg
60 · apply mul_nonneg
61 apply mul_nonneg