OAI/Computability/FourierCircuit/RawWordBound.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ExactFourier.Packing.RawPrice.word_le line 15
  2. theorem OAI.ExactFourier.Packing.RawPrice.word_bound line 39
  3. theorem OAI.ExactFourier.Packing.RawPrice.monomial_zero line 43
  4. theorem OAI.ExactFourier.Packing.RawPrice.one line 49
  5. theorem OAI.ExactFourier.Packing.RawPrice.reindex_le line 51
  6. theorem OAI.ExactFourier.Packing.RawPrice.reindex line 59
  7. theorem OAI.ExactFourier.Packing.RawPrice.mul_le line 66
  8. theorem OAI.ExactFourier.Packing.RawPrice.monomial line 78
  9. abbrev OAI.ExactFourier.Packing.BiDomain line 105
  10. instance OAI.ExactFourier.Packing.(instance at line 108) line 108
  11. instance OAI.ExactFourier.Packing.(instance at line 110) line 110
  12. abbrev OAI.ExactFourier.Packing.biMatrix line 112
  13. theorem OAI.ExactFourier.Packing.RawPrice.tensor_le line 119
  14. theorem OAI.ExactFourier.Packing.RawPrice.tensor_ge line 131
  15. theorem OAI.ExactFourier.Packing.RawPrice.tensor line 153
  16. theorem OAI.ExactFourier.Packing.RawPrice.directSum_le line 157
  17. def OAI.ExactFourier.Packing.Word.Pure line 181
  18. theorem OAI.ExactFourier.Packing.Word.pure_nil line 182
  19. theorem OAI.ExactFourier.Packing.Word.pure_cons line 183
  20. theorem OAI.ExactFourier.Packing.Word.pure_append line 185
  21. theorem OAI.ExactFourier.Packing.Word.Pure.embed line 188
  22. theorem OAI.ExactFourier.Packing.Word.Pure.reindex line 193
  23. theorem OAI.ExactFourier.Packing.Word.pure_blockSum line 195
  24. theorem OAI.ExactFourier.Packing.Word.Pure.leftTensor line 203
  25. theorem OAI.ExactFourier.Packing.Word.Pure.rightTensor line 205
  26. theorem OAI.ExactFourier.Packing.Word.Pure.kronecker line 207
  27. theorem OAI.ExactFourier.Packing.pure_callWord line 210
  28. theorem OAI.ExactFourier.Packing.Word.Pure.length_eq_count line 213
  29. def OAI.ExactFourier.Packing.purePower line 228
  30. theorem OAI.ExactFourier.Packing.purePower_matrix line 231
  31. theorem OAI.ExactFourier.Packing.purePower_pure line 235
  32. theorem OAI.ExactFourier.Packing.purePower_count line 239
  33. theorem OAI.ExactFourier.Embedded.matrix_sumMap line 255
  34. theorem OAI.ExactFourier.Packing.RawPrice.embedded_le line 276
  35. theorem OAI.ExactFourier.Packing.RawPrice.paired_le line 281
  36. theorem OAI.ExactFourier.Packing.RawPrice.sum_swap line 331
  37. theorem OAI.ExactFourier.Packing.RawPrice.duplicate line 341
  38. theorem OAI.ExactFourier.Packing.RawPrice.power line 350
  39. theorem OAI.ExactFourier.Packing.RawPrice.balanced_calls line 359
  40. theorem OAI.ExactFourier.Packing.RawPrice.directSum_ge_nonempty line 364
  41. theorem OAI.ExactFourier.Packing.RawPrice.directSum line 414