OAI/NumberTheory/Jacobsthal/Paths/NearPrefixOccurrence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.CompactPrefixOccurrence.selectedNode line 24
2. def OAI.Erdos970.NumberTheoryLean.CompactPrefixOccurrence.occurs line 28
3. theorem OAI.Erdos970.NumberTheoryLean.CompactPrefixOccurrence.occurs_measurable line 32
4. def OAI.Erdos970.NumberTheoryLean.CompactPrefixOccurrence.listSelection line 41
5. theorem OAI.Erdos970.NumberTheoryLean.CompactPrefixOccurrence.listSelection_nonneg line 44
6. theorem OAI.Erdos970.NumberTheoryLean.CompactPrefixOccurrence.selected_node_compact line 48
7. theorem OAI.Erdos970.NumberTheoryLean.CompactPrefixOccurrence.full_selected_le_occurrence line 60
8. theorem OAI.Erdos970.NumberTheoryLean.NearPrefixOccurrence.selected_near_prefix_occurs line 99
9. theorem OAI.Erdos970.NumberTheoryLean.NearPrefixOccurrence.near_prefix_occurrence_probability line 114