OAI/Geometry/LatticeCovering/Rounding.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.Folded.square_difference_le line 23
  2. lemma OAI.SingleLatticeCovering.Folded.gamma1_rounding_upper line 34
  3. lemma OAI.SingleLatticeCovering.Folded.gamma1_rounding line 42
  4. lemma OAI.SingleLatticeCovering.Folded.abs_sub_bitValue line 53
  5. lemma OAI.SingleLatticeCovering.Folded.density_rounding_upper line 59
  6. lemma OAI.SingleLatticeCovering.Folded.product_rounding line 73
  7. lemma OAI.SingleLatticeCovering.Folded.folded_rounding_upper line 82
  8. lemma OAI.SingleLatticeCovering.Folded.atom_eq_product line 90
  9. lemma OAI.SingleLatticeCovering.Folded.atom_rounding_upper line 94
  10. lemma OAI.SingleLatticeCovering.Folded.remove_exp_factor line 109
  11. theorem OAI.SingleLatticeCovering.Folded.rounding line 116
  12. lemma OAI.SingleLatticeCovering.Folded.grid_anchor_mem_cube line 138
  13. lemma OAI.SingleLatticeCovering.Folded.grid_distance line 146
  14. lemma OAI.SingleLatticeCovering.Folded.grid_folded_integrable line 151
  15. lemma OAI.SingleLatticeCovering.Folded.grid_integral_upper line 158
  16. lemma OAI.SingleLatticeCovering.Folded.grid_integral_lower line 170
  17. def OAI.SingleLatticeCovering.Folded.gridMass line 186
  18. lemma OAI.SingleLatticeCovering.Folded.grid_integral_total line 189
  19. lemma OAI.SingleLatticeCovering.Folded.halfCube_ae_cube line 220
  20. lemma OAI.SingleLatticeCovering.Folded.grid_selected_integral line 224
  21. lemma OAI.SingleLatticeCovering.Folded.grid_integral_event line 239
  22. lemma OAI.SingleLatticeCovering.Folded.log_folded_grid_distance line 258
  23. def OAI.SingleLatticeCovering.Folded.gridEligible line 273
  24. lemma OAI.SingleLatticeCovering.Folded.round_into_eligible line 278
  25. lemma OAI.SingleLatticeCovering.Folded.gridMass_nonneg line 321
  26. lemma OAI.SingleLatticeCovering.Folded.gridMass_mono line 325
  27. lemma OAI.SingleLatticeCovering.Folded.exp_small_upper line 330
  28. lemma OAI.SingleLatticeCovering.Folded.grid_from_continuous line 335
  29. def OAI.SingleLatticeCovering.Folded.continuousGood line 390
  30. lemma OAI.SingleLatticeCovering.Folded.continuousGood_measurable line 394
  31. lemma OAI.SingleLatticeCovering.Folded.prime_in_log_interval line 414
  32. theorem OAI.SingleLatticeCovering.Folded.block_prime line 434
  33. theorem OAI.SingleLatticeCovering.Folded.eventually_block_prime line 444
  34. lemma OAI.SingleLatticeCovering.Folded.eventually_totalMass_half line 472
  35. lemma OAI.SingleLatticeCovering.Folded.logMean_tendsto line 481
  36. def OAI.SingleLatticeCovering.Folded.heightR line 491
  37. lemma OAI.SingleLatticeCovering.Folded.heightR_tendsto line 493
  38. lemma OAI.SingleLatticeCovering.Folded.height_tendsto line 496
  39. lemma OAI.SingleLatticeCovering.Folded.heightR_sq line 499
  40. lemma OAI.SingleLatticeCovering.Folded.heightR_pos line 502
  41. lemma OAI.SingleLatticeCovering.Folded.heightR_exp line 505
  42. lemma OAI.SingleLatticeCovering.Folded.totalMass_power_loss line 511
  43. lemma OAI.SingleLatticeCovering.Folded.height_totalMass_power_loss line 522
  44. lemma OAI.SingleLatticeCovering.Folded.eventually_height_prime line 542
  45. lemma OAI.SingleLatticeCovering.Folded.eventually_logpow_bound line 557
  46. lemma OAI.SingleLatticeCovering.Folded.eventually_height_bound line 564
  47. lemma OAI.SingleLatticeCovering.Folded.eventually_height_square_le line 577
  48. lemma OAI.SingleLatticeCovering.Folded.eventually_central_mean line 584
  49. lemma OAI.SingleLatticeCovering.Folded.eventually_log_variance_tail line 611