ComputedCoarseHistorySpace.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EditApproximation.physicalCoarseHistoryEntry line 12

theorem OAI.EditApproximation.physicalCoarseHistoryEntry_fits line 19

Source documentation

The complete indexed history of each call fits the reserved capacity.

theorem physicalCoarseHistoryEntry_fits {M J : ℕ} :
    ∀ᶠ N : ℕ in atTop, ∀ B : ℕ, ∀ (_hB : NeZero B),
      ∀ (source target : List ℕ) (depth : PhysicalEntry M J target.length → ℕ),
      B = (integerParameters N).B →
      (∀ entry, depth entry = computedCoarseDepth N
        (coarseEntryWidth (physicalSource source entry.1) (substring target entry.2.lo entry.2.hi))) →
      source.length + target.length ≤ N →
      ∀ (draw : PhysicalCoarseDraw source target B depth) (entry : PhysicalEntry M J target.length),
        physicalCoarseHistoryEntry source target N depth draw entry ≤ (N + 2) ^ 37 := by
…

Mentions: OAI.EditApproximation.PhysicalEntry, OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.physicalSource, OAI.EditApproximation.substring, OAI.EditApproximation.PhysicalCoarseDraw, OAI.EditApproximation.physicalCoarseHistoryEntry

theorem OAI.EditApproximation.computedFamilyCoarseArrayCapacity_eq line 42
Source documentation
Reserve a complete-history buffer at each actual coarse cache miss. This conservatively retains those buffers until the memo run finishes.
```
theorem computedFamilyCoarseArrayCapacity_eq (source target : List ℕ) (N : ℕ)
    (input : ComputedFamilyInput source target N) :
    computedFamilyCoarseArrayCapacity source target N input =
      ((computedFamilyResult source target N input).freshKeys.map
        (coarseHistoryKeyCost (fun _ => (N + 2) ^ 37))).sum :=
…
```
Mentions: OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.computedFamilyCoarseArrayCapacity, OAI.EditApproximation.computedFamilyResult, OAI.EditApproximation.coarseHistoryKeyCost
theorem OAI.EditApproximation.computedFamilyCoarseArrayCapacity_bound line 49
theorem OAI.EditApproximation.computedFamilyCoarseArrayCapacity_polynomial line 56