OAI/Probability/DirectionalWalk/EntropyUpperBound.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalZeroOne.axisCube_log_bound line 12
  2. lemma OAI.DirectionalZeroOne.summable_shifted_axisTail line 43
  3. lemma OAI.DirectionalZeroOne.axis_delta_dyadic line 51
  4. lemma OAI.DirectionalZeroOne.dyadic_markov_ratio line 84
  5. lemma OAI.DirectionalZeroOne.commonBand_good_label line 92
  6. lemma OAI.DirectionalZeroOne.sum_trailing_windows line 127
  7. lemma OAI.DirectionalZeroOne.sum_early_labels line 153
  8. lemma OAI.DirectionalZeroOne.window_count_lower line 164
  9. lemma OAI.DirectionalZeroOne.tendsto_dyadic_quadratic line 207
  10. lemma OAI.DirectionalZeroOne.eventually_dyadic_quadratic_lt line 217
  11. lemma OAI.DirectionalZeroOne.dyadic_decay_le_quadratic line 223
  12. lemma OAI.DirectionalZeroOne.self_dyadic_decay_le_quadratic line 229
  13. lemma OAI.DirectionalZeroOne.dyadic_decay_antitone line 234
  14. lemma OAI.DirectionalZeroOne.dyadic_power_cancel line 238
  15. lemma OAI.DirectionalZeroOne.dyadic_delta_identity line 243
  16. lemma OAI.DirectionalZeroOne.dyadic_large_parameters line 248