ConstructedFixedCharacterPriors.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed character priors constructed from the tested shells and exact targets

theorem OAI.Ostmann.PublishedProgressionInput.constructed_fixed_character_priors line 13

Source documentation

All cells below are obtained from the published progression input. No pivot-word, cell-mean, or normalized-prior hypothesis is supplied here.

theorem PublishedProgressionInput.constructed_fixed_character_priors
    (P0 : PublishedProgressionInput) (c δ : ℝ) (hc : 0 < c) (hδ : 0 < δ) :
    ∃ C₀ : ℝ, 0 < C₀ ∧ ∀ (k : ℕ), 20000 ≤ k →
      C₀ ≤ Real.exp ((k : ℝ) / 10000) → ∀ (B z α β C : ℝ),
      0 ≤ B → 1 ≤ z → 0 < α → 0 ≤ C →
      ((characterTargetLabelBound c δ k + (k + 1) + (k + 1) : ℕ) : ℝ) ≤ z →
      ∀ᶠ L : ℝ in atTop, ∀ (U τ J : ℝ) (m D : ℕ),
      α * L ≤ U → U ≤ β * L → U ≤ Real.log τ →
      Real.log τ ≤ U + 2 * (k : ℝ) / 10000 → 0 < τ →
      (m : ℝ) ≤ z * L → z * L ≤ 2 * m → τ / 2 ≤ J → J ≤ 4 * τ →
      (D + 1 : ℕ) ≤ Real.exp (C * L) → 5 * k ≤ D →
      ∀ (P : Finset ℕ) (G : ℕ → ℕ → ℂ) (ζ : ℂ),
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.characterTargetLabelBound