OAI/NumberTheory/Jacobsthal/Estimates/ScalarErrorBudget.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosKloosterman.frequencyGcd line 17
  2. theorem OAI.Erdos970.ErdosKloosterman.dvd_frequencyGcd_iff line 19
  3. theorem OAI.Erdos970.ErdosKloosterman.frequencyGcd_scale line 23
  4. theorem OAI.Erdos970.ErdosKloosterman.frequencyGcd_coprime_mul line 45
  5. def OAI.Erdos970.ErdosKloosterman.envelope line 76
  6. theorem OAI.Erdos970.ErdosKloosterman.envelope_nonneg line 80
  7. theorem OAI.Erdos970.ErdosKloosterman.envelope_coprime_mul line 84
  8. theorem OAI.Erdos970.ErdosKloosterman.envelope_scale line 93
  9. theorem OAI.Erdos970.ErdosKloosterman.envelope_crt_scaled line 99
  10. theorem OAI.Erdos970.ErdosKloosterman.standardSum_one line 109
  11. theorem OAI.Erdos970.ErdosKloosterman.envelope_one line 116
  12. def OAI.Erdos970.ErdosKloosterman.BoundAt line 119
  13. theorem OAI.Erdos970.ErdosKloosterman.boundAt_zero line 122
  14. theorem OAI.Erdos970.ErdosKloosterman.boundAt_one line 126
  15. theorem OAI.Erdos970.ErdosKloosterman.boundAt_coprime line 130
  16. theorem OAI.Erdos970.ErdosKloosterman.boundAt_all_of_prime_powers line 142
  17. theorem OAI.Erdos970.ErdosHyperbolaIdentities.restricted_phase line 158
  18. theorem OAI.Erdos970.ErdosHyperbolaIdentities.restricted_average_mul line 188
  19. theorem OAI.Erdos970.ErdosHyperbolaIdentities.restricted_average line 207
  20. theorem OAI.Erdos970.ErdosKloosterman.boundAt_prime_power line 225
  21. theorem OAI.Erdos970.ErdosKloosterman.standardSum_bound line 233
  22. theorem OAI.Erdos970.ErdosKloosterman.standardSum_bound_half_gcd line 239
  23. def OAI.Erdos970.ErdosHyperbolaError.completeScale line 257
  24. theorem OAI.Erdos970.ErdosHyperbolaError.completeScale_nonneg line 260
  25. theorem OAI.Erdos970.ErdosHyperbolaError.sum_as_standard line 264
  26. theorem OAI.Erdos970.ErdosHyperbolaError.norm_sum_le_sqrt_second line 269
  27. theorem OAI.Erdos970.ErdosHyperbolaError.norm_sum_le_sqrt_first line 279
  28. def OAI.Erdos970.ErdosHyperbolaError.logFactor line 296
  29. def OAI.Erdos970.ErdosHyperbolaError.errorBase line 299
  30. theorem OAI.Erdos970.ErdosHyperbolaError.logFactor_one_le line 302
  31. theorem OAI.Erdos970.ErdosHyperbolaError.divisorCount_one_le line 310
  32. theorem OAI.Erdos970.ErdosHyperbolaError.completeScale_one_le line 315
  33. theorem OAI.Erdos970.ErdosHyperbolaError.sqrt_modulus_one_le line 321
  34. theorem OAI.Erdos970.ErdosHyperbolaError.errorBase_one_le line 325
  35. theorem OAI.Erdos970.ErdosHyperbolaError.errorBase_nonneg line 331
  36. theorem OAI.Erdos970.ErdosHyperbolaError.l1Norm_le_logFactor line 336
  37. theorem OAI.Erdos970.ErdosHyperbolaError.gcdL1Norm_le_logFactor line 342
  38. theorem OAI.Erdos970.ErdosHyperbolaError.errorBase_explicit line 348
  39. theorem OAI.Erdos970.ErdosHyperbolaError.restrictedSum_norm_le_average line 365
  40. theorem OAI.Erdos970.ErdosHyperbolaError.restrictedSum_norm_le_second line 383
  41. theorem OAI.Erdos970.ErdosHyperbolaError.restrictedSum_norm_le_first line 402
  42. theorem OAI.Erdos970.ErdosHyperbolaError.axis_quadrant_budget line 435
  43. theorem OAI.Erdos970.ErdosHyperbolaError.rounding_absorb line 480