CompleteTailGiantMean.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The original giant mean from favorable primes and tail collisions

All prime laws in the conclusion are the full smooth harmonic cell laws. The favorable set is only a mask on the Fourier test, never on the prior.

def OAI.Ostmann.tailGiantPhysical line 15
def OAI.Ostmann.tailGiantEndpointMean line 20
theorem OAI.Ostmann.tailGiantEndpointMean_eq line 27

theorem OAI.Ostmann.tail_giant_positive_cell line 36

Source documentation

A finite form of (7.2). The remaining numerical premise compares the favorable harmonic mass with the explicit collision loss and total cell mass; it does not assume any mean of the giant test.

theorem tail_giant_positive_cell {A B : Set ℕ} (hA : A.Infinite) (hB : B.Infinite)
    (N : ℕ) (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (hdisjoint : ∀ p ∈ P, Disjoint (tailResidues A N p) (negTailResidues B N p))
    (F E D : Finset ℕ) (hFP : F ⊆ P) (ν : ℕ → ℝ)
    (lo hi γ δ B₀ : ℝ) (hlo : 4 < lo)
    (hsub : ∀ n ∈ logBlockCenters lo hi, smoothGiantPrimeRange n ⊆ P)
    (hFlog : ∀ p ∈ F, lo ≤ Real.log p ∧ Real.log p ≤ hi)
    (hFbal : ∀ p ∈ F, ((tailSupport A N p).card : ℝ) ≤ 2 * p / 3)
    (hFγ : ∀ p (hp : p ∈ F), let _ : Fact p.Prime := ⟨hP p (hFP hp)⟩;
…

Mentions: OAI.Ostmann.tailResidues, OAI.Ostmann.negTailResidues, OAI.Ostmann.logBlockCenters, OAI.Ostmann.smoothGiantPrimeRange, OAI.Ostmann.tailSupport