OAI/NumberTheory/Ostmann/Construction/PrimeCellWordPriors.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.primeCellWordPrior line 14
2. theorem OAI.Ostmann.primeCellWordPrior_nonneg line 18
3. theorem OAI.Ostmann.primeCellWordPrior_mass line 25
4. theorem OAI.Ostmann.primeCellWordPrior_mean line 34
5. theorem OAI.Ostmann.primeCellWordPrior_support line 48
6. theorem OAI.Ostmann.PublishedProgressionInput.rich_prime_word_priors line 55

   Source documentation

   The selected cells carry genuine probability laws with the claimed positive complex means, so they can be used directly in independent words.

   theorem PublishedProgressionInput.rich_prime_word_priors
       (P0 : PublishedProgressionInput) (c δ : ℝ) (hc : 0 < c) (hδ : 0 < δ) :
       ∃ C : ℝ, 0 < C ∧ ∀ᶠ B : ℝ in atTop, ∀ (P : Finset ℕ) (F : ℕ → ℂ),
         (∀ p ∈ P, p.Prime) →
         (∀ p ∈ P, B ≤ primeLogIndex p ∧ (primeLogIndex p : ℝ) ≤ 3 * B) →
         (∀ p ∈ P, ‖F p‖ ≤ 1) → c ≤ ∑ p ∈ P, (p : ℝ)⁻¹ →
         δ * (∑ p ∈ P, (p : ℝ)⁻¹) ≤ ∑ p ∈ P, (p : ℝ)⁻¹ * (F p).re →
         ∀ T : ℝ, C * B ≤ T → ∃ (n : ℕ) (w : List ℕ),
           w.length = n ∧
           (∀ h ∈ w,
             δ * c / (32 * B) ≤ finiteCellMass P primeLogIndex (fun p => (p : ℝ)⁻¹) h ∧
             (∑ p : P, primeCellWordPrior P h p) = 1 ∧
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.primeLogIndex, OAI.Ostmann.finiteCellMass, OAI.Ostmann.primeCellWordPrior