module module

`IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (16)

abbrev DFTMode L29
theorem dftMode_count L31
def harmonicFrequency L34
def carrierFreq L38
theorem carrierFreq_pos L40
theorem carrier_gt_8 L45
theorem carrier_lt_8point1 L51
theorem harmonics_nonneg L57
theorem harmonics_factored L68
theorem mode_zero L74
theorem mode_seven L79
theorem mode_seven_lt_carrier L84
theorem mode_seven_lt_9 L95
theorem harmonic_strict_mono L102
structure DFTHarmonicSpectrumCert L109
def dftHarmonicSpectrumCert L118