OAI/NumberTheory/Jacobsthal/Estimates/InitialOddDraw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.InitialOddDraw.firstOddUpdate line 16
2. theorem OAI.Erdos970.NumberTheoryLean.InitialOddDraw.firstOddUpdate_measurable line 18
3. def OAI.Erdos970.NumberTheoryLean.InitialOddDraw.firstOdd line 21
4. instance OAI.Erdos970.NumberTheoryLean.InitialOddDraw.firstOdd_isMarkovKernel line 23
5. theorem OAI.Erdos970.NumberTheoryLean.InitialOddDraw.firstOdd_full_draw line 26
6. theorem OAI.Erdos970.NumberTheoryLean.InitialOddDraw.firstOdd_cost_bounds line 34
7. theorem OAI.Erdos970.NumberTheoryLean.InitialOddDraw.firstOdd_drift_lintegral line 42
8. theorem OAI.Erdos970.NumberTheoryLean.InitialOddDraw.firstOdd_weighted_exponential line 55