OAI/NumberTheory/DirichletL/Moments/SecondCanonicalFrequency.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentSecondCanonicalFrequency.commonFrequencyGenerator_ne_zero line 15
  2. theorem OAI.SevenEighths.CenteredMomentSecondCanonicalFrequency.commonFrequencyGenerator_dvd line 21
  3. theorem OAI.SevenEighths.CenteredMomentSecondCanonicalFrequency.idealCorrelation_zero_outside_common line 30
  4. theorem OAI.SevenEighths.CenteredMomentSecondCanonicalFrequency.idealCorrelation_tsum_common line 41
  5. def OAI.SevenEighths.CenteredMomentSecondCanonicalFrequency.canonicalPartition line 55
  6. def OAI.SevenEighths.CenteredMomentSecondCanonicalFrequency.canonicalPartitionScalar line 58
  7. theorem OAI.SevenEighths.CenteredMomentSecondCanonicalFrequency.actual_ideal_partition_scalar line 62