OAI/Probability/BinarySweep/Mixing/BinaryLineDisk.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.complexLineLaw line 12
2. lemma OAI.BinaryCoordinateSweeps.complexLineLaw_real line 15
3. lemma OAI.BinaryCoordinateSweeps.complexLine_average line 19
4. theorem OAI.BinaryCoordinateSweeps.binary_line_disk line 31
5. theorem OAI.BinaryCoordinateSweeps.binary_lines_disk line 52