OAI/MathematicalPhysics/Heisenberg/TwoEndedReturns.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Heisenberg.Pin.unpinned line 43
2. theorem OAI.Heisenberg.Pin.finite_pin_induction line 45
3. lemma OAI.Heisenberg.Clocks.factorial_lower_of_pos line 109
4. lemma OAI.Heisenberg.Clocks.geometric_le_recip line 120
5. theorem OAI.Heisenberg.Clocks.binomial_clock_tail line 128
6. lemma OAI.Heisenberg.Exposure.exposedStep_cutFactors line 166
7. theorem OAI.Heisenberg.Exposure.period_return_two_ends line 171