OAI/NumberTheory/GaussianMoat/Smoothing.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GaussianMoat.window_power_step line 9
  2. lemma OAI.GaussianMoat.window_power_nonneg line 15
  3. lemma OAI.GaussianMoat.window_power_one line 16
  4. lemma OAI.GaussianMoat.smaller_window_operations line 18
  5. lemma OAI.GaussianMoat.windowBlocks_length_bound line 45
  6. lemma OAI.GaussianMoat.windowBlocks_length_bound_of_bins line 60
  7. lemma OAI.GaussianMoat.eventually_window_length line 76
  8. def OAI.GaussianMoat.windowSmoothing line 86
  9. lemma OAI.GaussianMoat.windowSmoothing_pos line 89
  10. lemma OAI.GaussianMoat.windowSmoothing_bounds line 92
  11. theorem OAI.GaussianMoat.eventually_suffix_cost line 108
  12. def OAI.GaussianMoat.coverageRepetitions line 139
  13. lemma OAI.GaussianMoat.coverageRepetitions_pos line 141
  14. lemma OAI.GaussianMoat.coverageRepetitions_bounds line 144
  15. lemma OAI.GaussianMoat.eventually_coverage_hazard line 153
  16. lemma OAI.GaussianMoat.eventually_coverage_data_cost line 183
  17. lemma OAI.GaussianMoat.eventually_package_displacement line 210
  18. theorem OAI.GaussianMoat.coverage_from_scalar_guards line 227
  19. lemma OAI.GaussianMoat.binEntropy_small_exp line 249
  20. lemma OAI.GaussianMoat.exp_ratio_bound line 266
  21. theorem OAI.GaussianMoat.eventually_smoothing_guard line 276
  22. lemma OAI.GaussianMoat.eventually_smoothing_total line 318