OAI/NumberTheory/JointDickman/Amplification/MajorArcUnfolding.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.scaled_arc_window line 13
2. theorem OAI.JointDickman.rationalArcPiece_lifted line 19
3. theorem OAI.JointDickman.rationalArc_lifted_sum line 33
4. theorem OAI.JointDickman.rationalArc_integral_summable line 51
5. theorem OAI.JointDickman.majorArc_unfolded line 66

   Source documentation

   All translates, including arcs through zero, combine into exactly j lifts of each reduced coefficient fraction.

   theorem majorArc_unfolded :
       ∀ᶠ B : ℕ in atTop, ∀ X : ℝ, 0 < X → (9/10 : ℝ)*B ≤ Real.log X →
         ∀ j : ℕ, ∀ (_ : NeZero j), ∀ F : ℝ → ℂ, Continuous F → Periodic F 1 →
         (∫ x in majorArcRegion B j X, F x) =
           ∑' q : ℕ+, ∑ u : (ZMod (q : ℕ))ˣ, ∑ t : Fin j,
             if (q : ℝ) ≤ (B : ℝ)^12 then
               ∫ x in
                 ((((u : ZMod (q : ℕ)).val : ℝ)/(q : ℕ)+t.val)/j-((B : ℝ)^13/X)/j)..
                 ((((u : ZMod (q : ℕ)).val : ℝ)/(q : ℕ)+t.val)/j+((B : ℝ)^13/X)/j), F x
             else 0 := by
   …

   Mentions: OAI.JointDickman.majorArcRegion