OAI/Combinatorics/Progressions/Estimates/LinearQuotientCoverAverage.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.quotientIntegerCover line 13
  2. theorem OAI.Erdos3.quotientIntegerCover_mk line 16
  3. theorem OAI.Erdos3.quotientIntegerCover_surjective line 23
  4. theorem OAI.Erdos3.quotientIntegerCover_continuous line 32
  5. theorem OAI.Erdos3.character_half line 47
  6. theorem OAI.Erdos3.quotientLinearCharacter_integral line 52
  7. theorem OAI.Erdos3.quotientLinearCharacter_integrable line 77
  8. def OAI.Erdos3.probabilityAddHaar line 96
  9. instance OAI.Erdos3.probabilityAddHaar_probability line 101
  10. instance OAI.Erdos3.probabilityAddHaar_invariant line 106
  11. theorem OAI.Erdos3.compact_quotient_of_integral_basis line 111
  12. def OAI.Erdos3.linearQuotientEndomorphism line 142
  13. def OAI.Erdos3.linearQuotientAverage line 145
  14. theorem OAI.Erdos3.linearQuotientAverage_bound line 150
  15. theorem OAI.Erdos3.linearQuotientAverage_nonneg line 159
  16. theorem OAI.Erdos3.linearQuotientAverage_character line 163
  17. theorem OAI.Erdos3.linearQuotientEndomorphism_continuous line 192
  18. theorem OAI.Erdos3.linearQuotientAverage_invariant line 197
  19. theorem OAI.Erdos3.linearQuotientAverage_idempotent line 206
  20. theorem OAI.Erdos3.linearQuotientAverage_approx line 216
  21. theorem OAI.Erdos3.linearQuotientAverage_probability line 227
  22. theorem OAI.Erdos3.linearQuotientAverage_cover line 257
  23. theorem OAI.Erdos3.linearQuotientAverage_cover_eq_of_map_eq line 278