OAI/Computability/FourierTransform/NewtonFactorization.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Newton-factorization input to the Fourier compiler.

  1. def OAI.PowerSaving.Spectral.rise line 11

    Source documentation

    Toeplitz entries with lower triangular convention.

    def rise (h : Line) (i j : ℕ) : ℂ := if j ≤ i then h (i-j) else 0

    Mentions: OAI.PowerSaving.Line

  2. def OAI.PowerSaving.Spectral.stairs line 13
  3. def OAI.PowerSaving.Spectral.gap line 16
  4. def OAI.PowerSaving.Spectral.roof line 18
  5. def OAI.PowerSaving.Spectral.floorH line 20
  6. def OAI.PowerSaving.Spectral.cog line 22
  7. abbrev OAI.PowerSaving.Spectral.RootMat line 24
  8. def OAI.PowerSaving.Spectral.fade line 26
  9. def OAI.PowerSaving.Spectral.steps line 29

    Source documentation

    Matrix of Newton polynomial values, by its product formula.

    def steps (n : ℕ) (u : ℂ) : RootMat n :=
…

    Mentions: OAI.PowerSaving.Spectral.RootMat

  10. lemma OAI.PowerSaving.Spectral.steps_apply line 32
  11. lemma OAI.PowerSaving.Spectral.steps_diag line 38
  12. lemma OAI.PowerSaving.Spectral.steps_zero line 41
  13. lemma OAI.PowerSaving.Spectral.roof_ne_zero line 46
  14. lemma OAI.PowerSaving.Spectral.gap_ne_zero line 52
  15. lemma OAI.PowerSaving.Spectral.cog_ne_zero line 59
  16. def OAI.PowerSaving.Spectral.newton line 63

    Source comment

    P upper from monic Newton basis
    def newton (u : ℂ) : ℕ → Polynomial ℂ
  | 0 => 1
  | i+1 => newton u i * (X-C (u^i))
  17. def OAI.PowerSaving.Spectral.bridge line 67
  18. lemma OAI.PowerSaving.Spectral.newton_monic line 70
  19. lemma OAI.PowerSaving.Spectral.newton_natDegree line 75
  20. lemma OAI.PowerSaving.Spectral.bridge_zero line 82
  21. lemma OAI.PowerSaving.Spectral.bridge_diag line 88
  22. lemma OAI.PowerSaving.Spectral.bridge_unit line 92
  23. lemma OAI.PowerSaving.Spectral.newton_zero line 100
  24. lemma OAI.PowerSaving.Spectral.newton_eval line 110
  25. lemma OAI.PowerSaving.Spectral.winds_bridge line 134
  26. lemma OAI.PowerSaving.Spectral.winds_symm line 151
  27. lemma OAI.PowerSaving.Spectral.cog_products line 154
  28. theorem OAI.PowerSaving.Spectral.winds_reduction line 186

    Source documentation

    Newton reduction into diagonal and Toeplitz factors (and transpose).

    theorem winds_reduction (n : ℕ) (u : ℂ) (h : IsPrimitiveRoot u n) :
    winds n u =
      steps n u * fade n (fun i => (cog u i)⁻¹) * (steps n u)ᵀ := by
…

    Mentions: OAI.PowerSaving.Spectral.winds, OAI.PowerSaving.Spectral.steps, OAI.PowerSaving.Spectral.fade, OAI.PowerSaving.Spectral.cog