OAI/MathematicalPhysics/Heisenberg/PinDensity.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.Pin.pinDensity_comparison line 32
  2. def OAI.Heisenberg.Pin.testPins line 50
  3. lemma OAI.Heisenberg.Pin.mem_testPins line 54
  4. lemma OAI.Heisenberg.Pin.card_testPins line 58
  5. lemma OAI.Heisenberg.Pin.testPins_event line 64
  6. def OAI.Heisenberg.Pin.returnFraction line 76
  7. lemma OAI.Heisenberg.Pin.pinned_input_return_bound line 81
  8. theorem OAI.Heisenberg.Pin.finite_simultaneous_pin_test line 92
  9. def OAI.Heisenberg.FiniteExchange.Bits line 125
  10. instance OAI.Heisenberg.FiniteExchange.bitsFintype line 128
  11. def OAI.Heisenberg.FiniteExchange.weight line 132
  12. def OAI.Heisenberg.FiniteExchange.endpoint line 136
  13. lemma OAI.Heisenberg.FiniteExchange.weight_nonneg line 141
  14. lemma OAI.Heisenberg.FiniteExchange.weight_sum line 152
  15. theorem OAI.Heisenberg.FiniteExchange.endpoint_stable line 163
  16. theorem OAI.Heisenberg.FiniteExchange.finite_history_pin_test line 184
  17. lemma OAI.Heisenberg.Pin.lawSymbol_reparam line 219
  18. lemma OAI.Heisenberg.Pin.stable_array line 223
  19. theorem OAI.Heisenberg.LayeredExchange.stable_wiring line 249
  20. def OAI.Heisenberg.LayeredExchange.layerWeight line 268
  21. def OAI.Heisenberg.LayeredExchange.coinWiring line 271
  22. lemma OAI.Heisenberg.LayeredExchange.layerWeight_nonneg line 275
  23. lemma OAI.Heisenberg.LayeredExchange.layerWeight_sum line 282
  24. lemma OAI.Heisenberg.LayeredExchange.coinWiring_stable line 287
  25. theorem OAI.Heisenberg.LayeredExchange.layer_pin_test line 293