`dftHarmonicSpectrumCert`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum on GitHub at line 118.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 115  comb_monotone : ∀ j k : DFTMode, j.val < k.val →
 116    harmonicFrequency j < harmonicFrequency k
 117
 118noncomputable def dftHarmonicSpectrumCert : DFTHarmonicSpectrumCert where
 119  modes_eight := dftMode_count
 120  carrier_in_theta_band := ⟨carrier_gt_8, carrier_lt_8point1⟩
 121  all_modes_nonneg := harmonics_nonneg
 122  mode_zero_dc := mode_zero
 123  mode_seven_under_9 := mode_seven_lt_9
 124  comb_monotone := harmonic_strict_mono
 125
 126end IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum

papers checked against this theorem

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