OAI/NumberTheory/Ostmann/Characters/HigherBiasSourcePrimeSets.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.HigherBiasSource.boundedPrimeSet line 14
  2. lemma OAI.Ostmann.Characters.HigherBiasSource.mem_boundedPrimeSet line 17
  3. lemma OAI.Ostmann.Characters.HigherBiasSource.naturalPrimeSet_boundedPrimeSet line 20
  4. lemma OAI.Ostmann.Characters.HigherBiasSource.boundedPrimeSet_naturalPrimeSet line 30
  5. lemma OAI.Ostmann.Characters.HigherBiasSource.boundedPrimeSet_mass line 42
  6. lemma OAI.Ostmann.Characters.HigherBiasSource.sum_boundedPrimeSet line 46
  7. def OAI.Ostmann.Characters.HigherBiasSource.boundedInterval line 51
  8. lemma OAI.Ostmann.Characters.HigherBiasSource.boundedInterval_subset line 54
  9. lemma OAI.Ostmann.Characters.HigherBiasSource.naturalPrimeSet_boundedInterval line 57
  10. lemma OAI.Ostmann.Characters.HigherBiasSource.boundedInterval_mass line 71
  11. lemma OAI.Ostmann.Characters.HigherBiasSource.boundedInterval_log_bounds line 76
  12. lemma OAI.Ostmann.Characters.HigherBiasSource.boundedPrimeSet_subset line 86
  13. lemma OAI.Ostmann.Characters.HigherBiasSource.naturalPrimeSet_boundedInterval_of_cutoff line 89
  14. lemma OAI.Ostmann.Characters.HigherBiasSource.boundedInterval_mass_of_cutoff line 106