theorem
proved
carrier_gt_8
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 45.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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