OAI/Combinatorics/EditApproximation/Refinement/PhysicalFamilySampling.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite scalar family is exactly the accepted output of the independent literal rejection samplers. Only requested coordinates need be generated; their failure counts have a product law.

  1. theorem OAI.EditApproximation.physicalFamilyLaw_eq_rejectionAcceptedLaw line 25
  2. theorem OAI.EditApproximation.physicalFamily_rejection_runtime_law line 30
  3. theorem OAI.EditApproximation.physicalFamilyRange_bits_le line 37