OAI/NumberTheory/Ostmann/Characters/CharacterTargetCellData.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.CharacterTargetWord.cell line 11
2. theorem OAI.Ostmann.CharacterTargetWord.cell_subset line 15
3. theorem OAI.Ostmann.CharacterTargetWord.cell_mass line 20
4. theorem OAI.Ostmann.CharacterTargetWord.cell_mean line 26
5. theorem OAI.Ostmann.CharacterTargetWord.cell_prime_bounds line 33
6. theorem OAI.Ostmann.CharacterTargetWord.cell_mass_exponential line 39
7. theorem OAI.Ostmann.eventual_character_target_cell_mass line 57

   Source documentation

   This floor holds for every selected role and endpoint once the fixed late-block width has been absorbed into L.

   theorem eventual_character_target_cell_mass (c δ β : ℝ) (k : ℕ)
       (hc : 0 < c) (hδ : 0 < δ) :
       ∀ᶠ L : ℝ in atTop, ∀ (P : Finset ℕ) (F : ℕ → ℂ) (U T : ℝ),
         U ≤ β * L → ∀ (w : CharacterTargetWord P F c δ U k T) (h : ℕ),
         h ∈ w.indices → Real.exp (-(β + 1) * L) ≤ ∑ p ∈ w.cell h, (p : ℝ)⁻¹ := by
   …

   Mentions: OAI.Ostmann.CharacterTargetWord