OAI/Analysis/IrrationalRotation/Rotation/ContinuousWeightAssembly.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.CircleParameterLaws.measurable_rawBlock line 18
  2. theorem OAI.Invariant233.CircleParameterLaws.measurable_rawCost line 29
  3. theorem OAI.Invariant233.CircleParameterLaws.measurable_continuousCost line 32
  4. theorem OAI.Invariant233.CircleParameterLaws.continuousOn_continuousCost line 40
  5. theorem OAI.Invariant233.CircleParameterLaws.continuousCost_ge_half line 44
  6. theorem OAI.Invariant233.CircleParameterLaws.tendsto_continuousCost_atTop line 49
  7. theorem OAI.Invariant233.CircleParameterLaws.lintegral_continuousCost_eq_top line 54
  8. theorem OAI.Invariant233.CircleParameterLaws.isContinuousCircleWeight_continuousWeight line 61
  9. theorem OAI.Invariant233.CircleParameterLaws.continuousWeight_ae_exp_neg line 81
  10. theorem OAI.Invariant233.CircleParameterLaws.neg_log_continuousWeight_ae_coboundary line 88
  11. theorem OAI.Invariant233.CircleParameterLaws.exists_continuousWeight_factor_domain line 97
  12. theorem OAI.Invariant233.CircleParameterLaws.exists_continuous_weight_raw_coboundary line 114