OAI/Combinatorics/EditApproximation/Refinement/PhysicalFinalAccuracy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Accuracy of the final fresh refinement after adaptive median seed passes, under finite Bernstein bounds and an explicit incoming seed failure bound.

  1. abbrev OAI.EditApproximation.FinalProgramDraw line 28
  2. def OAI.EditApproximation.finalProgramDrawLaw line 32
  3. instance OAI.EditApproximation.finalProgramDrawLaw_probability line 37
  4. def OAI.EditApproximation.finalProgramValue line 42
  5. abbrev OAI.EditApproximation.FinalProgramOutcome line 49
  6. def OAI.EditApproximation.finalProgramLaw line 51
  7. instance OAI.EditApproximation.finalProgramLaw_probability line 57
  8. def OAI.EditApproximation.finalProgramAnswer line 64

    Source documentation

    Equality is tested before the final query, so equal strings return zero on every execution, including executions with a bad seed.

    noncomputable def finalProgramAnswer (rootQ : TargetInterval target.length)
    (pair : FinalProgramOutcome (M := M) (J := J) (R := R) source target N P T H) : ℕ :=
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.FinalProgramOutcome

  9. theorem OAI.EditApproximation.finalProgramAnswer_equal line 70
  10. theorem OAI.EditApproximation.finalProgram_accuracy line 87