MetaplecticActualInverse.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact inverse completion for the original angular, norm-twisted smooth Gauss sum. All cube-divisor sums are finite by the actual support of the weight, and the rescaled completed length is retained literally.

def OAI.CubicFirstMoment.metaplecticAngularSmoothSum line 13
lemma OAI.CubicFirstMoment.metaplecticAngularSmoothSum_finite line 18
theorem OAI.CubicFirstMoment.metaplectic_angular_actual_inverse line 44
Source documentation
Equation (angular-inversion), with the height-dependent inverse weight and the original compactly supported sum on its left.
```
theorem metaplectic_angular_actual_inverse
    (r : Eisenstein) (ℓ : ℤ) (W : ℝ → ℂ)
    {U B F : ℝ} (hU : 0 < U) (hB : 0 ≤ B) (hBF : B*U ≤ F)
    (hW : ∀ x : ℝ, B < x → W x = 0) (t : ℝ) :
    metaplecticAngularSmoothSum r ℓ W U t =
      ∑ c ∈ primaryElementBall F,
        ((idealMoebius c:ℂ)*metaplecticCompletionWeight r ℓ t c)*
          metaplecticHeightCompleted r ℓ W (U/norm c^3) t := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.metaplecticAngularSmoothSum, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.idealMoebius, OAI.CubicFirstMoment.metaplecticCompletionWeight, OAI.CubicFirstMoment.metaplecticHeightCompleted, OAI.CubicFirstMoment.norm