OAI/NumberTheory/DirichletL/Inversion/ClippingProfiles.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseClippingProfiles.logWindow line 15
  2. def OAI.SevenEighths.InverseClippingProfiles.rootedWindow line 17
  3. lemma OAI.SevenEighths.InverseClippingProfiles.logWindow_contDiff line 20
  4. lemma OAI.SevenEighths.InverseClippingProfiles.rootedWindow_contDiff line 24
  5. lemma OAI.SevenEighths.InverseClippingProfiles.logWindow_iteratedDeriv line 30
  6. lemma OAI.SevenEighths.InverseClippingProfiles.expAffine_iteratedDeriv line 42
  7. lemma OAI.SevenEighths.InverseClippingProfiles.logWindow_support line 57
  8. lemma OAI.SevenEighths.InverseClippingProfiles.rootedWindow_compact line 69
  9. def OAI.SevenEighths.InverseClippingProfiles.rootSchwartz line 78
  10. lemma OAI.SevenEighths.InverseClippingProfiles.rootSchwartz_apply line 84
  11. lemma OAI.SevenEighths.InverseClippingProfiles.derivative_support line 89
  12. lemma OAI.SevenEighths.InverseClippingProfiles.root_exp_le_one line 96
  13. lemma OAI.SevenEighths.InverseClippingProfiles.expAffine_iteratedFDeriv_norm line 115
  14. theorem OAI.SevenEighths.InverseClippingProfiles.rootSchwartz_seminorm line 122
  15. def OAI.SevenEighths.InverseClippingProfiles.rootDerivativeBound line 208
  16. def OAI.SevenEighths.InverseClippingProfiles.twistedDerivativeBound line 211
  17. lemma OAI.SevenEighths.InverseClippingProfiles.rootDerivativeBound_nonneg line 214
  18. lemma OAI.SevenEighths.InverseClippingProfiles.twistedDerivativeBound_nonneg line 220
  19. lemma OAI.SevenEighths.InverseClippingProfiles.rootSchwartz_derivativeSum line 224
  20. theorem OAI.SevenEighths.InverseClippingProfiles.rooted_twist_seminorm line 237
  21. def OAI.SevenEighths.InverseClippingProfiles.momentOrder line 255
  22. def OAI.SevenEighths.InverseClippingProfiles.windowSourceBound line 257
  23. lemma OAI.SevenEighths.InverseClippingProfiles.windowSourceBound_nonneg line 261
  24. theorem OAI.SevenEighths.InverseClippingProfiles.rooted_twist_moment_sources line 266
  25. lemma OAI.SevenEighths.InverseClippingProfiles.coefficientMomentBound_mul line 298
  26. theorem OAI.SevenEighths.InverseClippingProfiles.rooted_twist_fourier_moment line 303
  27. theorem OAI.SevenEighths.InverseClippingProfiles.child_log_window_parameters line 324
  28. theorem OAI.SevenEighths.InverseClippingProfiles.clipping_ratio_of_column_witness line 333
  29. theorem OAI.SevenEighths.InverseClippingProfiles.clipped_positive_support line 351
  30. theorem OAI.SevenEighths.InverseClippingProfiles.clipped_log_source line 365
  31. def OAI.SevenEighths.InverseClippingProfiles.firstRootExponent line 374
  32. def OAI.SevenEighths.InverseClippingProfiles.secondRootExponent line 377
  33. theorem OAI.SevenEighths.InverseClippingProfiles.first_root_coupled_identity line 380
  34. theorem OAI.SevenEighths.InverseClippingProfiles.second_root_coupled_identity line 386
  35. theorem OAI.SevenEighths.InverseClippingProfiles.first_root_budget line 392
  36. theorem OAI.SevenEighths.InverseClippingProfiles.second_root_budget line 408
  37. def OAI.SevenEighths.InverseClippingProfiles.firstRootSlope line 420
  38. def OAI.SevenEighths.InverseClippingProfiles.secondRootSlope line 421
  39. lemma OAI.SevenEighths.InverseClippingProfiles.inverseNormWindow_exp line 423
  40. lemma OAI.SevenEighths.InverseClippingProfiles.inverseRootWindow_exp line 428
  41. theorem OAI.SevenEighths.InverseClippingProfiles.firstRootWindows_exp line 433
  42. theorem OAI.SevenEighths.InverseClippingProfiles.secondRootWindows_exp line 439
  43. theorem OAI.SevenEighths.InverseClippingProfiles.firstRootWindows_prod line 445
  44. theorem OAI.SevenEighths.InverseClippingProfiles.secondRootWindows_prod line 456
  45. theorem OAI.SevenEighths.InverseClippingProfiles.first_profile_normalized_identity line 467
  46. theorem OAI.SevenEighths.InverseClippingProfiles.second_profile_normalized_identity line 480
  47. theorem OAI.SevenEighths.InverseClippingProfiles.fourier_phase_shift line 493
  48. theorem OAI.SevenEighths.InverseClippingProfiles.fourier_translate line 504
  49. theorem OAI.SevenEighths.InverseClippingProfiles.fourier_translated_twist line 519
  50. theorem OAI.SevenEighths.InverseClippingProfiles.norm_fourier_translated_twist line 524
  51. theorem OAI.SevenEighths.InverseClippingProfiles.rooted_family_fourier_joint_measurable line 528
  52. def OAI.SevenEighths.InverseClippingProfiles.childWindowDensity line 544
  53. def OAI.SevenEighths.InverseClippingProfiles.windowMomentConstant line 547
  54. theorem OAI.SevenEighths.InverseClippingProfiles.childWindowDensity_moment line 551
  55. theorem OAI.SevenEighths.InverseClippingProfiles.retained_clipped_column line 575
  56. theorem OAI.SevenEighths.InverseClippingProfiles.translated_twist_moment_uniform line 596
  57. theorem OAI.SevenEighths.InverseClippingProfiles.eventually_log_scale_pow_le line 615
  58. def OAI.SevenEighths.InverseClippingProfiles.firstBalancedSlope line 628
  59. def OAI.SevenEighths.InverseClippingProfiles.secondBalancedSlope line 629
  60. theorem OAI.SevenEighths.InverseClippingProfiles.first_root_normalization_split line 631
  61. theorem OAI.SevenEighths.InverseClippingProfiles.second_root_normalization_split line 642