ModFivePrimeBands.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Concrete modulus-five supplies and their reciprocal masses. We use half-open bands (exp A, exp B]; this harmless endpoint convention makes adjacent supplies exactly disjoint and matches finite Abel summation.

def OAI.TwoPointCorrelations.deletedModFiveLogWeight line 14
lemma OAI.TwoPointCorrelations.partialSum_deletedModFive line 17
def OAI.TwoPointCorrelations.modFivePrimeBand line 27
lemma OAI.TwoPointCorrelations.modFivePrimeBand_mem line 30
lemma OAI.TwoPointCorrelations.modFivePrimeBand_sum line 38
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.band_error line 56
Source documentation
Both selected prime classes have their correct logarithmic-band mass, uniformly over the upper endpoint and with any fixed finite exclusions.
```
theorem ModFiveThetaInput.band_error (hP : ModFiveThetaInput) (E : Finset ℕ) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ (one : Bool) (A B : ℝ), 1 ≤ A → A ≤ B →
      |(∑ p ∈ modFivePrimeBand E one (Real.exp A) (Real.exp B), 1 / (p : ℝ)) -
          modFiveDensity one * (Real.log B - Real.log A)| ≤ 4 * K / A := by
…
```
Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput, OAI.TwoPointCorrelations.modFivePrimeBand, OAI.TwoPointCorrelations.modFiveDensity

theorem OAI.TwoPointCorrelations.ModFiveThetaInput.centered_band_mass line 74

Source documentation

The concrete centered-prime supplies have reciprocal mass in [W,2W] once their lower logarithmic endpoint exceeds one fixed threshold.

theorem ModFiveThetaInput.centered_band_mass (hP : ModFiveThetaInput)
    (E : Finset ℕ) (W : ℝ) (hW : 0 < W) :
    ∃ A₀ : ℝ, 1 ≤ A₀ ∧ ∀ A : ℝ, A₀ ≤ A →
      W ≤ (∑ p ∈ modFivePrimeBand E true (Real.exp A)
        (Real.exp (A * Real.exp (6 * W))), 1 / (p : ℝ)) ∧
      (∑ p ∈ modFivePrimeBand E true (Real.exp A)
        (Real.exp (A * Real.exp (6 * W))), 1 / (p : ℝ)) ≤ 2 * W := by
…

Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput, OAI.TwoPointCorrelations.modFivePrimeBand