OAI/Combinatorics/EditApproximation/Geometry/CommonRangeSource.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The online draw range depends on earlier seed values. A common random source is indexed by the physical key and the requested positive range, not by an entire hypothetical seed table. The unused coordinates exist only in the probability space.

  1. theorem OAI.EditApproximation.positiveDrawRangeOfLE_val line 22
  2. abbrev OAI.EditApproximation.CommonRangeDraw line 27
  3. def OAI.EditApproximation.commonRangeLaw line 30
  4. instance OAI.EditApproximation.commonRangeLaw_probability line 35
  5. def OAI.EditApproximation.commonRangeSelectedKey line 45
  6. theorem OAI.EditApproximation.commonRangeSelectedKey_injective line 49
  7. def OAI.EditApproximation.commonRangeSample line 54
  8. theorem OAI.EditApproximation.commonRangeSample_law line 58