harmonic_strict_mono

formal source

  99  linarith
 100
 101/-- Strict monotonicity of the comb. -/
 102theorem harmonic_strict_mono (j k : DFTMode) (hjk : j.val < k.val) :
 103    harmonicFrequency j < harmonicFrequency k := by
 104  unfold harmonicFrequency
 105  apply div_lt_div_of_pos_right _ (by norm_num : (8 : ℝ) > 0)
 106  apply mul_lt_mul_of_pos_right _ phi_pos
 107  · exact mul_lt_mul_of_pos_right (Nat.cast_lt.mpr hjk) (by norm_num)
 108
 109structure DFTHarmonicSpectrumCert where
 110  modes_eight : Fintype.card DFTMode = 8
 111  carrier_in_theta_band : 8 < carrierFreq ∧ carrierFreq < 8.1
 112  all_modes_nonneg : ∀ k : DFTMode, 0 ≤ harmonicFrequency k
 113  mode_zero_dc : harmonicFrequency ⟨0, by decide⟩ = 0
 114  mode_seven_under_9 : harmonicFrequency ⟨7, by decide⟩ < 9
 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