OAI/Computability/FourierCircuit/RawPositive.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ExactFourier.Packing.RawPrice.embedded line 10
  2. theorem OAI.ExactFourier.Packing.RawPrice.zero_iff line 15
  3. theorem OAI.ExactFourier.MonomialMatrix.transpose line 44
  4. theorem OAI.ExactFourier.MatrixSymmetry.unit_transpose line 58
  5. theorem OAI.ExactFourier.MatrixSymmetry.inverse_tensor line 62
  6. theorem OAI.ExactFourier.MatrixSymmetry.inverse_sum line 68
  7. theorem OAI.ExactFourier.MatrixSymmetry.inverse_reindex line 75
  8. theorem OAI.ExactFourier.MatrixSymmetry.transpose_tensor line 81
  9. def OAI.ExactFourier.Packing.RawPrice.symValue line 98
  10. theorem OAI.ExactFourier.Packing.RawPrice.sym_nonneg line 101
  11. theorem OAI.ExactFourier.Packing.RawPrice.sym_zero line 109
  12. theorem OAI.ExactFourier.Packing.RawPrice.sym_reindex line 124
  13. theorem OAI.ExactFourier.Packing.RawPrice.sym_mul line 132
  14. theorem OAI.ExactFourier.Packing.RawPrice.sym_monomial line 147
  15. theorem OAI.ExactFourier.Packing.RawPrice.sym_tensor line 166
  16. theorem OAI.ExactFourier.Packing.RawPrice.sym_sum line 179
  17. theorem OAI.ExactFourier.Packing.RawPrice.sym_inverse line 193
  18. theorem OAI.ExactFourier.Packing.RawPrice.sym_transpose line 200
  19. theorem OAI.ExactFourier.Packing.RawPrice.shear_inverse line 213
  20. theorem OAI.ExactFourier.Packing.RawPrice.shear_transpose line 225
  21. theorem OAI.ExactFourier.Packing.RawPrice.shear_transpose_inverse line 231
  22. theorem OAI.ExactFourier.Packing.RawPrice.sym_normalized line 238
  23. def OAI.ExactFourier.Packing.RawPrice.toMatrixPrice line 242
  24. def OAI.ExactFourier.BasisExchange.rows line 263
  25. theorem OAI.ExactFourier.BasisExchange.rows_insert line 266
  26. theorem OAI.ExactFourier.BasisExchange.price_many line 275
  27. theorem OAI.ExactFourier.BasisExchange.rows_unit line 291
  28. theorem OAI.ExactFourier.BasisExchange.price_triangular line 303
  29. abbrev OAI.ExactFourier.SignedBits.Bits line 317
  30. instance OAI.ExactFourier.SignedBits.bitsFintype line 320
  31. instance OAI.ExactFourier.SignedBits.bitsDecidableEq line 323
  32. instance OAI.ExactFourier.SignedBits.bitsLinearOrder line 326
  33. instance OAI.ExactFourier.SignedBits.(instance at line 330) line 330
  34. theorem OAI.ExactFourier.SignedBits.bits_card line 333
  35. def OAI.ExactFourier.SignedBits.D line 338
  36. def OAI.ExactFourier.SignedBits.T line 341
  37. theorem OAI.ExactFourier.SignedBits.D_square line 343
  38. theorem OAI.ExactFourier.SignedBits.T_inv_mul line 348
  39. theorem OAI.ExactFourier.SignedBits.T_unit line 352
  40. theorem OAI.ExactFourier.SignedBits.T_inv line 357
  41. theorem OAI.ExactFourier.SignedBits.D_lower line 359
  42. theorem OAI.ExactFourier.SignedBits.D_diag line 374
  43. theorem OAI.ExactFourier.SignedBits.T_lower line 379
  44. theorem OAI.ExactFourier.SignedBits.T_diag line 384
  45. theorem OAI.ExactFourier.SignedBits.T_succ line 386