OAI/NumberTheory/CubicMoment/Angular/AngularStoppedMixedModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Coprimality removal in the literal stopped mixed model. Roughness is required only at nonzero coefficients; the original support is retained.

  1. theorem OAI.CubicFirstMoment.angular_stopped_mixed_model_log_saving line 20