BlockPairCount.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TreeEdit.BinaryLower.card_grid_chain_le line 10
Source documentation
A componentwise chain in a rectangular integer grid has at most M + N - 1 points. This counts the block pairs visited by an increasing subsequence matching; no alignment of block boundaries is assumed.
```
theorem card_grid_chain_le (s : Finset (ℕ × ℕ)) (M N : ℕ)
    (hbound : ∀ p ∈ s, p.1 < M ∧ p.2 < N)
    (hchain : ∀ p ∈ s, ∀ q ∈ s,
      (p.1 ≤ q.1 ∧ p.2 ≤ q.2) ∨ (q.1 ≤ p.1 ∧ q.2 ≤ p.2)) :
    s.card ≤ M + N - 1 := by
…
```

theorem OAI.TreeEdit.BinaryLower.card_monotone_pair_image_le line 39

Source documentation

The distinct values attained by a componentwise monotone sequence of block indices form a short grid chain.

theorem card_monotone_pair_image_le {r M N : ℕ}
    (f g : Fin r → ℕ) (hf : Monotone f) (hg : Monotone g)
    (hfb : ∀ a, f a < M) (hgb : ∀ a, g a < N) :
    (Finset.univ.image (fun a => (f a, g a))).card ≤ M + N - 1 := by
…

theorem OAI.TreeEdit.BinaryLower.card_block_pair_image_le line 56

Source documentation

The number of block pairs visited by an increasing bit matching between words with M and N blocks of width P is at most M + N - 1.

theorem card_block_pair_image_le {r M N P : ℕ} (hP : 0 < P)
    (f g : Fin r → ℕ) (hf : Monotone f) (hg : Monotone g)
    (hfb : ∀ a, f a < M * P) (hgb : ∀ a, g a < N * P) :
    (Finset.univ.image (fun a => (f a / P, g a / P))).card ≤ M + N - 1 := by
…

theorem OAI.TreeEdit.BinaryLower.card_equal_block_pair_image_le line 71

Source documentation

In the equal-length case, at most 2 * M - 1 block pairs occur.

theorem card_equal_block_pair_image_le {r M P : ℕ} (hP : 0 < P)
    (f g : Fin r → ℕ) (hf : Monotone f) (hg : Monotone g)
    (hfb : ∀ a, f a < M * P) (hgb : ∀ a, g a < M * P) :
    (Finset.univ.image (fun a => (f a / P, g a / P))).card ≤ 2 * M - 1 := by
…

theorem OAI.TreeEdit.BinaryLower.monotone_pair_fiber_convex line 80
Source documentation
A fixed block pair occupies a consecutive portion of the matching. This is the order-convexity fact needed for its minimal spans to contain no positions matched under a different pair.
```
theorem monotone_pair_fiber_convex {ι : Type*} [Preorder ι]
    (f g : ι → ℕ) (hf : Monotone f) (hg : Monotone g)
    {a b c : ι} (hab : a ≤ b) (hbc : b ≤ c)
    (h : (f a, g a) = (f c, g c)) : (f b, g b) = (f a, g a) := by
…
```