OAI/NumberTheory/DirichletL/Moments/ProductCRT.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentProductCRT.productCRT line 12
  2. theorem OAI.SevenEighths.CenteredMomentProductCRT.productCRT_mk line 19
  3. def OAI.SevenEighths.CenteredMomentProductCRT.jointCRT line 26
  4. theorem OAI.SevenEighths.CenteredMomentProductCRT.jointCRT_mk line 34
  5. def OAI.SevenEighths.CenteredMomentProductCRT.cofactor line 40
  6. theorem OAI.SevenEighths.CenteredMomentProductCRT.factor_mul_cofactor line 42
  7. theorem OAI.SevenEighths.CenteredMomentProductCRT.left_crt_component line 45
  8. theorem OAI.SevenEighths.CenteredMomentProductCRT.right_crt_component line 59
  9. theorem OAI.SevenEighths.CenteredMomentProductCRT.fullModulusCorrelation_product line 73
  10. theorem OAI.SevenEighths.CenteredMomentProductCRT.cross_cofactor_coprime line 101
  11. theorem OAI.SevenEighths.CenteredMomentProductCRT.local_cofactor_norm line 111
  12. theorem OAI.SevenEighths.CenteredMomentProductCRT.fullModulusCorrelation_product_norm line 133
  13. theorem OAI.SevenEighths.CenteredMomentProductCRT.supported_character_product line 154
  14. theorem OAI.SevenEighths.CenteredMomentProductCRT.actualCorrelation_product_norm line 166