OAI/Probability/ParisiFinite/ParisiCoshEntropy.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Parisi Cosh Entropy.

  1. def OAI.ParisiSpectral.ExpGrowth line 21
  2. lemma OAI.ParisiSpectral.ExpGrowth.add line 22
  3. lemma OAI.ParisiSpectral.ExpGrowth.const_mul line 28
  4. lemma OAI.ParisiSpectral.ExpGrowth.neg line 34
  5. lemma OAI.ParisiSpectral.ExpGrowth.sub line 36
  6. lemma OAI.ParisiSpectral.ExpGrowth.of_bounded line 38
  7. lemma OAI.ParisiSpectral.ExpGrowth.mono line 40
  8. lemma OAI.ParisiSpectral.cosh_le_exp_abs line 44
  9. lemma OAI.ParisiSpectral.sinh_abs_le_cosh line 47
  10. lemma OAI.ParisiSpectral.cosh_ExpGrowth line 50
  11. lemma OAI.ParisiSpectral.sinh_ExpGrowth line 53
  12. lemma OAI.ParisiSpectral.sech_ExpGrowth line 56
  13. lemma OAI.ParisiSpectral.sechCube_ExpGrowth line 61
  14. def OAI.ParisiSpectral.coshEntropy line 67
  15. def OAI.ParisiSpectral.coshEntropyD line 68
  16. def OAI.ParisiSpectral.coshEntropyU line 69
  17. def OAI.ParisiSpectral.coshEntropyUD line 70
  18. lemma OAI.ParisiSpectral.coshEntropy_hasDerivAt line 72
  19. lemma OAI.ParisiSpectral.coshEntropyD_hasDerivAt line 76
  20. lemma OAI.ParisiSpectral.coshEntropyU_hasDerivAt line 82
  21. lemma OAI.ParisiSpectral.coshEntropyUD_hasDerivAt line 86
  22. lemma OAI.ParisiSpectral.coshEntropy_ExpGrowth line 93
  23. lemma OAI.ParisiSpectral.sinh_log_ExpGrowth line 103
  24. lemma OAI.ParisiSpectral.coshEntropyD_ExpGrowth line 110
  25. lemma OAI.ParisiSpectral.coshEntropyU_ExpGrowth line 115
  26. lemma OAI.ParisiSpectral.coshEntropyUD_ExpGrowth line 117
  27. lemma OAI.ParisiSpectral.continuous_coshEntropy line 125
  28. lemma OAI.ParisiSpectral.continuous_coshEntropyD line 127
  29. lemma OAI.ParisiSpectral.continuous_coshEntropyU line 129
  30. lemma OAI.ParisiSpectral.continuous_coshEntropyUD line 131
  31. lemma OAI.ParisiSpectral.heatLaw_eq_map line 144
  32. lemma OAI.ParisiSpectral.heatObservation_eq_integral line 158
  33. lemma OAI.ParisiSpectral.ExpGrowth.integrable_heatLaw line 164
  34. lemma OAI.ParisiSpectral.ExpGrowth.integrable_heatObservation line 171
  35. lemma OAI.ParisiSpectral.heatObservation_add line 178
  36. lemma OAI.ParisiSpectral.heatObservation_const_mul line 183
  37. lemma OAI.ParisiSpectral.hasDerivAt_heatObservation_growth line 186
  38. lemma OAI.ParisiSpectral.continuous_heatObservation_growth line 197
  39. def OAI.ParisiSpectral.weightedHeat line 203
  40. lemma OAI.ParisiSpectral.weightedHeat_hasDerivAt line 206
  41. lemma OAI.ParisiSpectral.continuous_weightedHeat line 220
  42. lemma OAI.ParisiSpectral.weightedHeat_cosh_hasDerivAt line 227
  43. lemma OAI.ParisiSpectral.weightedHeat_G_hasDerivAt line 240
  44. lemma OAI.ParisiSpectral.weightedHeat_U_hasDerivAt line 248
  45. def OAI.ParisiSpectral.baseEntropy line 260
  46. def OAI.ParisiSpectral.baseEntropyD line 264
  47. def OAI.ParisiSpectral.baseCurvature line 268
  48. lemma OAI.ParisiSpectral.baseEntropy_hasDerivAt line 271
  49. lemma OAI.ParisiSpectral.baseEntropyD_hasDerivAt line 278
  50. lemma OAI.ParisiSpectral.continuous_baseCurvature line 285
  51. lemma OAI.ParisiSpectral.baseEntropy_eq_integral line 291
  52. lemma OAI.ParisiFinite.BoundedCoefficient.exp_field_backward line 320
  53. lemma OAI.ParisiFinite.BoundedCoefficient.plateau_backward_representation line 345
  54. lemma OAI.ParisiFinite.BoundedCoefficient.conjugateMeasure_eq_heatLaw line 363
  55. lemma OAI.ParisiSpectral.integrable_gaussian_exp_abs line 381
  56. lemma OAI.ParisiPath.brownian_solution_exp_abs line 394
  57. lemma OAI.ParisiFinite.BoundedCoefficient.conjugateMeasure_exp_abs line 416
  58. lemma OAI.ParisiFinite.BoundedCoefficient.conjugateMeasure_ne_zero line 443
  59. lemma OAI.ParisiFinite.BoundedCoefficient.conjugateMeasure_entropy line 456
  60. lemma OAI.ParisiFinite.BoundedCoefficient.field_along_solution_integrable line 470
  61. lemma OAI.ParisiFinite.BoundedCoefficient.conjugateMeasure_entropy_integrable line 478
  62. def OAI.ParisiFinite.BoundedCoefficient.fieldEntropy line 505
  63. lemma OAI.ParisiFinite.BoundedCoefficient.fieldEntropy_eq line 509
  64. lemma OAI.ParisiFinite.BoundedCoefficient.real_eq_on_plateau line 518
  65. lemma OAI.ParisiFinite.BoundedCoefficient.fieldEntropy_hasDerivAt line 525
  66. lemma OAI.ParisiFinite.BoundedCoefficient.fieldEntropyD_hasDerivAt line 543
  67. lemma OAI.ParisiSpectral.contDiffOn_two_of_derivatives line 557
  68. lemma OAI.ParisiSpectral.iteratedDeriv_two_of_derivatives line 569
  69. lemma OAI.ParisiSpectral.HankelPD.congr_on line 577
  70. lemma OAI.ParisiSpectral.HankelCPD.congr_on line 589
  71. lemma OAI.ParisiSpectral.HankelCPD.sub_const line 603
  72. lemma OAI.ParisiSpectral.HankelCPD.has_second_derivative line 615