OAI/NumberTheory/JointDickman/Analysis/MellinApplicationScales.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Qualitative application scales for the multiscale energy bound

The large fixed logarithmic exponent pays the explicit factorial budget. The application needs only a vanishing error as the short length grows.

  1. def OAI.JointDickman.mellinFirstPrime line 15
  2. def OAI.JointDickman.mellinLastPrime line 16
  3. def OAI.JointDickman.mellinResolution line 17
  4. lemma OAI.JointDickman.mellinFirstPrime_tendsto line 20
  5. lemma OAI.JointDickman.mellinLastPrime_tendsto line 23
  6. lemma OAI.JointDickman.mellinFirstPrime_div_last_tendsto line 26
  7. lemma OAI.JointDickman.mellinLastPrime_div_length_tendsto line 30
  8. lemma OAI.JointDickman.mellinResolution_eventually line 43
  9. lemma OAI.JointDickman.mellinResolution_tendsto line 54
  10. theorem OAI.JointDickman.eventually_mellin_application_scales line 66

    Source documentation

    All fixed-scale numerical hypotheses of the canonical partition hold for every sufficiently large short length.

    theorem eventually_mellin_application_scales :
    ∀ᶠ H : ℝ in atTop,
      2*Real.exp 1 ≤ mellinFirstPrime H ∧
      mellinFirstPrime H ≤ mellinLastPrime H ∧
      2 ≤ Real.log (mellinFirstPrime H) ∧ 1 ≤ Real.log (mellinLastPrime H) ∧
      8192*(Real.log (Real.log (mellinLastPrime H))+1) ≤
        (1/12 : ℝ)*Real.log (mellinFirstPrime H) ∧
      2 ≤ mellinResolution H := by
…

    Mentions: OAI.JointDickman.mellinFirstPrime, OAI.JointDickman.mellinLastPrime, OAI.JointDickman.mellinResolution

  11. theorem OAI.JointDickman.mellin_typical_cost_tendsto_zero line 91
  12. def OAI.JointDickman.mellinWindowCost line 107
  13. theorem OAI.JointDickman.mellinWindowCost_tendsto_zero line 112