OAI/NumberTheory/Ostmann/Arithmetic/RestoredHarmonicCells.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.primeSubsetLogMeasure_restored_mass line 11
2. theorem OAI.Ostmann.PublishedProgressionInput.harmonic_cells_mass_error line 21

   Source documentation

   The modulus-one comparison gives the exact error in replacing all harmonic prime atoms by the real harmonic masses of the cells.

   theorem PublishedProgressionInput.harmonic_cells_mass_error
       (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) :
       |(bulkCellMixture Z (fun c => primeLogCellMeasure 1 0 (u c) (v c))).real Set.univ -
         Z * ∑ c, ∫ x in Set.Ioc (u c) (v c), (x : ℝ)⁻¹| ≤
         Z * ∑ c, bulkPrimeErrorFactor P Q (u c) := by
   …

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

3. theorem OAI.Ostmann.PublishedProgressionInput.restored_harmonic_cells_le_two line 46

   Source documentation

   Small exceptional deletions and the interval error share the same unit error budget, while the normalization remains that of the deleted prime set.

   theorem PublishedProgressionInput.restored_harmonic_cells_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)
       (hsep : ∀ c d, c ≠ d → v c ≤ u d ∨ v d ≤ u c)
       (D : Finset ℕ)
       (hS : (∑ p ∈ primeCellSupport 1 (fun _ => 0) u v \ D, (p : ℝ)⁻¹) ≠ 0)
       (herror :
         (∑ p ∈ primeCellSupport 1 (fun _ => 0) u v \ D, (p : ℝ)⁻¹)⁻¹ *
           ((∑ p ∈ primeCellSupport 1 (fun _ => 0) u v ∩ D, (p : ℝ)⁻¹) +
             ∑ c, bulkPrimeErrorFactor P Q (u c)) ≤ 1) :
       (∑ p ∈ primeCellSupport 1 (fun _ => 0) u v \ D, (p : ℝ)⁻¹)⁻¹ *
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.primeCellSupport, OAI.Ostmann.bulkPrimeErrorFactor