OAI/NumberTheory/JointDickman/Amplification/CanonicalTypicalDensity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.canonical_typical_iff line 12
2. lemma OAI.JointDickman.uniformFiniteLaw_nat_count line 26
3. theorem OAI.JointDickman.canonical_typical_count line 36
4. lemma OAI.JointDickman.restrictArithmetic_eq_typical line 63
5. theorem OAI.JointDickman.canonical_typical_prefix_count line 71

   Source documentation

   The exact prefix removed by the short-energy transfer has small ordinary density. Its scale is three times the original short-average location.

   theorem canonical_typical_prefix_count : ∃ C : ℝ, 0 < C ∧
       ∀ᶠ L : ℝ in atTop, ∀ (P Q η X : ℝ) (J : ℕ),
         2 ≤ P → P ≤ Q → 1 ≤ Real.log Q → 1 ≤ X →
         (∀ j ∈ range J, mrtBandUpper Q (j+1) ≤ Real.exp (L^(99/100 : ℝ))) →
         (1/2 : ℝ)*Real.exp (L^(199/200 : ℝ)) ≤ 3*X →
         (((range (⌊3*X⌋₊+1)).filter fun n =>
             ¬mrtTypical (range J) (canonicalMellinBands P Q η).primes n).card : ℝ) / X ≤
           C*Real.log P/Real.log Q := by
   …

   Mentions: OAI.JointDickman.canonicalMellinBands