OAI/Combinatorics/SumProduct/Alignment/IntegerArrays03.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceIntegerArrays.GlobalJoint.FlatG line 28
  2. abbrev OAI.SourceIntegerArrays.GlobalJoint.FlatN line 29
  3. abbrev OAI.SourceIntegerArrays.GlobalJoint.FlatQ line 30
  4. abbrev OAI.SourceIntegerArrays.GlobalJoint.FlatM line 31
  5. abbrev OAI.SourceIntegerArrays.GlobalJoint.FlatC line 34
  6. abbrev OAI.SourceIntegerArrays.GlobalJoint.FlatSk line 38
  7. abbrev OAI.SourceIntegerArrays.GlobalJoint.FlatA line 42
  8. abbrev OAI.SourceIntegerArrays.GlobalJoint.FlatΓ line 43
  9. abbrev OAI.SourceIntegerArrays.GlobalJoint.FlatW line 47
  10. abbrev OAI.SourceIntegerArrays.GlobalJoint.FlatHA line 51
  11. abbrev OAI.SourceIntegerArrays.GlobalJoint.FlatHw line 55
  12. abbrev OAI.SourceIntegerArrays.GlobalJoint.Full line 57
  13. abbrev OAI.SourceIntegerArrays.GlobalJoint.FullDim line 59
  14. abbrev OAI.SourceIntegerArrays.GlobalJoint.FullLattice line 60
  15. abbrev OAI.SourceIntegerArrays.GlobalJoint.FullFiltration line 62
  16. def OAI.SourceIntegerArrays.GlobalJoint.targetHom line 66
  17. lemma OAI.SourceIntegerArrays.GlobalJoint.targetHom_continuous line 72
  18. lemma OAI.SourceIntegerArrays.GlobalJoint.targetHom_lattice line 78
  19. def OAI.SourceIntegerArrays.GlobalJoint.targetCoset line 85
  20. def OAI.SourceIntegerArrays.GlobalJoint.rawJoint line 94
  21. lemma OAI.SourceIntegerArrays.GlobalJoint.target_rawJoint line 102
  22. def OAI.SourceIntegerArrays.GlobalJoint.FactorizedHaar line 111
  23. def OAI.SourcePhysicalDecay.AllCenteredHaar line 147
  24. theorem OAI.SourcePhysicalDecay.compatible_haar_allCenters line 166
  25. theorem OAI.SourceIntegerArrays.source_global_all_order_haar line 274