OAI/NumberTheory/CubicMoment/Theta/CubicThetaAngularExponential.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubicFirstMoment.cubicThetaAngularAbsorption line 9
2. lemma OAI.CubicFirstMoment.cubicThetaAngularAbsorption_pos line 11
3. lemma OAI.CubicFirstMoment.cubicTheta_frequency_power_exp line 15
4. lemma OAI.CubicFirstMoment.cubicThetaAngular_kernel_exp_bound line 47
5. def OAI.CubicFirstMoment.cubicThetaAngularExpConstant line 77
6. lemma OAI.CubicFirstMoment.cubicThetaAngular_term_exp_bound line 81
7. theorem OAI.CubicFirstMoment.cubicThetaAngular_exponential_bound line 111

   Source documentation

   Uniform exponential decrease of each fixed angular theta series.

   theorem cubicThetaAngular_exponential_bound {a : Eisenstein → ℂ} {C v : ℝ}
       (hC : 0 ≤ C) (ha : ∀ n : Eisenstein, n ≠ 0 → ‖a n‖ ≤ C*norm n)
       (ℓ : ℤ) (hv : 1 ≤ v) (z : ℂ) :
       ‖cubicThetaNonconstant (cubicThetaAngularCoefficient a ℓ) (z,v)‖ ≤
         cubicThetaAngularExpConstant C ℓ*Real.exp (-(Real.pi/18)*v) := by
   …

   Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cubicThetaNonconstant, OAI.CubicFirstMoment.cubicThetaAngularCoefficient, OAI.CubicFirstMoment.cubicThetaAngularExpConstant