OAI/Combinatorics/EditApproximation/Geometry/LocalCommonOutput.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The charged memo answer under one common random source per pass and one fresh terminal source. Correct marginal laws suffice; hypothetical seed-indexed draw families are not part of the execution.

  1. abbrev OAI.EditApproximation.LocalCommonTerminalDraw line 27
  2. def OAI.EditApproximation.localCommonTerminalLaw line 30
  3. instance OAI.EditApproximation.localCommonTerminalLaw_probability line 34
  4. def OAI.EditApproximation.localCommonTerminalSample line 39
  5. theorem OAI.EditApproximation.localCommonTerminalSample_law line 48
  6. abbrev OAI.EditApproximation.LocalCommonFinalOutcome line 57
  7. def OAI.EditApproximation.localCommonFinalLaw line 61
  8. instance OAI.EditApproximation.localCommonFinalLaw_probability line 66
  9. def OAI.EditApproximation.localCommonFinalToTrace line 71
  10. def OAI.EditApproximation.localCommonMemoAnswer line 77
  11. theorem OAI.EditApproximation.localCommonMemoAnswer_eq line 84
  12. theorem OAI.EditApproximation.localCommonMemoAnswer_law line 95
  13. theorem OAI.EditApproximation.localCommonMemoAnswer_event line 137