OAI/NumberTheory/Jacobsthal/Estimates/MovingLocalReference.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.WeightDistantDecay.sided_rho_bounds line 14
  2. theorem OAI.Erdos970.NumberTheoryLean.WeightDistantDecay.compact_weight_lower line 23
  3. theorem OAI.Erdos970.NumberTheoryLean.WeightDistantDecay.rho_one_rate line 32
  4. theorem OAI.Erdos970.NumberTheoryLean.WeightDistantDecay.relative_weight_decay line 37
  5. theorem OAI.Erdos970.NumberTheoryLean.WeightDistantDecay.weight_exponential_majorant line 87
  6. theorem OAI.Erdos970.NumberTheoryLean.ReferenceResidualErrors.ratio_eq_gap_div_cutoff line 111
  7. theorem OAI.Erdos970.NumberTheoryLean.ReferenceResidualErrors.boundary_parent_eq line 117
  8. def OAI.Erdos970.NumberTheoryLean.ReferenceResidualErrors.boundaryProductError line 123
  9. def OAI.Erdos970.NumberTheoryLean.ReferenceResidualErrors.parentProductError line 126
  10. def OAI.Erdos970.NumberTheoryLean.ReferenceResidualErrors.primeProductError line 129
  11. def OAI.Erdos970.NumberTheoryLean.ReferenceResidualErrors.quadratureError line 134
  12. theorem OAI.Erdos970.NumberTheoryLean.ReferenceResidualErrors.actual_continuous_zero line 139
  13. theorem OAI.Erdos970.NumberTheoryLean.ReferenceResidualErrors.residual_error_identity line 152
  14. def OAI.Erdos970.NumberTheoryLean.ReferenceProductErrorBounds.primeError line 181
  15. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductErrorBounds.primeError_pos line 183
  16. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductErrorBounds.primeError_antitone line 185
  17. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductErrorBounds.divided_error_bound line 191
  18. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductErrorBounds.finite_product_error_bounds line 196
  19. def OAI.Erdos970.NumberTheoryLean.GlobalResidualScale.powerDecay line 261
  20. theorem OAI.Erdos970.NumberTheoryLean.GlobalResidualScale.powerDecay_pos line 263
  21. theorem OAI.Erdos970.NumberTheoryLean.GlobalResidualScale.primeError_le_one line 265
  22. theorem OAI.Erdos970.NumberTheoryLean.GlobalResidualScale.powerDecay_nat line 268
  23. theorem OAI.Erdos970.NumberTheoryLean.GlobalResidualScale.linear_log_cutoff_saving line 271
  24. theorem OAI.Erdos970.NumberTheoryLean.GlobalResidualScale.rebased_ratio_separation line 298
  25. theorem OAI.Erdos970.NumberTheoryLean.GlobalResidualScale.gap_over_linear_cutoff line 321
  26. theorem OAI.Erdos970.NumberTheoryLean.ReferenceLogScale.primeError_two_eq line 339
  27. theorem OAI.Erdos970.NumberTheoryLean.ReferenceLogScale.log_power_primeError_tendsto line 346
  28. theorem OAI.Erdos970.NumberTheoryLean.ReferenceLogScale.primeError_two_tendsto line 351
  29. theorem OAI.Erdos970.NumberTheoryLean.ReferenceResidualQuadrature.actual_quadrature_error line 365
  30. theorem OAI.Erdos970.NumberTheoryLean.WeightPowerBounds.relative_weight_power line 389
  31. theorem OAI.Erdos970.NumberTheoryLean.WeightPowerBounds.weight_power_at_ratio line 400
  32. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductLower.reference_product_lower line 427
  33. theorem OAI.Erdos970.NumberTheoryLean.ReferenceResidualPointwise.residual_abs_triangle line 468
  34. theorem OAI.Erdos970.NumberTheoryLean.ReferenceResidualPointwise.source_residual_pointwise line 479
  35. def OAI.Erdos970.NumberTheoryLean.ReferenceResidualSum.residualAbsoluteSum line 545
  36. theorem OAI.Erdos970.NumberTheoryLean.ReferenceResidualSum.uniform_weight_bound line 548
  37. theorem OAI.Erdos970.NumberTheoryLean.ReferenceResidualSum.uncapped_cutoff_le line 557
  38. theorem OAI.Erdos970.NumberTheoryLean.ReferenceResidualSum.summed_source_residual_bound line 571
  39. theorem OAI.Erdos970.NumberTheoryLean.ReferenceResidualSum.signed_residual_le_absolute line 623
  40. theorem OAI.Erdos970.NumberTheoryLean.ReferenceRelativeError.source_relative_reference_error line 642
  41. theorem OAI.Erdos970.NumberTheoryLean.MovingLocalReference.log_square_le_base line 698
  42. theorem OAI.Erdos970.NumberTheoryLean.MovingLocalReference.moving_local_reference line 706