mode_zero

formal source

  71  ring
  72
  73/-- Mode 0 has frequency 0 (DC). -/
  74theorem mode_zero : harmonicFrequency ⟨0, by decide⟩ = 0 := by
  75  unfold harmonicFrequency
  76  simp
  77
  78/-- Mode 7 = highest harmonic: 35φ/8. -/
  79theorem mode_seven : harmonicFrequency ⟨7, by decide⟩ = 35 * phi / 8 := by
  80  unfold harmonicFrequency
  81  push_cast; ring
  82
  83/-- Mode 7 < carrier (since 7/8 < 1). -/
  84theorem mode_seven_lt_carrier :
  85    harmonicFrequency ⟨7, by decide⟩ < carrierFreq := by
  86  rw [mode_seven]
  87  unfold carrierFreq
  88  -- 35φ/8 < 5φ iff 35/8 < 5, which is 4.375 < 5
  89  have hpos := phi_pos
  90  rw [div_lt_iff₀ (by norm_num : (8 : ℝ) > 0)]
  91  -- Goal: 35*phi < 5*phi*8 = 40*phi
  92  linarith [phi_pos]
  93
  94/-- The highest harmonic is bounded above by 9 Hz (still theta band). -/
  95theorem mode_seven_lt_9 : harmonicFrequency ⟨7, by decide⟩ < 9 := by
  96  rw [mode_seven]
  97  have := phi_lt_onePointSixTwo
  98  -- 35φ/8 < 35 · 1.62 / 8 = 56.7/8 = 7.0875 < 9
  99  linarith
 100
 101/-- Strict monotonicity of the comb. -/
 102theorem harmonic_strict_mono (j k : DFTMode) (hjk : j.val < k.val) :
 103    harmonicFrequency j < harmonicFrequency k := by
 104  unfold harmonicFrequency