OAI/MeasureTheory/SelfSimilar/ErgodicAverages.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyRateDimension.ErgodicAux.maxSum line 24
  2. theorem OAI.EntropyRateDimension.ErgodicAux.maxSum_zero line 28
  3. theorem OAI.EntropyRateDimension.ErgodicAux.maxSum_succ line 31
  4. theorem OAI.EntropyRateDimension.ErgodicAux.maxSum_nonneg line 34
  5. theorem OAI.EntropyRateDimension.ErgodicAux.maxSum_mono line 40
  6. theorem OAI.EntropyRateDimension.ErgodicAux.birkhoffSum_le_maxSum line 48
  7. theorem OAI.EntropyRateDimension.ErgodicAux.maxSum_measurable line 59
  8. theorem OAI.EntropyRateDimension.ErgodicAux.maxSum_integrable line 66
  9. theorem OAI.EntropyRateDimension.ErgodicAux.integral_comp_preserving line 74
  10. theorem OAI.EntropyRateDimension.ErgodicAux.hopf_finite line 83
  11. def OAI.EntropyRateDimension.ErgodicAux.boundedSums line 124
  12. theorem OAI.EntropyRateDimension.ErgodicAux.bddAbove_range_nat_iff line 128
  13. theorem OAI.EntropyRateDimension.ErgodicAux.sum_measurable line 137
  14. theorem OAI.EntropyRateDimension.ErgodicAux.boundedSums_measurable line 148
  15. theorem OAI.EntropyRateDimension.ErgodicAux.boundedSums_invariant line 159
  16. theorem OAI.EntropyRateDimension.ErgodicAux.hopf_of_ae_positive_sum line 183
  17. theorem OAI.EntropyRateDimension.ErgodicAux.ae_boundedSums_of_integral_neg line 208
  18. theorem OAI.EntropyRateDimension.ErgodicAux.sum_sub_const line 221
  19. theorem OAI.EntropyRateDimension.ErgodicAux.ae_upper_average line 225
  20. theorem OAI.EntropyRateDimension.ErgodicAux.ae_tendsto_average line 258