OAI/NumberTheory/JointDickman/Analysis/MellinBandSelection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Maximal band selection below the square-root logarithmic cutoff

  1. lemma OAI.JointDickman.exists_mellin_band_above line 10
  2. def OAI.JointDickman.mellinBandCount line 17
  3. lemma OAI.JointDickman.mellinBandCount_next line 20
  4. lemma OAI.JointDickman.mellinBandCount_good line 24
  5. lemma OAI.JointDickman.mellinBandCount_tendsto line 35
  6. lemma OAI.JointDickman.twice_exp_sqrt_log_le line 45
  7. lemma OAI.JointDickman.selected_mellin_bands_fit line 58
  8. lemma OAI.JointDickman.selected_mellin_bands_sieve line 67
  9. theorem OAI.JointDickman.selected_mellin_count line 77