OAI/NumberTheory/DirichletL/Inversion/KernelSourceUniform.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseKernelSourceUniform.smallScalar line 11
  2. lemma OAI.SevenEighths.InverseKernelSourceUniform.smallScalar_pos line 13
  3. def OAI.SevenEighths.InverseKernelSourceUniform.canonicalDensity line 16
  4. theorem OAI.SevenEighths.InverseKernelSourceUniform.paperKernel_window_source_bound line 20
  5. theorem OAI.SevenEighths.InverseKernelSourceUniform.localized_source_seminorm line 72
  6. theorem OAI.SevenEighths.InverseKernelSourceUniform.source_uniform_separation line 127
  7. def OAI.SevenEighths.InverseKernelSourceUniform.twistedDensity line 256
  8. theorem OAI.SevenEighths.InverseKernelSourceUniform.normTwistedSource_uniform_separation line 261
  9. theorem OAI.SevenEighths.InverseKernelSourceUniform.fourier_joint_stronglyMeasurable line 312
  10. theorem OAI.SevenEighths.InverseKernelSourceUniform.paperKernel_joint_stronglyMeasurable line 324
  11. theorem OAI.SevenEighths.InverseKernelSourceUniform.twistedDensity_measurable_of_profile line 347
  12. theorem OAI.SevenEighths.InverseKernelSourceUniform.exists_measurable_twisted_source line 358
  13. theorem OAI.SevenEighths.InverseKernelSourceUniform.twistedDensity_joint_stronglyMeasurable line 390