OAI/Combinatorics/EditApproximation/Geometry/CommonArrayFinal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A final independent draw may be stored as the last array row. These maps expose the literal product law used by the scheduled seed passes.

  1. def OAI.EditApproximation.commonArrayFinal line 14
  2. def OAI.EditApproximation.commonFinalArray line 18
  3. theorem OAI.EditApproximation.commonArrayFinal_inverse line 23
  4. theorem OAI.EditApproximation.commonFinalArray_inverse line 32
  5. theorem OAI.EditApproximation.commonArrayFinal_law line 48
  6. def OAI.EditApproximation.mapCommonTrace line 75
  7. theorem OAI.EditApproximation.mapCommonTrace_array line 80
  8. theorem OAI.EditApproximation.mapCommonTrace_law line 98