OAI/Computability/FourierCircuit/SignedPrice.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactFourier.SignedBits.start line 13
  2. def OAI.ExactFourier.SignedBits.oldInputs line 15
  3. def OAI.ExactFourier.SignedBits.oldOutputs line 17
  4. def OAI.ExactFourier.SignedBits.transition line 19
  5. theorem OAI.ExactFourier.SignedBits.start_lower line 22
  6. theorem OAI.ExactFourier.SignedBits.start_diag line 33
  7. def OAI.ExactFourier.SignedBits.bottom line 36
  8. theorem OAI.ExactFourier.SignedBits.input_rows line 38
  9. theorem OAI.ExactFourier.SignedBits.output_rows line 42
  10. theorem OAI.ExactFourier.SignedBits.transition_solve line 46
  11. theorem OAI.ExactFourier.SignedBits.transition_eq line 50
  12. def OAI.ExactFourier.SignedBits.zdiag line 54
  13. theorem OAI.ExactFourier.SignedBits.zdiag_monomial line 57
  14. theorem OAI.ExactFourier.SignedBits.transition_sign line 61
  15. theorem OAI.ExactFourier.SignedBits.start_tensor line 66
  16. theorem OAI.ExactFourier.SignedBits.price_step line 71
  17. theorem OAI.ExactFourier.SignedBits.price line 84
  18. def OAI.ExactFourier.SignedBits.J line 100
  19. theorem OAI.ExactFourier.SignedBits.J_commute line 105
  20. theorem OAI.ExactFourier.SignedBits.J_orthogonal line 113
  21. theorem OAI.ExactFourier.SignedBits.J_sign line 121
  22. theorem OAI.ExactFourier.SignedBits.offDiagonal_monomial line 133
  23. theorem OAI.ExactFourier.SignedBits.J_monomial line 143
  24. def OAI.ExactFourier.SignedBits.Gamma line 151
  25. theorem OAI.ExactFourier.SignedBits.Gamma_square line 154
  26. theorem OAI.ExactFourier.SignedBits.Gamma_unit line 156
  27. theorem OAI.ExactFourier.SignedBits.Gamma_symmetry line 159
  28. theorem OAI.ExactFourier.SignedBits.D_star line 162
  29. theorem OAI.ExactFourier.SignedBits.J_star line 169
  30. theorem OAI.ExactFourier.SignedBits.Gamma_star line 176
  31. def OAI.ExactFourier.support line 191
  32. def OAI.ExactFourier.nnz line 192
  33. theorem OAI.ExactFourier.mem_support line 194
  34. theorem OAI.ExactFourier.nnz_zero line 196
  35. theorem OAI.ExactFourier.nnz_neg line 199
  36. theorem OAI.ExactFourier.nnz_add_le line 202
  37. theorem OAI.ExactFourier.nnz_sub_le line 211
  38. theorem OAI.ExactFourier.nnz_one line 214
  39. theorem OAI.ExactFourier.nnz_kronecker line 220
  40. theorem OAI.ExactFourier.nnz_monomial_mul line 230
  41. theorem OAI.ExactFourier.nnz_sum line 254
  42. theorem OAI.ExactFourier.nnz_fromBlocks line 259
  43. theorem OAI.ExactFourier.SignedBits.D_count line 267
  44. theorem OAI.ExactFourier.SignedBits.Gamma_count line 275
  45. def OAI.ExactFourier.Similarity.conj line 290
  46. theorem OAI.ExactFourier.Similarity.one line 292
  47. theorem OAI.ExactFourier.Similarity.add line 295
  48. theorem OAI.ExactFourier.Similarity.sub line 297
  49. theorem OAI.ExactFourier.Similarity.smul line 299
  50. theorem OAI.ExactFourier.Similarity.zero line 301
  51. theorem OAI.ExactFourier.Similarity.mul line 303
  52. theorem OAI.ExactFourier.Similarity.unit line 309
  53. theorem OAI.ExactFourier.Similarity.diagonal_linear line 312
  54. theorem OAI.ExactFourier.Similarity.diagonal_linear_sub line 318
  55. def OAI.ExactFourier.RealMatrix.complex line 331
  56. theorem OAI.ExactFourier.RealMatrix.map_mul line 333
  57. theorem OAI.ExactFourier.RealMatrix.map_one line 336
  58. theorem OAI.ExactFourier.RealMatrix.map_zero line 338
  59. theorem OAI.ExactFourier.RealMatrix.map_transpose line 340
  60. theorem OAI.ExactFourier.RealMatrix.map_diagonal line 342
  61. theorem OAI.ExactFourier.RealMatrix.map_add line 345
  62. theorem OAI.ExactFourier.RealMatrix.map_sub line 348
  63. theorem OAI.ExactFourier.RealMatrix.unit line 352
  64. theorem OAI.ExactFourier.RealMatrix.inv line 358
  65. theorem OAI.ExactFourier.RealMatrix.diagonalization line 363
  66. theorem OAI.ExactFourier.RealMatrix.complex_re line 383
  67. theorem OAI.ExactFourier.RealMatrix.re_symm line 394