OAI/Probability/BinarySweep/SparseBounds/SparseSignGeometry.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.BinaryCoordinateSweeps.exists_untouched_lineline 13 - lemma
OAI.BinaryCoordinateSweeps.signed_path_weight_zero_sparseline 22 - lemma
OAI.BinaryCoordinateSweeps.two_outside_embeddingline 29 - lemma
OAI.BinaryCoordinateSweeps.exists_line_two_freeline 41 - lemma
OAI.BinaryCoordinateSweeps.signed_path_weight_zero_fewline 67