FirstCounts.lean`

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.firstLabel_zero line 9
theorem OAI.Problem346.firstLabel_succ line 14
theorem OAI.Problem346.firstLabel_zero_ne_x line 19
theorem OAI.Problem346.firstLabel_zero_eq_t_iff line 24
theorem OAI.Problem346.firstLabel_zero_eq_y_iff line 30
def OAI.Problem346.firstLabelCount line 46
Source documentation
Number of individual factors labelled by a given vector block.
```
def firstLabelCount (r m k : ℕ) (c : FirstBlock m) : ℕ :=
…
```
Mentions: OAI.Problem346.FirstBlock
theorem OAI.Problem346.firstLabelCount_x line 50
theorem OAI.Problem346.firstLabelCount_t line 61
theorem OAI.Problem346.firstLabelCount_y line 80
theorem OAI.Problem346.firstLabel_step line 100
theorem OAI.Problem346.firstLabel_card line 127
Source documentation
The sum-of-indicators count agrees with the cardinality used by polynomial block-degree statements.
```
theorem firstLabel_card (r m k : ℕ) (c : FirstBlock m) :
    (Finset.univ.filter (fun p => firstLabel r m k p = c)).card =
      firstLabelCount r m k c := by
…
```
Mentions: OAI.Problem346.FirstBlock, OAI.Problem346.firstLabel, OAI.Problem346.firstLabelCount
theorem OAI.Problem346.firstLabel_card_t line 133
theorem OAI.Problem346.firstLabel_card_y line 137
theorem OAI.Problem346.firstLabel_card_y_next line 142
theorem OAI.Problem346.firstLabel_eq_t_iff line 148
Source documentation
Only unreplaced positions of the distinguished row carry the source label.
```
theorem firstLabel_eq_t_iff (r m k : ℕ) (hk : k ≤ m)
    (p : Fin (r + 1) × Fin (r + m)) :
    firstLabel r m k p = some none ↔ p.1 = 0 ∧ k ≤ p.2.val := by
…
```
Mentions: OAI.Problem346.firstLabel