OAI/NumberTheory/TwoPoint/Walks/ManyUnlitNumericalWords.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The many-unlit bound for the actual full numerical word catalog.

  1. def OAI.TwoPointCorrelations.largeUnlitCatalog line 13
  2. def OAI.TwoPointCorrelations.designationExtra line 19
  3. lemma OAI.TwoPointCorrelations.twice_designationExtra line 25
  4. theorem OAI.TwoPointCorrelations.eventually_many_unlit_numerical_words line 32

    Source documentation

    All extra reciprocals, including a different exponent for every word/designation pair, are summed here. No crude-catalog hypothesis remains.

    theorem eventually_many_unlit_numerical_words (C Cexternal Csingle : ℝ)
    (hC : 0 ≤ C) (hCe : 0 ≤ Cexternal) (hCs : 0 ≤ Csingle) :
    ∀ᶠ L : ℝ in atTop, ∀ (R J T S : ℕ) (ι : Type) [Fintype ι] [DecidableEq ι] (P Q : Finset ℕ)
      (F : Finset (Fin R → SignedStep))
      (label : (Fin R → SignedStep) → Fin R × Fin J → ι) (external H : ℝ),
      1 ≤ R → (R : ℝ) ≤ 2 * L →
      ((S + R * J : ℕ) : ℝ) ≤ Csingle * L * Real.log L →
      0 ≤ external → external ≤ Real.exp (Cexternal * L) →
      (T : ℝ) ≤ C * R * Real.log L →
      (T : ℝ) + 1 ≤ L ^ (2 : ℕ) → (R : ℝ) + 1 ≤ L ^ (2 : ℕ) →
      primeHarmonicMass P ≤ L ^ (2 : ℕ) → primeHarmonicMass Q ≤ L ^ (2 : ℕ) →
      (∀ w ∈ F, Fintype.card (ActualPrimeSlot w) ≤ T) →
…

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.ActualPrimeSlot