OAI/MeasureTheory/SelfSimilar/FiniteRefinement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyRateDimension.FiniteRefinement.cellMean line 17
  2. theorem OAI.EntropyRateDimension.FiniteRefinement.distance_mean_le line 20
  3. theorem OAI.EntropyRateDimension.FiniteRefinement.mass_pos line 38
  4. theorem OAI.EntropyRateDimension.FiniteRefinement.cellMass_eq line 46
  5. theorem OAI.EntropyRateDimension.FiniteRefinement.conditional_mean_eq line 50
  6. theorem OAI.EntropyRateDimension.FiniteRefinement.conditional_mean_distance_le line 56
  7. theorem OAI.EntropyRateDimension.FiniteRefinement.fiber_entropy_hit_bound line 72
  8. theorem OAI.EntropyRateDimension.FiniteRefinement.entropy_step_hit_bound line 121
  9. theorem OAI.EntropyRateDimension.FiniteRefinement.mean_deviation_le_coupling line 167
  10. theorem OAI.EntropyRateDimension.FiniteRefinement.product_mean_deviation line 203
  11. theorem OAI.EntropyRateDimension.FiniteRefinement.exists_entropy_step line 219
  12. theorem OAI.EntropyRateDimension.FiniteRefinement.refinement_increment line 240