OAI/Analysis/IrrationalRotation/Product/ProductBlockTailBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.ProductModel.block_angle_sum_le line 14
  2. theorem OAI.Invariant233.ProductModel.enumerated_tail_angle_sum_le line 29
  3. def OAI.Invariant233.ProductModel.strictBlockTailEquiv line 72
  4. theorem OAI.Invariant233.ProductModel.enumerated_tail_angle_sum_le_four_div line 78
  5. theorem OAI.Invariant233.ProductModel.sampling_horizon_ratio_le_decay line 103
  6. theorem OAI.Invariant233.ProductModel.enumerated_sampled_tail_angle_sum_le_decay line 116
  7. def OAI.Invariant233.ProductModel.blockPrefixCoordinates line 145
  8. theorem OAI.Invariant233.ProductModel.mem_blockPrefixCoordinates line 149
  9. theorem OAI.Invariant233.ProductModel.blockPrefix_tail_tsum line 154
  10. theorem OAI.Invariant233.ProductModel.weighted_block_tailOrderFailure_le_decay line 162
  11. theorem OAI.Invariant233.ProductModel.orbitAverage_block_unordered_le_decay line 182
  12. theorem OAI.Invariant233.ProductModel.tendsto_four_mul_block_decay line 209
  13. theorem OAI.Invariant233.ProductModel.tendsto_four_mul_block_decay_of_growth line 220