OAI/Analysis/IrrationalRotation/Product/ProductScaleConsequences.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.ProductScaleLaws.m_pos line 15
  2. theorem OAI.Invariant233.ProductScaleLaws.C_pos line 17
  3. theorem OAI.Invariant233.ProductScaleLaws.real_K_pos line 22
  4. theorem OAI.Invariant233.ProductScaleLaws.real_K_double line 24
  5. theorem OAI.Invariant233.ProductScaleLaws.summable_reciprocal line 27
  6. theorem OAI.Invariant233.ProductScaleLaws.reciprocal_tail_bound line 30
  7. theorem OAI.Invariant233.ProductScaleLaws.prefix_count_succ_le line 34
  8. theorem OAI.Invariant233.ProductScaleLaws.N_le_square line 40
  9. theorem OAI.Invariant233.ProductScaleLaws.a_bounds line 45
  10. theorem OAI.Invariant233.ProductScaleLaws.b_bounds line 56
  11. theorem OAI.Invariant233.ProductScaleLaws.K_strictMono line 75
  12. theorem OAI.Invariant233.ProductScaleLaws.m_lt_next_K line 81
  13. theorem OAI.Invariant233.ProductScaleLaws.m_strictMono line 89
  14. theorem OAI.Invariant233.ProductScaleLaws.N_strictMono line 94
  15. theorem OAI.Invariant233.ProductScaleLaws.K_ge_100 line 100
  16. theorem OAI.Invariant233.ProductScaleLaws.m_ge_pow_self line 103
  17. theorem OAI.Invariant233.ProductScaleLaws.reciprocal_sum_le line 110
  18. theorem OAI.Invariant233.ProductScaleLaws.prefixCost_nonneg line 117
  19. theorem OAI.Invariant233.ProductScaleLaws.coefficientBound_ge_one line 122
  20. theorem OAI.Invariant233.ProductScaleLaws.one_le_C_div_K line 126