CubicWhittakerBounds.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Local regularity and explicit majorants of the cubic theta Fourier kernel.

def OAI.CubicFirstMoment.cubicWhittakerPowerConstant line 12
lemma OAI.CubicFirstMoment.cubicWhittakerPowerConstant_pos line 15
lemma OAI.CubicFirstMoment.cubicThetaWhittaker_norm line 22
lemma OAI.CubicFirstMoment.cubicThetaWhittaker_continuousAt line 29
theorem OAI.CubicFirstMoment.cubicThetaWhittaker_power_bound line 40
Source documentation
Every fixed power majorant is available on the full positive axis.
```
theorem cubicThetaWhittaker_power_bound (k : ℕ) (hk : 1 ≤ k) {v : ℝ} (hv : 0 < v) :
    ‖cubicThetaWhittaker v‖ ≤ cubicWhittakerPowerConstant k*v^(4/3-2*(k:ℝ)) := by
…
```
Mentions: OAI.CubicFirstMoment.cubicThetaWhittaker, OAI.CubicFirstMoment.cubicWhittakerPowerConstant