TaggedArrays.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Ordered-tag alignment bounds for arrays.

theorem OAI.TreeEdit.BinaryLower.Tagged.tagged_arrays_harmonic line 13

Source documentation

Harmonic deficit bound for literal arrays of fixed-width, ordered-tag blocks.

theorem tagged_arrays_harmonic {α : Type*} {T m B : ℕ}
    (hT : 0 < T) (hm : 2 ≤ m) (hB : 0 < B)
    (X Y : Fin T → Fin m → Word α B) (tag : α → Fin m)
    (hX : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (X a i).val → tag s = i)
    (hY : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (Y a i).val → tag s = i)
    (d : ℝ) (hd : 0 ≤ d)
    (hlocal : ∀ a b, d ≤ ∑ i, (deficit B (X a i).val (Y b i).val : ℝ)) :
    (T : ℝ) * d * (((m - 1) * B : ℕ) : ℝ) /
      (d + (((m - 1) * B : ℕ) : ℝ)) ≤
        (deficit (T * m * B) (rows X) (rows Y) : ℝ) := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.deficit

theorem OAI.TreeEdit.BinaryLower.Tagged.tagged_arrays_bounds line 35

Source documentation

Both inequalities in eq:tagged-result, with no matching-alignment premise.

theorem tagged_arrays_bounds {α : Type*} {T m B : ℕ}
    (hT : 0 < T) (hm : 2 ≤ m) (hB : 0 < B)
    (X Y : Fin T → Fin m → Word α B) (tag : α → Fin m)
    (hX : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (X a i).val → tag s = i)
    (hY : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (Y a i).val → tag s = i)
    (d : ℝ) (hd : 0 ≤ d)
    (hlocal : ∀ a b, d ≤ ∑ i, (deficit B (X a i).val (Y b i).val : ℝ)) :
    ((T : ℝ) * d * (((m - 1) * B : ℕ) : ℝ) /
      (d + (((m - 1) * B : ℕ) : ℝ)) ≤
        (deficit (T * m * B) (rows X) (rows Y) : ℝ)) ∧
    ((T : ℝ) / 2 * min d (((m - 1) * B : ℕ) : ℝ) ≤
      (T : ℝ) * d * (((m - 1) * B : ℕ) : ℝ) /
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.deficit

theorem OAI.TreeEdit.BinaryLower.Tagged.tagged_arrays_half line 53

Source documentation

The convenient Td/2 form used in both tree separation inductions.

theorem tagged_arrays_half {α : Type*} {T m B : ℕ}
    (hT : 0 < T) (hm : 2 ≤ m) (hB : 0 < B)
    (X Y : Fin T → Fin m → Word α B) (tag : α → Fin m)
    (hX : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (X a i).val → tag s = i)
    (hY : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (Y a i).val → tag s = i)
    (d : ℝ) (hd : 0 ≤ d)
    (hlocal : ∀ a b, d ≤ ∑ i, (deficit B (X a i).val (Y b i).val : ℝ))
    (hdg : d ≤ (((m - 1) * B : ℕ) : ℝ)) :
    (T : ℝ) * d / 2 ≤ (deficit (T * m * B) (rows X) (rows Y) : ℝ) := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.deficit

theorem OAI.TreeEdit.BinaryLower.Tagged.rows_with_ordered_tags line 69

Source documentation

Ordered-tag alignment for pairwise disjoint alphabets. The decoder used internally is constructed, not an additional hypothesis.

theorem rows_with_ordered_tags {α : Type*} {T m B : ℕ}
    (hT : 0 < T) (hm : 2 ≤ m) (hB : 0 < B)
    (Γ : Fin m → Set α) (hΓ : Pairwise fun i j => Disjoint (Γ i) (Γ j))
    (X Y : Fin T → Fin m → Word α B)
    (hX : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (X a i).val → s ∈ Γ i)
    (hY : ∀ (a : Fin T) (i : Fin m) (s : α), s ∈ (Y a i).val → s ∈ Γ i)
    (d : ℝ) (hd : 0 ≤ d)
    (hlocal : ∀ a b, d ≤ ∑ i, (deficit B (X a i).val (Y b i).val : ℝ)) :
    ((T : ℝ) * d * (((m - 1) * B : ℕ) : ℝ) /
      (d + (((m - 1) * B : ℕ) : ℝ)) ≤
        (deficit (T * m * B) (rows X) (rows Y) : ℝ)) ∧
    ((T : ℝ) / 2 * min d (((m - 1) * B : ℕ) : ℝ) ≤
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.deficit