OAI/Geometry/LatticeCovering/Rates.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleLatticeCovering.FinalRates.firstSize line 12
  2. lemma OAI.SingleLatticeCovering.FinalRates.loglog_nat_atTop line 14
  3. lemma OAI.SingleLatticeCovering.FinalRates.log_nat_atTop line 17
  4. lemma OAI.SingleLatticeCovering.FinalRates.loglog_sq_littleO line 20
  5. lemma OAI.SingleLatticeCovering.FinalRates.firstSize_tendsto line 26
  6. lemma OAI.SingleLatticeCovering.FinalRates.eventually_firstSize_le_log line 30
  7. lemma OAI.SingleLatticeCovering.FinalRates.eventually_dimension_power line 43
  8. lemma OAI.SingleLatticeCovering.FinalRates.eventually_superlinear_power line 61
  9. lemma OAI.SingleLatticeCovering.FinalRates.cap_log_tendsto line 75
  10. lemma OAI.SingleLatticeCovering.FinalRates.eventually_log_power_bound line 107
  11. lemma OAI.SingleLatticeCovering.FinalRates.eventually_dimension_small line 117
  12. def OAI.SingleLatticeCovering.FinalRates.eta line 131
  13. lemma OAI.SingleLatticeCovering.FinalRates.eta_linear_lower line 133
  14. lemma OAI.SingleLatticeCovering.FinalRates.eventually_cap_linear line 142
  15. lemma OAI.SingleLatticeCovering.FinalRates.eventually_cap_eta line 157
  16. lemma OAI.SingleLatticeCovering.FinalRates.eventually_rpow_bound line 174
  17. lemma OAI.SingleLatticeCovering.FinalRates.sqrt_nat_atTop line 187
  18. lemma OAI.SingleLatticeCovering.FinalRates.sqrt_half_bound line 191
  19. lemma OAI.SingleLatticeCovering.FinalRates.eventually_discard_bound line 200
  20. lemma OAI.SingleLatticeCovering.FinalRates.eventually_label_criterion line 220
  21. def OAI.SingleLatticeCovering.Shear.pointBudget line 288
  22. lemma OAI.SingleLatticeCovering.Shear.pointBudget_pos line 291
  23. lemma OAI.SingleLatticeCovering.Shear.alphabetPoints_card_le_budget line 296
  24. def OAI.SingleLatticeCovering.Shear.patternTotal line 311
  25. lemma OAI.SingleLatticeCovering.Shear.patternTotal_bound line 314
  26. lemma OAI.SingleLatticeCovering.Shear.log_pointBudget line 318
  27. lemma OAI.SingleLatticeCovering.Shear.scalar_pattern_cost line 325
  28. lemma OAI.SingleLatticeCovering.Shear.all_pattern_cost line 362
  29. lemma OAI.SingleLatticeCovering.Shear.polynomial_pattern_cost line 379
  30. lemma OAI.SingleLatticeCovering.Shear.log_label_count line 407
  31. lemma OAI.SingleLatticeCovering.Shear.log_alphabet_bound line 429
  32. lemma OAI.SingleLatticeCovering.Shear.eventually_pattern_cost line 445
  33. lemma OAI.SingleLatticeCovering.FinalRates.exp_error line 501
  34. theorem OAI.SingleLatticeCovering.FinalRates.final_conditions line 515
  35. lemma OAI.SingleLatticeCovering.Horizontal.finite_threshold_selection line 580
  36. lemma OAI.SingleLatticeCovering.Horizontal.common_hole_sample line 617