pith. machine review for the scientific record. sign in
def definition def or abbrev

dftHarmonicSpectrumCert

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

formal statement (Lean)

 118noncomputable def dftHarmonicSpectrumCert : DFTHarmonicSpectrumCert where
 119  modes_eight := dftMode_count

proof body

Definition body.

 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

depends on (8)

Lean names referenced from this declaration's body.