OAI/NumberTheory/DirichletL/CubicSieve/LiteralSources.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.globalSecondLiteralBinSource line 85
  2. theorem OAI.SecondPassArithmetic.sum_globalArithmeticBin line 92
  3. theorem OAI.SecondPassArithmetic.globalSecondLiteralBinSource_transfer line 101
  4. lemma OAI.CubicEisenstein.complex_norm_mul_add_sq line 170
  5. lemma OAI.CubicEisenstein.matrixFrobenius_nonneg line 176
  6. lemma OAI.CubicEisenstein.matrixFrobenius_mul_le line 180
  7. lemma OAI.CubicEisenstein.matrixFrobenius_inv line 187
  8. lemma OAI.CubicEisenstein.hyperbolicFrobenius_nonneg line 194
  9. lemma OAI.CubicEisenstein.matrixFrobenius_le_displacement line 198
  10. instance OAI.CubicEisenstein.integralSubgroupContinuousAction line 206
  11. instance OAI.CubicEisenstein.integralSubgroupProperlyDiscontinuous line 210
  12. instance OAI.CubicEisenstein.upperCoordinatesLocallyCompact line 241
  13. instance OAI.CubicEisenstein.hyperbolicLocallyCompact line 243
  14. instance OAI.CubicEisenstein.hyperbolicSecondCountable line 245
  15. instance OAI.CubicEisenstein.upperCoordinatesPolish line 248
  16. instance OAI.CubicEisenstein.hyperbolicPolish line 250
  17. lemma OAI.CubicEisenstein.integralOrbitRel_eq line 253
  18. instance OAI.CubicEisenstein.integralOrbitQuotientT2 line 263
  19. lemma OAI.CubicEisenstein.integralSubgroupFree line 268
  20. lemma OAI.CubicEisenstein.integralOrbitProjection_eq_iff line 272
  21. theorem OAI.CubicEisenstein.integralOrbitProjection_quotientCovering line 283
  22. lemma OAI.CubicEisenstein.integralOrbitProjection_covering line 289
  23. lemma OAI.CubicEisenstein.integralOrbitProjection_openQuotient line 293
  24. instance OAI.CubicEisenstein.kernelQuotientLocallyCompact line 298
  25. instance OAI.CubicEisenstein.kernelQuotientSecondCountable line 300
  26. instance OAI.CubicEisenstein.kernelQuotientBorel line 304
  27. lemma OAI.CubicEisenstein.kernelQuotient_localHomeomorph line 307
  28. lemma OAI.CubicEisenstein.integralOrbitProjection_preimage_image line 315
  29. lemma OAI.CubicEisenstein.kernelProjection_translates_disjoint line 327
  30. theorem OAI.CubicEisenstein.kernelProjection_measure_image line 344
  31. theorem OAI.CubicEisenstein.kernelProjection_measurePreserving_on line 360
  32. theorem OAI.CubicEisenstein.kernelL2_continuous_compact_approx line 381
  33. structure OAI.SecondPassArithmetic.GlobalFirstData line 396
  34. def OAI.SecondPassArithmetic.GlobalFirstData.append line 404
  35. def OAI.SecondPassArithmetic.GlobalSecondData.first line 410
  36. theorem OAI.SecondPassArithmetic.GlobalSecondData.append_first line 412
  37. theorem OAI.SecondPassArithmetic.GlobalSecondData.first_append line 413
  38. theorem OAI.SecondPassArithmetic.GlobalSecondData.source_append line 414
  39. def OAI.SecondPassArithmetic.globalFirstRawPool line 420
  40. def OAI.SecondPassArithmetic.globalFirstExpansionPool line 423
  41. theorem OAI.SecondPassArithmetic.mem_globalFirstExpansionPool line 427
  42. theorem OAI.SecondPassArithmetic.sum_globalFirstExpansionPool line 438
  43. def OAI.SecondPassArithmetic.globalFirstBlockColumnScale line 464
  44. def OAI.SecondPassArithmetic.globalFirstBlockLabel line 467
  45. def OAI.SecondPassArithmetic.globalFirstBlockBadLabel line 470
  46. def OAI.SecondPassArithmetic.globalFirstBlockTest line 473
  47. def OAI.SecondPassArithmetic.globalFirstTruncatedSource line 477
  48. theorem OAI.SecondPassArithmetic.globalFirstTruncatedSource_eq_literal line 488
  49. def OAI.SecondPassArithmetic.globalFirstCoreRow line 527
  50. def OAI.SecondPassArithmetic.globalFirstCoreCorrection line 537
  51. def OAI.SecondPassArithmetic.globalFirstSourceTail line 542
  52. def OAI.SecondPassArithmetic.globalFirstSourceZero line 552
  53. theorem OAI.SecondPassArithmetic.globalFirstTruncatedSource_split line 562
  54. theorem OAI.SecondPassArithmetic.globalFirstCoreRows_smoothed line 577
  55. theorem OAI.SecondPassArithmetic.globalFirstCoreRows_finite_le_sources line 608