OAI/Analysis/IrrationalRotation/Rotation/CircleCocycleWindow.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.CircleParameterData.sum_flattenedCost_prefix line 14
  2. theorem OAI.Invariant233.CircleParameterData.coordinate_mem_Ico line 35

    Also declared: OAI/Analysis/IrrationalRotation/Analysis/RationalGraphTrimming.lean:13 (same declaration text).

  3. theorem OAI.Invariant233.CircleParameterData.exists_late_block line 40
  4. theorem OAI.Invariant233.CircleParameterData.coordinate_circleValue line 53
  5. theorem OAI.Invariant233.CocycleWindowBounds.exclusions_of_rounding line 65
  6. theorem OAI.Invariant233.CircleParameterLaws.coordinate_raw_error_le line 82
  7. theorem OAI.Invariant233.CircleParameterLaws.raw_good_event_exclusions line 97
  8. theorem OAI.Invariant233.CircleParameterLaws.current_margin_eq line 121
  9. theorem OAI.Invariant233.CircleParameterLaws.source_good_event_exclusions line 128
  10. theorem OAI.Invariant233.CircleParameterLaws.finite_window_coefficients line 153