BackgroundAllocation.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Executable background allocation and its entropy error

def OAI.LowSpaceSubsetSum.binomialBits line 11
Source documentation
The implementation computes the bit length of a positive binomial count.
```
def binomialBits (m k : ℕ) : ℕ := (m.choose k).log2
```
theorem OAI.LowSpaceSubsetSum.binomialBits_eq_floor line 13
theorem OAI.LowSpaceSubsetSum.binomialBits_entropy_error line 18
def OAI.LowSpaceSubsetSum.allocateLeft line 26
Source documentation
Signed arithmetic prevents truncation before the final division.
```
def allocateLeft (r a b : ℕ) : ℕ := (((r : ℤ) + b - a) / 2).toNat
```
def OAI.LowSpaceSubsetSum.allocateRight line 28
theorem OAI.LowSpaceSubsetSum.allocateLeft_eq_floor line 30
theorem OAI.LowSpaceSubsetSum.allocation_feasible line 40
theorem OAI.LowSpaceSubsetSum.allocateLeft_error line 50
Source documentation
Integer division contributes less than one to each balancing step.
```
theorem allocateLeft_error (r a b : ℕ) (ha : a ≤ r + b) :
    |(allocateLeft r a b : ℝ) - ((r : ℝ) + b - a) / 2| < 1 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.allocateLeft

theorem OAI.LowSpaceSubsetSum.allocateLeft_entropy_error line 62

Source documentation

One balancing step converts bit-length errors into an allocation error.

theorem allocateLeft_entropy_error (r a b : ℕ) (ha : a ≤ r + b)
    {A B e : ℝ} (haE : |(a : ℝ) - A| ≤ e) (hbE : |(b : ℝ) - B| ≤ e) :
    |(allocateLeft r a b : ℝ) - ((r : ℝ) / 2 + (B - A) / 2)| < e + 1 := by
…

Mentions: OAI.LowSpaceSubsetSum.allocateLeft

theorem OAI.LowSpaceSubsetSum.allocateRight_entropy_error line 71

theorem OAI.LowSpaceSubsetSum.binomial_allocation_error line 81

Source documentation

The manuscript's executable binomial balancing, with an explicit logarithmic error.

theorem binomial_allocation_error (r m k l : ℕ) (hk : k ≤ m) (hl : l ≤ m)
    (ha : binomialBits m k ≤ r + binomialBits m l)
    (hb : binomialBits m l ≤ r + binomialBits m k) :
    let A := (m : ℝ) * binaryEntropy ((k : ℝ) / m)
…

Mentions: OAI.LowSpaceSubsetSum.binomialBits, OAI.LowSpaceSubsetSum.binaryEntropy

theorem OAI.LowSpaceSubsetSum.allocation_feasible_of_difference line 98
Source documentation
A sufficient, symmetric feasibility test computed from the two bit lengths.
```
theorem allocation_feasible_of_difference (r a b : ℕ)
    (h : |(b : ℤ) - a| ≤ r) :
    allocateLeft r a b ≤ r ∧ allocateLeft r a b + allocateRight r a b = r := by
…
```
Mentions: OAI.LowSpaceSubsetSum.allocateLeft, OAI.LowSpaceSubsetSum.allocateRight
theorem OAI.LowSpaceSubsetSum.binomialBits_difference line 104
theorem OAI.LowSpaceSubsetSum.allocated_sides_lower line 122
Source documentation
Either parent's background size is bounded from below by the imbalance bound, with only the single integer-rounding loss.
```
theorem allocated_sides_lower (r a b : ℕ) {d : ℝ}
    (hd : |(b : ℝ) - a| ≤ d) (hdr : d ≤ r) :
    (r : ℝ) / 2 - d / 2 - 1 < allocateLeft r a b ∧
    (r : ℝ) / 2 - d / 2 - 1 < allocateRight r a b := by
…
```
Mentions: OAI.LowSpaceSubsetSum.allocateLeft, OAI.LowSpaceSubsetSum.allocateRight
def OAI.LowSpaceSubsetSum.leafBackgroundSize line 139
Source documentation
The two leaves split each child's background with at most half an item of error, because the remainder is assigned to the second leaf.
```
def leafBackgroundSize (r : ℕ) (i : Fin 2) : ℕ := if i = 0 then r / 2 else r - r / 2
```
theorem OAI.LowSpaceSubsetSum.leafBackgroundSize_sum line 141
theorem OAI.LowSpaceSubsetSum.leafBackgroundSize_error line 146

theorem OAI.LowSpaceSubsetSum.allocation_error_compose line 164

Source documentation

Replacing the current total by its ideal value costs half the previous error. This is the two-level substitution used in the leaf-size estimate.

theorem allocation_error_compose (r a b : ℕ) (ha : a ≤ r + b)
    {ideal A B e0 e1 : ℝ} (hr : |(r : ℝ) - ideal| ≤ e0)
    (hA : |(a : ℝ) - A| ≤ e1) (hB : |(b : ℝ) - B| ≤ e1) :
    |(allocateLeft r a b : ℝ) - (ideal / 2 + (B - A) / 2)| < e0 / 2 + e1 + 1 := by
…

Mentions: OAI.LowSpaceSubsetSum.allocateLeft

theorem OAI.LowSpaceSubsetSum.leaf_error_compose line 173