CharacterTargetWords.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous positive-length words for every character pivot and the filler

structure OAI.Ostmann.CharacterTargetWord line 11
Source documentation
A word consists of cells from one whole, previously tested rich shell.
```
structure CharacterTargetWord (P : Finset ℕ) (F : ℕ → ℂ)
    (c δ U : ℝ) (k : ℕ) (T : ℝ) where
…
```
theorem OAI.Ostmann.CharacterTargetWord.length_pos line 27

theorem OAI.Ostmann.PublishedProgressionInput.character_target_words line 38

Source documentation

All nonanchor roles are chosen after fixing the word bin. Their total length is bounded by the number of actual roles times the single-word bound.

theorem PublishedProgressionInput.character_target_words
    (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