OAI/NumberTheory/Jacobsthal/Partitions/ReferenceIntervalBound.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.primeInterval line 19
  2. def OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.intervalPrimes line 22
  3. def OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.rebase line 25
  4. def OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.intervalResidual line 28
  5. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.primeInterval_measurable line 34
  6. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.primeInterval_orderConnected line 37
  7. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.primeInterval_subset line 42
  8. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.primeInterval_integral line 49
  9. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.intervalPrimes_eq_filter line 56
  10. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.intervalPrime_sum line 68
  11. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.lowerHigh_subset line 73
  12. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.highPrimes_split line 84
  13. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.highPrimes_split_disjoint line 98
  14. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.highPrime_sum_split line 106
  15. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.residual_split line 111
  16. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalCutoff.rebase_invariants line 118
  17. def OAI.Erdos970.NumberTheoryLean.ReferenceIntervalErrors.lowerProductError line 145
  18. def OAI.Erdos970.NumberTheoryLean.ReferenceIntervalErrors.intervalPrimeError line 148
  19. def OAI.Erdos970.NumberTheoryLean.ReferenceIntervalErrors.intervalQuadratureError line 153
  20. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalErrors.continuous_interval_cancellation line 158
  21. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalErrors.normalized_interval_zero line 182
  22. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalErrors.interval_error_identity line 195
  23. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalProductBounds.finite_interval_product_bounds line 226
  24. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalQuadrature.actual_interval_quadrature line 299
  25. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalBound.interval_abs_triangle line 334
  26. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalBound.actual_interval_residual_bound line 345
  27. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIntervalBound.source_residual_split_bound line 400