OAI/MathematicalPhysics/Heisenberg/CycleWeights.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.Cycle.weight_left_swap_le line 18
  2. lemma OAI.Heisenberg.Exposure.layerHistory_insert line 41
  3. def OAI.Heisenberg.Exposure.layerWeight line 56
  4. lemma OAI.Heisenberg.Exposure.layerWeight_nonneg line 60
  5. lemma OAI.Heisenberg.Exposure.layerWeight_one_le line 64
  6. lemma OAI.Heisenberg.Exposure.layerWeight_insertion line 67
  7. def OAI.Heisenberg.Exposure.layerPartition line 82
  8. def OAI.Heisenberg.Exposure.layerMass line 85
  9. lemma OAI.Heisenberg.Exposure.coin_weight_sum line 88
  10. lemma OAI.Heisenberg.Exposure.layerPartition_one_le line 92
  11. lemma OAI.Heisenberg.Exposure.layerMass_nonneg line 98
  12. lemma OAI.Heisenberg.Exposure.layerMass_sum line 104
  13. theorem OAI.Heisenberg.Exposure.layer_factorial_bound line 110
  14. theorem OAI.Heisenberg.Exposure.layer_nonquiet_bound line 127
  15. lemma OAI.Heisenberg.Exposure.bounded_euclidean_sq line 152
  16. theorem OAI.Heisenberg.Exposure.tilted_nonquiet_error line 159
  17. lemma OAI.Heisenberg.Exposure.exposedSweep_coins line 196
  18. theorem OAI.Heisenberg.Exposure.tilted_sweep_energy line 206
  19. abbrev OAI.Heisenberg.Geometry.Site line 246
  20. def OAI.Heisenberg.Geometry.Step line 248
  21. def OAI.Heisenberg.Geometry.Box line 251
  22. def OAI.Heisenberg.Geometry.Shell line 252
  23. def OAI.Heisenberg.Geometry.Reach line 254
  24. lemma OAI.Heisenberg.Geometry.step_symm line 257
  25. lemma OAI.Heisenberg.Geometry.reach_refl line 261
  26. lemma OAI.Heisenberg.Geometry.reach_trans line 264
  27. lemma OAI.Heisenberg.Geometry.reach_symm line 267
  28. lemma OAI.Heisenberg.Geometry.reach_mono line 274
  29. lemma OAI.Heisenberg.Geometry.step_update_succ line 278
  30. lemma OAI.Heisenberg.Geometry.reach_axis_nat line 285
  31. lemma OAI.Heisenberg.Geometry.reach_axis line 296