OAI/NumberTheory/CubicMoment/Angular/AngularTypeIMixedPrime.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The mixed-term replacement for the literal logarithmic prime convolution, including its norm phase. Coefficient size is derived from the fixed number of prime factors and the actual weight family.

  1. theorem OAI.CubicFirstMoment.angular_logarithmic_prime_typeI_mixed line 19