OAI/Analysis/IrrationalRotation/Couplings/CircleCouplingAttenuation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Invariant233.CircleCoupling.measurableSet_tagEvent line 18
  2. lemma OAI.Invariant233.CircleCoupling.actual_tail_attenuation_of_ac_order line 28