OAI/Combinatorics/EditApproximation/Refinement/PhysicalProgramAccuracy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Expected root-excess accuracy of the finite selection program under finite Bernstein bounds.

  1. theorem OAI.EditApproximation.physicalProgramNodeCoefficient_nonneg line 13
  2. theorem OAI.EditApproximation.physicalProgram_expected_root_excess line 52

    Source documentation

    A pass of the actual rational recurrence has expected positive root error at most the actual edit cost divided by the computed small logarithm.

    theorem physicalProgram_expected_root_excess :
    (∫ draw : Draw, max ((physicalRefinement source target U N P ell A T delta (choices draw)
      (Sigma.mk (Fin.mk 0 (Nat.zero_lt_succ J)) PUnit.unit : PhysicalNode M J) S rootQ : ℝ) -
        stateEditCost source target rootQ) 0 ∂globalLaw) ≤
      (1 / (ell : ℝ)) * stateEditCost source target rootQ := by
…

    Mentions: OAI.EditApproximation.physicalRefinement, OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.stateEditCost