OAI/Geometry/HeilbronnTriangle/AllowedShifts.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem355.Auxiliary.badShifts line 16
2. def OAI.Problem355.Auxiliary.allowedShifts line 19
3. lemma OAI.Problem355.Auxiliary.mem_badShifts_iff line 23
4. lemma OAI.Problem355.Auxiliary.mem_allowedShifts_iff line 33
5. lemma OAI.Problem355.Auxiliary.card_badShifts_le line 39
6. lemma OAI.Problem355.Auxiliary.card_le_allowedShifts_add line 43
7. def OAI.Problem355.Auxiliary.integerWindow line 53
8. lemma OAI.Problem355.Auxiliary.card_integerWindow_le line 57
9. lemma OAI.Problem355.Auxiliary.intCast_mem_integerWindow line 66
10. def OAI.Problem355.Auxiliary.positiveMultipliers line 73
11. lemma OAI.Problem355.Auxiliary.card_positiveMultipliers_le line 77
12. lemma OAI.Problem355.Auxiliary.positiveMultipliers_ne_zero line 86
13. lemma OAI.Problem355.Auxiliary.card_allowed_auxiliary_shifts line 96
14. lemma OAI.Problem355.Auxiliary.auxiliary_bad_count_lt_half line 111
15. lemma OAI.Problem355.Auxiliary.auxiliary_multiplier_range line 118
16. lemma OAI.Problem355.Auxiliary.auxiliary_allowed_card_gt_half line 123
17. lemma OAI.Problem355.Auxiliary.exists_auxiliary_allowed_shift line 132
18. lemma OAI.Problem355.Auxiliary.neg_mem_integerWindow line 150
19. lemma OAI.Problem355.Auxiliary.int_mul_not_mem_integerWindow line 160
20. lemma OAI.Problem355.Auxiliary.abs_sum_three_le line 186
21. lemma OAI.Problem355.Auxiliary.shifted_scalar_short_relation_ne_zero line 193
22. lemma OAI.Problem355.Auxiliary.exists_auxiliary_allowed_shift_div line 221
23. lemma OAI.Problem355.Auxiliary.shifted_vector_short_relation_ne_zero line 228
24. def OAI.Problem355.Auxiliary.vectorShifts line 251
25. lemma OAI.Problem355.Auxiliary.mem_vectorShifts_iff line 254
26. lemma OAI.Problem355.Auxiliary.card_vectorShifts line 266
27. lemma OAI.Problem355.Auxiliary.auxiliary_allowed_vector_card_gt_half line 280