OAI/MathematicalPhysics/Heisenberg/SimultaneousPins.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.Pin.subsetLaw line 24
  2. lemma OAI.Heisenberg.Pin.subsetLaw_nonneg line 28
  3. lemma OAI.Heisenberg.Pin.presence_subsetLaw line 34
  4. lemma OAI.Heisenberg.Pin.presencePolynomial_subsetLaw line 54
  5. lemma OAI.Heisenberg.Pin.subsetMonomial_image line 66
  6. lemma OAI.Heisenberg.Pin.subsetLaw_output line 71
  7. theorem OAI.Heisenberg.Pin.finite_output_return_bound line 77
  8. lemma OAI.Heisenberg.Cycle.missingCount_antitone line 101
  9. lemma OAI.Heisenberg.Cycle.missingCount_union_le line 108
  10. theorem OAI.Heisenberg.Cycle.pin_weight_comparison line 134
  11. theorem OAI.Heisenberg.Return.nextPoint_preserves_iff line 154
  12. lemma OAI.Heisenberg.Return.subset_image_iff_mapsTo line 188
  13. lemma OAI.Heisenberg.Pin.input_output_card line 213
  14. lemma OAI.Heisenberg.Pin.input_output_sum line 229
  15. def OAI.Heisenberg.Pin.pinPartition line 238
  16. lemma OAI.Heisenberg.Pin.pinPartition_pos line 242
  17. def OAI.Heisenberg.Pin.pinDensity line 250
  18. lemma OAI.Heisenberg.Pin.pinDensity_nonneg line 254
  19. lemma OAI.Heisenberg.Pin.pinDensity_sum line 260
  20. lemma OAI.Heisenberg.Pin.stable_pinDensity line 267
  21. lemma OAI.Heisenberg.Pin.finite_input_return_bound line 286