OAI/Dynamics/EntropyCounterexample/MapPassagePhase.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem340.Construction.finite_main_step_of_rawMap line 10
2. def OAI.Problem340.Construction.passageWeight line 22
3. def OAI.Problem340.Construction.orbitReadoutCoeff line 25
4. def OAI.Problem340.Construction.orbitSaturatedRegister line 28
5. lemma OAI.Problem340.Construction.passageWeight_nonneg line 31
6. theorem OAI.Problem340.Construction.rawMap_passage_phase line 35
7. theorem OAI.Problem340.Construction.rawMap_passage_square_le line 62
8. theorem OAI.Problem340.Construction.rawMap_passage_escape line 88