OAI/Combinatorics/EditApproximation/Refinement/ComputedCoarseBits.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.coarseEncoding_scalar line 10
2. theorem OAI.EditApproximation.computedCoarse_root_encoding_bits line 34

   Source documentation

   Every root cell of every computed coarse call has polynomial bit width, without conditioning on the accuracy event or on its threshold labels.

    theorem computedCoarse_root_encoding_bits :
       ∀ᶠ N : ℕ in atTop, ∀ B d n k : ℕ,
         B = (integerParameters N).B → d = computedCoarseDepth N n →
         n ≤ N → k ≤ 2 * (N + 2) →
         ∀ {α : Type} [DecidableEq α] (frame : List (Option α))
           (tree : CoarseSourceTree B α d) (draws : CoarseThresholdDraws B d),
           tree.word.length ≤ N → ∀ start shift,
         rationalEncodingBits (coarseThresholdEstimate k (initialThresholdQ N) (initialLambda N)
           frame tree draws k start shift) ≤ inputHeight N ^ 3 := by
   …

   Mentions: OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.rationalEncodingBits, OAI.EditApproximation.coarseThresholdEstimate, OAI.EditApproximation.initialThresholdQ, OAI.EditApproximation.initialLambda, OAI.EditApproximation.inputHeight