MetaplecticTransformBounds.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Bounds for the literal angular Voronoi transform. Its Gamma quotient is a product of two ordinary shifted Hecke quotients, so the only special-function input is the same precise DLMF bounded-strip estimate.

def OAI.CubicFirstMoment.metaplecticAngularShift line 15
lemma OAI.CubicFirstMoment.metaplecticAngularShift_nonneg line 17
lemma OAI.CubicFirstMoment.metaplecticGammaQuotient_factor line 21
theorem OAI.CubicFirstMoment.metaplecticGamma_vertical_bound line 44

lemma OAI.CubicFirstMoment.metaplecticTransform_bound_of_majorant line 66

Source documentation

A uniform weighted Mellin bound gives a uniform transform bound. This form permits the actual common-support smooth weight families.

lemma metaplecticTransform_bound_of_majorant (ℓ : ℤ) (W : ℝ → ℂ) {σ C B : ℝ}
    (hC : 0 ≤ C) (_hB : 0 ≤ B) (N : ℕ)
    (hQ : ∀ t : ℝ, ‖metaplecticGammaQuotient ℓ ((-σ:ℝ)+(t:ℂ)*Complex.I)‖ ≤
      C*(1+|t|)^N)
    (hW : ∀ t : ℝ, ‖mellin W ((-σ:ℝ)+(t:ℂ)*Complex.I)‖*(1+|t|)^N ≤
      mellinEdgeMajorant B t) {v : ℝ} (hv : 0 < v) :
    ‖metaplecticTransform ℓ W σ v‖ ≤
      (‖((1/(2*Real.pi):ℝ):ℂ)‖*C*B*(∫ t : ℝ, mellinEdgeMajorant 1 t))*v^(-σ) := by
…

Mentions: OAI.CubicFirstMoment.metaplecticGammaQuotient, OAI.CubicFirstMoment.mellinEdgeMajorant, OAI.CubicFirstMoment.metaplecticTransform

theorem OAI.CubicFirstMoment.metaplecticTransform_small_line_bound line 102
theorem OAI.CubicFirstMoment.UniformLogWeights.metaplecticTransform_bound line 121
Source documentation
Uniformity in a genuine smooth family follows from its fixed log support and derivative bounds.
```
theorem UniformLogWeights.metaplecticTransform_bound {ι : Type*} {W : ι → ℝ → ℂ}
    (hW : UniformLogWeights W) (ℓ : ℤ) {σ : ℝ} (hσ : 0 < σ)
    (hGamma : AngularGammaQuotientStripBound (metaplecticAngularShift ℓ) (-σ-1/6)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ i v, 0 < v →
      ‖metaplecticTransform ℓ (W i) σ v‖ ≤ C*v^(-σ) := by
…
```
Mentions: OAI.CubicFirstMoment.UniformLogWeights, OAI.CubicFirstMoment.AngularGammaQuotientStripBound, OAI.CubicFirstMoment.metaplecticAngularShift, OAI.CubicFirstMoment.metaplecticTransform