OAI/Analysis/IrrationalRotation/Rotation/ExponentialWeightIntegral.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.tendsto_integral_min_atTop line 15
2. theorem OAI.Invariant233.truncatedLog_exponentialWeight_of_ne line 43
3. theorem OAI.Invariant233.lintegral_neg_log_exponentialWeight line 53
4. theorem OAI.Invariant233.tendsto_integral_truncatedLog_atBot line 63
5. theorem OAI.Invariant233.exists_truncatedLog_integral_lt line 81
6. theorem OAI.Invariant233.negLogCost_exponentialWeight_of_ne line 93
7. theorem OAI.Invariant233.hasNegInfiniteLogIntegral_exponentialWeight line 98
8. theorem OAI.Invariant233.scalarWeightDeterminant_eq_zero_of_log line 110
9. theorem OAI.Invariant233.isContinuousCircleWeight_exponentialWeight line 115