OAI/NumberTheory/DirichletL/Moments/SourceRectangle.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentSourceRectangle.tuplePools line 19
  2. def OAI.SevenEighths.CenteredMomentSourceRectangle.tuplePool line 22
  3. def OAI.SevenEighths.CenteredMomentSourceRectangle.pack line 25
  4. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.pack_slot line 29
  5. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.pack_left line 32
  6. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.pack_right line 35
  7. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.pack_product line 38
  8. def OAI.SevenEighths.CenteredMomentSourceRectangle.tuplePoolEquiv line 43
  9. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.sum_tuplePool line 62
  10. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.finite_column_regroup line 72
  11. def OAI.SevenEighths.CenteredMomentSourceRectangle.PlainCoverage line 86
  12. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.rectangle_zero_left line 89
  13. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.rectangle_zero_right line 99
  14. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.finite_plain_rectangle line 109
  15. def OAI.SevenEighths.CenteredMomentSourceRectangle.fullMaskedRectangle line 128
  16. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.source_polynomial_eq_full_masked_rectangle line 138
  17. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.fullMaskedRectangle_pullback line 161
  18. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.pullback_same_product line 171
  19. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.fullMaskedRectangle_modulus_one line 177
  20. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.source_polynomial_eq_maskedRectangle line 192
  21. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.plainCoverage_residualPool line 209
  22. def OAI.SevenEighths.CenteredMomentSourceRectangle.plainSupportPool line 217
  23. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.plainSupportPool_coverage line 219
  24. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.extracted_plainSupportPool_coverage line 237
  25. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.supported_source_polynomial_eq_full_rectangle line 244
  26. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.liveBox_eq_tuplePool line 264
  27. theorem OAI.SevenEighths.CenteredMomentSourceRectangle.live_source_polynomial_eq_full_rectangle line 281