OAI/NumberTheory/CubicMoment/Theta/CubicThetaCommonCoefficientBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A sharp coordinate majorant for the actual three-cusp coefficient. The ramified shift lowers its amplitude by three, exactly compensating for the prefactor in the shifted-cusp expansion.

  1. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.coefficient_norm_le_amplitude line 13

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

  2. lemma OAI.CubicFirstMoment.cubicThetaArithmetic_coordinate_bound line 25
  3. lemma OAI.CubicFirstMoment.cubicTheta_coordinate_shift_amplitude line 41
  4. theorem OAI.CubicFirstMoment.cubicThetaCommon_coordinate_bound line 50