OAI/MeasureTheory/SelfSimilar/Boundary.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.EntropyRateDimension.Boundary.incrementline 14 - theorem
OAI.EntropyRateDimension.Boundary.increment_periodicline 16 - theorem
OAI.EntropyRateDimension.Boundary.increment_boundsline 21 - theorem
OAI.EntropyRateDimension.Boundary.increment_measurableline 31 - theorem
OAI.EntropyRateDimension.Boundary.increment_integrableline 37 - theorem
OAI.EntropyRateDimension.Boundary.increment_eq_indicatorline 46 - theorem
OAI.EntropyRateDimension.Boundary.integral_incrementline 58 - theorem
OAI.EntropyRateDimension.Boundary.integral_increment_shiftline 78 - theorem
OAI.EntropyRateDimension.Boundary.increment_eq_iteline 84 - theorem
OAI.EntropyRateDimension.Boundary.increment_prod_integrableline 95 - theorem
OAI.EntropyRateDimension.Boundary.increment_measure_intervalIntegrableline 108 - theorem
OAI.EntropyRateDimension.Boundary.integral_increment_measureline 115