UnequalSegments.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TreeEdit.BinaryLower.Code.BlockSegmentSeparation line 11
Source documentation
Concrete separation of segments in a selected pair of width-P blocks. The words here are indexed functions solely to avoid casts in total length.
```
def BlockSegmentSeparation {α : Type*} {M P : ℕ}
    (x y : Fin (M * P) → α) (bad : ℕ × ℕ → Prop) (a₀ : ℕ) : Prop :=
…
```

theorem OAI.TreeEdit.BinaryLower.Code.ofFn_segment_length_of_span line 23

Source documentation

Endpoint descriptions give the literal (untruncated) lengths of the contiguous spans in the corresponding word.

theorem ofFn_segment_length_of_span {α : Type*} {r n : ℕ}
    (x : Fin n → α) (f : Fin r → Fin n) {β : Type*} [DecidableEq β]
    (label : Fin r → β) (b : β) (i j : Fin r)
    (hcard : (matchingSpan f label b).card = (f j).val + 1 - (f i).val)
    (hij : f i ≤ f j) :
    (((List.ofFn x).drop (f i).val).take (matchingSpan f label b).card).length =
      (matchingSpan f label b).card := by
…

Mentions: OAI.TreeEdit.BinaryLower.matchingSpan

theorem OAI.TreeEdit.BinaryLower.Code.block_pair_charge_of_segment_separation line 38

Source documentation

Local charge for a visited bad block pair, using only actual contiguous segments of the two binary words.

theorem block_pair_charge_of_segment_separation
    {α : Type*} {r M P : ℕ} (hP : 0 < P)
    (x y : Fin (M * P) → α)
    (f g : Fin r → Fin (M * P)) (hf : StrictMono f) (hg : StrictMono g)
    (hmatch : ∀ t, x (f t) = y (g t))
    (bad : ℕ × ℕ → Prop) (a₀ : ℕ)
    (hsep : BlockSegmentSeparation x y bad a₀)
    (b : ℕ × ℕ) (hb : bad b)
    (hvisit : ∃ t, ((f t).val / P, (g t).val / P) = b)
    (hlarge : a₀ ≤
      (Finset.univ.filter (fun t => ((f t).val / P, (g t).val / P) = b)).card) :
    (Finset.univ.filter (fun t => ((f t).val / P, (g t).val / P) = b)).card ≤
…

Mentions: OAI.TreeEdit.BinaryLower.Code.BlockSegmentSeparation

theorem OAI.TreeEdit.BinaryLower.Code.unequal_matches_le_of_segment_separation line 138

Source documentation

The manuscript's unequal-label estimate for an arbitrary increasing bit matching, from concrete separation of the segments in bad block pairs.

theorem unequal_matches_le_of_segment_separation
    {α : Type*} {r M P : ℕ} (hP : 0 < P)
    (x y : Fin (M * P) → α)
    (f g : Fin r → Fin (M * P)) (hf : StrictMono f) (hg : StrictMono g)
    (hmatch : ∀ t, x (f t) = y (g t))
    (bad : ℕ × ℕ → Prop) [DecidablePred bad] (a₀ : ℕ)
    (hsep : BlockSegmentSeparation x y bad a₀) :
    (Finset.univ.filter (fun t => bad ((f t).val / P, (g t).val / P))).card ≤
      200 * (M * P - r) + 2 * M * a₀ := by
…

Mentions: OAI.TreeEdit.BinaryLower.Code.BlockSegmentSeparation