OAI/NumberTheory/Jacobsthal/Primes/ActualPrimeQuadrature.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.HarmonicPrimeAtomicMeasure.primeAtom line 18
  2. def OAI.Erdos970.NumberTheoryLean.HarmonicPrimeAtomicMeasure.primeMeasure line 21
  3. instance OAI.Erdos970.NumberTheoryLean.HarmonicPrimeAtomicMeasure.primeAtom_finite line 24
  4. instance OAI.Erdos970.NumberTheoryLean.HarmonicPrimeAtomicMeasure.primeMeasure_finite line 28
  5. theorem OAI.Erdos970.NumberTheoryLean.HarmonicPrimeAtomicMeasure.integrable_primeAtom line 32
  6. theorem OAI.Erdos970.NumberTheoryLean.HarmonicPrimeAtomicMeasure.primeMeasure_integral line 36
  7. theorem OAI.Erdos970.NumberTheoryLean.HarmonicPrimeAtomicMeasure.primeMeasure_setIntegral line 45
  8. theorem OAI.Erdos970.NumberTheoryLean.HarmonicPrimeAtomicMeasure.primeMeasure_real line 53
  9. theorem OAI.Erdos970.NumberTheoryLean.HarmonicPrimeAtomicMeasure.intervalGuard_measurable line 59
  10. theorem OAI.Erdos970.NumberTheoryLean.HarmonicPrimeAtomicMeasure.primeMeasure_interval line 63
  11. def OAI.Erdos970.ErdosContinuousBoundary.boundaryPrimeError line 100
  12. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryPrimeError_tendsto_zero line 102
  13. theorem OAI.Erdos970.ErdosContinuousBoundary.boundary_interval_discrepancy line 109
  14. theorem OAI.Erdos970.ErdosContinuousBoundary.reference_unit_interval_mass line 133
  15. theorem OAI.Erdos970.ErdosContinuousBoundary.boundary_measure_control line 138
  16. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeQuadrature.actual_interval_discrepancy line 175
  17. theorem OAI.Erdos970.NumberTheoryLean.ActualPrimeQuadrature.actual_weighted_prime_quadrature line 194