OAI/Combinatorics/EditApproximation/Coarse/CoarseInitialAllocation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.arithmeticMapAllocation_with_indices_le_work line 10

   Source documentation

   Besides each result cell, reserve one index-list cell for each callback.

   theorem arithmeticMapAllocation_with_indices_le_work {α β : Type*} (f : α → β × ℕ)
       (allocation : α → ℕ) (values : List α)
       (h : ∀ a ∈ values, allocation a ≤ 2 * (f a).2) :
       arithmeticMapAllocation allocation values + values.length ≤
         2 * (arithmeticMapWithWork f values).2 := by
   …

   Mentions: OAI.EditApproximation.arithmeticMapAllocation, OAI.EditApproximation.arithmeticMapWithWork

2. def OAI.EditApproximation.BinaryFraction.coarseIndexedRootAllocation line 25
3. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedRootAllocation_le_work line 36
4. def OAI.EditApproximation.BinaryFraction.coarseIndexedCandidateAllocation line 63
5. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedCandidateAllocation_le_work line 72
6. def OAI.EditApproximation.BinaryFraction.coarseMinimumListAllocation line 90
7. theorem OAI.EditApproximation.BinaryFraction.coarseMinimumListAllocation_le_work line 94
8. def OAI.EditApproximation.BinaryFraction.coarseMinimumAllocation line 103
9. theorem OAI.EditApproximation.BinaryFraction.coarseMinimumAllocation_le_work line 107
10. def OAI.EditApproximation.BinaryFraction.coarseIndexedInitialAllocation line 116

    Source documentation

    Fresh arithmetic cells and root/index list spines. Constant words and preexisting input/cached words are shared. The retained input and output words are counted separately by the global storage capacity.

    def coarseIndexedInitialAllocation {B d : ℕ} (q L N : ℕ)
        (hB : 0 < B) (hq : 0 < q) (hL : 0 < L) (x y : List ℕ)
        (draws : CoarseGuessIndex (coarseEntryWidth x y) → CoarseThresholdDraws B d) : ℕ :=
    …

    Mentions: OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.CoarseThresholdDraws

11. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedInitialAllocation_le_work line 129
12. theorem OAI.EditApproximation.BinaryFraction.computedCoarseIndexedInitialAllocation_polynomial line 162

    Source documentation

    Every draw has polynomial scratch, including outcomes outside the success event.

    theorem computedCoarseIndexedInitialAllocation_polynomial :
        ∀ᶠ N : ℕ in atTop, ∀ B d : ℕ, ∀ x y : List ℕ,
          B = (integerParameters N).B → d = computedCoarseDepth N (coarseEntryWidth x y) →
          coarseEntryWidth x y ≤ N → (∀ a ∈ x ++ y, Nat.size a ≤ inputHeight N ^ 3) →
          ∀ (hB : 0 < B) (hq : 0 < inputHeight N ^ 4) (hL : 0 < 64 * inputHeight N)
          (draws : CoarseGuessIndex (coarseEntryWidth x y) → CoarseThresholdDraws B d),
          coarseIndexedInitialAllocation (inputHeight N ^ 4) (64 * inputHeight N) N
            hB hq hL x y draws ≤ (N + 2) ^ 181 := by
    …

    Mentions: OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.inputHeight, OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.coarseIndexedInitialAllocation