SecondCounts.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.SecondTransfer.label_eq_source_iff line 12
Source documentation
A source occurrence lies in exactly one nonzero row and beyond its already-transferred prefix.
```
theorem label_eq_source_iff {r b : ℕ} (k : Fin r → ℕ)
    (i : Fin r) (p : Fin (r+1) × Fin b) :
    label k p = some i.succ ↔ p.1 = i.succ ∧ k i ≤ p.2.val := by
…
```
Mentions: OAI.Problem346.SecondTransfer.label
theorem OAI.Problem346.SecondTransfer.sum_fin_ite_lt line 23
theorem OAI.Problem346.SecondTransfer.sum_fin_ite_le line 36

theorem OAI.Problem346.SecondTransfer.source_occurrences line 52

Source documentation

Number of occurrences of the still-independent vector in row i.

theorem source_occurrences {r b : ℕ} (k : Fin r → ℕ)
    (hk : ∀ i, k i ≤ b) (i : Fin r) :
    (∑ p : Fin (r+1) × Fin b, if label k p = some i.succ then 1 else 0) = b-k i := by
…

Mentions: OAI.Problem346.SecondTransfer.label

theorem OAI.Problem346.SecondTransfer.destination_occurrences line 73
Source documentation
Number of occurrences of the shared destination vector.
```
theorem destination_occurrences {r b : ℕ} (k : Fin r → ℕ)
    (hk : ∀ i, k i ≤ b) :
    (∑ p : Fin (r+1) × Fin b, if label k p = none then 1 else 0) = ∑ i, k i := by
…
```
Mentions: OAI.Problem346.SecondTransfer.label

theorem OAI.Problem346.SecondTransfer.source_card line 88

Source documentation

Cardinality version of the source occurrence formula.

theorem source_card {r b : ℕ} (k : Fin r → ℕ)
    (hk : ∀ i, k i ≤ b) (i : Fin r) :
    (Finset.univ.filter (fun p : Fin (r+1) × Fin b => label k p = some i.succ)).card =
      b-k i := by
…

Mentions: OAI.Problem346.SecondTransfer.label

theorem OAI.Problem346.SecondTransfer.destination_card line 97

Source documentation

Cardinality version of the destination occurrence formula.

theorem destination_card {r b : ℕ} (k : Fin r → ℕ)
    (hk : ∀ i, k i ≤ b) :
    (Finset.univ.filter (fun p : Fin (r+1) × Fin b => label k p = none)).card =
      ∑ i, k i := by
…

Mentions: OAI.Problem346.SecondTransfer.label

theorem OAI.Problem346.SecondTransfer.source_degree_gt_destination line 107
Source documentation
At every unfinished row, the quadratic threshold makes the source degree strictly larger than the accumulated shared-destination degree.
```
theorem source_degree_gt_destination {r b : ℕ} (k : Fin r → ℕ)
    (hb : r * (r+1) ≤ b) (hk : ∀ j, k j ≤ r)
    (i : Fin r) (hi : k i < r) :
    (∑ j, k j) < b - k i := by
…
```

theorem OAI.Problem346.SecondTransfer.destination_occurrences_lt_source line 120

Source documentation

The actual occurrence counts satisfy the positive-weight hypothesis used to cancel a shift at any unfinished row.

theorem destination_occurrences_lt_source {r b : ℕ} (k : Fin r → ℕ)
    (hb : r * (r+1) ≤ b) (hk : ∀ j, k j ≤ r)
    (i : Fin r) (hi : k i < r) :
    (∑ p : Fin (r+1) × Fin b, if label k p = none then 1 else 0) <
      ∑ p : Fin (r+1) × Fin b, if label k p = some i.succ then 1 else 0 := by
…

Mentions: OAI.Problem346.SecondTransfer.label