OAI/Combinatorics/EditApproximation/Refinement/PhysicalUniformAccuracy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.physicalLargeInput_eventually line 21

   Source documentation

   Every test is on a bounded word prefix or on the computed input parameters. Rejected inputs use the exact suffix dynamic program.

    theorem physicalLargeInput_eventually (epsilon : BinaryFraction) (hepsilon : 0 < epsilon.value) :
       ∀ᶠ N in atTop, physicalLargeInput N epsilon := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.physicalLargeInput

2. abbrev OAI.EditApproximation.PhysicalUniformOutcome line 41
3. instance OAI.EditApproximation.physicalUniformOutcome_measurableSingleton line 44
4. def OAI.EditApproximation.physicalUniformLaw line 50
5. instance OAI.EditApproximation.physicalUniformLaw_probability line 57
6. def OAI.EditApproximation.physicalUniformAnswer line 63
7. theorem OAI.EditApproximation.physicalUniformAnswer_equal line 71
8. theorem OAI.EditApproximation.physical_uniform_conditional_accuracy line 86

   Source documentation

   Uniform correctness of the memo evaluator driven by rejection trials, under finite Bernstein bounds for coarse and group coordinates.

   theorem physical_uniform_conditional_accuracy (epsilon : BinaryFraction) (hH : 0 < H) (bits : ℕ)
       (encode : Sum Key Table → ℕ)
       (hcode : physicalLargeInput N epsilon → Function.Injective encode)
       (hfits : physicalLargeInput N epsilon → ∀ key, encode key < 2 ^ bits)
       (hsize : source.length + target.length ≤ N)
       (hMeq : M = (integerParameters N).M) (hJeq : J = intervalTreeDepth M source.length)
       (hPeq : P = (integerParameters N).P) (hTeq : T = (integerParameters N).T)
       (hSeq : S = (integerParameters N).S) (hHeq : H = inputHeight N)
       (hB : B = (integerParameters N).B)
       (hdepth : ∀ state, depth state = computedCoarseDepth N
         (coarseEntryWidth (physicalSource source state.1) (substring target state.2.lo state.2.hi)))
       (coarseBernstein : FiniteBernsteinInput (Measure.pi fun _ : Fin B =>
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.physicalLargeInput, OAI.EditApproximation.integerParameters, OAI.EditApproximation.intervalTreeDepth, OAI.EditApproximation.inputHeight, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.physicalSource, OAI.EditApproximation.substring, OAI.EditApproximation.FiniteBernsteinInput