CubicThetaAngularPowers.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact frequency powers in the fixed-angular theta Mellin transform.

def OAI.CubicFirstMoment.cubicThetaAngularCoefficient line 12
Source documentation
The frequency multiplier produced by the derivative of order |ell|, with its signed angular component kept explicit.
```
def cubicThetaAngularCoefficient (a : Eisenstein → ℂ) (ℓ : ℤ) (n : Eisenstein) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.cubicThetaAngularCoefficient_norm line 15
lemma OAI.CubicFirstMoment.cubicThetaAngular_real_power line 21
lemma OAI.CubicFirstMoment.cubicThetaAngular_complex_power line 28
lemma OAI.CubicFirstMoment.cubicThetaAngular_weight line 37
Source documentation
The growing derivative factor exactly cancels the shifted Mellin exponent; the remaining coefficient mass is the original bounded one.
```
lemma cubicThetaAngular_weight {a : Eisenstein → ℂ} (ℓ : ℤ)
    {n : Eisenstein} (hn : n ≠ 0) (s : ℂ) :
    ‖cubicThetaAngularCoefficient a ℓ n‖*
      ‖cubicThetaFrequency n‖^(-(2*s+(ℓ.natAbs:ℂ)-1).re) =
        ‖a n‖*‖cubicThetaFrequency n‖^(-(2*s-1).re) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicThetaAngularCoefficient, OAI.CubicFirstMoment.cubicThetaFrequency
lemma OAI.CubicFirstMoment.cubicThetaAngular_dirichlet_term line 48