theorem
proved
harmonics_nonneg
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum on GitHub at line 57.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
62 · exact Nat.cast_nonneg _
63 · norm_num
64 · exact le_of_lt phi_pos
65 · norm_num
66
67/-- The k-th harmonic is k · (carrier / 8). -/
68theorem harmonics_factored (k : DFTMode) :
69 harmonicFrequency k = (k.val : ℝ) * (carrierFreq / 8) := by
70 unfold harmonicFrequency carrierFreq
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