OAI/Probability/SKFluctuations/CompletedIndex.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Completed Index.

  1. abbrev OAI.SKFluctuations.CompletedIndex line 18
  2. abbrev OAI.SKFluctuations.StandardCompletedDisorder line 19
  3. def OAI.SKFluctuations.standardCompletedLaw line 21
  4. def OAI.SKFluctuations.toCompletedDisorder line 24
  5. def OAI.SKFluctuations.liftedFreeEnergy line 27
  6. def OAI.SKFluctuations.liftedHamiltonian line 30
  7. theorem OAI.SKFluctuations.continuous_liftedFreeEnergy line 34
  8. theorem OAI.SKFluctuations.convexOn_liftedFreeEnergy line 40
  9. theorem OAI.SKFluctuations.exp_liftedFreeEnergy line 55
  10. def OAI.SKFluctuations.liftedCoefficients line 63
  11. theorem OAI.SKFluctuations.liftedHamiltonian_eq_sum line 67
  12. def OAI.SKFluctuations.liftedGauge line 78
  13. theorem OAI.SKFluctuations.liftedFreeEnergy_gauge line 83
  14. theorem OAI.SKFluctuations.liftedHamiltonian_gauge line 91
  15. theorem OAI.SKFluctuations.measurePreserving_liftedGauge line 100
  16. instance OAI.SKFluctuations.standardCompletedLaw_isProbability line 123
  17. theorem OAI.SKFluctuations.measurePreserving_toCompletedDisorder line 128
  18. theorem OAI.SKFluctuations.integrable_exp_liftedFreeEnergy line 158
  19. theorem OAI.SKFluctuations.integrable_exp_liftedHamiltonian line 168
  20. def OAI.SKFluctuations.spinEpigraphIntegrand line 174
  21. theorem OAI.SKFluctuations.integrable_spinEpigraphIntegrand line 178
  22. theorem OAI.SKFluctuations.integral_spinEpigraphIntegrand_eq line 183
  23. def OAI.SKFluctuations.augmentedDensity line 195
  24. theorem OAI.SKFluctuations.augmentedDensity_eq_gaussianEpigraphTilt line 199
  25. theorem OAI.SKFluctuations.logConcave_augmentedDensity line 220
  26. theorem OAI.SKFluctuations.map_add_expMeasure_withDensity line 231
  27. def OAI.SKFluctuations.augmentedLaw line 261
  28. theorem OAI.SKFluctuations.augmentedDensity_nonneg line 265
  29. theorem OAI.SKFluctuations.ofReal_augmentedDensity line 273
  30. theorem OAI.SKFluctuations.augmentedLaw_withDensity line 297
  31. instance OAI.SKFluctuations.expMeasure_one_isProbability line 311
  32. lemma OAI.SKFluctuations.exponentialPDF_one_toReal line 314
  33. lemma OAI.SKFluctuations.integral_expMeasure_one line 321
  34. lemma OAI.SKFluctuations.integrable_expMeasure_one_iff line 333
  35. lemma OAI.SKFluctuations.integrable_exp_expMeasure_one line 348
  36. lemma OAI.SKFluctuations.mgf_expMeasure_one line 357
  37. lemma OAI.SKFluctuations.expMeasure_one_mem_interior line 367
  38. lemma OAI.SKFluctuations.memLp_expMeasure_one line 373
  39. lemma OAI.SKFluctuations.hasDerivAt_one_div_one_sub line 376
  40. lemma OAI.SKFluctuations.mean_expMeasure_one line 382
  41. lemma OAI.SKFluctuations.secondMoment_expMeasure_one line 391
  42. lemma OAI.SKFluctuations.variance_expMeasure_one line 409
  43. theorem OAI.SKFluctuations.continuous_completedFreeEnergy line 421
  44. theorem OAI.SKFluctuations.memLp_liftedFreeEnergy line 425
  45. theorem OAI.SKFluctuations.mean_liftedFreeEnergy line 430
  46. theorem OAI.SKFluctuations.variance_liftedFreeEnergy line 438
  47. theorem OAI.SKFluctuations.mgf_liftedFreeEnergy line 445
  48. instance OAI.SKFluctuations.augmentedLaw_isProbability line 456
  49. theorem OAI.SKFluctuations.mean_augmentedLaw line 461
  50. theorem OAI.SKFluctuations.variance_augmentedLaw line 475
  51. theorem OAI.SKFluctuations.mgf_augmentedLaw line 486
  52. theorem OAI.SKFluctuations.centeredLogLaplace_augmentedLaw line 500
  53. theorem OAI.SKFluctuations.PreKopa.LogConcave.mul line 527
  54. theorem OAI.SKFluctuations.PreKopa.LogConcave.concaveOn_log line 539
  55. theorem OAI.SKFluctuations.PreKopa.LogConcave.continuous_of_pos line 549
  56. def OAI.SKFluctuations.PreKopa.survivalApprox line 559
  57. def OAI.SKFluctuations.PreKopa.survivalIntegral line 562
  58. theorem OAI.SKFluctuations.PreKopa.logConcave_survivalApprox line 564
  59. theorem OAI.SKFluctuations.PreKopa.survivalApprox_bound line 585
  60. theorem OAI.SKFluctuations.PreKopa.integrable_survivalApprox line 592
  61. theorem OAI.SKFluctuations.PreKopa.tendsto_survivalApprox line 597
  62. theorem OAI.SKFluctuations.PreKopa.logConcave_survivalIntegral line 622