OAI/NumberTheory/DirichletL/Moments/ZeroMeanBridge.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentZeroMeanBridge.quotientMean line 18
  2. lemma OAI.SevenEighths.CenteredMomentZeroMeanBridge.normValue_ne_zero line 21
  3. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.quotientMean_pullback line 26
  4. def OAI.SevenEighths.CenteredMomentZeroMeanBridge.dilationMask line 43
  5. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.dilationMask_mk line 47
  6. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.dilationMask_sum line 53
  7. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.quotientMean_dilation line 75
  8. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.quotientMean_finite_sum line 84
  9. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.row_mask_expansion line 111
  10. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.quotientMean_mask_expansion line 128
  11. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.tripleResidue_mul line 155
  12. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.original_pair_reduced_mask line 165
  13. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.original_pair_mean line 192
  14. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.canonicalZeroTerm_eq_mean line 229
  15. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.canonicalZeroPair_eq_original line 246
  16. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.quotientMean_congr line 264
  17. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.scaled_pairFourier_eq_mean line 272
  18. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.canonicalZeroPair_eq_generators line 280
  19. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.canonical_ideal_zero_sum line 295
  20. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.zeroEnergy_eq_original line 312
  21. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.productColumnCoefficient_mul_whole line 323
  22. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.zeroEnergy_product_eq line 332
  23. theorem OAI.SevenEighths.CenteredMomentZeroMeanBridge.normalized_zeroEnergy_product_bound line 353