OAI/NumberTheory/JointDickman/Amplification/LogOscillatoryTest.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Oscillation of the actual major-arc tests in logarithmic coordinates

  1. def OAI.JointDickman.logOscillatoryTest line 12
  2. def OAI.JointDickman.logOscillatoryTestDeriv line 15
  3. theorem OAI.JointDickman.hasDerivAt_logOscillatoryTest line 18
  4. theorem OAI.JointDickman.logOscillatoryTest_norm line 32
  5. theorem OAI.JointDickman.logOscillatoryTest_deriv_bound line 36
  6. theorem OAI.JointDickman.logOscillatoryTest_lipschitz line 50
  7. theorem OAI.JointDickman.logOscillatoryTest_majorArc line 65

    Source documentation

    Exact major-arc phase after the logarithmic change of variables.

    theorem logOscillatoryTest_majorArc (w : ℝ → ℝ) {B N j X k ξ : ℝ}
    (hB : B ≠ 0) (hN : N ≠ 0) (hk : 0 < k) :
    logOscillatoryTest w B N (ξ*N/(j*X)) (Real.log k/B) =
      (w (k/N) : ℂ)*additivePhase (ξ*k/(j*X)) := by
…

    Mentions: OAI.JointDickman.logOscillatoryTest, OAI.JointDickman.additivePhase