OAI/Combinatorics/BalancedRyser/Candidates/OppositeTail.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.OppositeTail.power_tail_le line 15
2. theorem OAI.Balanced.OppositeTail.exposedLaw_empty line 34
3. theorem OAI.Balanced.OppositeTail.conditional_witness_tail_le line 41
4. def OAI.Balanced.OppositeTail.tailConstant line 61
5. theorem OAI.Balanced.OppositeTail.single_direction_tail_le line 63
6. theorem OAI.Balanced.OppositeTail.some_direction_tail_le line 79
7. theorem OAI.Balanced.OppositeTail.tendsto_some_direction_tail line 114
8. theorem OAI.Balanced.OppositeTail.tendsto_all_directions_small line 131