OAI/NumberTheory/DirichletL/Mellin/ReflectedKernel.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicReflectionKernel.reflectedLogProfile_deriv_bound line 78
  2. def OAI.CubicReflectionKernel.momentScale line 97
  3. theorem OAI.CubicReflectionKernel.momentScale_nonneg line 101
  4. theorem OAI.CubicReflectionKernel.reflectedLogProfile_source_bound line 107
  5. def OAI.CubicReflectionKernel.paperScale line 158
  6. theorem OAI.CubicReflectionKernel.paperScale_pos line 160
  7. def OAI.CubicReflectionKernel.paperKernel line 164
  8. theorem OAI.CubicReflectionKernel.logProfile_compact line 167
  9. def OAI.CubicReflectionKernel.logSchwartz line 179
  10. theorem OAI.CubicReflectionKernel.logSchwartz_apply line 184
  11. theorem OAI.CubicReflectionKernel.compact_source_mellin_convergent line 188
  12. theorem OAI.CubicReflectionKernel.mellin_axis_eq_fourier line 209
  13. theorem OAI.CubicReflectionKernel.paperKernel_eq_logFourier line 227
  14. theorem OAI.CubicReflectionKernel.kernel_vertical_eq_spectralProfile line 250
  15. theorem OAI.CubicReflectionKernel.kernel_vertical_integrable line 258
  16. theorem OAI.CubicReflectionKernel.paperKernel_integrable line 267
  17. theorem OAI.CubicReflectionKernel.paperKernel_contDiffOn line 281
  18. theorem OAI.CubicReflectionKernel.paperKernel_euler_eq line 294
  19. theorem OAI.CubicReflectionKernel.paperKernel_source_euler_bound line 307
  20. theorem OAI.CubicReflectionKernel.paperKernel_compact_source_integrable line 320
  21. theorem OAI.CubicReflectionKernel.paperKernel_compact_source_smooth line 328
  22. theorem OAI.CubicReflectionKernel.reflectedLogProfile_deriv_vanish line 334
  23. theorem OAI.CubicReflectionKernel.paperKernel_euler_vanish_infty line 339
  24. theorem OAI.CubicReflectionKernel.paperKernel_euler_vanish_zero line 349
  25. theorem OAI.CubicReflectionKernel.compact_source_mellin_hasDerivAt line 365
  26. theorem OAI.CubicReflectionKernel.compact_source_mellin_differentiable line 387
  27. theorem OAI.CubicReflectionKernel.Gamma_differentiableAt_of_re_pos line 393
  28. theorem OAI.CubicReflectionKernel.gammaMultiplier_differentiableAt line 402
  29. theorem OAI.CubicReflectionKernel.kernelMellinIntegrand_differentiableAt line 419
  30. theorem OAI.DescentWeightedCauchy.weighted_cauchy_sq line 433
  31. theorem OAI.DescentWeightedCauchy.weighted_cauchy line 449
  32. theorem OAI.DescentWeightedCauchy.weighted_energy_pushforward line 467
  33. theorem OAI.DescentWeightedCauchy.bounded_energy_pushforward line 488
  34. abbrev OAI.DescentWeightedCauchy.O line 501
  35. def OAI.DescentWeightedCauchy.firstRowMap line 503
  36. theorem OAI.DescentWeightedCauchy.firstRowMap_fst_dvd line 506
  37. theorem OAI.DescentWeightedCauchy.firstRowMap_fst_injective_on_fiber line 512
  38. theorem OAI.DescentWeightedCauchy.firstRowMap_fiber_card_le line 530
  39. theorem OAI.DescentWeightedCauchy.first_energy_pushforward line 544
  40. def OAI.DescentWeightedCauchy.firstElementRowMap line 558
  41. theorem OAI.DescentWeightedCauchy.firstElementRowMap_label_dvd line 561
  42. theorem OAI.DescentWeightedCauchy.firstElementRowMap_fiber_card_le line 569
  43. theorem OAI.DescentWeightedCauchy.first_element_energy_pushforward line 600