OAI/Combinatorics/EditApproximation/Refinement/PhysicalScalarFamily.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite independent scalar sources for all passes and copies. The incoming seed selects the range only after the earlier passes are evaluated.

  1. def OAI.EditApproximation.physicalFamilyDraw line 28
  2. def OAI.EditApproximation.physicalFamilySample line 38
  3. def OAI.EditApproximation.physicalFamilySeed line 45
  4. def OAI.EditApproximation.physicalFamilyGroup line 54
  5. def OAI.EditApproximation.physicalFamilyInteger line 59
  6. theorem OAI.EditApproximation.physicalFamilySeed_eq line 69
  7. theorem OAI.EditApproximation.physicalFamilyGroupRead_value line 83
  8. theorem OAI.EditApproximation.physicalFamilyOnlineRead_value line 92