OAI/NumberTheory/CubicMoment/Angular/AngularRealScaleLargeMoment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The large-conductor estimate in the actual real dyadic scales. The exponents are constructed from logarithms, not supplied as extra data.

  1. theorem OAI.CubicFirstMoment.angular_large_conductor_real_scales line 14