OAI/NumberTheory/DirichletL/Fourier/PositiveLogProfiles.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TwoPassProfiles.log_dyad_bound line 54
  2. theorem OAI.ActualEisensteinCubic.A3_primary_unit_eq_one line 66
  3. theorem OAI.ActualEisensteinCubic.A3_ramified_zero_lower_left line 89
  4. theorem OAI.ActualEisensteinCubic.A3_unramified_zero_lower_left line 107
  5. theorem OAI.FourierBridge.coupled_double_log_separation_schwartz line 124
  6. theorem OAI.InitialMeanSquareProfile.dual_profile line 247
  7. def OAI.LocalLogFourier.eulerDeriv line 264
  8. theorem OAI.LocalLogFourier.iteratedDeriv_log_eq_euler line 267
  9. theorem OAI.LocalLogFourier.euler_two_regime_bound line 280
  10. def OAI.LocalLogFourier.positiveLogProfile line 312
  11. theorem OAI.LocalLogFourier.positiveLogProfile_apply line 331
  12. theorem OAI.LocalLogFourier.positive_log_separation line 340
  13. theorem OAI.LocalLogFourier.euler_derivative_scale line 352
  14. theorem OAI.LocalLogFourier.positive_log_product_derivative_bound line 374
  15. theorem OAI.LocalLogFourier.positive_log_uniform_seminorm line 429
  16. def OAI.LocalLogFourier.derivativeConstant line 513
  17. def OAI.LocalLogFourier.momentConstant line 516
  18. theorem OAI.LocalLogFourier.derivativeConstant_nonneg line 521
  19. theorem OAI.LocalLogFourier.momentConstant_nonneg line 527
  20. theorem OAI.LocalLogFourier.momentConstant_dominates line 536
  21. theorem OAI.LocalLogFourier.positive_log_source_pair line 552
  22. theorem OAI.LocalLogFourier.positive_log_fourier_moment line 613
  23. theorem OAI.LocalLogFourier.positive_log_fourier_bound line 654
  24. theorem OAI.LocalLogFourier.coupled_positive_log_separation line 686
  25. theorem OAI.LocalLogFourier.coupled_positive_log_separation_uniform line 745
  26. theorem OAI.LocalLogFourier.coupled_positive_log_separation_two_regimes line 819
  27. theorem OAI.LocalLogFourier.coupled_double_positive_log_separation line 852