OAI/Computability/FourierCircuit/ComparisonRename.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactFourier.Packing.mapPair line 15
  2. def OAI.ExactFourier.Packing.speciesEquiv line 23
  3. abbrev OAI.ExactFourier.Packing.pairEquiv line 27
  4. theorem OAI.ExactFourier.Packing.speciesEquiv_matrix line 31
  5. theorem OAI.ExactFourier.Packing.pairEquiv_matrix line 40
  6. abbrev OAI.ExactFourier.Packing.PairComparison.rename line 47
  7. theorem OAI.ExactFourier.Packing.pairPrice_map line 55
  8. theorem OAI.ExactFourier.Packing.PairComparison.rename_ineq line 65
  9. structure OAI.ExactFourier.Packing.GMatrix line 79
  10. abbrev OAI.ExactFourier.Packing.GMatrix.domain line 83
  11. def OAI.ExactFourier.Packing.shearG line 85
  12. abbrev OAI.ExactFourier.Packing.shearD line 86
  13. abbrev OAI.ExactFourier.Packing.shearA line 87
  14. theorem OAI.ExactFourier.Packing.GMatrix.upper_exists line 89
  15. def OAI.ExactFourier.Packing.GMatrix.upperCost line 94
  16. def OAI.ExactFourier.Packing.GMatrix.upperWord line 95
  17. theorem OAI.ExactFourier.Packing.GMatrix.upperWord_matrix line 96
  18. theorem OAI.ExactFourier.Packing.GMatrix.upperWord_weight line 98
  19. structure OAI.ExactFourier.Packing.GlobalComparison line 101
  20. def OAI.ExactFourier.Packing.GlobalComparison.holds line 106
  21. def OAI.ExactFourier.Packing.GlobalConstraints line 110
  22. theorem OAI.ExactFourier.Packing.Word.continuous_weight line 112
  23. theorem OAI.ExactFourier.Packing.GlobalComparison.closed line 123
  24. theorem OAI.ExactFourier.Packing.family_cast_matrix line 134
  25. abbrev OAI.ExactFourier.Packing.toGlobalComparison line 141
  26. theorem OAI.ExactFourier.Packing.GlobalConstraints.apply line 148
  27. theorem OAI.ExactFourier.Packing.pair_baseline_sum line 169
  28. abbrev OAI.ExactFourier.Packing.familyKey line 236
  29. def OAI.ExactFourier.Packing.familyProgram line 240
  30. def OAI.ExactFourier.Packing.familyMultiplicity line 245
  31. theorem OAI.ExactFourier.Packing.familyProgram_matrix line 250
  32. theorem OAI.ExactFourier.Packing.familyMultiplicity_key line 257
  33. theorem OAI.ExactFourier.Packing.familyMultiplicity_scale line 266
  34. theorem OAI.ExactFourier.Packing.family_saving line 281
  35. theorem OAI.ExactFourier.Packing.family_total_scale line 303
  36. def OAI.ExactFourier.Packing.framedSlot line 325
  37. def OAI.ExactFourier.Packing.slotCall line 328
  38. def OAI.ExactFourier.Packing.slotMono line 332
  39. theorem OAI.ExactFourier.Packing.slotMono_monomial line 336
  40. def OAI.ExactFourier.Packing.slotMatrix line 342
  41. theorem OAI.ExactFourier.Packing.slotMatrix_extend line 344
  42. theorem OAI.ExactFourier.Packing.slotMatrix_product line 355
  43. def OAI.ExactFourier.Packing.framedLayer line 367
  44. theorem OAI.ExactFourier.Packing.framedLayer_product line 371
  45. theorem OAI.ExactFourier.Packing.gather_framed_slot line 390