OAI/Computability/FourierTransform/ChirpConvolution.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PowerSaving.Spectral.pr line 13

    Source comment

    ret true for inverse signs
    def pr : Bool→ℕ→ℂ
  | false => root
  | true => fun n => (root n)⁻¹

    Mentions: OAI.PowerSaving.root

  2. lemma OAI.PowerSaving.Spectral.primitive_pr line 17
  3. lemma OAI.PowerSaving.Spectral.twice_pr line 22
  4. lemma OAI.PowerSaving.Spectral.cyc_formula line 27
  5. lemma OAI.PowerSaving.Spectral.range_pad line 33
  6. def OAI.PowerSaving.Spectral.epschirp line 40
  7. lemma OAI.PowerSaving.Spectral.eps_eq_sq line 42
  8. def OAI.PowerSaving.Spectral.chirp_seed line 51
  9. def OAI.PowerSaving.Spectral.legdist line 54
  10. def OAI.PowerSaving.Spectral.fall line 56
  11. lemma OAI.PowerSaving.Spectral.chirp line 59
  12. def OAI.PowerSaving.Spectral.pointC line 72
  13. def OAI.PowerSaving.Spectral.fetchC line 75
  14. lemma OAI.PowerSaving.Spectral.chirps line 78
  15. def OAI.PowerSaving.Spectral.padline line 89
  16. lemma OAI.PowerSaving.Spectral.conv_pad_row line 91
  17. lemma OAI.PowerSaving.Spectral.cyclic_pad line 106
  18. lemma OAI.PowerSaving.Spectral.cyclic_pad_front line 114
  19. lemma OAI.PowerSaving.Spectral.freq_pad_row line 125
  20. lemma OAI.PowerSaving.Spectral.dft_front line 141
  21. def OAI.PowerSaving.Spectral.extendLine line 145
  22. lemma OAI.PowerSaving.Spectral.front_exact line 146