OAI/NumberTheory/Jacobsthal/Estimates/ActualPointSlopes.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosInverseSaving.mean_envelope line 19
  2. theorem OAI.Erdos970.ErdosInverseSaving.spectral_factor_bound line 54
  3. theorem OAI.Erdos970.ErdosInverseSaving.log_square_absorption line 77
  4. theorem OAI.Erdos970.ErdosInverseSaving.common_length_bin_lower line 100
  5. def OAI.Erdos970.ErdosInverseSampleCost.totalCost line 133
  6. theorem OAI.Erdos970.ErdosInverseSampleCost.totalCost_nonneg line 137
  7. theorem OAI.Erdos970.ErdosInverseSampleCost.totalCost_average_bound line 142
  8. theorem OAI.Erdos970.ErdosInverseSampleCost.slopes_card_le_primeCost line 177
  9. theorem OAI.Erdos970.ErdosInverseSampleCost.slopes_sum_le_totalCost line 187
  10. def OAI.Erdos970.ErdosInverseSaving.frozenPrimeMean line 215
  11. def OAI.Erdos970.ErdosInverseSaving.meanCoefficient line 220
  12. theorem OAI.Erdos970.ErdosInverseSaving.actual_mean_envelope line 223
  13. theorem OAI.Erdos970.ErdosInverseSaving.uniform_mean_power line 267
  14. theorem OAI.Erdos970.ErdosInverseSaving.source_mean_power line 332
  15. def OAI.Erdos970.ErdosInverseSampleCost.actualFamily line 357
  16. theorem OAI.Erdos970.ErdosInverseSampleCost.actual_family_mean_eq line 362
  17. def OAI.Erdos970.ErdosInverseSampleCost.actualCost line 372
  18. theorem OAI.Erdos970.ErdosInverseSampleCost.actualCost_nonneg line 377
  19. theorem OAI.Erdos970.ErdosInverseSampleCost.actualCost_average_bound line 384
  20. theorem OAI.Erdos970.ErdosInverseSampleCost.smallModulus_coprime_largePrime line 409
  21. theorem OAI.Erdos970.ErdosInverseSampleCost.actual_slopes_thin line 421
  22. theorem OAI.Erdos970.ErdosInverseSampleCost.source_expected_cost line 463
  23. theorem OAI.Erdos970.ErdosInverseSampleCost.source_expected_cost_small line 520
  24. def OAI.Erdos970.ErdosInverseSampleCost.sampleGamma line 565
  25. theorem OAI.Erdos970.ErdosInverseSampleCost.sampleGamma_pos line 567
  26. theorem OAI.Erdos970.ErdosInverseSampleCost.source_good_sample line 571
  27. def OAI.Erdos970.ErdosInverseRefinement.pointSlopes line 638
  28. theorem OAI.Erdos970.ErdosInverseRefinement.pointSlopes_eq line 649
  29. theorem OAI.Erdos970.ErdosInverseRefinement.pointSlopes_thin line 660
  30. theorem OAI.Erdos970.ErdosInverseRefinement.parentSlope_incidence line 675