`carrierFreq`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum on GitHub at line 38.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  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
  65  · norm_num
  66
  67/-- The k-th harmonic is k · (carrier / 8). -/
  68theorem harmonics_factored (k : DFTMode) :

papers checked against this theorem

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