OAI/NumberTheory/CubicMoment/Theta/CubicThetaMains.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact first moment and both fixed-angular main theorems.

  1. theorem OAI.CubicFirstMoment.patterson_angularComparison line 10

    Distinct definitions of this name: ComparatorChallenges/PattersonFirstMoment.lean:88 (same statement text; different proof or body). Qualify references as OAI.CubicFirstMoment.patterson_angularComparison@path.

  2. theorem OAI.CubicFirstMoment.patterson_angularCancellation line 13

    Distinct definitions of this name: ComparatorChallenges/PattersonFirstMoment.lean:92 (same statement text; different proof or body). Qualify references as OAI.CubicFirstMoment.patterson_angularCancellation@path.

  3. theorem OAI.CubicFirstMoment.patterson_firstMoment line 17

    Distinct definitions of this name: ComparatorChallenges/PattersonFirstMoment.lean:84 (same statement text; different proof or body). Qualify references as OAI.CubicFirstMoment.patterson_firstMoment@path.

  4. theorem OAI.CubicFirstMoment.patterson_mainResults line 31