OAI/NumberTheory/DirichletL/Detector/GramJointConstruction.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ProbeGramJointConstruction.q1 line 14
  2. def OAI.ProbeGramJointConstruction.q2 line 15
  3. lemma OAI.ProbeGramJointConstruction.q1_smooth line 17
  4. lemma OAI.ProbeGramJointConstruction.q2_smooth line 19
  5. lemma OAI.ProbeGramJointConstruction.norm_sq_eq line 22
  6. def OAI.ProbeGramJointConstruction.log1 line 25
  7. def OAI.ProbeGramJointConstruction.log2 line 27
  8. def OAI.ProbeGramJointConstruction.phase line 29
  9. def OAI.ProbeGramJointConstruction.rootScale line 31
  10. def OAI.ProbeGramJointConstruction.amplitude line 33
  11. lemma OAI.ProbeGramJointConstruction.patchedLog_smooth line 36
  12. lemma OAI.ProbeGramJointConstruction.log1_smooth line 39
  13. lemma OAI.ProbeGramJointConstruction.log2_smooth line 41
  14. lemma OAI.ProbeGramJointConstruction.phase_smooth line 43
  15. lemma OAI.ProbeGramJointConstruction.rootScale_smooth line 45
  16. lemma OAI.ProbeGramJointConstruction.rootScale_pos line 47
  17. lemma OAI.ProbeGramJointConstruction.amplitude_smooth line 49
  18. def OAI.ProbeGramJointConstruction.rawProfile line 59
  19. def OAI.ProbeGramJointConstruction.patchedProfile line 64
  20. lemma OAI.ProbeGramJointConstruction.patchedProfile_smooth line 69
  21. lemma OAI.ProbeGramJointConstruction.rawProfile_zero_left line 81
  22. lemma OAI.ProbeGramJointConstruction.rawProfile_zero_right line 83
  23. lemma OAI.ProbeGramJointConstruction.patchedProfile_zero_left line 85
  24. lemma OAI.ProbeGramJointConstruction.patchedProfile_zero_right line 88
  25. def OAI.ProbeGramJointConstruction.sourceCompact line 92
  26. lemma OAI.ProbeGramJointConstruction.sourceCompact_isCompact line 93
  27. lemma OAI.ProbeGramJointConstruction.support_amplitude line 96
  28. lemma OAI.ProbeGramJointConstruction.annulus_subset_sourceCompact line 104
  29. lemma OAI.ProbeGramJointConstruction.tsupport_amplitude_subset line 113
  30. lemma OAI.ProbeGramJointConstruction.amplitude_hasCompactSupport line 119
  31. lemma OAI.ProbeGramJointConstruction.patchedProfile_hasCompactSupport line 124
  32. lemma OAI.ProbeGramJointConstruction.norm_power_pair line 129
  33. lemma OAI.ProbeGramJointConstruction.sqrt_reciprocal_product line 146
  34. theorem OAI.ProbeGramJointConstruction.rawProfile_eq_patchedProfile line 160
  35. def OAI.ProbeGramJointConstruction.amplitudeSchwartz line 187
  36. lemma OAI.ProbeGramJointConstruction.amplitudeSchwartz_apply line 191
  37. lemma OAI.ProbeGramJointConstruction.rawProfile_smooth line 195
  38. lemma OAI.ProbeGramJointConstruction.support_rawProfile line 203
  39. lemma OAI.ProbeGramJointConstruction.rawProfile_hasCompactSupport line 211
  40. def OAI.ProbeGramJointConstruction.jointProfile line 217
  41. theorem OAI.ProbeGramJointConstruction.jointProfile_apply line 223
  42. theorem OAI.ProbeGramJointConstruction.jointProfile_factorization line 228
  43. theorem OAI.ProbeGramJointConstruction.jointProfile_annularSupport line 237
  44. lemma OAI.ProbeGramJointConstruction.jointProfile_zero_scale line 244
  45. lemma OAI.ProbeGramJointConstruction.jointProfile_zero_of_left_small line 252
  46. lemma OAI.ProbeGramJointConstruction.jointProfile_zero_of_right_small line 261