PhysicalFamilyAccuracy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite family is consumed through actual source reads in the shared memo evaluator. Its final value and law agree with the proved local answer.

theorem OAI.EditApproximation.physicalFamilyMemoAnswer_event line 33

theorem OAI.EditApproximation.physicalFamilyMemoAnswer_conditional_accuracy line 52

Source documentation

Accuracy of the shared source/table memo evaluator under finite Bernstein bounds.

 theorem physicalFamilyMemoAnswer_conditional_accuracy (hP : 0 < P) (hH : 0 < H) (bits : ℕ)
    (encode : Sum Key Table → ℕ) (hinjective : Function.Injective encode)
    (hbounded : ∀ key, encode key < 2 ^ bits)
    (hN : 0 < N) (hell : 2 ^ 1000 ≤ inputSmallLog N)
    (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.inputSmallLog, OAI.EditApproximation.integerParameters, OAI.EditApproximation.intervalTreeDepth, OAI.EditApproximation.inputHeight, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.physicalSource, OAI.EditApproximation.substring, OAI.EditApproximation.FiniteBernsteinInput