OAI/NumberTheory/JointDickman/Analysis/MellinLastBandGrowth.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The final selected band lies beyond every fixed logarithmic power

  1. lemma OAI.JointDickman.next_band_log_le_lower_sq line 10
  2. theorem OAI.JointDickman.last_selected_band_lower line 43

    Source documentation

    Maximality below exp(sqrt(log X)) and the explicit adjacent-band formula force the lower endpoint to grow faster than exp(log X^(1/4)).

    theorem last_selected_band_lower (P Q : ℝ) (hP : 1 ≤ Real.log P)
    (hQ : 1 ≤ Real.log Q) :
    ∀ᶠ X : ℝ in atTop, let J := mellinBandCount Q (Real.sqrt (Real.log X)) hQ
…

    Mentions: OAI.JointDickman.mellinBandCount