OAI/Combinatorics/EditApproximation/Probability/FiniteProductWork.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The executed sampler law supports both selected rejection work and work depending only on the accepted finite draws.

  1. theorem OAI.EditApproximation.finite_outer_integrable line 11
  2. theorem OAI.EditApproximation.finite_outer_expected_le line 20
  3. def OAI.EditApproximation.rejectionProductAccepted line 38
  4. theorem OAI.EditApproximation.rejectionProductAccepted_measurable line 42
  5. theorem OAI.EditApproximation.rejectionProductAccepted_law line 46
  6. theorem OAI.EditApproximation.rejectionProductWork_integral line 54
  7. theorem OAI.EditApproximation.rejectionProductWork_expected_le line 62