BackgroundDomains.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A concrete ordered partition of the background indices

def OAI.LowSpaceSubsetSum.eightLeafCounts line 14
Source documentation
Four children, each split into its two consecutive leaf parts.
```
def eightLeafCounts (a b c d : ℕ) : Fin 8 → ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.eightLeafCounts_sum line 20
def OAI.LowSpaceSubsetSum.computedLeafCounts line 31
Source documentation
The exact two-level integer allocations in the implementation.
```
def computedLeafCounts (r a0 b0 aL bL aR bR : ℕ) : Fin 8 → ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.computedLeafCounts_sum line 37
def OAI.LowSpaceSubsetSum.backgroundIndexEquiv line 50
Source documentation
Successive blocks in the sorted outside domain, with the prescribed eight sizes. The library equivalence uses prefix sums of these sizes.
```
def backgroundIndexEquiv {n : ℕ} (V : Finset (Fin n)) (c : Fin 8 → ℕ)
    (hc : ∑ i, c i = V.card) : ↥V ≃ ((i : Fin 8) × Fin (c i)) :=
…
```
def OAI.LowSpaceSubsetSum.backgroundColor line 54
theorem OAI.LowSpaceSubsetSum.backgroundColor_card line 58
def OAI.LowSpaceSubsetSum.backgroundPairColor line 93
Source documentation
The eight linear labels are the two parents and four leaves of the table.
```
def backgroundPairColor {n : ℕ} (V : Finset (Fin n)) (c : Fin 8 → ℕ)
    (hc : ∑ i, c i = V.card) (x : Fin n) : Fin 2 × Fin 4 :=
…
```
theorem OAI.LowSpaceSubsetSum.backgroundPairColor_eq_iff line 99
theorem OAI.LowSpaceSubsetSum.backgroundPairColor_card line 110