HeightMeanSquare.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact finite spectral expansion of the height-averaged square. The diagonal and every off-diagonal pair are retained.

lemma OAI.CubicFirstMoment.continuous_normTwist line 12
lemma OAI.CubicFirstMoment.norm_square_twisted_sum line 16
lemma OAI.CubicFirstMoment.averaged_finite_mean_square line 30
lemma OAI.CubicFirstMoment.height_diagonal_coefficient line 62
Source documentation
The zero spectral difference contributes the exact coefficient square, even when different elements have the same norm.
```
lemma height_diagonal_coefficient (c : ℂ) {T : ℝ} (hT : T ≠ 0) (u : ℝ) (b : Eisenstein) :
    (c*star c)*(normTwist u b*star (normTwist u b))*
      mellinHeightKernel T (Real.log (norm b)-Real.log (norm b)) = ((‖c‖^2:ℝ):ℂ) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.normTwist, OAI.CubicFirstMoment.mellinHeightKernel, OAI.CubicFirstMoment.norm
lemma OAI.CubicFirstMoment.averaged_finite_mean_square_diagonal line 72