BinomialIndex.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExternalTensor.Binomial.Branch line 11
Source documentation
A branch records the choices of the two summands during iteration.
```
def Branch : ℕ → Type
  | 0 => Unit
  | n + 1 => Branch n ⊕ Branch n
```
instance OAI.ExternalTensor.Binomial.branchFintype line 15
def OAI.ExternalTensor.Binomial.weight line 19
theorem OAI.ExternalTensor.Binomial.weight_le line 24
def OAI.ExternalTensor.Binomial.zeroFiber line 30
Source documentation
The left branch has weight zero exactly when the old branch does.
```
def zeroFiber (n : ℕ) : {x : Branch (n+1) // weight x = 0} ≃
    {x : Branch n // weight x = 0} where
…
```
Mentions: OAI.ExternalTensor.Binomial.Branch, OAI.ExternalTensor.Binomial.weight
def OAI.ExternalTensor.Binomial.succFiber line 43
Source documentation
The two disjoint ways to achieve weight q+1 give Pascal's recurrence.
```
def succFiber (n q : ℕ) : {x : Branch (n+1) // weight x = q+1} ≃
    ({x : Branch n // weight x = q+1} ⊕ {x : Branch n // weight x = q}) where
…
```
Mentions: OAI.ExternalTensor.Binomial.Branch, OAI.ExternalTensor.Binomial.weight
theorem OAI.ExternalTensor.Binomial.card_weight line 54
def OAI.ExternalTensor.Binomial.degree line 74
def OAI.ExternalTensor.Binomial.degreeFiber line 76
def OAI.ExternalTensor.Binomial.fiberFin line 80
def OAI.ExternalTensor.Binomial.groupEquiv line 86
Source documentation
Group branches by their weight, with the binomial coefficient as the exact fiber size.
```
def groupEquiv (n : ℕ) : Branch n ≃ Σ q : Fin (n+1), Fin (Nat.choose n q.val) :=
…
```
Mentions: OAI.ExternalTensor.Binomial.Branch
theorem OAI.ExternalTensor.Binomial.groupEquiv_fst line 89