`harmonicFrequency`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum on GitHub at line 34.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  62    · exact Nat.cast_nonneg _
  63    · norm_num
  64    · exact le_of_lt phi_pos

papers checked against this theorem

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