OAI/Combinatorics/EditApproximation/Geometry/LocalFinalAccuracy.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The final fresh bounded-key local query, following the actual local median schedule, has the required approximation probability. The incoming law is supplied by the concrete coarse sampler in the final theorem.

  1. abbrev OAI.EditApproximation.LocalFinalProgramDraw line 30
  2. def OAI.EditApproximation.localFinalProgramDrawLaw line 34
  3. instance OAI.EditApproximation.localFinalProgramDrawLaw_probability line 39
  4. def OAI.EditApproximation.localFinalProgramValue line 44
  5. abbrev OAI.EditApproximation.LocalFinalProgramOutcome line 50
  6. def OAI.EditApproximation.localFinalProgramLaw line 53
  7. instance OAI.EditApproximation.localFinalProgramLaw_probability line 59
  8. def OAI.EditApproximation.localFinalProgramAnswer line 64
  9. theorem OAI.EditApproximation.localFinalProgramAnswer_equal line 71
  10. theorem OAI.EditApproximation.localFinalProgramValue_eq line 78
  11. theorem OAI.EditApproximation.localFinalProgram_accuracy line 103
  12. def OAI.EditApproximation.localWholeFinalAnswer line 204
  13. theorem OAI.EditApproximation.localWholeFinalAnswer_equal line 209
  14. theorem OAI.EditApproximation.local_physical_conditional_accuracy line 225