OAI/NumberTheory/DirichletL/CubicSieve/ResidualSectors.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.second_common_support_reconstruct line 79
  2. def OAI.SecondPassArithmetic.secondSourcePairKernel line 104
  3. theorem OAI.SecondPassArithmetic.secondFrequencyKernel_eq_kernelPair line 111
  4. theorem OAI.SecondPassArithmetic.secondFrequencyKernel_eq_child_sectors line 130
  5. def OAI.SecondPassArithmetic.secondSourceCommonCoefficient line 144
  6. def OAI.SecondPassArithmetic.truncatedSecondSource line 149
  7. def OAI.SecondPassArithmetic.secondSourceTail line 158
  8. theorem OAI.SecondPassArithmetic.inputConjugateRow_eq_truncated_add_tail line 168
  9. theorem OAI.SecondPassArithmetic.truncatedSecondSource_eq_child_sectors line 199
  10. structure OAI.SecondPassArithmetic.SecondExpansionData line 240
  11. def OAI.SecondPassArithmetic.InSecondQuotientSector line 251
  12. def OAI.SecondPassArithmetic.expansionSupportData line 255
  13. theorem OAI.SecondPassArithmetic.expansionSupportData_injOn line 262
  14. theorem OAI.SecondPassArithmetic.primeProductNorm_quotient_sector line 286
  15. theorem OAI.SecondPassArithmetic.residual_scale_quotient_sector line 297
  16. theorem OAI.SecondPassArithmetic.rowCoprimeMask_eq_of_span_eq line 306
  17. theorem OAI.SecondPassArithmetic.rowCoprimeMask_mul_eq_of_span_eq line 313
  18. def OAI.SecondPassIntegration.residualColumnScale line 326
  19. theorem OAI.SecondPassIntegration.residualColumnScale_pos line 329
  20. theorem OAI.SecondPassIntegration.secondSectorZ_residualColumnScale line 333
  21. theorem OAI.SecondPassIntegration.second_divisor_residual_normalization line 345
  22. def OAI.SecondPassArithmetic.actualSecondRawVariableSector line 370
  23. theorem OAI.SecondPassArithmetic.actualSecondRawVariableSector_fixed_profiles line 385
  24. theorem OAI.SecondPassArithmetic.outerWindow_global_bound line 437
  25. theorem OAI.SecondPassArithmetic.actual_raw_variable_sector_transfer line 457
  26. theorem OAI.SecondPassArithmetic.secondSourcePairKernel_normalized_shift line 523
  27. abbrev OAI.UnrestrictedIdealReindex.O line 548
  28. abbrev OAI.UnrestrictedIdealReindex.NonzeroIdeal line 552
  29. abbrev OAI.UnrestrictedIdealReindex.NonzeroElement line 553
  30. theorem OAI.UnrestrictedIdealReindex.span_unit_generator line 555
  31. def OAI.UnrestrictedIdealReindex.unitIdealToElement line 559
  32. theorem OAI.UnrestrictedIdealReindex.unitIdealToElement_bijective line 562
  33. def OAI.UnrestrictedIdealReindex.unitIdealEquiv line 583
  34. theorem OAI.UnrestrictedIdealReindex.tsum_nonzero_unit_invariant line 586
  35. theorem OAI.UnrestrictedIdealReindex.tsum_unit_invariant_of_zero line 602