OAI/MathematicalPhysics/Heisenberg/LayerExposure.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.Exposure.layerHistory line 22
  2. def OAI.Heisenberg.Exposure.layerRevealed line 25
  3. lemma OAI.Heisenberg.Exposure.layer_matches_iff line 29
  4. def OAI.Heisenberg.Exposure.layerExposure line 51
  5. lemma OAI.Heisenberg.Exposure.layerExposure_iff line 56
  6. lemma OAI.Heisenberg.Exposure.layerExposure_weight line 68
  7. theorem OAI.Heisenberg.Exposure.layer_exposure_disintegration line 73
  8. lemma OAI.Heisenberg.Exposure.invariant_of_agree line 107
  9. def OAI.Heisenberg.Exposure.residualCoins line 121
  10. lemma OAI.Heisenberg.Exposure.residual_agrees line 125
  11. lemma OAI.Heisenberg.Exposure.residual_invariant line 135
  12. lemma OAI.Heisenberg.Exposure.residual_determinantLaw line 144
  13. def OAI.Heisenberg.Exposure.residualHolePerm line 164
  14. theorem OAI.Heisenberg.Exposure.residual_holes_determinantLaw line 174
  15. lemma OAI.Heisenberg.Exposure.sameCycle_congr line 197
  16. def OAI.Heisenberg.Exposure.splitHolePerm line 206
  17. lemma OAI.Heisenberg.Exposure.allHit_splitHolePerm line 213
  18. theorem OAI.Heisenberg.Exposure.exposed_nextPin_first_moment line 238