MatchingSpanBudget.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TreeEdit.BinaryLower.matchingSpan line 11
Source documentation
The integer interval hull of the positions bearing one matching label. The empty fiber has empty span.
```
def matchingSpan {r n : ℕ} {β : Type*} [DecidableEq β] (f : Fin r → Fin n)
    (label : Fin r → β) (b : β) : Finset (Fin n) := by
…
```
theorem OAI.TreeEdit.BinaryLower.mem_matchingSpan line 17

theorem OAI.TreeEdit.BinaryLower.matchingSpan_contains_match line 25

Source documentation

Each matched position of a fiber belongs to its span.

theorem matchingSpan_contains_match {r n : ℕ} {β : Type*} [DecidableEq β]
    (f : Fin r → Fin n) (label : Fin r → β) {b : β} {i : Fin r}
    (hi : label i = b) : f i ∈ matchingSpan f label b :=
…

Mentions: OAI.TreeEdit.BinaryLower.matchingSpan

theorem OAI.TreeEdit.BinaryLower.matchingSpan_inter_image line 31

Source documentation

An order-convex label fiber contains every matched position in its span.

theorem matchingSpan_inter_image {r n : ℕ} {β : Type*} [DecidableEq β]
    (f : Fin r → Fin n) (hf : StrictMono f) (label : Fin r → β)
    (hc : ∀ {i j k}, i ≤ j → j ≤ k → label i = label k → label j = label i)
    (b : β) :
    matchingSpan f label b ∩ Finset.univ.image f =
      (Finset.univ.filter fun i => label i = b).image f := by
…

Mentions: OAI.TreeEdit.BinaryLower.matchingSpan

theorem OAI.TreeEdit.BinaryLower.matchingSpan_disjoint line 61

Source documentation

Distinct order-convex label fibers have disjoint interval hulls.

theorem matchingSpan_disjoint {r n : ℕ} {β : Type*} [DecidableEq β]
    (f : Fin r → Fin n) (hf : StrictMono f) (label : Fin r → β)
    (hc : ∀ {i j k}, i ≤ j → j ≤ k → label i = label k → label j = label i)
    {b c : β} (hbc : b ≠ c) :
    Disjoint (matchingSpan f label b) (matchingSpan f label c) := by
…

Mentions: OAI.TreeEdit.BinaryLower.matchingSpan

theorem OAI.TreeEdit.BinaryLower.matchingSpan_unmatched_card line 81

Source documentation

The number of unmatched positions in a span is its length minus the number of matching entries in the corresponding fiber.

theorem matchingSpan_unmatched_card {r n : ℕ} {β : Type*} [DecidableEq β]
    (f : Fin r → Fin n) (hf : StrictMono f) (label : Fin r → β)
    (hc : ∀ {i j k}, i ≤ j → j ≤ k → label i = label k → label j = label i)
    (b : β) :
    (matchingSpan f label b \ Finset.univ.image f).card =
      (matchingSpan f label b).card - (Finset.univ.filter fun i => label i = b).card := by
…

Mentions: OAI.TreeEdit.BinaryLower.matchingSpan

theorem OAI.TreeEdit.BinaryLower.matchingSpan_gap_budget line 93

Source documentation

All span gaps together use at most the global number of unmatched positions. This holds for any selected collection of label fibers.

theorem matchingSpan_gap_budget {r n : ℕ} {β : Type*} [DecidableEq β]
    (f : Fin r → Fin n) (hf : StrictMono f) (label : Fin r → β)
    (hc : ∀ {i j k}, i ≤ j → j ≤ k → label i = label k → label j = label i)
    (s : Finset β) :
    (∑ b ∈ s, ((matchingSpan f label b).card -
      (Finset.univ.filter fun i => label i = b).card)) ≤ n - r := by
…

Mentions: OAI.TreeEdit.BinaryLower.matchingSpan

theorem OAI.TreeEdit.BinaryLower.matchingSpan_fiber_card_le line 126

Source documentation

There cannot be more matching entries in a fiber than positions in its span.

theorem matchingSpan_fiber_card_le {r n : ℕ} {β : Type*} [DecidableEq β]
    (f : Fin r → Fin n) (hf : StrictMono f) (label : Fin r → β)
    (hc : ∀ {i j k}, i ≤ j → j ≤ k → label i = label k → label j = label i)
    (b : β) :
    (Finset.univ.filter fun i => label i = b).card ≤ (matchingSpan f label b).card := by
…

Mentions: OAI.TreeEdit.BinaryLower.matchingSpan

theorem OAI.TreeEdit.BinaryLower.matchingSpan_two_sided_gap_budget line 141

Source documentation

The two words' losses can be added because their total lengths are equal.

theorem matchingSpan_two_sided_gap_budget {r n : ℕ} {β : Type*} [DecidableEq β]
    (f g : Fin r → Fin n) (hf : StrictMono f) (hg : StrictMono g)
    (label : Fin r → β)
    (hc : ∀ {i j k}, i ≤ j → j ≤ k → label i = label k → label j = label i)
    (s : Finset β) :
    (∑ b ∈ s,
      (((matchingSpan f label b).card - (Finset.univ.filter fun i => label i = b).card) +
       ((matchingSpan g label b).card - (Finset.univ.filter fun i => label i = b).card)))
      ≤ 2 * (n - r) := by
…

Mentions: OAI.TreeEdit.BinaryLower.matchingSpan

theorem OAI.TreeEdit.BinaryLower.matchingSpan_eq_Icc line 155

Source documentation

Specifying the first and last entries of a fiber gives its exact interval.

theorem matchingSpan_eq_Icc {r n : ℕ} {β : Type*} [DecidableEq β]
    (f : Fin r → Fin n) (hf : Monotone f) (label : Fin r → β)
    (b : β) (i j : Fin r) (hi : label i = b) (hj : label j = b)
    (hext : ∀ k, label k = b → i ≤ k ∧ k ≤ j) :
    matchingSpan f label b = Finset.Icc (f i) (f j) := by
…

Mentions: OAI.TreeEdit.BinaryLower.matchingSpan

theorem OAI.TreeEdit.BinaryLower.matchingSpan_exists_endpoints line 172

Source documentation

Every nonempty fiber admits endpoints describing the length of its span.

theorem matchingSpan_exists_endpoints {r n : ℕ} {β : Type*} [DecidableEq β]
    (f : Fin r → Fin n) (hf : Monotone f) (label : Fin r → β)
    (b : β) (hex : ∃ i, label i = b) :
    ∃ i j, label i = b ∧ label j = b ∧ i ≤ j ∧
      matchingSpan f label b = Finset.Icc (f i) (f j) ∧
      (matchingSpan f label b).card = (f j).val + 1 - (f i).val := by
…

Mentions: OAI.TreeEdit.BinaryLower.matchingSpan

theorem OAI.TreeEdit.BinaryLower.block_pair_fiber_convex line 195

Source documentation

The concrete block-pair label of an increasing matching has convex fibers.

theorem block_pair_fiber_convex {r n : ℕ} (P : ℕ)
    (f g : Fin r → Fin n) (hf : Monotone f) (hg : Monotone g)
    {i j k : Fin r} (hij : i ≤ j) (hjk : j ≤ k)
    (heq : ((f i).val / P, (g i).val / P) = ((f k).val / P, (g k).val / P)) :
    ((f j).val / P, (g j).val / P) = ((f i).val / P, (g i).val / P) := by
…

theorem OAI.TreeEdit.BinaryLower.block_pair_two_sided_gap_budget line 209
Source documentation
For the actual quotient block-pair labels, the span losses over any selected pairs are at most twice the global one-sided matching deficit.
```
theorem block_pair_two_sided_gap_budget {r n : ℕ} (P : ℕ)
    (f g : Fin r → Fin n) (hf : StrictMono f) (hg : StrictMono g)
    (s : Finset (ℕ × ℕ)) :
    let label := fun i => ((f i).val / P, (g i).val / P)
…
```

theorem OAI.TreeEdit.BinaryLower.source_matchingSpan_block line 222

Source documentation

Every source span position remains in the source block of its pair.

theorem source_matchingSpan_block {r n : ℕ} (P : ℕ)
    (f g : Fin r → Fin n) (b : ℕ × ℕ) {p : Fin n}
    (hp : p ∈ matchingSpan f (fun i => ((f i).val / P, (g i).val / P)) b) :
    p.val / P = b.1 := by
…

Mentions: OAI.TreeEdit.BinaryLower.matchingSpan

theorem OAI.TreeEdit.BinaryLower.target_matchingSpan_block line 235

Source documentation

Every target span position remains in the target block of its pair.

theorem target_matchingSpan_block {r n : ℕ} (P : ℕ)
    (f g : Fin r → Fin n) (b : ℕ × ℕ) {p : Fin n}
    (hp : p ∈ matchingSpan g (fun i => ((f i).val / P, (g i).val / P)) b) :
    p.val / P = b.2 := by
…

Mentions: OAI.TreeEdit.BinaryLower.matchingSpan

theorem OAI.TreeEdit.BinaryLower.same_block_interval_length line 249
Source documentation
A span between two positions in one block fits within that block after subtracting its initial block offset.
```
theorem same_block_interval_length {P A B : ℕ} (hP : 0 < P)
    (hAB : A ≤ B) (hblock : A / P = B / P) :
    A % P + (B + 1 - A) ≤ P ∧ B + 1 - A ≤ P := by
…
```