OAI/Combinatorics/EditApproximation/Refinement/PhysicalScalarFamilyLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Regrouping the finite physical scalar source gives exactly one fresh common draw for each pass and copy. This is equality of product laws, not an assumption about the sampler.

  1. theorem OAI.EditApproximation.finite_pi_product_curry line 13
  2. def OAI.EditApproximation.physicalFamilyLaw line 47
  3. instance OAI.EditApproximation.physicalFamilyLaw_probability line 51
  4. def OAI.EditApproximation.physicalFamilyCurry line 56
  5. theorem OAI.EditApproximation.physicalFamilyCurry_law line 62
  6. def OAI.EditApproximation.physicalFamilyPack line 84
  7. theorem OAI.EditApproximation.physicalFamilyPack_law line 90