OAI/NumberTheory/DirichletL/QuadraticSieve/GlobalBinLoss.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.list_prod_le_power line 76
  2. theorem OAI.CanonicalQuadraticSieve.list_prod_budget line 87
  3. theorem OAI.CanonicalQuadraticSieve.poisson_nine_terms_box line 93
  4. def OAI.CanonicalQuadraticSieve.poissonUnitBudget line 157
  5. theorem OAI.CanonicalQuadraticSieve.poissonComparisonMajorant_unit_box line 176
  6. theorem OAI.SecondPassArithmetic.globalBin_mask_bound line 233
  7. theorem OAI.SecondPassArithmetic.globalBin_invariant line 268
  8. theorem OAI.SecondPassArithmetic.globalBin_invariant_small_padding line 299
  9. def OAI.SecondPassArithmetic.globalBinTriples line 330
  10. def OAI.SecondPassArithmetic.globalBinLossScale line 334
  11. def OAI.SecondPassArithmetic.globalDescentWeight line 337
  12. theorem OAI.SecondPassArithmetic.globalPooledRowScale_pos line 345
  13. theorem OAI.SecondPassArithmetic.globalBinFirstCoefficient_nonneg line 353
  14. theorem OAI.SecondPassArithmetic.globalDescentWeight_nonneg line 360
  15. theorem OAI.SecondPassArithmetic.globalPositiveBin_transfer line 376
  16. theorem OAI.SecondPassArithmetic.globalBinTriples_label_bound line 446
  17. theorem OAI.SecondPassArithmetic.globalDescentWeight_mass line 460
  18. def OAI.CubicEisenstein.matrixGram line 543
  19. lemma OAI.CubicEisenstein.matrixGram_right_unitary line 546
  20. def OAI.CubicEisenstein.hyperbolicGram line 558
  21. lemma OAI.CubicEisenstein.hyperbolicGram_continuous line 566
  22. lemma OAI.CubicEisenstein.hyperbolicGram_injective line 570
  23. instance OAI.CubicEisenstein.hyperbolicT2Space line 597
  24. def OAI.CubicEisenstein.complexMatrixRow line 600
  25. lemma OAI.CubicEisenstein.complexMatrixRow_mul line 602
  26. def OAI.CubicEisenstein.matrixFrobenius line 608
  27. lemma OAI.CubicEisenstein.matrixFrobenius_right_unitary line 611
  28. def OAI.CubicEisenstein.hyperbolicFrobenius line 615
  29. lemma OAI.CubicEisenstein.matrixFrobenius_continuous line 623
  30. lemma OAI.CubicEisenstein.hyperbolicFrobenius_continuous line 630