OAI/Combinatorics/SumProduct/Alignment/RoughArray01.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RoughArrayFace.Component line 32
  2. abbrev OAI.RoughArrayFace.Carrier line 33
  3. abbrev OAI.RoughArrayFace.Index line 34
  4. def OAI.RoughArrayFace.lattice line 37
  5. def OAI.RoughArrayFace.sourceState line 45
  6. def OAI.RoughArrayFace.inputShift line 53
  7. def OAI.RoughArrayFace.faceMap line 56
  8. lemma OAI.RoughArrayFace.faceMap_continuous line 64
  9. def OAI.RoughArrayFace.faceAction line 71
  10. def OAI.RoughArrayFace.coefficientsHomeomorph line 106
  11. def OAI.RoughArrayFace.jointWeight line 123
  12. lemma OAI.RoughArrayFace.coefficientsHomeomorph_one line 126
  13. lemma OAI.RoughArrayFace.joint_law line 131
  14. lemma OAI.RoughArrayFace.joint_law_polynomial line 144
  15. lemma OAI.RoughArrayFace.joint_law_weighted line 156
  16. def OAI.RoughArrayFace.jointChart line 168
  17. lemma OAI.RoughArrayFace.jointChart_at line 173
  18. lemma OAI.RoughArrayFace.jointChart_natpow line 181
  19. lemma OAI.RoughArrayFace.jointChart_canonicalLog line 187
  20. lemma OAI.RoughArrayFace.jointChart_grid line 201
  21. lemma OAI.RoughArrayFace.oneWeight_degree line 231
  22. lemma OAI.RoughArrayFace.oneWeight_mul line 239
  23. lemma OAI.RoughArrayFace.oneWeight_prod line 246
  24. lemma OAI.RoughArrayFace.source_coefficients_weighted line 264
  25. theorem OAI.RoughArrayFace.source_joint_geometry line 302