OAI/NumberTheory/CubicMoment/Angular/AngularStructuredSupportBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The independent coordinate support bounds remain unchanged by the fixed angular factor. Its finite sum is dominated by the original coefficient mass.

  1. lemma OAI.CubicFirstMoment.structuredAngularPrimeSum_norm_le line 14