BlockPartition.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.blockLengths line 9
Source documentation
Full blocks followed by one possible shorter final block.
```
def blockLengths (n t : ℕ) : List ℕ :=
…
```
theorem OAI.Problem335.blockLengths_sum line 12
theorem OAI.Problem335.blockLengths_pos line 19
theorem OAI.Problem335.blockLengths_le line 31
theorem OAI.Problem335.blockLengths_length line 42
def OAI.Problem335.consecutiveBlocks line 63
Source documentation
Consecutive blocks, with their lengths prescribed explicitly.
```
def consecutiveBlocks {α : Type*} (t : ℕ) (l : List α) : List (List α) :=
…
```
theorem OAI.Problem335.consecutiveBlocks_flatten line 66
theorem OAI.Problem335.consecutiveBlocks_map_length line 71
theorem OAI.Problem335.consecutiveBlocks_length line 76
theorem OAI.Problem335.consecutiveBlocks_length_pos line 81
theorem OAI.Problem335.consecutiveBlocks_length_le line 87
theorem OAI.Problem335.consecutiveBlocks_nonempty line 93
theorem OAI.Problem335.consecutiveBlocks_prod line 99
theorem OAI.Problem335.consecutiveBlocks_map_prod line 103
def OAI.Problem335.layerBlocks line 113
Source documentation
The consecutive blocks of the matrix-layer index list.
```
def layerBlocks (n t : ℕ) : List (List (Fin n)) :=
…
```
theorem OAI.Problem335.layerBlocks_flatten line 116
theorem OAI.Problem335.layerBlocks_length line 120
theorem OAI.Problem335.layerBlocks_length_pos line 128
theorem OAI.Problem335.layerBlocks_length_le line 132
theorem OAI.Problem335.layerBlocks_nonempty line 136
theorem OAI.Problem335.layerBlocks_get_length_pos line 140
theorem OAI.Problem335.layerBlocks_get_length_le line 144
theorem OAI.Problem335.layerBlocks_sum_lengths line 148
theorem OAI.Problem335.layerBlocks_map_prod line 152

theorem OAI.Problem335.imm_eq_layerBlocks line 157

Source documentation

The entry defining IMM can be computed from the consecutive block products.

theorem imm_eq_layerBlocks (K : Type*) [CommSemiring K] {n : ℕ} (hn : 0 < n) (t : ℕ) :
    imm K n =
      (((layerBlocks n t).map (fun b : List (Fin n) => (b.map (immLayer K n)).prod)).prod)
        ⟨0, hn⟩ ⟨0, hn⟩ := by
…

Mentions: OAI.Problem335.imm, OAI.Problem335.layerBlocks, OAI.Problem335.immLayer

theorem OAI.Problem335.layerBlocks_power_sum_le line 165

Source documentation

The block-expansion lower-product gate budget.

theorem layerBlocks_power_sum_le {n t : ℕ} (hn : 0 < n) (ht : 0 < t) :
    ((layerBlocks n t).map (fun b => n ^ (b.length + 1))).sum ≤
      ceilDiv n t * n ^ (t + 1) := by
…

Mentions: OAI.Problem335.layerBlocks, OAI.Problem335.ceilDiv