PrimeMassSplit.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Split a finite prime family at an arbitrary coordinate without multiplying by the number of possible prefixes.

def OAI.TotientAsymptotic.primeInitial line 13
def OAI.TotientAsymptotic.primeFinal line 16
lemma OAI.TotientAsymptotic.prime_parts_injective line 19
lemma OAI.TotientAsymptotic.reciprocalShiftWeight_split line 28
lemma OAI.TotientAsymptotic.prime_pi_mass line 42

theorem OAI.TotientAsymptotic.prime_mass_split line 52

Source documentation

Each suffix coordinate can have its own arithmetic restriction. The prefix is counted once, with its original reciprocal mass.

theorem prime_mass_split {N n : ℕ} (hn : n ≤ N) (Q : Finset (Fin N → ℕ))
    (T : Fin (N-n) → Finset ℕ)
    (hT : ∀ p ∈ Q, ∀ j, primeFinal p n j ∈ T j) :
    (∑ p ∈ Q, reciprocalShiftWeight p) ≤
      (∑ p ∈ Q.image (fun p => primeInitial p n hn), reciprocalShiftWeight p)*
        ∏ j, ∑ q ∈ T j, ((q-1 : ℕ) : ℝ)⁻¹ := by
…

Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.primeFinal, OAI.TotientAsymptotic.reciprocalShiftWeight, OAI.TotientAsymptotic.primeInitial

lemma OAI.TotientAsymptotic.remainderInitial_geometry line 79
Source documentation
The same projected geometry used for collisions holds for every basic remainder, independently of its largest-prime completion.
```
lemma remainderInitial_geometry {x : ℝ} {H K : ℕ} (hn : R x K ≤ L x H)
    (hL : 0 < L x H) {η : RemainderDatum (L x H)} (hη : IsBasicRemainder x H η) :
    (∀ j, (primeInitial η.primes (R x K) hn j).Prime) ∧
    primePrefixCoord (primeInitial η.primes (R x K) hn) ∈ prefixBandRegion x K ∧
    primePrefixCoord (primeInitial η.primes (R x K) hn) ∈
      enlargedSimplex (R x K) (B x) (xi x 0) (fun j => xi x (j.val+1)) := by
…
```
Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.primeInitial, OAI.TotientAsymptotic.primePrefixCoord, OAI.TotientAsymptotic.prefixBandRegion, OAI.TotientAsymptotic.enlargedSimplex, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.xi