OAI/NumberTheory/Ostmann/Construction/PrimePriorAtoms.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.primeSamplePrior_value_mul line 13
2. theorem OAI.Ostmann.primeSamplePrior_atom_le line 20
3. theorem OAI.Ostmann.sum_primeLogCellSet_weight line 37
4. theorem OAI.Ostmann.PublishedProgressionInput.prime_interval_atom_bounds line 45

   Source documentation

   The input needed by repeated-prior domination and accidental polynomial zeros follows from the original prime prior and the published normalization estimate. The same bound is uniform in every atom of the log interval.

   theorem PublishedProgressionInput.prime_interval_atom_bounds (P : PublishedProgressionInput) :
       ∀ᶠ u : ℝ in atTop, ∀ (s t : ℝ) (w : ℝ → ℝ) (b W : ℝ),
         s ≤ u → u + 1 ≤ t → 0 < b → 0 ≤ W →
         (∀ y ∈ Set.Ioc s t, 0 ≤ w y) →
         (∀ y ∈ Set.Ioc s t, w y ≤ W) →
         (∀ y ∈ Set.Ioc u (u + 1), b ≤ w y) →
         let S := primeLogCellSet 1 0 s t
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.primeLogCellSet