OAI/NumberTheory/DirichletL/Moments/Forcing.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentForcing.movingIdeal line 14
  2. def OAI.SevenEighths.CenteredMomentForcing.forcingSet line 17
  3. def OAI.SevenEighths.CenteredMomentForcing.forcingIdeal line 20
  4. theorem OAI.SevenEighths.CenteredMomentForcing.valuation_product line 24
  5. theorem OAI.SevenEighths.CenteredMomentForcing.valuation_prime line 35
  6. theorem OAI.SevenEighths.CenteredMomentForcing.valuation_prime_product line 44
  7. theorem OAI.SevenEighths.CenteredMomentForcing.valuation_prime_power_product line 51
  8. theorem OAI.SevenEighths.CenteredMomentForcing.movingIdeal_ne_zero line 59
  9. theorem OAI.SevenEighths.CenteredMomentForcing.movingIdeal_valuation line 65
  10. theorem OAI.SevenEighths.CenteredMomentForcing.forcing_valuation_two line 73
  11. theorem OAI.SevenEighths.CenteredMomentForcing.forcingIdeal_squarefree line 81
  12. theorem OAI.SevenEighths.CenteredMomentForcing.forcing_prime_mem line 93
  13. theorem OAI.SevenEighths.CenteredMomentForcing.forcing_norm_scale line 108
  14. def OAI.SevenEighths.CenteredMomentForcing.movingElement line 117
  15. theorem OAI.SevenEighths.CenteredMomentForcing.movingElement_span line 121
  16. theorem OAI.SevenEighths.CenteredMomentForcing.actual_forcing_exceptional_count line 126