OAI/Probability/Ballisticity/Entropy/EntropyPlus.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TailDecorrelation.entropyPlus line 13
  2. lemma OAI.TailDecorrelation.entropyPlus_nonneg line 15
  3. lemma OAI.TailDecorrelation.measurable_entropyPlus line 18
  4. lemma OAI.TailDecorrelation.entropy_young line 22
  5. lemma OAI.TailDecorrelation.integrable_density_mul_of_entropy line 42
  6. lemma OAI.TailDecorrelation.exp_on_density_tail_pointwise line 56
  7. lemma OAI.TailDecorrelation.density_tail_pointwise line 81
  8. lemma OAI.TailDecorrelation.integrable_entropy_tail line 99
  9. lemma OAI.TailDecorrelation.entropy_tail_tendsto line 109
  10. lemma OAI.TailDecorrelation.density_tail_integral_le line 134
  11. lemma OAI.TailDecorrelation.remainder_cap_pointwise line 171
  12. lemma OAI.TailDecorrelation.exp_neg_nat_tendsto line 187
  13. lemma OAI.TailDecorrelation.uniform_density_tail line 195
  14. lemma OAI.TailDecorrelation.cap_error_integrable line 252
  15. lemma OAI.TailDecorrelation.cap_error_integral_le line 267
  16. lemma OAI.TailDecorrelation.uniform_remainder_cap line 280