OAI/Computability/FourierCircuit/ToeplitzCross.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactFourier.ToeplitzLayers.cross line 11
  2. theorem OAI.ExactFourier.ToeplitzLayers.cross_succ line 14
  3. theorem OAI.ExactFourier.ToeplitzLayers.sum_upper_shift line 24
  4. def OAI.ExactFourier.ToeplitzLayers.lowerCross line 37
  5. theorem OAI.ExactFourier.ToeplitzLayers.cross_mul line 40
  6. theorem OAI.ExactFourier.ToeplitzLayers.cross_interior line 54
  7. theorem OAI.ExactFourier.ToeplitzLayers.trunc_split line 71
  8. theorem OAI.ExactFourier.ToeplitzLayers.lower_shear line 81
  9. theorem OAI.ExactFourier.ToeplitzLayers.cross_layer line 91
  10. theorem OAI.ExactFourier.ToeplitzLayers.recursion line 106
  11. theorem OAI.ExactFourier.ToeplitzLayers.trunc_small line 133
  12. theorem OAI.ExactFourier.ToeplitzLayers.trunc_layers_pow line 145
  13. theorem OAI.ExactFourier.ToeplitzLayers.trunc_layers line 168
  14. theorem OAI.ExactFourier.Layered.symmetric_triangular line 183

    Source documentation

    Symmetric Gaussian factorization, avoiding an appeal to LDU uniqueness.

    theorem symmetric_triangular {F P N : Matrix ι ι ℂ} {d : ℕ}
 (hN : Layered N d) (hP : IsUnit P) (hU : P.IsUpperTriangular)
 (hL : N.IsLowerTriangular) (hFP : F*P=N) (hF : F.transpose=F) :
 Layered F (2*d+1) := by
…

    Mentions: OAI.ExactFourier.Layered

  15. def OAI.ExactFourier.NewtonFourier.invH line 230
  16. theorem OAI.ExactFourier.NewtonFourier.invH_constant line 232
  17. theorem OAI.ExactFourier.NewtonFourier.N_toeplitz line 235
  18. theorem OAI.ExactFourier.NewtonFourier.P_unit line 254
  19. theorem OAI.ExactFourier.NewtonFourier.N_layers line 262
  20. theorem OAI.ExactFourier.NewtonFourier.dft_layers line 274

    Source documentation

    Exact-width Fourier layer theorem, with an absolute constant and a stronger quadratic logarithmic bound.

    theorem dft_layers {n : ℕ} (hn : 0 < n) {ω : ℂ} (hω : IsPrimitiveRoot ω n) :
 Layered (RadixTwo.dft n ω) (8388608*(Nat.log 2 n+2)^2+5) := by
…

    Mentions: OAI.ExactFourier.Layered, OAI.ExactFourier.RadixTwo.dft

  21. def OAI.ExactFourier.FourierCRT.finZMod line 290
  22. theorem OAI.ExactFourier.FourierCRT.char_nat line 296
  23. theorem OAI.ExactFourier.FourierCRT.root_primitive line 299
  24. def OAI.ExactFourier.FourierCRT.singleAdd line 308
  25. theorem OAI.ExactFourier.FourierCRT.singleAdd_injective line 317
  26. theorem OAI.ExactFourier.FourierCRT.sum_singleAdd line 323
  27. theorem OAI.ExactFourier.FourierCRT.char_sum line 332
  28. def OAI.ExactFourier.FourierCRT.component line 341
  29. theorem OAI.ExactFourier.FourierCRT.component_injective line 345
  30. theorem OAI.ExactFourier.FourierCRT.character_factor line 349
  31. theorem OAI.ExactFourier.FourierCRT.standard_root line 356
  32. theorem OAI.ExactFourier.FourierCRT.factorization line 360