OAI/NumberTheory/JointDickman/Analysis/CharacterDistanceDivergence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The qualitative character-distance divergence needed by the application

This is weaker than the quantitative KMT input. Its proof uses the Euler comparison, finite differencing of logarithmic phases and partial summation.

  1. theorem OAI.JointDickman.characterDistanceDivergence line 16

    Source documentation

    Qualitative uniform divergence of the nonprincipal-character distance on the entire frequency interval.

    theorem characterDistanceDivergence : CharacterDistanceDivergence := by
…

    Mentions: OAI.JointDickman.CharacterDistanceDivergence