OAI/NumberTheory/JointDickman/Amplification/LocalArcIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.local_arc_change_variables line 11
2. theorem OAI.JointDickman.local_arc_main_term line 21

   Source documentation

   The X in the published coefficient main term cancels its part of the arc Jacobian, leaving precisely the manuscript's factor k B / j.

   theorem local_arc_main_term {j X : ℝ} (hj : j ≠ 0) (hX : X ≠ 0)
       (c R kB B : ℝ) (a : ℂ) (F W : ℝ → ℂ) :
       ((kB*B : ℝ) : ℂ)*
         (∫ θ in c-R/(j*X)..c+R/(j*X),
           F θ*((X : ℂ)*a*W ((θ-c)*(j*X)))) =
         ((kB*B/j : ℝ) : ℂ)*a*
           (∫ ξ in -R..R, F (c+ξ/(j*X))*W ξ) := by
   …