OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoefficientTailSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact support and coefficient bounds for the arithmetic remainder after removing the two leading Fourier frequencies.

  1. lemma OAI.CubicFirstMoment.cubic_primary_norm_ge_four line 12
  2. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.coefficient_norm_le_amplitude line 32

    Distinct definitions of this name: OAI/NumberTheory/CubicMoment/Theta/CubicThetaCommonCoefficientBound.lean:13 (same statement text; different proof or body). Qualify references as OAI.CubicFirstMoment.CubicThetaCoordinates.coefficient_norm_le_amplitude@path.

  3. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.amplitude_order_one_bound line 37
  4. lemma OAI.CubicFirstMoment.cubicThetaArithmetic_remainder_support line 57