OAI/Probability/CriticalPercolation/Entropy/BinaryInterpolation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BinaryInterpolation.midpoint line 10
2. def OAI.CriticalPercolation.BinaryInterpolation.bisect line 12
3. lemma OAI.CriticalPercolation.BinaryInterpolation.midpoint_strict line 15
4. lemma OAI.CriticalPercolation.BinaryInterpolation.bisect_bounds line 20
5. lemma OAI.CriticalPercolation.BinaryInterpolation.bisect_length line 33
6. lemma OAI.CriticalPercolation.BinaryInterpolation.bisect_clog line 39
7. def OAI.CriticalPercolation.BinaryInterpolation.terminal line 47
8. lemma OAI.CriticalPercolation.BinaryInterpolation.terminal_bounds line 51
9. lemma OAI.CriticalPercolation.BinaryInterpolation.terminal_eq_of_adjacent line 62
10. theorem OAI.CriticalPercolation.BinaryInterpolation.terminal_adjacent line 68
11. def OAI.CriticalPercolation.BinaryInterpolation.anchors line 88
12. lemma OAI.CriticalPercolation.BinaryInterpolation.terminal_mem_anchors line 92
13. lemma OAI.CriticalPercolation.BinaryInterpolation.midpoint_internal line 99
14. abbrev OAI.CriticalPercolation.BinaryInterpolation.Descriptor line 104
15. lemma OAI.CriticalPercolation.BinaryInterpolation.descriptor_card line 106
16. lemma OAI.CriticalPercolation.BinaryInterpolation.descriptor_card_le line 110