OAI/Combinatorics/EditApproximation/Refinement/PhysicalScalarSource.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Each common array source is realized by scalar exact uniform draws. Regrouping finite coordinates recovers the common source law; unused coordinates belong only to the probability space.

  1. theorem OAI.EditApproximation.finite_pi_curry line 16
  2. theorem OAI.EditApproximation.finite_uniform_three_curry line 26
  3. abbrev OAI.EditApproximation.PhysicalScalarDraw line 57
  4. def OAI.EditApproximation.physicalScalarLaw line 61
  5. instance OAI.EditApproximation.physicalScalarLaw_probability line 66
  6. def OAI.EditApproximation.physicalScalarCoordinatePack line 71
  7. def OAI.EditApproximation.physicalScalarPack line 80
  8. theorem OAI.EditApproximation.physicalScalarCoordinatePack_law line 89
  9. theorem OAI.EditApproximation.physicalScalarPack_law line 98
  10. theorem OAI.EditApproximation.physicalRejectionArray_pack_law line 115