OAI/NumberTheory/CubicMoment/Angular/AngularStoppedHeightFactors.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Multiplicative angular phases in the two coefficients give exactly the angular phase of the original centered height kernel.

  1. lemma OAI.CubicFirstMoment.centeredHeightSum_angular_factors line 12