OAI/Geometry/HeilbronnTriangle/ConditionalDigits.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem355.ConditionalDigits.encoded_digits_injective line 11
2. theorem OAI.Problem355.ConditionalDigits.card_prefix_event_le line 32
3. theorem OAI.Problem355.ConditionalDigits.prefix_probability_le line 57
4. theorem OAI.Problem355.ConditionalDigits.card_residue_event_le line 85
5. theorem OAI.Problem355.ConditionalDigits.residue_event_probability_le line 131
6. theorem OAI.Problem355.ConditionalDigits.unit_equation_event_probability_le line 161
7. theorem OAI.Problem355.ConditionalDigits.conditional_divisor_moment_le_two line 188