OAI/NumberTheory/Ostmann/Construction/OriginalHarmonicMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.PublishedProgressionInput.primeCellSupport_harmonic_error line 12
2. theorem OAI.Ostmann.deleted_harmonic_mass_le_two line 38

   Source documentation

   Deleting a small amount of original prime mass does not invalidate the required bound on the normalized real box mass.

   theorem deleted_harmonic_mass_le_two (S D : Finset ℕ) (a I err : ℝ)
       (ha : 0 < a) (hmass : a ≤ ∑ p ∈ S, (p : ℝ)⁻¹)
       (hdeleted : (∑ p ∈ S ∩ D, (p : ℝ)⁻¹) ≤ a / 4)
       (herror : |(∑ p ∈ S, (p : ℝ)⁻¹) - I| ≤ err) (herr : err ≤ a / 4) :
       0 < (∑ p ∈ S \ D, (p : ℝ)⁻¹) ∧
         (∑ p ∈ S \ D, (p : ℝ)⁻¹)⁻¹ * I ≤ 2 := by
   …

3. theorem OAI.Ostmann.PublishedProgressionInput.original_harmonic_box_mass line 52