OAI/NumberTheory/JointDickman/Analysis/MellinIntegerKernel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.mellin_integer_kernel_phase line 10
2. theorem OAI.JointDickman.mellin_integer_kernel_bound line 23

   Source documentation

   A sharp dyadic Mellin kernel has reciprocal decay below its length, and a square-root error beyond it.

   theorem mellin_integer_kernel_bound {U : ℝ} (hU : 1 ≤ U) (L R : ℕ)
       (hL : U ≤ (L:ℝ)) (hR : (R:ℝ) ≤ 2*U) (t : ℝ) :
       ‖mellinSampleKernel (Icc L R) (fun _ => 1) t‖ ≤
         16000*(U/(1+|t|)+Real.sqrt |t|) := by
   …

   Mentions: OAI.JointDickman.mellinSampleKernel

3. theorem OAI.JointDickman.mellin_integer_kernel_rows line 51

   Source documentation

   The concrete sharp integer kernel has a logarithmic row bound, plus a cost proportional to the number of sampled frequencies.

   theorem mellin_integer_kernel_rows {U : ℝ} (hU : 1 ≤ U) (L R : ℕ)
       (hL : U ≤ (L:ℝ)) (hR : (R:ℝ) ≤ 2*U)
       (S : Finset ℝ) (hsep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x-y|)
       {T : ℝ} (hT : 0 ≤ T)
       (hdiam : ∀ x ∈ S, ∀ y ∈ S, |x-y| ≤ T) (t : ℝ) (ht : t ∈ S) :
       (∑ u ∈ S, ‖mellinSampleKernel (Icc L R) (fun _ => 1) (t-u)‖) ≤
         16000*(2*U*(1+Real.log (T+1))+(S.card:ℝ)*Real.sqrt T) := by
   …

   Mentions: OAI.JointDickman.mellinSampleKernel