OAI/Combinatorics/EditApproximation/Geometry/SourceRankedProgram.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Random source coordinates and recursive table entries share the same memo evaluator. Source coordinates have rank zero; each table rank is shifted by one. Consequently repeated source reads reuse their stored draw.

  1. def OAI.EditApproximation.SourceRanked.value line 24
  2. theorem OAI.EditApproximation.SourceRanked.body_value line 27
  3. theorem OAI.EditApproximation.SourceRanked.program_value line 45
  4. theorem OAI.EditApproximation.SourceRanked.memo_value line 54