OAI/NumberTheory/CubicMoment/Theta/CubicThetaCentralAngularLargeTupleRestrictedSmoothed.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Full Mellin smoothing for the precise predicate-indexed coefficients in the actual regrouping identity. The two independent coordinate products have exactly their original smooth weights.

  1. theorem OAI.CubicFirstMoment.angular_large_tuple_restricted_smoothed_actual line 16