OAI/Analysis/IrrationalRotation/Rotation/CircleFutureEndpointLoss.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.CircleCoupling.coordinateLaw_raw_endpoint_le line 19
  2. theorem OAI.Invariant233.CircleCoupling.law_raw_endpoint_le line 38
  3. theorem OAI.Invariant233.CircleCoupling.raw_endpoint_pair_loss_le line 51
  4. def OAI.Invariant233.CircleCoupling.futureBadEvent line 64
  5. theorem OAI.Invariant233.CircleCoupling.futureBadEvent_measurable line 70
  6. theorem OAI.Invariant233.CircleCoupling.future_block_loss_le line 81
  7. theorem OAI.Invariant233.CircleCoupling.futureBadEvent_mass_le line 108
  8. theorem OAI.Invariant233.CircleCoupling.futureBadEvent_mass_le_ratio line 124
  9. theorem OAI.Invariant233.CircleCoupling.not_mem_futureBadEvent_iff line 136
  10. theorem OAI.Invariant233.CircleParameterLaws.cutoff_le_sampling_horizon line 156
  11. theorem OAI.Invariant233.CircleParameterLaws.tendsto_successive_cutoff_ratio line 166
  12. theorem OAI.Invariant233.CircleCoupling.tendsto_futureBadEvent_mass line 182