CharacterBackwardsWords.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Whole-shell words for the actual backwards pivot and filler targets

theorem OAI.Ostmann.PublishedProgressionInput.character_backwards_words line 13

Source documentation

The words are constructed after fixing the bin and anchor indices. The large-parameter threshold is uniform over those choices and the endpoint test.

theorem PublishedProgressionInput.character_backwards_words
    (P0 : PublishedProgressionInput) (c δ : ℝ) (hc : 0 < c) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (k : ℕ), 20000 ≤ k →
      C ≤ Real.exp ((k : ℝ) / 10000) → ∀ (B z α : ℝ),
      0 ≤ B → 1 ≤ z → 0 < α →
      ∀ᶠ L : ℝ in atTop, ∀ (U τ J : ℝ) (m : ℕ),
      α * L ≤ U → U ≤ Real.log τ → Real.log τ ≤ U + 2 * (k : ℝ) / 10000 →
      0 < τ → (m : ℝ) ≤ z * L → τ / 2 ≤ J → J ≤ 4 * τ →
      ∀ (a : Fin k → Bool → ℕ),
      (∀ j, (a j false : ℝ) + a j true ≤ 4 * τ) →
      ∀ (P : Finset ℕ) (F : ℕ → ℂ), (∀ p ∈ P, p.Prime) →
      (∀ p ∈ P, ‖F p‖ ≤ 1) →
…

Mentions: OAI.Ostmann.PublishedProgressionInput