MetaplecticGammaRecurrence.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact far-left metaplectic Gamma growth from the finite recurrence. Choosing Re s = 1/2-m gives the sharp height exponent 4m = 2+4A, A=m-1/2. No additional Stirling or completed-height input is needed.

lemma OAI.CubicFirstMoment.metaplectic_ascPochhammer_norm line 11

lemma OAI.CubicFirstMoment.metaplectic_symmetric_gamma_ratio line 29

Source documentation

A symmetric Gamma ratio for any fixed real shift, retaining the zero values at the totalized Gamma poles.

lemma metaplectic_symmetric_gamma_ratio (k : ℝ) (m : ℕ) (t : ℝ) :
    ‖Complex.Gamma ((1/2:ℂ)+(m:ℂ)+(k:ℂ)-(t:ℂ)*Complex.I) /
      Complex.Gamma ((1/2:ℂ)-(m:ℂ)+(k:ℂ)+(t:ℂ)*Complex.I)‖ ≤
      (|k|+3*(m:ℝ)+1)^(2*m)*(1+|t|)^(2*m) := by
…

lemma OAI.CubicFirstMoment.metaplecticGamma_symmetric_factor line 71
theorem OAI.CubicFirstMoment.metaplecticGamma_half_integer_bound line 105
Source documentation
Sharp exponent on the far-left half-integral lines, sufficient for arbitrary-power angular dual truncation. Constants depend only on ℓ,m.
```
theorem metaplecticGamma_half_integer_bound (ℓ : ℤ) (m : ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ t : ℝ,
      ‖metaplecticGammaQuotient ℓ ((1/2:ℂ)-(m:ℂ)+(t:ℂ)*Complex.I)‖ ≤
        C*(1+|t|)^(4*m) := by
…
```
Mentions: OAI.CubicFirstMoment.metaplecticGammaQuotient