OAI/NumberTheory/DirichletL/Inversion/InitialProfile.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseInitialProfile.clippedTwist line 14
  2. theorem OAI.SevenEighths.InverseInitialProfile.clippedTwist_apply line 17
  3. def OAI.SevenEighths.InverseInitialProfile.sourceDensity line 21
  4. theorem OAI.SevenEighths.InverseInitialProfile.fourier_clippedTwist line 24
  5. theorem OAI.SevenEighths.InverseInitialProfile.sourceDensity_joint_measurable line 32
  6. theorem OAI.SevenEighths.InverseInitialProfile.sourceDensity_norm line 40
  7. theorem OAI.SevenEighths.InverseInitialProfile.sourceDensity_moment_uniform line 44
  8. def OAI.SevenEighths.InverseInitialProfile.clippedSource line 55
  9. theorem OAI.SevenEighths.InverseInitialProfile.clipped_log_source line 58
  10. def OAI.SevenEighths.InverseInitialProfile.rootExponent line 67
  11. theorem OAI.SevenEighths.InverseInitialProfile.root_coupled_identity line 69
  12. theorem OAI.SevenEighths.InverseInitialProfile.root_budget line 74
  13. def OAI.SevenEighths.InverseInitialProfile.normalizedProfile line 85
  14. theorem OAI.SevenEighths.InverseInitialProfile.normalizedProfile_exact line 89
  15. def OAI.SevenEighths.InverseInitialProfile.familyDensity line 112
  16. theorem OAI.SevenEighths.InverseInitialProfile.familyDensity_formula line 117
  17. theorem OAI.SevenEighths.InverseInitialProfile.familyDensity_weighted_integrable line 126
  18. theorem OAI.SevenEighths.InverseInitialProfile.familyDensity_weighted_integral line 140
  19. def OAI.SevenEighths.InverseInitialProfile.logFamilyProfile line 167
  20. theorem OAI.SevenEighths.InverseInitialProfile.family_common_measure line 175
  21. theorem OAI.SevenEighths.InverseInitialProfile.sourceDensity_moment_seminorm line 254
  22. theorem OAI.SevenEighths.InverseInitialProfile.clippedSource_conjugate line 275
  23. theorem OAI.SevenEighths.InverseInitialProfile.familyDensity_joint_measurable line 280
  24. theorem OAI.SevenEighths.InverseInitialProfile.fresh_cutoff_one line 295
  25. def OAI.SevenEighths.InverseInitialProfile.columnCenter line 324
  26. def OAI.SevenEighths.InverseInitialProfile.prefactorCenter line 325
  27. def OAI.SevenEighths.InverseInitialProfile.radialCenter line 326
  28. theorem OAI.SevenEighths.InverseInitialProfile.original_column_scale line 328
  29. theorem OAI.SevenEighths.InverseInitialProfile.initial_prefactor_scale line 335
  30. theorem OAI.SevenEighths.InverseInitialProfile.initial_radial_scale line 344
  31. theorem OAI.SevenEighths.InverseInitialProfile.initial_normalization_scalar line 354
  32. def OAI.SevenEighths.InverseInitialProfile.physicalKernel line 364
  33. theorem OAI.SevenEighths.InverseInitialProfile.physicalKernel_eq_secondNorm line 370
  34. theorem OAI.SevenEighths.InverseInitialProfile.physicalKernel_nominal line 381
  35. theorem OAI.SevenEighths.InverseInitialProfile.normalizedProfile_eq_family line 401
  36. theorem OAI.SevenEighths.InverseInitialProfile.fresh_profile_restore line 415
  37. def OAI.SevenEighths.InverseInitialProfile.relativeNorm line 431
  38. def OAI.SevenEighths.InverseInitialProfile.relativeLog line 434
  39. theorem OAI.SevenEighths.InverseInitialProfile.relativeNorm_pos line 437
  40. theorem OAI.SevenEighths.InverseInitialProfile.initial_kernel_restore line 445
  41. def OAI.SevenEighths.InverseInitialProfile.PhysicalIdentityAt line 472
  42. theorem OAI.SevenEighths.InverseInitialProfile.initial_physical_family_common_measure line 493
  43. theorem OAI.SevenEighths.InverseInitialProfile.fresh_cutoff_one_clippedSource line 530
  44. theorem OAI.SevenEighths.InverseInitialProfile.clipped_column_ratio line 540
  45. theorem OAI.SevenEighths.InverseInitialProfile.clipped_column_source_identity line 546
  46. theorem OAI.SevenEighths.InverseInitialProfile.retained_initial_clipping line 557