OAI/NumberTheory/Ostmann/Construction/HarmonicBoxMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.pageAtModulus_one line 13
2. theorem OAI.Ostmann.selectedPrimeLogDensity_one line 19
3. theorem OAI.Ostmann.primeGiantMeasure_one_mass line 23
4. theorem OAI.Ostmann.bulkCellMixture_mass line 31
5. theorem OAI.Ostmann.PublishedProgressionInput.harmonic_box_mass_le_two line 40

   Source documentation

   Comparison with the modulus-one prime law bounds the sum of the real harmonic box masses, with the original normalization and no count of boxes.

   theorem PublishedProgressionInput.harmonic_box_mass_le_two
       (P : PublishedProgressionInput) {C : Type*} [Fintype C]
       (Q : ℕ) (hQ : 2 ≤ Q) (u v : 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 1 0 (u c) (v c))).real Set.univ ≤ 1)
       (herror : Z * ∑ c, bulkPrimeErrorFactor P Q (u c) ≤ 1) :
       Z * ∑ c, ∫ x in Set.Ioc (u c) (v c), (x : ℝ)⁻¹ ≤ 2 := by
   …

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

6. theorem OAI.Ostmann.harmonic_box_mass_log line 55