OAI/NumberTheory/DirichletL/Moments/FirstNestedSeededGaussianPower.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.CenteredMomentFirstNestedSeededGaussianPower.NestedIndex line 62
  2. def OAI.SevenEighths.CenteredMomentFirstNestedSeededGaussianPower.emptyIndex line 64
  3. theorem OAI.SevenEighths.CenteredMomentFirstNestedSeededGaussianPower.nested_source_descent line 66
  4. theorem OAI.SevenEighths.CenteredMomentFirstNestedSeededGaussianPower.nested_power_descent line 195
  5. theorem OAI.SevenEighths.CenteredMomentFirstNestedSeededGaussianPower.nested_seeded_power_descent line 293
  6. theorem OAI.SevenEighths.CenteredMomentFirstNestedSeededGaussianPower.nested_reference_seeded_power_descent line 406
  7. theorem OAI.SevenEighths.CenteredMomentFirstNestedSeededGaussianPower.actual_nested_subsets_seeded_gaussian_power line 507