CountedBinomial.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Constant-state multiplicative binomial computation

Each iteration uses one multiplication and one exact division. The three state fields and the division numerator have linearly bounded bit lengths.

structure OAI.LowSpaceSubsetSum.CountedBinomial.State line 14
def OAI.LowSpaceSubsetSum.CountedBinomial.initial line 19
def OAI.LowSpaceSubsetSum.CountedBinomial.step line 21
def OAI.LowSpaceSubsetSum.CountedBinomial.runAcc line 24
def OAI.LowSpaceSubsetSum.CountedBinomial.run line 28
theorem OAI.LowSpaceSubsetSum.CountedBinomial.recurrence line 31
theorem OAI.LowSpaceSubsetSum.CountedBinomial.step_value line 36
theorem OAI.LowSpaceSubsetSum.CountedBinomial.runAcc_index line 41
theorem OAI.LowSpaceSubsetSum.CountedBinomial.runAcc_steps line 48
theorem OAI.LowSpaceSubsetSum.CountedBinomial.runAcc_value line 55
theorem OAI.LowSpaceSubsetSum.CountedBinomial.run_value line 63
theorem OAI.LowSpaceSubsetSum.CountedBinomial.run_steps line 70
theorem OAI.LowSpaceSubsetSum.CountedBinomial.step_divides line 78
Source documentation
The division numerator is exactly divisible by the current index.
```
theorem step_divides (n : ℕ) (s : State) (h : s.value = n.choose s.index) :
    s.index + 1 ∣ s.value * (n - s.index) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.CountedBinomial.State
theorem OAI.LowSpaceSubsetSum.CountedBinomial.value_bound line 83
theorem OAI.LowSpaceSubsetSum.CountedBinomial.numerator_bound line 88
theorem OAI.LowSpaceSubsetSum.CountedBinomial.prefix_bounds line 98
Source documentation
This bounds every intermediate prefix state of the multiplicative loop, not only its final returned value.
```
theorem prefix_bounds (n k j : ℕ) (hj : j ≤ k) (hk : k ≤ n) :
    let s := runAcc n j initial
…
```
Mentions: OAI.LowSpaceSubsetSum.CountedBinomial.runAcc, OAI.LowSpaceSubsetSum.CountedBinomial.initial