MetaplecticDecompletion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Removal of the actual completion factor, including its contribution to the residue. This is an internal analytic bridge: the completed continuation must still be constructed from the Voronoi identity.

def OAI.CubicFirstMoment.metaplecticCompletedResidue line 15
lemma OAI.CubicFirstMoment.metaplectic_completed_residue_div line 18
lemma OAI.CubicFirstMoment.metaplectic_decompletion_regular line 27
Source documentation
The regular part after division includes the divided difference of the inverse Euler factor. In particular its value at the pole is obtained by the derivative, without changing any value away from the pole.
```
lemma metaplectic_decompletion_regular {r : Eisenstein} (hr : r ≠ 0)
    (g : ℂ → ℂ) (hg : DifferentiableOn ℂ g {s : ℂ | (1/2:ℝ) < s.re}) :
    ∃ h : ℂ → ℂ, DifferentiableOn ℂ h {s : ℂ | (1/2:ℝ) < s.re} ∧
      ∀ s : ℂ, (1/2:ℝ) < s.re → s ≠ (5/6:ℂ) →
        (g s+metaplecticCompletedResidue r/(s-5/6))/metaplecticCompletionEuler r s =
          h s+metaplecticResidue r/(s-5/6) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.metaplecticCompletedResidue, OAI.CubicFirstMoment.metaplecticCompletionEuler, OAI.CubicFirstMoment.metaplecticResidue
lemma OAI.CubicFirstMoment.metaplectic_decompletion_right line 53