OAI/NumberTheory/DirichletL/PrimeRows/NormFiberExtraction.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ConcretePrimeRowBridge.K line 50
  2. abbrev OAI.ConcretePrimeRowBridge.O line 51
  3. instance OAI.ConcretePrimeRowBridge.(instance at line 53) line 53
  4. instance OAI.ConcretePrimeRowBridge.(instance at line 56) line 56
  5. def OAI.ConcretePrimeRowBridge.idealGenerator line 59
  6. theorem OAI.ConcretePrimeRowBridge.span_idealGenerator line 62
  7. theorem OAI.ConcretePrimeRowBridge.idealGenerator_injective line 66
  8. def OAI.ConcretePrimeRowBridge.idealsUpTo line 73
  9. theorem OAI.ConcretePrimeRowBridge.mem_idealsUpTo line 77
  10. def OAI.ConcretePrimeRowBridge.columnsUpTo line 82
  11. def OAI.ConcretePrimeRowBridge.columnWeight line 87
  12. theorem OAI.ConcretePrimeRowBridge.columnWeight_idealGenerator line 91
  13. theorem OAI.ConcretePrimeRowBridge.columnsUpTo_sum_eq_ideal_sum line 97
  14. def OAI.ConcretePrimeRowBridge.goodLambda line 110
  15. def OAI.ConcretePrimeRowBridge.primePool line 113
  16. theorem OAI.ConcretePrimeRowBridge.mem_primePool_iff line 116
  17. theorem OAI.ConcretePrimeRowBridge.primePool_maximal line 122
  18. theorem OAI.ConcretePrimeRowBridge.primePool_good line 129
  19. def OAI.ConcretePrimeRowBridge.idealSupport line 137
  20. theorem OAI.ConcretePrimeRowBridge.mem_idealSupport_iff line 141
  21. theorem OAI.ConcretePrimeRowBridge.idealGenerator_mem_prime_of_support line 147
  22. def OAI.ConcretePrimeRowBridge.idealSexticRow line 158
  23. theorem OAI.ConcretePrimeRowBridge.idealSexticRow_one line 170
  24. theorem OAI.ConcretePrimeRowBridge.baseChangeWeight_zero_of_not_squarefree line 181
  25. theorem OAI.ConcretePrimeRowBridge.idealMoebius_norm_le_one line 187
  26. theorem OAI.ConcretePrimeRowBridge.baseChangeWeight_norm_le_one line 196
  27. theorem OAI.ConcretePrimeRowBridge.columnWeight_norm_le_one line 204
  28. def OAI.ConcretePrimeRowBridge.elementRow line 213
  29. def OAI.ConcretePrimeRowBridge.idealRowSum line 227
  30. theorem OAI.ConcretePrimeRowBridge.elementRow_eq_idealRowSum line 237
  31. theorem OAI.ConcretePrimeRowBridge.idealRowSum_one line 256
  32. def OAI.ConcretePrimeRowBridge.rowNormDisk line 273
  33. theorem OAI.ConcretePrimeRowBridge.mem_rowNormDisk line 279
  34. theorem OAI.ConcretePrimeRowBridge.sixth_power_rows_in_rowNormDisk line 291
  35. theorem OAI.ConcretePrimeRowBridge.baseChange_prime_extraction_from_MS line 327
  36. def OAI.ConcretePrimeRowBridge.outsideIdealsUpTo line 415
  37. theorem OAI.ConcretePrimeRowBridge.mem_outsideIdealsUpTo line 420
  38. theorem OAI.ConcretePrimeRowBridge.outsideIdealsUpTo_ne_bot line 428
  39. theorem OAI.ConcretePrimeRowBridge.outsideIdealsUpTo_norm_le line 435
  40. theorem OAI.ConcretePrimeRowBridge.goodLambda_prime line 440
  41. theorem OAI.ConcretePrimeRowBridge.goodLambdaIdeal_maximal line 446
  42. theorem OAI.ConcretePrimeRowBridge.badPrime_cover_of_lambdaIdeal_mem line 454
  43. theorem OAI.ConcretePrimeRowBridge.outsideIdealsUpTo_good line 465
  44. theorem OAI.ConcretePrimeRowBridge.idealsUpTo_eq_biUnion_fibers line 480
  45. theorem OAI.ConcretePrimeRowBridge.normFibers_pairwiseDisjoint line 485
  46. theorem OAI.ConcretePrimeRowBridge.outsideIdealSum_eq_outsideCoeff_sum line 494
  47. theorem OAI.ConcretePrimeRowBridge.outsideCoeff_prime_extraction_from_MS line 521
  48. theorem OAI.ConcretePrimeRowBridge.eventually_absorb_MS_and_count_constants line 561
  49. theorem OAI.ConcretePrimeRowBridge.outsideCoeff_prime_extraction_with_constants line 578