OAI/Analysis/IrrationalRotation/Rotation/AnalyticWeightBridge.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.negLogCost_zero line 12
  2. theorem OAI.Invariant233.negLogCost_of_pos line 15
  3. theorem OAI.Invariant233.lintegral_negLogCost_eq_of_ae_pos line 21
  4. theorem OAI.Invariant233.hasNegInfiniteLogIntegral_iff_of_ae_pos line 29
  5. theorem OAI.Invariant233.scalarWeightDeterminant_eq_zero_of_log_integral line 36
  6. theorem OAI.Invariant233.ae_pos_of_nonneg_singleton_zero line 43
  7. theorem OAI.Invariant233.circleMeasure_singleton line 51
  8. theorem OAI.Invariant233.IsContinuousCircleWeight.ae_pos line 56
  9. theorem OAI.Invariant233.exists_continuous_circle_weight_of_cost line 63
  10. theorem OAI.Invariant233.IsContinuousCircleWeight.exists_truncated_log_integral_lt line 79