OAI/NumberTheory/Jacobsthal/Partitions/BandShiftTransport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.BandShiftTransport.bandExpectation line 15
2. def OAI.Erdos970.NumberTheoryLean.BandShiftTransport.zeroBandExpectation line 18
3. theorem OAI.Erdos970.NumberTheoryLean.BandShiftTransport.stateBandReward_measurable line 21
4. theorem OAI.Erdos970.NumberTheoryLean.BandShiftTransport.bandExpectation_measurable line 25
5. theorem OAI.Erdos970.NumberTheoryLean.BandShiftTransport.zeroBandExpectation_measurable line 28
6. theorem OAI.Erdos970.NumberTheoryLean.BandShiftTransport.stateBandReward_shift line 32
7. theorem OAI.Erdos970.NumberTheoryLean.BandShiftTransport.bandExpectation_translation line 41
8. theorem OAI.Erdos970.NumberTheoryLean.BandShiftTransport.stateBandReward_mono line 52
9. theorem OAI.Erdos970.NumberTheoryLean.BandShiftTransport.bandExpectation_mono line 63
10. theorem OAI.Erdos970.NumberTheoryLean.BandShiftTransport.remove_prefix_cost line 68
11. theorem OAI.Erdos970.NumberTheoryLean.BandShiftTransport.restore_prefix_cost line 78
12. theorem OAI.Erdos970.NumberTheoryLean.BandShiftTransport.prefix_band_domination line 88