OAI/NumberTheory/Ostmann/Characters/CharacterAnchorCells.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.CharacterAnchorCell line 11
2. def OAI.Ostmann.CharacterAnchorCell.cell line 21
3. theorem OAI.Ostmann.CharacterAnchorCell.cell_subset line 25
4. theorem OAI.Ostmann.CharacterAnchorCell.cell_eq_of_index line 29
5. theorem OAI.Ostmann.CharacterAnchorCell.cell_mass_pos line 34
6. theorem OAI.Ostmann.CharacterAnchorCell.index_le line 39
7. theorem OAI.Ostmann.CharacterAnchorCell.cell_probability line 53
8. theorem OAI.Ostmann.CharacterAnchorCell.cell_prime_bounds line 58
9. theorem OAI.Ostmann.CharacterAnchorCell.unrotated_mean line 64
10. theorem OAI.Ostmann.CharacterAnchorCell.cell_mass_exponential line 70
11. theorem OAI.Ostmann.PublishedProgressionInput.character_anchor_cell line 82

    Source documentation

    Anchor selection uses the same whole-shell progression theorem as the pivot words, without clipping either boundary cell.

    theorem PublishedProgressionInput.character_anchor_cell
        (P0 : PublishedProgressionInput) (c δ : ℝ) (hc : 0 < c) (hδ : 0 < δ) :
        ∀ᶠ u : ℝ in atTop, ∀ (P : Finset ℕ) (F : ℕ → ℂ),
          (∀ p ∈ P, p.Prime) → (∀ p ∈ P, ‖F p‖ ≤ 1) →
          c ≤ ∑ p ∈ loglogShell P u, (p : ℝ)⁻¹ →
          δ * (∑ p ∈ loglogShell P u, (p : ℝ)⁻¹) ≤
            ∑ p ∈ loglogShell P u, (p : ℝ)⁻¹ * (F p).re →
          Nonempty (CharacterAnchorCell P F c δ u) := by
    …

    Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.loglogShell, OAI.Ostmann.CharacterAnchorCell

12. theorem OAI.Ostmann.character_anchor_pair_bound line 99