OAI/NumberTheory/DirichletL/Inversion/InitialOverlap.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.InverseInitialOverlap.O line 13
  2. def OAI.SevenEighths.InverseInitialOverlap.residual line 15
  3. def OAI.SevenEighths.InverseInitialOverlap.column line 17
  4. def OAI.SevenEighths.InverseInitialOverlap.reconstruct line 19
  5. def OAI.SevenEighths.InverseInitialOverlap.original line 21
  6. def OAI.SevenEighths.InverseInitialOverlap.columns line 24
  7. theorem OAI.SevenEighths.InverseInitialOverlap.mem_original line 27
  8. theorem OAI.SevenEighths.InverseInitialOverlap.residual_mul line 31
  9. theorem OAI.SevenEighths.InverseInitialOverlap.residual_squarefree line 34
  10. theorem OAI.SevenEighths.InverseInitialOverlap.quotient_mul_cancel line 38
  11. theorem OAI.SevenEighths.InverseInitialOverlap.column_properties line 42
  12. theorem OAI.SevenEighths.InverseInitialOverlap.reconstruct_column line 59
  13. theorem OAI.SevenEighths.InverseInitialOverlap.reconstruct_properties line 66
  14. theorem OAI.SevenEighths.InverseInitialOverlap.column_reconstruct line 82
  15. theorem OAI.SevenEighths.InverseInitialOverlap.mem_columns line 88
  16. theorem OAI.SevenEighths.InverseInitialOverlap.column_injOn line 103
  17. def OAI.SevenEighths.InverseInitialOverlap.overlapEquiv line 111
  18. theorem OAI.SevenEighths.InverseInitialOverlap.reconstruct_mul_residual line 121
  19. theorem OAI.SevenEighths.InverseInitialOverlap.norm_reconstruct line 126
  20. theorem OAI.SevenEighths.InverseInitialOverlap.cutoff_argument line 131
  21. theorem OAI.SevenEighths.InverseInitialOverlap.columns_filter line 145
  22. theorem OAI.SevenEighths.InverseInitialOverlap.sum_reconstruct line 153
  23. theorem OAI.SevenEighths.InverseInitialOverlap.coefficient_identity line 162
  24. theorem OAI.SevenEighths.InverseInitialOverlap.polynomial_fixed_overlap line 181
  25. theorem OAI.SevenEighths.InverseInitialOverlap.sum_original_partition line 199
  26. theorem OAI.SevenEighths.InverseInitialOverlap.polynomial_all_overlaps line 209
  27. theorem OAI.SevenEighths.InverseInitialOverlap.scaled_cutoff_argument line 224
  28. theorem OAI.SevenEighths.InverseInitialOverlap.normalization_split line 245
  29. theorem OAI.SevenEighths.InverseInitialOverlap.normalized_polynomial_fixed_overlap line 251
  30. theorem OAI.SevenEighths.InverseInitialOverlap.normalized_polynomial_all_overlaps line 279
  31. theorem OAI.SevenEighths.InverseInitialOverlap.sum_moebius_filter line 298
  32. theorem OAI.SevenEighths.InverseInitialOverlap.original_normalized_polynomial line 307
  33. theorem OAI.SevenEighths.InverseInitialOverlap.overlap_coefficient_norm_le line 326