OAI/NumberTheory/DirichletL/GaussSum/ResidualEquivalence.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompletedGauss.nonzeroDualDilation_residual_equiv line 84
  2. lemma OAI.CompletedGauss.unextractedCuspCoefficient_residual_equiv line 103
  3. lemma OAI.CubicEisenstein.FixedFourierGeometry.stratumBranchTerm_residual_zero_equiv line 126
  4. theorem OAI.CubicEisenstein.FixedFourierGeometry.smoothedValue_eq_nonresidual_equiv line 137
  5. def OAI.CubicEisenstein.primeInactiveFourierWeight line 202
  6. lemma OAI.CubicEisenstein.primeRow_fourier_by_active line 209
  7. def OAI.CubicEisenstein.activeStratumDatum line 231
  8. theorem OAI.CubicEisenstein.activeStratum_fourier_multiplier line 242
  9. abbrev OAI.CubicEisenstein.FixedActiveCuspIndex line 307
  10. def OAI.CubicEisenstein.fixedActiveCuspDatum line 319
  11. def OAI.CubicEisenstein.fixedActiveCuspWeight line 323
  12. theorem OAI.CubicEisenstein.fixedActiveCusp_fourier_multiplier line 328
  13. theorem OAI.CubicEisenstein.completedT_fixed_active_strata line 364
  14. def OAI.CanonicalRowCompletion.actualControlledSource line 407
  15. theorem OAI.CanonicalRowCompletion.fixedFree_completedT_eq_actualControlledSource line 428
  16. theorem OAI.CanonicalRowCompletion.rowTwist_completedT_eq_actualControlledSource line 460
  17. structure OAI.CanonicalRowCompletion.GoodMaskRowData line 490
  18. theorem OAI.CanonicalRowCompletion.exists_goodMaskRowData line 506
  19. def OAI.CanonicalRowCompletion.goodMaskRowData line 513
  20. def OAI.CanonicalRowCompletion.GoodMaskRowData.movingIdeal line 519
  21. lemma OAI.CanonicalRowCompletion.GoodMaskRowData.movingSupported line 521
  22. def OAI.CanonicalRowCompletion.GoodMaskRowData.fixedFactor line 524
  23. lemma OAI.CanonicalRowCompletion.GoodMaskRowData.numeratorFactor_norm line 528
  24. lemma OAI.CanonicalRowCompletion.GoodMaskRowData.fixedFactor_periodic line 535
  25. lemma OAI.CanonicalRowCompletion.GoodMaskRowData.fixedFactor_norm line 547
  26. theorem OAI.CanonicalRowCompletion.GoodMaskRowData.row_primary line 554
  27. theorem OAI.CanonicalRowCompletion.GoodMaskRowData.completedT_eq_fixedFactor line 567
  28. lemma OAI.CanonicalRowCompletion.GoodMaskRowData.fixedCoefficient_norm line 574
  29. def OAI.CanonicalRowCompletion.GoodMaskRowData.primeFiberEquiv line 595
  30. lemma OAI.CanonicalRowCompletion.GoodMaskRowData.primeFiberEquiv_val line 603
  31. lemma OAI.CanonicalRowCompletion.GoodMaskRowData.primeFiberEquiv_exponent line 609
  32. def OAI.CanonicalRowCompletion.GoodMaskRowData.activePrimeEquiv line 621
  33. lemma OAI.CanonicalRowCompletion.GoodMaskRowData.activePrimeEquiv_exponent line 626
  34. def OAI.CanonicalRowCompletion.fiberGoodMaskRowData line 638