OAI/NumberTheory/Ostmann/Characters/CharacterRoundedEndpoint.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.characterEndpointFactor line 10
2. def OAI.Ostmann.characterRoundedEndpoint line 11
3. def OAI.Ostmann.characterRoundedTau line 13
4. theorem OAI.Ostmann.characterEndpointFactor_pos line 16
5. theorem OAI.Ostmann.character_rounded_endpoint_bounds line 20
6. theorem OAI.Ostmann.character_rounded_top_shell line 69

   Source documentation

   The floor perturbation leaves every prime of the entire top shell in its required original logarithmic word range.

   theorem character_rounded_top_shell (k : ℕ) (v U : ℝ) (hv : 2 ≤ v) (hUv : U + 1 ≤ v)
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) :
       ∀ p ∈ loglogShell P v, characterRoundedTau k v ≤ Real.log (p : ℝ) ∧
         Real.log (p : ℝ) ≤ 3 * characterRoundedTau k v := by
   …

   Mentions: OAI.Ostmann.loglogShell, OAI.Ostmann.characterRoundedTau

7. theorem OAI.Ostmann.character_rounded_anchor_pair line 82