OAI/NumberTheory/DirichletL/RowCompletion/FixedCuspBranches.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CanonicalRowCompletion.prime_dvd_iff_factor_count_pos line 85
  2. theorem OAI.CanonicalRowCompletion.goodMaskMovingIdeal_dvd_iff line 89
  3. theorem OAI.CanonicalRowCompletion.goodMaskMovingIdeal_primeSupport line 106
  4. def OAI.CanonicalRowCompletion.goodMaskNonresidualPool line 138
  5. theorem OAI.CanonicalRowCompletion.goodMaskNonresidualPool_eq line 142
  6. theorem OAI.CanonicalRowCompletion.goodMaskNonresidualPool_eq_on_fiber line 155
  7. theorem OAI.CanonicalRowCompletion.goodMaskNonresidualPool_free_eq line 172
  8. theorem OAI.CanonicalRowCompletion.goodMaskMovingIdeal_principal_row line 188
  9. theorem OAI.CanonicalRowCompletion.rowTwist_eq_computed_principal_row line 212
  10. theorem OAI.CanonicalRowCompletion.goodMaskMovingIdeal_exponent_eq_on_fiber line 234
  11. lemma OAI.CubicEisenstein.FixedCuspShape.amplitude_source_nonzero line 269
  12. lemma OAI.CubicEisenstein.FixedCuspShape.amplitude_integral_phase line 280
  13. lemma OAI.CubicEisenstein.FixedCuspShape.datum_integral_phase line 293
  14. def OAI.CubicEisenstein.FixedCuspShape.stratumShapeFactor line 319
  15. lemma OAI.CubicEisenstein.FixedCuspShape.datum_common_row_factor line 323
  16. theorem OAI.CubicEisenstein.FixedCuspShape.sum_smoothedKernel_integral_phase line 343
  17. lemma OAI.CubicEisenstein.FixedCuspShape.stratumShapeFactor_norm line 410
  18. def OAI.CompletedGauss.fixedCuspArrayWithPhase line 433
  19. lemma OAI.CompletedGauss.fixedCuspArrayWithPhase_norm_le_one line 437
  20. lemma OAI.CompletedGauss.fixedCuspArrayWithPhase_zero line 444
  21. def OAI.CompletedGauss.ReflectedBranchData.extractedFixedCuspArrayWithPhase line 452
  22. lemma OAI.CompletedGauss.ReflectedBranchData.extractedFixedCuspArrayWithPhase_norm_le_one line 461
  23. lemma OAI.CompletedGauss.ReflectedBranchData.extractedFixedCuspArrayWithPhase_eq line 467
  24. lemma OAI.CompletedGauss.ReflectedBranchData.extractedFixedCuspArrayWithPhase_zero line 478
  25. def OAI.CompletedGauss.ReflectedBranchData.withExtractedFixedCuspArrayWithPhase line 489
  26. lemma OAI.CompletedGauss.ReflectedBranchData.withExtractedFixedCuspArrayWithPhase_amplitude line 498
  27. theorem OAI.CompletedGauss.ReflectedBranchData.withExtractedFixedCuspArrayWithPhase_value line 506
  28. def OAI.CompletedGauss.sixPhaseFixedCuspBranch line 530
  29. lemma OAI.CompletedGauss.sixPhaseFixedCuspBranch_primes line 540
  30. lemma OAI.CompletedGauss.sixPhaseFixedCuspBranch_amplitude line 548
  31. lemma OAI.CompletedGauss.sixPhaseFixedCuspBranch_scale line 562
  32. def OAI.CompletedGauss.sixPhaseFixedCuspFiber line 578
  33. theorem OAI.CompletedGauss.sixPhaseFixedCuspFiber_value line 599