OAI/NumberTheory/Ostmann/Arithmetic/BulkPrimeCellMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.bulkConstant line 12
2. theorem OAI.Ostmann.bulkConstant_average_one line 17
3. theorem OAI.Ostmann.primeLogCell_page_mass_error line 23
4. theorem OAI.Ostmann.PublishedProgressionInput.bulk_cell_page_mass_le_two line 37

   Source documentation

   If the original normalized prime law has mass at most one, the ideal Page law has mass at most two once its derived interval error is at most one.

   theorem PublishedProgressionInput.bulk_cell_page_mass_le_two
       (P : PublishedProgressionInput) {C : Type*} [Fintype C]
       (Q : ℕ) (hQ : 2 ≤ Q) (q a : C → ℕ) (u v : C → ℝ)
       (hq : ∀ c, 1 ≤ q c) (hqQ : ∀ c, q c ≤ Q) (ha : ∀ c, (a c).Coprime (q c))
       (hu : ∀ c, 1 ≤ u c) (huv : ∀ c, u c ≤ v c) (hshort : ∀ c, v c ≤ u c + 1)
       (Z : ℝ) (hZ : 0 ≤ Z)
       (hmass : (bulkCellMixture Z (fun c => primeLogCellMeasure (q c) (a c) (u c) (v c))).real Set.univ ≤ 1)
       (herror : Z * ∑ c, bulkPrimeErrorFactor P Q (u c) ≤ 1) :
       (bulkCellMixture Z (fun c => primeGiantMeasure P Q (q c) (a c) (u c) (v c))).real Set.univ ≤ 2 := by
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.bulkCellMixture, OAI.Ostmann.primeLogCellMeasure, OAI.Ostmann.bulkPrimeErrorFactor, OAI.Ostmann.primeGiantMeasure