LargeTupleRestrictedSmoothed.lean`

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.

theorem OAI.CubicFirstMoment.large_tuple_restricted_smoothed line 16