OAI/Dynamics/ConditionalShuffle/ScheduledRate.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Revealed.Scheduled.symbolFintype line 12
2. def OAI.Revealed.Scheduled.segmentLength line 15
3. def OAI.Revealed.Scheduled.segmentSchedule line 17
4. lemma OAI.Revealed.Scheduled.segmentSchedule_fin line 20
5. lemma OAI.Revealed.Scheduled.segment_marginal_rate line 26
6. lemma OAI.Revealed.Scheduled.segment_discarded_le line 67
7. def OAI.Revealed.Scheduled.groupRate line 100
8. lemma OAI.Revealed.Scheduled.groupRate_tendsto line 103
9. lemma OAI.Revealed.Scheduled.group_distance_bound line 110