OAI/NumberTheory/DirichletL/GaussSum/PowerfulParts.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompletedGauss.rowPowerfulPart line 80
  2. def OAI.CompletedGauss.rowSimplePart line 83
  3. theorem OAI.CompletedGauss.rowPowerfulPart_ne_zero line 86
  4. theorem OAI.CompletedGauss.rowSimplePart_ne_zero line 89
  5. theorem OAI.CompletedGauss.normalizedFactors_rowPowerfulPart line 92
  6. theorem OAI.CompletedGauss.normalizedFactors_rowSimplePart line 97
  7. theorem OAI.CompletedGauss.rowPowerfulPart_powerful line 102
  8. theorem OAI.CompletedGauss.rowSimplePart_squarefree line 110
  9. theorem OAI.CompletedGauss.row_powerful_simple_product line 118
  10. theorem OAI.CompletedGauss.row_powerful_simple_coprime line 123
  11. theorem OAI.CompletedGauss.rowSimplePart_norm line 134
  12. def OAI.CompletedGauss.squarefreeMaskPart line 147
  13. def OAI.CompletedGauss.squarefreeResidualPart line 150
  14. theorem OAI.CompletedGauss.squarefreeMaskPart_ne_zero line 153
  15. theorem OAI.CompletedGauss.squarefreeResidualPart_ne_zero line 156
  16. theorem OAI.CompletedGauss.normalizedFactors_squarefreeMaskPart line 159
  17. theorem OAI.CompletedGauss.normalizedFactors_squarefreeResidualPart line 163
  18. theorem OAI.CompletedGauss.squarefreeMaskPart_squarefree line 167
  19. theorem OAI.CompletedGauss.squarefreeResidualPart_squarefree line 172
  20. theorem OAI.CompletedGauss.squarefree_mask_residual_product line 177
  21. theorem OAI.CompletedGauss.squarefreeResidualPart_coprime line 182
  22. theorem OAI.CompletedGauss.squarefreeMaskPart_dvd line 190
  23. def OAI.CompletedGauss.rowMaskPart line 208
  24. def OAI.CompletedGauss.rowResidualPart line 209
  25. theorem OAI.CompletedGauss.row_powerful_mask_residual_product line 211
  26. theorem OAI.CompletedGauss.rowMaskPart_dvd line 216
  27. theorem OAI.CompletedGauss.rowResidualPart_squarefree line 219
  28. theorem OAI.CompletedGauss.rowResidualPart_admissible line 222
  29. theorem OAI.CompletedGauss.rowResidualPart_prime_exponent line 227
  30. theorem OAI.CompletedGauss.rowResidualPart_norm line 236
  31. def OAI.SecondPassArithmetic.firstCoreUniformWeight line 260
  32. def OAI.SecondPassArithmetic.GlobalCubeAdmissible line 267
  33. theorem OAI.SecondPassArithmetic.globalFirstFamilyWeight_bounds line 270
  34. theorem OAI.SecondPassArithmetic.globalFirstPooledRow_block line 293
  35. theorem OAI.SecondPassArithmetic.firstCoreUniformWeight_mass line 301
  36. def OAI.SecondPassArithmetic.globalFirstFamilyBudget line 314
  37. theorem OAI.SecondPassArithmetic.globalCubeInputFamilyEnergy_transfer line 331
  38. theorem OAI.SecondPassArithmetic.globalCubeColumnScale_pos line 398
  39. theorem OAI.SecondPassArithmetic.globalCubeCoefficient_side line 403
  40. theorem OAI.SecondPassArithmetic.globalFirstPooledRow_side line 409
  41. theorem OAI.SecondPassArithmetic.globalCube_first_scalar_bound line 415
  42. def OAI.SecondPassArithmetic.globalCubeFirstBlock line 429
  43. theorem OAI.SecondPassArithmetic.globalCubeFirstBlock_input_transfer line 446
  44. theorem OAI.SecondPassArithmetic.globalTwoPassage_transfer line 571