OAI/NumberTheory/CubicMoment/Theta/CubicThetaCentralTypeIMixedPrime.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.logarithmic_prime_typeI_mixed_actual line 15