OAI/Analysis/IrrationalRotation/Sampling/SamplingHorizon.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.SamplingHorizon.rpow_ratio_le_inv line 12
  2. theorem OAI.Invariant233.SamplingHorizon.horizon_ratio_le_inv line 20
  3. theorem OAI.Invariant233.SamplingHorizon.decay_le_inv line 31
  4. theorem OAI.Invariant233.SamplingHorizon.tendsto_horizon_ratio line 36
  5. theorem OAI.Invariant233.SamplingHorizon.tendsto_horizon_ratio_of_pow_two_le line 49
  6. theorem OAI.Invariant233.SamplingHorizon.ceiling_ratio_le_decay line 57
  7. theorem OAI.Invariant233.SamplingHorizon.ceiling_ratio_le_inv line 77
  8. theorem OAI.Invariant233.SamplingHorizon.tendsto_ceiling_ratio line 82
  9. theorem OAI.Invariant233.SamplingHorizon.eventually_scale_gap line 94
  10. theorem OAI.Invariant233.SamplingHorizon.twice_lt_ceiling_cutoff line 107
  11. theorem OAI.Invariant233.SamplingHorizon.tendsto_ceiling_cutoff line 117
  12. theorem OAI.Invariant233.SamplingHorizon.eventually_block_size line 124
  13. theorem OAI.Invariant233.SamplingHorizon.exists_block_size line 152
  14. theorem OAI.Invariant233.SamplingHorizon.eventually_stage_size line 161
  15. theorem OAI.Invariant233.SamplingHorizon.exists_stage_size line 180
  16. theorem OAI.Invariant233.SamplingHorizon.exists_attenuation line 190
  17. theorem OAI.Invariant233.SamplingHorizon.exists_next_gain line 208