OAI/MathematicalPhysics/Heisenberg/KilledContractions.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.MeshPair.killedPermutation line 26
  2. def OAI.Heisenberg.MeshPair.killedCoin line 29
  3. lemma OAI.Heisenberg.MeshPair.killedCoin_generator line 32
  4. lemma OAI.Heisenberg.MeshPair.killedCoin_support line 54
  5. lemma OAI.Heisenberg.MeshPair.killedCoin_bound line 60
  6. def OAI.Heisenberg.MeshPair.killedSweep line 66
  7. lemma OAI.Heisenberg.MeshPair.killedSweep_support line 71
  8. lemma OAI.Heisenberg.MeshPair.killedSweep_eq line 78
  9. theorem OAI.Heisenberg.MeshPair.killedSweep_energy line 90
  10. structure OAI.Heisenberg.MatrixContraction.DoublySubstochastic line 111
  11. lemma OAI.Heisenberg.MatrixContraction.DoublySubstochastic.transpose line 116
  12. lemma OAI.Heisenberg.MatrixContraction.DoublySubstochastic.mul line 119
  13. lemma OAI.Heisenberg.MatrixContraction.weighted_square line 138
  14. theorem OAI.Heisenberg.MatrixContraction.contraction line 145
  15. theorem OAI.Heisenberg.MatrixContraction.of_partial_permutation line 160
  16. theorem OAI.Heisenberg.MatrixContraction.weighted_average line 178
  17. def OAI.Heisenberg.MatrixContraction.squareNorm line 200
  18. def OAI.Heisenberg.MatrixContraction.dot line 202
  19. lemma OAI.Heisenberg.MatrixContraction.dot_half line 204
  20. lemma OAI.Heisenberg.MatrixContraction.dot_transpose line 213
  21. theorem OAI.Heisenberg.MatrixContraction.two_ends line 223
  22. def OAI.Heisenberg.MeshPair.killedMatrix line 242
  23. lemma OAI.Heisenberg.MeshPair.killedMatrix_substochastic line 245
  24. def OAI.Heisenberg.MeshPair.residualMatrix line 263
  25. lemma OAI.Heisenberg.MeshPair.residualMatrix_substochastic line 267
  26. def OAI.Heisenberg.MeshPair.euclideanMap line 285
  27. lemma OAI.Heisenberg.MeshPair.euclideanMap_apply line 291
  28. lemma OAI.Heisenberg.MeshPair.euclideanMap_contraction line 295
  29. lemma OAI.Heisenberg.MeshPair.killedMatrix_apply line 301
  30. lemma OAI.Heisenberg.MeshPair.killedMatrix_identity line 313
  31. lemma OAI.Heisenberg.MeshPair.residual_quiet line 322