OAI/NumberTheory/Jacobsthal/Estimates/CorrectionFloorRemainder.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosInverseBoxHeight.sourceW line 17
  2. def OAI.Erdos970.ErdosInverseBoxHeight.sourceB line 18
  3. def OAI.Erdos970.ErdosInverseBoxHeight.sourceY line 19
  4. theorem OAI.Erdos970.ErdosInverseBoxHeight.source_B_bounds line 21
  5. theorem OAI.Erdos970.ErdosInverseBoxHeight.sourceY_le_square line 56
  6. theorem OAI.Erdos970.ErdosInverseBoxHeight.source_cofactor_le_square line 61
  7. theorem OAI.Erdos970.ErdosSourceLineBudget.source_W_power_quarter line 77
  8. theorem OAI.Erdos970.ErdosSourceLineBudget.source_Y_three_halves line 96
  9. theorem OAI.Erdos970.ErdosSourceLineBudget.source_parent_square_lower line 129
  10. theorem OAI.Erdos970.ErdosSourceLineBudget.source_Z_ge_two line 176
  11. theorem OAI.Erdos970.ErdosSourceLineBudget.extraction_small_power line 193
  12. theorem OAI.Erdos970.ErdosSourceLineBudget.minimum_line_size_power line 214
  13. theorem OAI.Erdos970.ErdosSourceLineBudget.finite_extraction_budget line 241
  14. def OAI.Erdos970.ErdosSourcePolynomial.sourceDegree line 283
  15. theorem OAI.Erdos970.ErdosSourcePolynomial.sourceDegree_le line 285
  16. theorem OAI.Erdos970.ErdosSourcePolynomial.sourceDegree_le_R line 289
  17. theorem OAI.Erdos970.ErdosSourcePolynomial.source_degree_factor line 293
  18. theorem OAI.Erdos970.ErdosSourcePolynomial.dimension_le_square line 305
  19. theorem OAI.Erdos970.ErdosSourcePolynomial.source_dimension_log_bound line 309
  20. theorem OAI.Erdos970.ErdosSourceLineBudget.uniform_extraction_budget line 337
  21. def OAI.Erdos970.ErdosCorrectionLimit.sourcePrefactor line 372
  22. theorem OAI.Erdos970.ErdosCorrectionLimit.sourcePrefactor_continuousAt line 374
  23. theorem OAI.Erdos970.ErdosCorrectionLimit.sourcePrefactor_two line 377
  24. theorem OAI.Erdos970.ErdosCorrectionLimit.sourcePrefactor_limit line 383
  25. def OAI.Erdos970.ErdosCorrectionLimit.paperGap line 387
  26. theorem OAI.Erdos970.ErdosCorrectionLimit.paper_ratio_tendsto line 390
  27. theorem OAI.Erdos970.ErdosCorrectionLimit.paper_prefactor_tendsto line 405
  28. def OAI.Erdos970.ErdosCorrectionLimit.unroundedY line 425
  29. def OAI.Erdos970.ErdosCorrectionLimit.floorRemainder line 427
  30. theorem OAI.Erdos970.ErdosCorrectionLimit.unroundedY_tendsto line 430
  31. theorem OAI.Erdos970.ErdosCorrectionLimit.floor_log_error_tendsto line 433
  32. theorem OAI.Erdos970.ErdosCorrectionLimit.floorRemainder_tendsto line 450
  33. theorem OAI.Erdos970.ErdosCorrectionLimit.sourceY_exp line 453
  34. theorem OAI.Erdos970.ErdosCorrectionLimit.paperGap_floor_eq line 460