OAI/Analysis/IrrationalRotation/Product/ProductNorm.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.ProductNorm.floor_lower_bound line 10
  2. theorem OAI.Invariant233.ProductNorm.finite_cost_lower_bound line 15
  3. theorem OAI.Invariant233.ProductNorm.finite_weight_upper_bound line 32
  4. theorem OAI.Invariant233.ProductNorm.infinite_weight_upper_bound line 41
  5. theorem OAI.Invariant233.ProductNorm.root_upper_bound line 58
  6. theorem OAI.Invariant233.ProductNorm.tendsto_root_zero_of_exponential_bounds line 71
  7. theorem OAI.Invariant233.ProductNorm.block_angle_sum_lower_bound line 94
  8. theorem OAI.Invariant233.ProductNorm.one_le_block_cost line 107
  9. theorem OAI.Invariant233.ProductNorm.unbounded_prefix_cost line 119
  10. theorem OAI.Invariant233.ProductNorm.block_cost_tsum_eq_top line 128
  11. theorem OAI.Invariant233.ProductNorm.exists_finite_sum_gt_of_tsum_eq_top line 140
  12. theorem OAI.Invariant233.ProductNorm.tsum_eq_top_of_disjoint_blocks line 156
  13. theorem OAI.Invariant233.ProductNorm.block_coordinate_cost_tsum_eq_top line 181
  14. theorem OAI.Invariant233.ProductNorm.tendsto_root_zero_of_block_bounds line 212