OAI/InformationTheory/PhotonNumber/Functions.lean

GitHub source file

155 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyPhotonNumber.f line 17
  2. def OAI.EntropyPhotonNumber.b line 19
  3. theorem OAI.EntropyPhotonNumber.f_zero line 21
  4. theorem OAI.EntropyPhotonNumber.b_zero line 22
  5. theorem OAI.EntropyPhotonNumber.f_of_ne_zero line 24
  6. theorem OAI.EntropyPhotonNumber.f_neg line 27
  7. theorem OAI.EntropyPhotonNumber.b_neg line 32
  8. theorem OAI.EntropyPhotonNumber.f_pos line 35
  9. theorem OAI.EntropyPhotonNumber.b_pos line 43
  10. theorem OAI.EntropyPhotonNumber.f_mul_sinh line 45
  11. theorem OAI.EntropyPhotonNumber.b_sq line 50
  12. theorem OAI.EntropyPhotonNumber.f_mul_exp line 57
  13. theorem OAI.EntropyPhotonNumber.f_mul_exp_neg line 64
  14. def OAI.EntropyPhotonNumber.fourWeightTarget line 67
  15. theorem OAI.EntropyPhotonNumber.fourWeightTarget_pos line 69
  16. theorem OAI.EntropyPhotonNumber.target_mul_add line 93
  17. theorem OAI.EntropyPhotonNumber.target_eq_of_add_ne_zero line 112
  18. theorem OAI.EntropyPhotonNumber.target_opposite line 116
  19. theorem OAI.EntropyPhotonNumber.f_eq_inv_dslope line 119
  20. theorem OAI.EntropyPhotonNumber.continuous_f line 125
  21. theorem OAI.EntropyPhotonNumber.continuous_b line 140
  22. theorem OAI.EntropyPhotonNumber.f_le_one line 142
  23. theorem OAI.EntropyPhotonNumber.f_lt_one line 152
  24. theorem OAI.EntropyPhotonNumber.sinh_lt_mul_cosh line 160
  25. theorem OAI.EntropyPhotonNumber.one_lt_b line 173
  26. theorem OAI.EntropyPhotonNumber.hasDerivAt_f line 182
  27. theorem OAI.EntropyPhotonNumber.strictAntiOn_f line 190
  28. theorem OAI.EntropyPhotonNumber.f_injOn_nonneg line 198
  29. theorem OAI.EntropyPhotonNumber.hasDerivAt_b line 200
  30. theorem OAI.EntropyPhotonNumber.hasDerivAt_f_sq line 212
  31. theorem OAI.EntropyPhotonNumber.strictAntiOn_f_sq line 220
  32. theorem OAI.EntropyPhotonNumber.f_eq_exp line 224
  33. theorem OAI.EntropyPhotonNumber.tendsto_f_atTop line 238
  34. theorem OAI.EntropyPhotonNumber.range_f_nonneg line 253
  35. theorem OAI.EntropyPhotonNumber.existsUnique_f_sq_parameter line 266
  36. theorem OAI.EntropyPhotonNumber.mul_cos_lt_sin line 279
  37. def OAI.EntropyPhotonNumber.bParameter line 295
  38. def OAI.EntropyPhotonNumber.B line 297
  39. theorem OAI.EntropyPhotonNumber.bParameter_nonneg line 299
  40. theorem OAI.EntropyPhotonNumber.f_sq_bParameter line 304
  41. theorem OAI.EntropyPhotonNumber.f_sq_mem line 310
  42. theorem OAI.EntropyPhotonNumber.bParameter_f_sq line 313
  43. theorem OAI.EntropyPhotonNumber.B_f_sq line 317
  44. theorem OAI.EntropyPhotonNumber.bParameter_one line 320
  45. theorem OAI.EntropyPhotonNumber.B_one line 323
  46. theorem OAI.EntropyPhotonNumber.bParameter_pos line 325
  47. theorem OAI.EntropyPhotonNumber.strictAntiOn_bParameter line 333
  48. theorem OAI.EntropyPhotonNumber.range_bParameter line 341
  49. theorem OAI.EntropyPhotonNumber.continuousAt_bParameter line 351
  50. theorem OAI.EntropyPhotonNumber.hasDerivAt_bParameter line 360
  51. theorem OAI.EntropyPhotonNumber.hasDerivAt_B line 372
  52. def OAI.EntropyPhotonNumber.sineParameter line 382
  53. def OAI.EntropyPhotonNumber.cotParameter line 384
  54. theorem OAI.EntropyPhotonNumber.normSq_sin line 386
  55. theorem OAI.EntropyPhotonNumber.sin_ne_zero_of_im_pos line 400
  56. theorem OAI.EntropyPhotonNumber.cotParameter_im line 405
  57. theorem OAI.EntropyPhotonNumber.cotParameter_im_neg line 424
  58. theorem OAI.EntropyPhotonNumber.hasDerivAt_sineParameter line 436
  59. theorem OAI.EntropyPhotonNumber.deriv_sineParameter_ne_zero line 441
  60. theorem OAI.EntropyPhotonNumber.covering_bijective_of_simplyConnected line 453
  61. def OAI.EntropyPhotonNumber.csinc line 477
  62. theorem OAI.EntropyPhotonNumber.csinc_zero line 479
  63. theorem OAI.EntropyPhotonNumber.csinc_of_ne line 483
  64. theorem OAI.EntropyPhotonNumber.analyticAt_csinc line 486
  65. theorem OAI.EntropyPhotonNumber.continuous_csinc line 497
  66. theorem OAI.EntropyPhotonNumber.sin_sub_mul_cos_pos line 500
  67. theorem OAI.EntropyPhotonNumber.sineParameter_re line 516
  68. theorem OAI.EntropyPhotonNumber.sineParameter_im line 528
  69. theorem OAI.EntropyPhotonNumber.sineParameter_im_neg line 540
  70. theorem OAI.EntropyPhotonNumber.half_sq_le_sinh line 558
  71. def OAI.EntropyPhotonNumber.sineDomain line 576
  72. def OAI.EntropyPhotonNumber.sineQuadrant line 577
  73. def OAI.EntropyPhotonNumber.sineStrip line 578
  74. theorem OAI.EntropyPhotonNumber.isOpen_sineDomain line 580
  75. theorem OAI.EntropyPhotonNumber.isOpen_sineQuadrant line 586
  76. theorem OAI.EntropyPhotonNumber.isClosed_sineStrip line 590
  77. theorem OAI.EntropyPhotonNumber.csinc_mapsTo line 595
  78. theorem OAI.EntropyPhotonNumber.csinc_strip_bound line 601
  79. theorem OAI.EntropyPhotonNumber.csinc_strip_quadrant line 628
  80. theorem OAI.EntropyPhotonNumber.isCompact_strip_preimage line 651
  81. def OAI.EntropyPhotonNumber.sineMap line 662
  82. theorem OAI.EntropyPhotonNumber.continuous_sineMap line 664
  83. theorem OAI.EntropyPhotonNumber.proper_sineMap line 667
  84. theorem OAI.EntropyPhotonNumber.deriv_csinc_ne_zero line 684
  85. theorem OAI.EntropyPhotonNumber.localHomeomorphOn_csinc line 692
  86. theorem OAI.EntropyPhotonNumber.localHomeomorph_sineMap line 699
  87. theorem OAI.EntropyPhotonNumber.covering_sineMap line 708
  88. theorem OAI.EntropyPhotonNumber.strictAnti_boundaryRatio line 718
  89. theorem OAI.EntropyPhotonNumber.csinc_re_pos_of_small_re line 745
  90. theorem OAI.EntropyPhotonNumber.csinc_re_pos_iff_of_large_re line 755
  91. theorem OAI.EntropyPhotonNumber.sineDomain_horizontal line 767
  92. def OAI.EntropyPhotonNumber.sineMidPoint line 787
  93. theorem OAI.EntropyPhotonNumber.sineMidPoint_mem line 789
  94. theorem OAI.EntropyPhotonNumber.joined_horizontal line 794
  95. theorem OAI.EntropyPhotonNumber.joined_sineMidPoints line 808
  96. theorem OAI.EntropyPhotonNumber.isPathConnected_sineDomain line 822
  97. theorem OAI.EntropyPhotonNumber.convex_sineQuadrant line 827
  98. theorem OAI.EntropyPhotonNumber.bijective_sineMap line 830
  99. def OAI.EntropyPhotonNumber.sineInverse line 838
  100. theorem OAI.EntropyPhotonNumber.sineInverse_mem line 844
  101. theorem OAI.EntropyPhotonNumber.csinc_sineInverse line 849
  102. theorem OAI.EntropyPhotonNumber.sineInverse_csinc line 855
  103. theorem OAI.EntropyPhotonNumber.analyticAt_sineInverse line 862
  104. theorem OAI.EntropyPhotonNumber.inv_sqrt_mem_sineQuadrant line 874
  105. def OAI.EntropyPhotonNumber.upperB line 894
  106. theorem OAI.EntropyPhotonNumber.analyticAt_upperB line 896
  107. theorem OAI.EntropyPhotonNumber.upperB_im_neg line 914
  108. def OAI.EntropyPhotonNumber.sinhc line 918
  109. theorem OAI.EntropyPhotonNumber.sinhc_zero line 920
  110. theorem OAI.EntropyPhotonNumber.sinhc_of_ne line 923
  111. theorem OAI.EntropyPhotonNumber.continuous_sinhc line 926
  112. theorem OAI.EntropyPhotonNumber.strictMonoOn_sinhc line 933
  113. theorem OAI.EntropyPhotonNumber.strictAntiOn_sinc line 946
  114. theorem OAI.EntropyPhotonNumber.csinc_ofReal line 961
  115. theorem OAI.EntropyPhotonNumber.csinc_mul_I line 967
  116. def OAI.EntropyPhotonNumber.closedSineQuadrant line 975
  117. def OAI.EntropyPhotonNumber.closedSineDomain line 976
  118. theorem OAI.EntropyPhotonNumber.csinc_strip_re_lt_pi line 978
  119. theorem OAI.EntropyPhotonNumber.csinc_boundary_axes line 991
  120. theorem OAI.EntropyPhotonNumber.sinc_eq_sinhc_only_zero line 1000
  121. theorem OAI.EntropyPhotonNumber.eq_of_im_zero line 1018
  122. theorem OAI.EntropyPhotonNumber.eq_mul_I_of_re_zero line 1021
  123. theorem OAI.EntropyPhotonNumber.csinc_eq_sinhc_of_re_zero line 1024
  124. theorem OAI.EntropyPhotonNumber.csinc_eq_sinc_of_im_zero line 1028
  125. theorem OAI.EntropyPhotonNumber.csinc_injOn_closedSineDomain line 1032
  126. def OAI.EntropyPhotonNumber.closedSineMap line 1066
  127. theorem OAI.EntropyPhotonNumber.continuous_closedSineMap line 1068
  128. theorem OAI.EntropyPhotonNumber.proper_closedSineMap line 1071
  129. theorem OAI.EntropyPhotonNumber.closedSineMap_injective line 1088
  130. theorem OAI.EntropyPhotonNumber.range_closedSineMap_of_im_neg line 1093
  131. theorem OAI.EntropyPhotonNumber.closedSineMap_surjective line 1102
  132. def OAI.EntropyPhotonNumber.closedSineHomeomorph line 1129
  133. def OAI.EntropyPhotonNumber.closedSineInverse line 1132
  134. theorem OAI.EntropyPhotonNumber.closedSineInverse_mem line 1136
  135. theorem OAI.EntropyPhotonNumber.csinc_closedSineInverse line 1141
  136. theorem OAI.EntropyPhotonNumber.continuousOn_closedSineInverse line 1147
  137. theorem OAI.EntropyPhotonNumber.closedSineInverse_eq_sineInverse line 1156
  138. def OAI.EntropyPhotonNumber.ccot line 1164
  139. theorem OAI.EntropyPhotonNumber.ccot_zero line 1166
  140. theorem OAI.EntropyPhotonNumber.ccot_eq_cotParameter line 1168
  141. theorem OAI.EntropyPhotonNumber.continuousAt_ccot line 1172
  142. theorem OAI.EntropyPhotonNumber.ccot_boundary_im line 1175
  143. def OAI.EntropyPhotonNumber.upperReflect line 1196
  144. theorem OAI.EntropyPhotonNumber.continuous_upperReflect line 1198
  145. theorem OAI.EntropyPhotonNumber.upperReflect_eq line 1205
  146. theorem OAI.EntropyPhotonNumber.inv_sqrt_mem_closedSineQuadrant line 1208
  147. def OAI.EntropyPhotonNumber.boundaryB line 1223
  148. theorem OAI.EntropyPhotonNumber.boundaryB_eq_upperB line 1225
  149. theorem OAI.EntropyPhotonNumber.analyticAt_boundaryB line 1231
  150. theorem OAI.EntropyPhotonNumber.boundaryB_im_neg line 1236
  151. theorem OAI.EntropyPhotonNumber.continuousAt_reflectedRoot line 1240
  152. theorem OAI.EntropyPhotonNumber.continuousAt_boundaryB line 1252
  153. theorem OAI.EntropyPhotonNumber.boundaryB_real line 1269
  154. theorem OAI.EntropyPhotonNumber.closedSineInverse_one line 1280
  155. theorem OAI.EntropyPhotonNumber.boundaryB_one line 1289