OAI/NumberTheory/JointDickman/Analysis/LogPhaseDifferencingBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.logarithmic_differencing_budget line 13

   Source documentation

   The natural cutoff in van der Corput differencing preserves a power saving. All size conditions here are scalar and hold eventually for fixed parameters.

   theorem logarithmic_differencing_budget (r N : ℕ) (U α C : ℝ)
       (hU : 1 ≤ U) (_hα : 0 < α) (hα1 : α ≤ 1) (hC : 0 ≤ C)
       (hcut : 4 ≤ U ^ α)
       (herror : C * U ^ (-(1 : ℝ) / 5) ≤ 4 * U ^ (-α))
       (hUN : U ≤ (N : ℝ)) (hNU : (N : ℝ) ≤ 3 * U)
       (a : ℤ → ℂ)
       (hsupport : ∀ n : ℤ, n ∉ Finset.Icc (1 : ℤ) N → a n = 0)
       (hnorm : ∀ n : ℤ, ‖a n‖ ≤ 1)
       (hterminal : ∀ hs : List ℤ, hs.length = r →
         (∀ h ∈ hs, 0 < h ∧ h < (Nat.floor (U ^ α) : ℤ)) →
         ‖∑ n ∈ Finset.Icc (1 : ℤ) N, iteratedCorrelation a hs n‖ ≤
           C * U ^ ((4 : ℝ) / 5)) :
   …

2. theorem OAI.JointDickman.logarithmic_differencing_budget_eventually line 96

   Source documentation

   For fixed parameters the scalar cutoff conditions are automatic.

   theorem logarithmic_differencing_budget_eventually (r : ℕ) (α C : ℝ)
       (hα : 0 < α) (hαsmall : α < (1 : ℝ) / 5) (hC : 0 ≤ C) :
       ∀ᶠ (U : ℝ) in atTop, ∀ N : ℕ,
         U ≤ (N : ℝ) → (N : ℝ) ≤ 3 * U → ∀ a : ℤ → ℂ,
         (∀ n : ℤ, n ∉ Finset.Icc (1 : ℤ) N → a n = 0) →
         (∀ n : ℤ, ‖a n‖ ≤ 1) →
         (∀ hs : List ℤ, hs.length = r →
           (∀ h ∈ hs, 0 < h ∧ h < (Nat.floor (U ^ α) : ℤ)) →
           ‖∑ n ∈ Finset.Icc (1 : ℤ) N, iteratedCorrelation a hs n‖ ≤
             C * U ^ ((4 : ℝ) / 5)) →
         ‖∑ n ∈ Finset.Icc (1 : ℤ) N, a n‖ ≤
           36 * U ^ (1 - α / (2 : ℝ) ^ r) := by
   …