OAI/MeasureTheory/SelfSimilar/WindowGain.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.EntropyRateDimension.Typed.retainedCapacityline 12 - def
OAI.EntropyRateDimension.Typed.retainedDropline 17 - theorem
OAI.EntropyRateDimension.Typed.three_segmentline 24 - theorem
OAI.EntropyRateDimension.Typed.three_takeline 33 - theorem
OAI.EntropyRateDimension.Typed.three_retainedline 38 - theorem
OAI.EntropyRateDimension.Typed.suffixLaw_at_appendline 44 - theorem
OAI.EntropyRateDimension.Typed.three_suffix_startline 48 - theorem
OAI.EntropyRateDimension.Typed.three_suffix_endline 58 - theorem
OAI.EntropyRateDimension.Typed.expected_retained_gainline 67 - theorem
OAI.EntropyRateDimension.Typed.expected_capacity_targetsline 94