OAI/NumberTheory/Ostmann/Arithmetic/PrimeCellActualErrorBudgetMixedBasic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.PrimeCellActualErrorBudget.integerDensityMass_abs_le line 13
2. def OAI.Ostmann.Arithmetic.PrimeCellActualErrorBudget.primeEnvelope line 34
3. theorem OAI.Ostmann.Arithmetic.PrimeCellActualErrorBudget.correctedPrimeError_le_envelope line 37
4. def OAI.Ostmann.Arithmetic.PrimeCellActualErrorBudget.dimensionCoefficient line 45
5. theorem OAI.Ostmann.Arithmetic.PrimeCellActualErrorBudget.tensor_two_factors_le line 47
6. lemma OAI.Ostmann.Arithmetic.PrimeCellActualErrorBudget.smoothGrowthFactor_mul line 73
7. lemma OAI.Ostmann.Arithmetic.PrimeCellActualErrorBudget.smoothGrowth_mul_normalizer_le_add line 80
8. theorem OAI.Ostmann.Arithmetic.PrimeCellActualErrorBudget.eventually_primeEnvelope_budget line 89