OAI/NumberTheory/PiExponent/Polynomials/SimplexCounting.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.natWeightedSimplex line 10
  2. theorem OAI.PiExponent.mem_natWeightedSimplex line 14
  3. def OAI.PiExponent.residueRectangle line 29
  4. theorem OAI.PiExponent.mem_residueRectangle line 32
  5. theorem OAI.PiExponent.card_residueRectangle line 36
  6. theorem OAI.PiExponent.simplex_count_lower_sandwich line 40
  7. theorem OAI.PiExponent.simplex_count_upper_sandwich line 71
  8. theorem OAI.PiExponent.natWeightedSimplex_one line 112
  9. theorem OAI.PiExponent.tendsto_card_natWeightedSimplex line 120
  10. def OAI.PiExponent.realWeightedSimplex line 154
  11. def OAI.PiExponent.strictWeightedSimplex line 160
  12. theorem OAI.PiExponent.mem_realWeightedSimplex line 165
  13. theorem OAI.PiExponent.mem_strictWeightedSimplex line 182
  14. theorem OAI.PiExponent.realWeightedSimplex_scaled line 190
  15. theorem OAI.PiExponent.strictWeightedSimplex_scaled line 202
  16. theorem OAI.PiExponent.tendsto_card_realWeightedSimplex_scaled line 218
  17. theorem OAI.PiExponent.tendsto_card_strictWeightedSimplex_scaled line 228
  18. theorem OAI.PiExponent.card_strictWeightedSimplex_dilate line 261
  19. theorem OAI.PiExponent.strictWeightedSimplex_lower_of_limit line 304