OAI/NumberTheory/DirichletL/Moments/FirstMaskedFamily.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.fixed_mask_ne_zero line 26
  2. def OAI.SevenEighths.CenteredMomentFirstMaskedFamily.idealMask line 29
  3. def OAI.SevenEighths.CenteredMomentFirstMaskedFamily.maskedSource line 31
  4. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.idealMask_span line 33
  5. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.idealMask_primary line 37
  6. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.row_mask_factor line 41
  7. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.rowWeight_mask_factor line 51
  8. theorem OAI.SevenEighths.CenteredMomentFirstMaskedFamily.exists_first_masked_character line 70
  9. theorem OAI.SevenEighths.CenteredMomentFirstMaskedFamily.exists_canonical_masked_pair line 89
  10. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.divisor_column_masked line 120
  11. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.sourceGaussEnergy_congr line 133
  12. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.first_source_energy line 141
  13. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.maskedSource_eq_of_live line 154
  14. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.extracted_masked_coefficient line 161
  15. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.idealMask_generator line 169
  16. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.maskedSource_punctured line 173
  17. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.first_gauss_row line 179
  18. theorem OAI.SevenEighths.CenteredMomentFirstMaskedFamily.exists_canonical_source_pair line 196
  19. def OAI.SevenEighths.CenteredMomentFirstMaskedFamily.rayHeight line 232
  20. def OAI.SevenEighths.CenteredMomentFirstMaskedFamily.extractedSource line 235
  21. theorem OAI.SevenEighths.CenteredMomentFirstMaskedFamily.exists_masked_radical_family line 239
  22. theorem OAI.SevenEighths.CenteredMomentFirstMaskedFamily.exists_masked_error_source line 266
  23. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.idealMask_mul line 291
  24. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.extractedSource_whole_mask line 296
  25. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.extracted_gauss_row line 303
  26. theorem OAI.SevenEighths.CenteredMomentFirstMaskedFamily.exists_masked_error_rows line 326
  27. lemma OAI.SevenEighths.CenteredMomentFirstMaskedFamily.paired_gauss_rows line 353