OAI/Probability/SpanningForest/PosteriorTiltLimit.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.TiltLimit.tiltedMean line 14
  2. theorem OAI.Problem336.TiltLimit.tendsto_integral_continuous line 18
  3. theorem OAI.Problem336.TiltLimit.integral_exp_pos line 26
  4. theorem OAI.Problem336.TiltLimit.tendsto_tiltedMean line 32
  5. theorem OAI.Problem336.TiltLimit.response_bound_of_tendsto line 39
  6. theorem OAI.Problem336.TiltLimit.measurable_tiltedMean line 51
  7. theorem OAI.Problem336.TiltLimit.tiltedMean_mem_Icc line 59
  8. theorem OAI.Problem336.TiltLimit.tiltedMean_map line 75
  9. def OAI.Problem336.TiltLimit.bit line 89
  10. theorem OAI.Problem336.TiltLimit.continuous_bit line 91
  11. def OAI.Problem336.TiltLimit.finiteEnergy line 93
  12. theorem OAI.Problem336.TiltLimit.continuous_finiteEnergy line 96
  13. def OAI.Problem336.TiltLimit.finiteTiltMean line 102
  14. theorem OAI.Problem336.TiltLimit.tendsto_finiteTiltMean line 107
  15. theorem OAI.Problem336.TiltLimit.finiteTiltMean_response_bound_of_tendsto line 115
  16. theorem OAI.Problem336.TiltLimit.finiteTiltMean_mem_Icc line 125
  17. theorem OAI.Problem336.TiltLimit.measurable_finitePosterior line 135
  18. def OAI.Problem336.TiltLimit.reindex line 154
  19. theorem OAI.Problem336.TiltLimit.measurable_reindex line 158
  20. theorem OAI.Problem336.TiltLimit.finiteEnergy_reindex line 162
  21. theorem OAI.Problem336.TiltLimit.finiteTiltMean_reindex line 170