OAI/NumberTheory/DirichletL/Detector/GramJointProfile.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ProbeGramJointProfile.rayControl line 15
  2. lemma OAI.ProbeGramJointProfile.rayControl_nonneg line 18
  3. lemma OAI.ProbeGramJointProfile.mul_derivative_bound line 21
  4. lemma OAI.ProbeGramJointProfile.compact_derivatives line 41
  5. lemma OAI.ProbeGramJointProfile.compact_positive_margin line 59
  6. lemma OAI.ProbeGramJointProfile.scaled_argument_derivative line 68
  7. lemma OAI.ProbeGramJointProfile.normalized_phase_derivative line 93
  8. lemma OAI.ProbeGramJointProfile.phase_derivative_bound line 100
  9. lemma OAI.ProbeGramJointProfile.kernel_derivative_bound line 126
  10. def OAI.ProbeGramJointProfile.amplitudeControl line 175
  11. lemma OAI.ProbeGramJointProfile.amplitudeControl_nonneg line 178
  12. lemma OAI.ProbeGramJointProfile.amplitude_derivative_bound line 181
  13. theorem OAI.ProbeGramJointProfile.compact_profile_seminorm line 191
  14. lemma OAI.ProbeGramJointProfile.amplitudeControl_mono line 269
  15. lemma OAI.ProbeGramJointProfile.rayControl_mono line 275
  16. def OAI.ProbeGramJointProfile.heightOrder line 281
  17. theorem OAI.ProbeGramJointProfile.compact_profile_finite line 283
  18. lemma OAI.ProbeGramJointProfile.sqrt_decay_absorption line 323
  19. theorem OAI.ProbeGramJointProfile.compact_fourier_profile_finite line 331
  20. theorem OAI.ProbeGramJointProfile.jointProfile_homogeneous line 370
  21. theorem OAI.ProbeGramJointProfile.jointProfile_uniform_degree line 389