OAI/NumberTheory/DirichletL/Dictionary/InverseClippedUniform.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.source_support line 18
  2. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.source_zero_of_ratio line 48
  3. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.exists_reference_window line 52
  4. def OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.referenceWindow line 62
  5. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.referenceWindow_compact line 64
  6. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.referenceWindow_support line 67
  7. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.referenceWindow_one line 71
  8. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.referenceWindow_agrees line 75
  9. def OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.logSource line 86
  10. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.logSource_apply line 90
  11. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.logSource_eq_logSchwartz line 96
  12. def OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.familyDensity line 104
  13. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.familyDensity_formula line 107
  14. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.familyDensity_norm line 111
  15. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.familyDensity_integrable line 115
  16. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.familyDensity_moment line 121
  17. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.canonical_family_mode_integrable line 177
  18. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.canonical_clipped_family_fourier line 188
  19. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.canonical_clipped_family_energy line 208
  20. theorem OAI.SevenEighths.DetectorDictionaryInverseClippedUniform.initial_raw_family_energy line 244