MertensShortBlockMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Mertens bounds for the complete giant cell family

theorem OAI.Ostmann.mertens_log_block_upper line 11

theorem OAI.Ostmann.logBlock_family_mass_upper line 46

Source documentation

The total mass of all complete cells near the block is of order its length divided by its location, including the overlapping boundary cells.

theorem logBlock_family_mass_upper {C : ℝ} (hM : MertensEstimate C)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (lo hi : ℝ)
    (hlo : 5 ≤ lo) (hlohi : lo ≤ hi) :
    (∑ p ∈ P, (p : ℝ)⁻¹ * logCellFamilyWeight (logBlockCenters lo hi) p) ≤
      (hi - lo + 8 + Real.log 2 + 2 * C) / (lo - 4) := by
…

Mentions: OAI.Ostmann.MertensEstimate, OAI.Ostmann.logCellFamilyWeight, OAI.Ostmann.logBlockCenters

theorem OAI.Ostmann.logBlock_family_collision_weight line 95
Source documentation
Localized harmonic weights fit directly under the logarithmic collision budget. The zero-weight primes in the large container need no lower bound.
```
theorem logBlock_family_collision_weight (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (lo hi : ℝ) (hlo : 4 < lo) (p : P) :
    ((p : ℝ)⁻¹ * logCellFamilyWeight (logBlockCenters lo hi) p) * (p : ℝ) ≤
      Real.log (p : ℝ) / (lo - 4) := by
…
```
Mentions: OAI.Ostmann.logCellFamilyWeight, OAI.Ostmann.logBlockCenters