OAI/NumberTheory/TotientAsymptotic/GeometricPrefixMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.relaxed_geometric_projection line 14
2. theorem OAI.TotientAsymptotic.geometric_projected_prime_mass line 54
3. lemma OAI.TotientAsymptotic.late_prefix_volume_le line 88
4. lemma OAI.TotientAsymptotic.late_prefix_volume_monotone line 101
5. theorem OAI.TotientAsymptotic.geometric_initial_mass_le line 127
6. theorem OAI.TotientAsymptotic.geometric_initial_mass_le_base line 163
7. theorem OAI.TotientAsymptotic.geometric_local_exception_mass line 199

   Source documentation

   A literal local exceptional-prime restriction, retaining the original prefix geometry rather than counting each prefix separately.

   theorem geometric_local_exception_mass {c : ℝ} (hc : 0 < c) :
       ∃ C : ℝ,0 < C ∧ ∀ᶠ H : ℕ in atTop,∀ᶠ x : ℝ in atTop,
         ∀ N n : ℕ,N+H=m x → ∀ hn : n < N,0 < n →
         ∀ (Q : Finset (Fin N → ℕ)) (U V : Finset ℕ),
           (∀ p ∈ Q,(∀ i,(p i).Prime) ∧
             primePrefixCoord p ∈ relaxedGeometricFamily (m x) N (B x) c) →
           (∀ p ∈ Q,∀ i : Fin (N-n),primeFinal p n i ∈ U) →
           (∀ p ∈ Q,primeFinal p n ⟨0,by omega⟩ ∈ V) →
         (∑ p ∈ Q,reciprocalShiftWeight p) ≤
           C*G x n*(∑ p ∈ V,((p-1:ℕ):ℝ)⁻¹)*
             (∑ p ∈ U,((p-1:ℕ):ℝ)⁻¹)^(N-n-1) := by
   …

   Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.primePrefixCoord, OAI.TotientAsymptotic.relaxedGeometricFamily, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.primeFinal, OAI.TotientAsymptotic.reciprocalShiftWeight, OAI.TotientAsymptotic.G