OAI/Analysis/IrrationalRotation/Rotation/CircleBackgroundCost.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.BackgroundCost.backgroundNegative_eq_finiteAverage line 18
2. theorem OAI.Invariant233.BackgroundCost.backgroundNegative_bounds line 29
3. theorem OAI.Invariant233.BackgroundCost.continuous_backgroundNegative line 44
4. theorem OAI.Invariant233.BackgroundCost.measurable_backgroundCost line 56
5. theorem OAI.Invariant233.BackgroundCost.backgroundCost_ge_half line 62
6. theorem OAI.Invariant233.BackgroundCost.continuousOn_backgroundCost line 71
7. theorem OAI.Invariant233.BackgroundCost.tendsto_backgroundCost_atTop line 80
8. theorem OAI.Invariant233.BackgroundCost.integrable_backgroundCost line 91
9. theorem OAI.Invariant233.BackgroundCost.exists_background_cost line 111