`mode_seven`

proved

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum
domain: CrossDomain
line: 79 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum on GitHub at line 79.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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
 105  apply div_lt_div_of_pos_right _ (by norm_num : (8 : ℝ) > 0)
 106  apply mul_lt_mul_of_pos_right _ phi_pos
 107  · exact mul_lt_mul_of_pos_right (Nat.cast_lt.mpr hjk) (by norm_num)
 108
 109structure DFTHarmonicSpectrumCert where

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.