OAI/Analysis/MarkovType/FiniteGeometricBands.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.dyadicMagnitudeBand line 21
  2. theorem OAI.MarkovSuperreflexivity.half_pow_antitone line 24
  3. theorem OAI.MarkovSuperreflexivity.dyadicMagnitudeBand_exists line 30
  4. theorem OAI.MarkovSuperreflexivity.dyadicMagnitudeBand_unique line 34
  5. theorem OAI.MarkovSuperreflexivity.dyadicMagnitudeBand_pos line 46
  6. theorem OAI.MarkovSuperreflexivity.finite_dyadicMagnitudeBand_cutoff line 50
  7. theorem OAI.MarkovSuperreflexivity.dyadicMagnitudeBand_card_lt line 61
  8. theorem OAI.MarkovSuperreflexivity.norm_le_band_bound line 87
  9. def OAI.MarkovSuperreflexivity.bandGeometricRatio line 95
  10. theorem OAI.MarkovSuperreflexivity.bandGeometricRatio_pos line 98
  11. theorem OAI.MarkovSuperreflexivity.bandGeometricRatio_lt_one line 101
  12. theorem OAI.MarkovSuperreflexivity.band_length_times_size line 113
  13. theorem OAI.MarkovSuperreflexivity.finite_geometric_sum_le line 124
  14. theorem OAI.MarkovSuperreflexivity.finite_band_bound line 136