OAI/Probability/BinarySweep/FiniteLaws/IndependentPush.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.BinaryCoordinateSweeps.finitePushline 13 - lemma
OAI.BinaryCoordinateSweeps.finitePush_piline 17 - lemma
OAI.BinaryCoordinateSweeps.finitePush_expectationline 28 - lemma
OAI.BinaryCoordinateSweeps.independentPush_expectationline 40