OAI/NumberTheory/DirichletL/RowCompletion/ControlledPrimeStrata.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalRowCompletion.freePrimaryPrime line 82
  2. lemma OAI.CanonicalRowCompletion.freePrimaryPrime_ne_zero line 84
  3. lemma OAI.CanonicalRowCompletion.freePrimaryPrime_span line 89
  4. lemma OAI.CanonicalRowCompletion.freePrimaryPrime_primary line 93
  5. lemma OAI.CanonicalRowCompletion.freePrimaryPrime_maximal line 97
  6. lemma OAI.CanonicalRowCompletion.freePrimaryPrime_good line 102
  7. lemma OAI.CanonicalRowCompletion.freePrimaryPrime_odd line 107
  8. lemma OAI.CanonicalRowCompletion.freePrimaryPrime_injective line 112
  9. lemma OAI.CanonicalRowCompletion.freePrimaryPrime_coprime line 119
  10. lemma OAI.CanonicalRowCompletion.freePrimaryPrime_coprime_fixed line 126
  11. lemma OAI.CanonicalRowCompletion.freePrimaryPrime_product_span line 131
  12. lemma OAI.CanonicalRowCompletion.freePrimaryPrime_product_coprime_fixed line 139
  13. lemma OAI.CanonicalRowCompletion.actualSextic_power_transport line 144
  14. theorem OAI.CanonicalRowCompletion.freePrimeRow_eq_primary_family line 151
  15. theorem OAI.FixedRayActiveSet.fourier_inversion_by_active_set line 169
  16. theorem OAI.CubicEisenstein.completedBesselProfile_of_finite_cusp_multiplier line 218
  17. theorem OAI.CubicEisenstein.completedT_of_finite_cusp_multiplier line 240
  18. lemma OAI.CubicEisenstein.theta_lifted_phase line 269
  19. lemma OAI.CubicEisenstein.breveE_finset_sum line 282
  20. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.datum_fourier_phase line 289
  21. def OAI.CompletedGauss.unextractedCuspCoefficient line 323
  22. lemma OAI.CompletedGauss.unextractedCuspCoefficient_norm line 330
  23. theorem OAI.CompletedGauss.unextractedCuspCoefficient_summable line 367
  24. def OAI.CubicEisenstein.FixedFourierGeometry.stratumBranchTerm line 395
  25. theorem OAI.CubicEisenstein.FixedFourierGeometry.stratumBranchTerm_summable line 406
  26. theorem OAI.CubicEisenstein.FixedFourierGeometry.stratumBranchTerm_fubini line 424
  27. theorem OAI.CubicEisenstein.FixedFourierGeometry.reflectedValue_eq_branch_sums line 460
  28. theorem OAI.CubicEisenstein.FixedFourierGeometry.stratumBranchTerm_tsum_extract line 505
  29. theorem OAI.CubicEisenstein.FixedFourierGeometry.smoothedValue_eq_extracted_branch_sums line 531
  30. lemma OAI.CanonicalRowCompletion.freePrimaryPrime_coprime_completion line 569
  31. theorem OAI.CanonicalRowCompletion.exists_freePrimary_controlled_stratum line 583
  32. def OAI.CanonicalRowCompletion.freePrimaryControlledStratum line 603