OAI/NumberTheory/JointDickman/Analysis/MellinSieveHighFrequency.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.mellin_profile_high_blocks line 15

   Source documentation

   Dyadic recombination of logarithmic phase cancellation, with explicit frequency and cutoff inequalities.

   theorem mellin_profile_high_blocks (B : ℝ) (hB : 1/2 ≤ B) :
       ∃ A δ V : ℝ, 0 < A ∧ 0 < δ ∧ δ ≤ 1 ∧
         ∀ (N d t : ℝ) (Z K J : ℕ), 0 < d → d ≤ N → 0 < Z → V ≤ Z →
           K ≤ 2^J*Z → ((2^J*Z:ℕ):ℝ)^(1/2:ℝ) ≤ |t/(2*Real.pi)| →
           |t/(2*Real.pi)| ≤ (Z:ℝ)^B →
           ‖∑ n ∈ Ioc Z K, mellinSieveFunction N t (d*n)‖ ≤
             (J:ℝ)*A*(N/d)^(1-δ) := by
   …

   Mentions: OAI.JointDickman.mellinSieveFunction

2. lemma OAI.JointDickman.mellin_profile_small_sum line 62
3. lemma OAI.JointDickman.mellinSieveDiscreteKernel_grid line 77
4. theorem OAI.JointDickman.mellinSieve_high_error line 90

   Source documentation

   The actual high-frequency divisor-kernel error. Every term on the right is explicit; the phase saving comes from the proved derivative estimates.

   theorem mellinSieve_high_error (B : ℝ) (hB : 1/2 ≤ B) :
       ∃ A δ V : ℝ, 0 < A ∧ 0 < δ ∧ δ ≤ 1 ∧
         ∀ (N t : ℝ) (d K Z J : ℕ), 0 < d → (d:ℝ) ≤ N → 0 < Z → V ≤ Z →
           K/d ≤ 2^J*Z → ((2^J*Z:ℕ):ℝ)^(1/2:ℝ) ≤ |t/(2*Real.pi)| →
           |t/(2*Real.pi)| ≤ (Z:ℝ)^B →
           ‖mellinSieveDiscreteKernel K d N t-mellinSieveMainKernel N t/(d:ℂ)‖ ≤
             (d:ℝ)*(Z:ℝ)^2/N + (J:ℝ)*A*(N/d)^(1-δ) + 4*N/((d:ℝ)*(4+t^2)) := by
   …

   Mentions: OAI.JointDickman.mellinSieveDiscreteKernel, OAI.JointDickman.mellinSieveMainKernel