OAI/Analysis/Herglotz.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyPhotonNumber.Herglotz.densityMeasure line 30
  2. theorem OAI.EntropyPhotonNumber.Herglotz.integral_densityMeasure line 36
  3. theorem OAI.EntropyPhotonNumber.Herglotz.mass_densityMeasure line 45
  4. theorem OAI.EntropyPhotonNumber.Herglotz.tendsto_integral_varying line 56
  5. theorem OAI.EntropyPhotonNumber.Herglotz.continuous_integral_varying line 82
  6. abbrev OAI.EntropyPhotonNumber.Herglotz.Angle line 91
  7. instance OAI.EntropyPhotonNumber.Herglotz.(instance at line 95) line 95
  8. theorem OAI.EntropyPhotonNumber.Herglotz.integral_angle line 104
  9. def OAI.EntropyPhotonNumber.Herglotz.RadialDensity line 110
  10. theorem OAI.EntropyPhotonNumber.Herglotz.radialDensity_nonneg line 121
  11. def OAI.EntropyPhotonNumber.Herglotz.radialMeasure line 130
  12. theorem OAI.EntropyPhotonNumber.Herglotz.integral_radialMeasure line 134
  13. theorem OAI.EntropyPhotonNumber.Herglotz.mass_radialMeasure line 146
  14. def OAI.EntropyPhotonNumber.Herglotz.radialKernel line 161
  15. theorem OAI.EntropyPhotonNumber.Herglotz.continuous_radialKernel line 174
  16. theorem OAI.EntropyPhotonNumber.Herglotz.integral_radialKernel line 188
  17. def OAI.EntropyPhotonNumber.Herglotz.approachRadius line 204
  18. theorem OAI.EntropyPhotonNumber.Herglotz.approachRadius_mem line 206
  19. theorem OAI.EntropyPhotonNumber.Herglotz.approachRadius_tendsto line 213
  20. def OAI.EntropyPhotonNumber.Herglotz.clippedRadius line 221
  21. def OAI.EntropyPhotonNumber.Herglotz.clippedKernel line 226
  22. theorem OAI.EntropyPhotonNumber.Herglotz.continuous_clippedKernel line 229
  23. theorem OAI.EntropyPhotonNumber.Herglotz.clippedKernel_one line 235
  24. theorem OAI.EntropyPhotonNumber.Herglotz.clippedKernel_eq line 240
  25. def OAI.EntropyPhotonNumber.Herglotz.radialSequence line 245
  26. theorem OAI.EntropyPhotonNumber.Herglotz.exists_radialSequence_cluster line 249
  27. theorem OAI.EntropyPhotonNumber.Herglotz.eventually_integral_clippedKernel line 266
  28. theorem OAI.EntropyPhotonNumber.Herglotz.radialCluster_represents line 278
  29. theorem OAI.EntropyPhotonNumber.Herglotz.positive_harmonic_disk_representation line 302
  30. def OAI.EntropyPhotonNumber.Herglotz.diskKernel line 313
  31. def OAI.EntropyPhotonNumber.Herglotz.diskIntegral line 325
  32. theorem OAI.EntropyPhotonNumber.Herglotz.diskKernel_integrable line 328
  33. theorem OAI.EntropyPhotonNumber.Herglotz.hasDerivAt_diskIntegral line 334
  34. theorem OAI.EntropyPhotonNumber.Herglotz.analyticOnNhd_diskIntegral line 368
  35. theorem OAI.EntropyPhotonNumber.Herglotz.positive_real_disk_representation line 374
  36. def OAI.EntropyPhotonNumber.Herglotz.toDisk line 397
  37. def OAI.EntropyPhotonNumber.Herglotz.toHalfPlane line 398
  38. theorem OAI.EntropyPhotonNumber.Herglotz.add_I_ne_zero line 400
  39. theorem OAI.EntropyPhotonNumber.Herglotz.one_sub_ne_zero line 406
  40. theorem OAI.EntropyPhotonNumber.Herglotz.norm_toDisk_lt_one line 411
  41. theorem OAI.EntropyPhotonNumber.Herglotz.im_toHalfPlane line 420
  42. theorem OAI.EntropyPhotonNumber.Herglotz.im_toHalfPlane_pos line 429
  43. theorem OAI.EntropyPhotonNumber.Herglotz.toHalfPlane_toDisk line 434
  44. theorem OAI.EntropyPhotonNumber.Herglotz.toDisk_toHalfPlane line 441
  45. theorem OAI.EntropyPhotonNumber.Herglotz.analyticAt_toHalfPlane line 448
  46. theorem OAI.EntropyPhotonNumber.Herglotz.analyticAt_toDisk line 453
  47. theorem OAI.EntropyPhotonNumber.Herglotz.upper_half_plane_representation line 459
  48. theorem OAI.EntropyPhotonNumber.Herglotz.continuous_weighted_radial line 483
  49. theorem OAI.EntropyPhotonNumber.Herglotz.tendsto_radial_test_zero line 509
  50. theorem OAI.EntropyPhotonNumber.Herglotz.radialCluster_integral_zero line 553
  51. theorem OAI.EntropyPhotonNumber.Herglotz.radialCluster_no_mass line 569
  52. theorem OAI.EntropyPhotonNumber.Herglotz.positive_real_disk_representation_with_support line 593
  53. theorem OAI.EntropyPhotonNumber.Herglotz.re_toHalfPlane line 621
  54. theorem OAI.EntropyPhotonNumber.Herglotz.one_sub_ne_zero_of_im_neg line 629
  55. theorem OAI.EntropyPhotonNumber.Herglotz.boundary_toHalfPlane line 635
  56. theorem OAI.EntropyPhotonNumber.Herglotz.analyticAt_toHalfPlane_of_ne line 643
  57. theorem OAI.EntropyPhotonNumber.Herglotz.upper_half_plane_representation_with_support_of_continuous line 650
  58. def OAI.EntropyPhotonNumber.Herglotz.boundaryParameter line 702
  59. def OAI.EntropyPhotonNumber.Herglotz.boundaryWeight line 706
  60. theorem OAI.EntropyPhotonNumber.Herglotz.boundaryParameter_mem line 709
  61. theorem OAI.EntropyPhotonNumber.Herglotz.boundaryWeight_pos line 720
  62. theorem OAI.EntropyPhotonNumber.Herglotz.boundaryWeight_le_one line 724
  63. theorem OAI.EntropyPhotonNumber.Herglotz.continuous_boundaryParameter line 728
  64. theorem OAI.EntropyPhotonNumber.Herglotz.continuous_boundaryWeight line 734
  65. def OAI.EntropyPhotonNumber.Herglotz.compactKernel line 741
  66. theorem OAI.EntropyPhotonNumber.Herglotz.compactDen_ne_zero line 743
  67. theorem OAI.EntropyPhotonNumber.Herglotz.compactKernel_boundary line 761
  68. def OAI.EntropyPhotonNumber.Herglotz.compactIntegral line 805
  69. theorem OAI.EntropyPhotonNumber.Herglotz.compactKernel_integrable line 808
  70. theorem OAI.EntropyPhotonNumber.Herglotz.compactKernel_norm_le_two line 819
  71. theorem OAI.EntropyPhotonNumber.Herglotz.continuousAt_compactIntegral_one line 839
  72. theorem OAI.EntropyPhotonNumber.Herglotz.pick_divided_difference_of_continuous line 860
  73. theorem OAI.EntropyPhotonNumber.Herglotz.pick_divided_difference line 898
  74. theorem OAI.EntropyPhotonNumber.Herglotz.compactKernel_im line 907
  75. theorem OAI.EntropyPhotonNumber.Herglotz.mul_compactKernel_im line 914
  76. theorem OAI.EntropyPhotonNumber.Herglotz.complex_im_integral line 922
  77. theorem OAI.EntropyPhotonNumber.Herglotz.compactIntegral_im_nonpos line 926
  78. theorem OAI.EntropyPhotonNumber.Herglotz.mul_compactIntegral_im_nonneg line 937
  79. theorem OAI.EntropyPhotonNumber.Herglotz.compactIntegral_ne_zero line 948
  80. theorem OAI.EntropyPhotonNumber.Herglotz.continuousAt_compactIntegral line 982
  81. theorem OAI.EntropyPhotonNumber.Herglotz.upper_boundary_eq line 1016
  82. theorem OAI.EntropyPhotonNumber.Herglotz.analyticAt_dslope line 1029
  83. theorem OAI.EntropyPhotonNumber.Herglotz.pick_dslope_representation line 1039
  84. theorem OAI.EntropyPhotonNumber.Herglotz.real_compactDen_pos line 1060
  85. def OAI.EntropyPhotonNumber.Herglotz.realResolvent line 1067
  86. def OAI.EntropyPhotonNumber.Herglotz.resolventDensity line 1073
  87. theorem OAI.EntropyPhotonNumber.Herglotz.resolventDensity_nonneg line 1080
  88. def OAI.EntropyPhotonNumber.Herglotz.resolventMeasure line 1086
  89. theorem OAI.EntropyPhotonNumber.Herglotz.mass_resolventMeasure line 1089
  90. theorem OAI.EntropyPhotonNumber.Herglotz.integrable_realKernel line 1097
  91. theorem OAI.EntropyPhotonNumber.Herglotz.resolvent_algebra line 1104
  92. theorem OAI.EntropyPhotonNumber.Herglotz.compact_stieltjes_of_difference line 1130
  93. theorem OAI.EntropyPhotonNumber.Herglotz.compactIntegral_real line 1177
  94. theorem OAI.EntropyPhotonNumber.Herglotz.compact_stieltjes_representation line 1188
  95. theorem OAI.EntropyPhotonNumber.Herglotz.compactDen_loc_lower line 1213
  96. theorem OAI.EntropyPhotonNumber.Herglotz.hasDerivAt_compactKernel line 1239
  97. theorem OAI.EntropyPhotonNumber.Herglotz.differentiableAt_compactIntegral line 1248
  98. theorem OAI.EntropyPhotonNumber.Herglotz.analyticAt_compactIntegral line 1294
  99. theorem OAI.EntropyPhotonNumber.Herglotz.compactIntegral_real_pos line 1305