TaggedNonsplit.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Loss counting for nonsplit rows with a local row-pair matching bound.

def OAI.TreeEdit.BinaryLower.TaggedNonsplit.rowCount line 12
Source documentation
Number of matched source positions assigned to a specified row.
```
def rowCount {N T : ℕ} (row : Fin N → Fin T) (r : Fin T) : ℕ :=
…
```
theorem OAI.TreeEdit.BinaryLower.TaggedNonsplit.sum_rowCount line 16
Source documentation
Partition the matching by its source row.
```
theorem sum_rowCount {N T : ℕ} (row : Fin N → Fin T) :
    ∑ r, rowCount row r = N := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.TaggedNonsplit.rowCount
theorem OAI.TreeEdit.BinaryLower.TaggedNonsplit.rowCount_le_width line 23
Source documentation
An injective matching cannot use more than W positions in one row of width W. The row indices are specified by Euclidean division.
```
theorem rowCount_le_width {N T W : ℕ}
    (u : Fin N → ℕ) (row : Fin N → Fin T)
    (hW : 0 < W) (hu : Function.Injective u)
    (hrow : ∀ i, u i / W = (row i).val) (r : Fin T) :
    rowCount row r ≤ W := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.TaggedNonsplit.rowCount

theorem OAI.TreeEdit.BinaryLower.TaggedNonsplit.nonsplit_loss_bound line 49

Source documentation

Sum the losses in nonsplit rows. The rows in S may have no local loss estimate; the capacity bound alone makes their losses nonnegative.

theorem nonsplit_loss_bound {N T : ℕ} (row : Fin N → Fin T)
    (S : Finset (Fin T)) (W d : ℝ)
    (hcapacity : ∀ r, (rowCount row r : ℝ) ≤ W)
    (hnonsplit : ∀ r, r ∉ S → (rowCount row r : ℝ) ≤ W - d) :
    d * ((T : ℝ) - S.card) ≤ (T : ℝ) * W - N := by
…

Mentions: OAI.TreeEdit.BinaryLower.TaggedNonsplit.rowCount

theorem OAI.TreeEdit.BinaryLower.TaggedNonsplit.nonsplit_loss_bound_of_positions line 79

Source documentation

Nonsplit tagged-row loss for an actual injective list of source positions.

theorem nonsplit_loss_bound_of_positions {N T W : ℕ}
    (u : Fin N → ℕ) (row : Fin N → Fin T)
    (S : Finset (Fin T)) (d : ℝ)
    (hW : 0 < W) (hu : Function.Injective u)
    (hrow : ∀ i, u i / W = (row i).val)
    (hnonsplit : ∀ r, r ∉ S → (rowCount row r : ℝ) ≤ (W : ℝ) - d) :
    d * ((T : ℝ) - S.card) ≤ (T : ℝ) * W - N := by
…

Mentions: OAI.TreeEdit.BinaryLower.TaggedNonsplit.rowCount

def OAI.TreeEdit.BinaryLower.TaggedNonsplit.rowPairCount line 92
Source documentation
Matched positions in a specified source/target row pair.
```
def rowPairCount {N T U : ℕ} (row : Fin N → Fin T)
    (target : Fin N → Fin U) (r : Fin T) (b : Fin U) : ℕ :=
…
```

theorem OAI.TreeEdit.BinaryLower.TaggedNonsplit.rowCount_eq_rowPairCount line 97

Source documentation

In a nonsplit row with a match, every match belongs to the same row pair.

theorem rowCount_eq_rowPairCount {N T U : ℕ}
    (row : Fin N → Fin T) (target : Fin N → Fin U) (r : Fin T)
    (hconstant : ∀ i j, row i = r → row j = r → target i = target j)
    (i : Fin N) (hi : row i = r) :
    rowCount row r = rowPairCount row target r (target i) := by
…

Mentions: OAI.TreeEdit.BinaryLower.TaggedNonsplit.rowCount, OAI.TreeEdit.BinaryLower.TaggedNonsplit.rowPairCount

theorem OAI.TreeEdit.BinaryLower.TaggedNonsplit.nonsplit_rowCount_le line 110
Source documentation
Local row-pair bounds apply to a nonsplit row, including the case of a row with no matches. The latter case uses the necessary bound d≤W.
```
theorem nonsplit_rowCount_le {N T U : ℕ}
    (row : Fin N → Fin T) (target : Fin N → Fin U) (r : Fin T)
    (W d : ℝ) (hdW : d ≤ W)
    (hconstant : ∀ i j, row i = r → row j = r → target i = target j)
    (hpair : ∀ b, (rowPairCount row target r b : ℝ) ≤ W - d) :
    (rowCount row r : ℝ) ≤ W - d := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.TaggedNonsplit.rowPairCount, OAI.TreeEdit.BinaryLower.TaggedNonsplit.rowCount

theorem OAI.TreeEdit.BinaryLower.TaggedNonsplit.nonsplit_loss_of_pair_bounds line 132

Source documentation

The source-loss estimate E ≥ d(T-s) from semantic nonsplitting and local row-pair bounds. All finite matching positions, including an empty matching and rows without matches, are covered.

theorem nonsplit_loss_of_pair_bounds {N T U W : ℕ}
    (u : Fin N → ℕ) (row : Fin N → Fin T) (target : Fin N → Fin U)
    (S : Finset (Fin T)) (d : ℝ)
    (hW : 0 < W) (hu : Function.Injective u)
    (hrow : ∀ i, u i / W = (row i).val) (hdW : d ≤ (W : ℝ))
    (hconstant : ∀ r, r ∉ S →
      ∀ i j, row i = r → row j = r → target i = target j)
    (hpair : ∀ r b, (rowPairCount row target r b : ℝ) ≤ (W : ℝ) - d) :
    d * ((T : ℝ) - S.card) ≤ (T : ℝ) * W - N := by
…

Mentions: OAI.TreeEdit.BinaryLower.TaggedNonsplit.rowPairCount

def OAI.TreeEdit.BinaryLower.TaggedNonsplit.natRowCount line 147
Source documentation
Number of matches assigned to a natural row index.
```
def natRowCount {N : ℕ} (row : Fin N → ℕ) (r : ℕ) : ℕ :=
…
```
theorem OAI.TreeEdit.BinaryLower.TaggedNonsplit.sum_natRowCount line 151
Source documentation
Partition the matching by natural row indices in [0,T).
```
theorem sum_natRowCount {N T : ℕ} (row : Fin N → ℕ)
    (hrow : ∀ i, row i < T) :
    ∑ r ∈ Finset.range T, natRowCount row r = N := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.TaggedNonsplit.natRowCount

theorem OAI.TreeEdit.BinaryLower.TaggedNonsplit.nonsplit_loss_bound_nat line 161

Source documentation

Nonsplit summation with natural row indices, avoiding any conversion of splitRows to a Fin-indexed set.

theorem nonsplit_loss_bound_nat {N T : ℕ} (row : Fin N → ℕ)
    (S : Finset ℕ) (W d : ℝ)
    (hrow : ∀ i, row i < T) (hS : S ⊆ Finset.range T)
    (hcapacity : ∀ r < T, (natRowCount row r : ℝ) ≤ W)
    (hnonsplit : ∀ r < T, r ∉ S → (natRowCount row r : ℝ) ≤ W - d) :
    d * ((T : ℝ) - S.card) ≤ (T : ℝ) * W - N := by
…

Mentions: OAI.TreeEdit.BinaryLower.TaggedNonsplit.natRowCount

theorem OAI.TreeEdit.BinaryLower.TaggedNonsplit.natRowCount_div_le_width line 198
Source documentation
Capacity of one natural-indexed row under an injective source map.
```
theorem natRowCount_div_le_width {N : ℕ}
    (u : Fin N → ℕ) (hu : Function.Injective u) (W : ℕ) (hW : 0 < W) (r : ℕ) :
    natRowCount (fun i => u i / W) r ≤ W := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.TaggedNonsplit.natRowCount

theorem OAI.TreeEdit.BinaryLower.TaggedNonsplit.nonsplit_loss_numeric line 222

Source documentation

Numeric nonsplit estimate with exactly the row convention position/B/m and the natural unmatched count.

theorem nonsplit_loss_numeric {N T m B : ℕ}
    (u : Fin N → ℕ) (hu : Function.Injective u)
    (hm : 0 < m) (hB : 0 < B) (hub : ∀ i, u i < T * m * B)
    (S : Finset ℕ) (hS : S ⊆ Finset.range T) (d : ℝ)
    (hnonsplit : ∀ r < T, r ∉ S →
      ((Finset.univ.filter fun i => u i / B / m = r).card : ℝ) ≤
        (m * B : ℕ) - d) :
    d * ((T : ℝ) - S.card) ≤ ((T * m * B - N : ℕ) : ℝ) := by
…