LeafAllocationBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Quantitative leaf entropy after both integer allocations

def OAI.LowSpaceSubsetSum.allocateSide line 12
Source documentation
A Boolean selects the two complementary allocations without changing the fixed remainder convention.
```
def allocateSide (right : Bool) (r a b : ℕ) : ℕ :=
…
```
def OAI.LowSpaceSubsetSum.idealSide line 15
theorem OAI.LowSpaceSubsetSum.allocateSide_error line 18

theorem OAI.LowSpaceSubsetSum.allocated_leaf_entropy_bound line 28

Source documentation

The error of a two-level allocation followed by the leaf split is small uniformly in the parent/child orientations.

theorem allocated_leaf_entropy_bound (parent child : Bool) (leaf : Fin 2)
    (r a0 b0 a1 b1 : ℕ) {A0 B0 A1 B1 e : ℝ}
    (h0a : a0 ≤ r + b0) (h0b : b0 ≤ r + a0)
    (h1a : a1 ≤ allocateSide parent r a0 b0 + b1)
    (h1b : b1 ≤ allocateSide parent r a0 b0 + a1)
    (hA0 : |(a0 : ℝ) - A0| ≤ e) (hB0 : |(b0 : ℝ) - B0| ≤ e)
    (hA1 : |(a1 : ℝ) - A1| ≤ e) (hB1 : |(b1 : ℝ) - B1| ≤ e)
    {top localPart : ℝ}
    (htop : top ≤ (if parent then B0 else A0) / 4 + 3)
    (hlocal : localPart ≤ (if child then B1 else A1) / 2 + 3) :
    top + localPart + (leafBackgroundSize
      (allocateSide child (allocateSide parent r a0 b0) a1 b1) leaf : ℝ) ≤
…

Mentions: OAI.LowSpaceSubsetSum.allocateSide, OAI.LowSpaceSubsetSum.leafBackgroundSize

theorem OAI.LowSpaceSubsetSum.allocated_leaf_error_absorbed line 51
Source documentation
Once the input scale dominates the domain size, the ten-power leaf cap absorbs the explicit allocation and rounding errors.
```
theorem allocated_leaf_error_absorbed {u m : ℝ} (hu : 2 ≤ u) (hm : 0 ≤ m)
    (hmu : m + 1 ≤ u) :
    (3 / 4 : ℝ) * (Real.logb 2 (m + 1) + 1) + 29 / 4 ≤ Real.logb 2 (u ^ 10) := by
…
```

theorem OAI.LowSpaceSubsetSum.rounded_leaf_component line 66

Source documentation

A prescribed integer count within one of its ideal count changes its weighted entropy by at most three.

theorem rounded_leaf_component {b : ℕ} {k p : ℝ} (hb : 24 ≤ b)
    (hp : p ∈ Set.Icc (1 / 6) (1 / 3)) (hk : |k - (b : ℝ) * p| ≤ 1) :
    (b : ℝ) * binaryEntropy (k / b) ≤ (b : ℝ) * binaryEntropy p + 3 := by
…

Mentions: OAI.LowSpaceSubsetSum.binaryEntropy