TargetPrimeWords.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual prime-cell words for every pivot and filler target

def OAI.Ostmann.loglogShell line 14
theorem OAI.Ostmann.loglogShell_mass line 18

theorem OAI.Ostmann.PublishedProgressionInput.target_prime_word line 26

Source documentation

A target window contains a whole rich tested shell. Its good cell word has bounded length, positive means, and bounded target error. All constants are independent of the late block's location.

theorem PublishedProgressionInput.target_prime_word
    (P0 : PublishedProgressionInput) (c δ : ℝ) (hc : 0 < c) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ U : ℝ in atTop,
      ∀ (k : ℕ), 20000 ≤ k → C ≤ Real.exp ((k : ℝ) / 10000) →
      ∀ (τ : ℝ), 0 < τ → U ≤ Real.log τ →
      Real.log τ ≤ U + 2 * (k : ℝ) / 10000 →
      ∀ (P : Finset ℕ) (F : ℕ → ℂ), (∀ p ∈ P, p.Prime) →
      (∀ p ∈ P, ‖F p‖ ≤ 1) →
      (∀ u v : ℝ, U ≤ u → v ≤ U + 5 * k → (k : ℝ) / 10000 ≤ v - u →
        ∃ j : ℕ, u ≤ U + j ∧ U + j + 1 ≤ v ∧
          c ≤ ∑ p ∈ loglogShell P (U + j), (p : ℝ)⁻¹) →
      (∀ j : ℕ, j ≤ 5 * k → c ≤ ∑ p ∈ loglogShell P (U + j), (p : ℝ)⁻¹ →
…

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