OAI/Combinatorics/EditApproximation/Geometry/ChargedRandomMemo.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The charged evaluator actually caches random source coordinates and physical entries in one rank-decreasing memo computation.

  1. theorem OAI.EditApproximation.chargedRandomMemoEvaluate_value line 27