OAI/Geometry/LatticeCovering/PrimeGrids.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.RogersPreparation.eventually_const_mul_rpow_lt line 32
  2. lemma OAI.SingleLatticeCovering.RogersPreparation.eventually_subcritical_minor_bound line 51
  3. def OAI.SingleLatticeCovering.ConvexGrid.primeScale line 75
  4. lemma OAI.SingleLatticeCovering.ConvexGrid.primeScale_tendsto line 77
  5. lemma OAI.SingleLatticeCovering.ConvexGrid.primeScale_pos line 81
  6. lemma OAI.SingleLatticeCovering.ConvexGrid.primeScale_pow line 84
  7. lemma OAI.SingleLatticeCovering.ConvexGrid.primeScale_pow_mul line 88
  8. lemma OAI.SingleLatticeCovering.ConvexGrid.prime_grid_density line 92
  9. lemma OAI.SingleLatticeCovering.ConvexGrid.eventually_prime_grid_bound line 101
  10. theorem OAI.SingleLatticeCovering.ConvexGrid.eventually_prime_circuit_count_le line 129
  11. lemma OAI.SingleLatticeCovering.GridProbability.cardinality_tendsto_atTop line 152
  12. lemma OAI.SingleLatticeCovering.GridProbability.normalized_choose_tendsto line 162
  13. lemma OAI.SingleLatticeCovering.GridProbability.binomial_polynomial_limit line 191
  14. lemma OAI.SingleLatticeCovering.GridProbability.binomial_envelope_le_exp line 199
  15. lemma OAI.SingleLatticeCovering.GridProbability.upper_envelope_limit line 208
  16. def OAI.SingleLatticeCovering.ConvexGrid.primeGridVoid line 229
  17. def OAI.SingleLatticeCovering.ConvexGrid.continuumCircuitError line 235
  18. theorem OAI.SingleLatticeCovering.ConvexGrid.eventually_primeGridVoid_le line 241
  19. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexConstant_sq_ratio line 308
  20. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexConstant_succ_sq line 316
  21. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexConstant_succ_le line 333
  22. def OAI.SingleLatticeCovering.SimplexYoung.circuitTerm line 354
  23. lemma OAI.SingleLatticeCovering.SimplexYoung.circuitTerm_nonneg line 357
  24. lemma OAI.SingleLatticeCovering.SimplexYoung.circuitTerm_succ_le line 363
  25. lemma OAI.SingleLatticeCovering.SimplexYoung.circuitTerm_add_three_le line 414
  26. theorem OAI.SingleLatticeCovering.SimplexYoung.tsum_circuitTerm_le line 428
  27. lemma OAI.SingleLatticeCovering.SimplexYoung.sharpParallelogramConstant_pos line 448
  28. lemma OAI.SingleLatticeCovering.SimplexYoung.sharpParallelogramConstant_sq line 450
  29. lemma OAI.SingleLatticeCovering.SimplexYoung.sharpParallelogramConstant_exp line 456
  30. def OAI.SingleLatticeCovering.SimplexYoung.sourceEta line 471
  31. lemma OAI.SingleLatticeCovering.SimplexYoung.sourceLog_pos line 473
  32. lemma OAI.SingleLatticeCovering.SimplexYoung.sourceLog_le_one line 475
  33. lemma OAI.SingleLatticeCovering.SimplexYoung.sourceEta_le_dim line 479
  34. lemma OAI.SingleLatticeCovering.SimplexYoung.log_27_16_le line 487
  35. lemma OAI.SingleLatticeCovering.SimplexYoung.sourceEta_le_linear line 493
  36. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexConstant_three line 500
  37. lemma OAI.SingleLatticeCovering.SimplexYoung.circuitTerm_three_source line 505
  38. theorem OAI.SingleLatticeCovering.SimplexYoung.circuit_series_at_sourceEta line 537
  39. def OAI.SingleLatticeCovering.RogersPreparation.poissonPartial line 563
  40. lemma OAI.SingleLatticeCovering.RogersPreparation.poissonPartial_zero line 566
  41. lemma OAI.SingleLatticeCovering.RogersPreparation.taylor_exp_neg_eq line 571
  42. theorem OAI.SingleLatticeCovering.RogersPreparation.poissonPartial_error line 586
  43. theorem OAI.SingleLatticeCovering.RogersPreparation.poissonPartial_upper line 606
  44. lemma OAI.SingleLatticeCovering.SimplexYoung.log_four_thirds_ge line 617
  45. lemma OAI.SingleLatticeCovering.SimplexYoung.log_three_quarters_le line 624
  46. lemma OAI.SingleLatticeCovering.SimplexYoung.factorial_quotient_chernoff line 629
  47. theorem OAI.SingleLatticeCovering.SimplexYoung.poisson_remainder_circuitCutoff line 647