Marked Dyck paths

InductiveSteps of a marked Dyck path#✓fully proved

A step of a marked Dyck path is one of three kinds: a horizontal step \(E = (1, 0)\), an unmarked vertical step \(N = (0, 1)\), or a marked vertical step \(N^* = (0, 1)\).

inductive MarkedDyckStep : Type where
  | E : MarkedDyckStep
  | N : MarkedDyckStep
  | Nstar : MarkedDyckStep

Used by 7

Used byMarked step of a marked Dyck path · Number of horizontal steps in a marked Dyck step sequence · Number of unmarked vertical steps · Number of marked vertical steps · Marked Dyck path · Size of a marked Dyck path · Size of a marked Dyck path in vertical steps

DefinitionNumber of horizontal steps in a marked Dyck step sequence#✓fully proved

For a finite sequence \(P\) of marked Dyck steps, \(E(P)\) is the number of horizontal steps \(E\) in \(P\).

def markedDyckCountE : List MarkedDyckStep → Nat
  | [] => 0
  | .E :: t => markedDyckCountE t + 1
  | _ :: t => markedDyckCountE t

Uses 1 · Used by 3

Statement usesSteps of a marked Dyck path

Used byMarked Dyck path · Size of a marked Dyck path · Size of a marked Dyck path in vertical steps

DefinitionNumber of unmarked vertical steps#✓fully proved

For a finite sequence \(P\) of marked Dyck steps, \(N(P)\) is the number of unmarked vertical steps \(N\) in \(P\).

def markedDyckCountN : List MarkedDyckStep → Nat
  | [] => 0
  | .N :: t => markedDyckCountN t + 1
  | _ :: t => markedDyckCountN t

Uses 1 · Used by 2

Statement usesSteps of a marked Dyck path

Used byMarked Dyck path · Size of a marked Dyck path in vertical steps

DefinitionNumber of marked vertical steps#✓fully proved

For a finite sequence \(P\) of marked Dyck steps, \(N^*(P)\) is the number of marked vertical steps \(N^*\) in \(P\).

def markedDyckCountNstar : List MarkedDyckStep → Nat
  | [] => 0
  | .Nstar :: t => markedDyckCountNstar t + 1
  | _ :: t => markedDyckCountNstar t

Uses 1 · Used by 3

Statement usesSteps of a marked Dyck path

Used byMarked Dyck path · Size of a marked Dyck path · Size of a marked Dyck path in vertical steps

StructureMarked Dyck path#✓fully proved

Let \(E(Q)\), \(N(Q)\) and \(N^*(Q)\) denote the numbers of horizontal steps \(E\), unmarked vertical steps \(N\) and marked vertical steps \(N^*\) in a finite sequence \(Q\) of marked Dyck steps. A marked Dyck path is a finite sequence \(P\) of marked Dyck steps such that \(E(P) = N(P) + N^*(P)\) and every prefix \(Q\) of \(P\) satisfies \(N(Q) + N^*(Q) \le E(Q)\): a lattice path from \((0, 0)\) that ends on the diagonal and never goes above it.

structure MarkedDyckPath : Type where
  steps : List MarkedDyckStep
  balanced : markedDyckCountE steps = markedDyckCountN steps + markedDyckCountNstar steps
  staysUnder : ∀ n, markedDyckCountN (steps.take n) + markedDyckCountNstar (steps.take n) ≤
    markedDyckCountE (steps.take n)

Uses 4 · Used by 3

Statement usesSteps of a marked Dyck path · Number of horizontal steps in a marked Dyck step sequence · Number of unmarked vertical steps · Number of marked vertical steps

Used byMarked step of a marked Dyck path · Size of a marked Dyck path · Size of a marked Dyck path in vertical steps

DefinitionMarked step of a marked Dyck path#✓fully proved

Let \(P\) be a marked Dyck path with \(\ell\) steps. For a position \(i\) with \(0 \le i < \ell\), the step of \(P\) at position \(i\) is marked when it is the marked vertical step \(N^*\) (rather than an unmarked vertical step \(N\) or a horizontal step \(E\)).

def IsMarkedStep (P : MarkedDyckPath) (i : Fin P.steps.length) : Prop :=
  P.steps.get i = MarkedDyckStep.Nstar

Uses 2

Statement usesMarked Dyck path · Steps of a marked Dyck path

DefinitionSize of a marked Dyck path#✓fully proved

The size of a marked Dyck path \(P\) is \(N^*(P) + E(P)\), where \(N^*(P)\) is the number of marked vertical steps of \(P\) and \(E(P)\) the number of its horizontal steps.

def MarkedDyckPath.pathSize (P : MarkedDyckPath) : Nat :=
  markedDyckCountNstar P.steps + markedDyckCountE P.steps

Uses 4 · Used by 1

Statement usesMarked Dyck path · Steps of a marked Dyck path · Number of horizontal steps in a marked Dyck step sequence · Number of marked vertical steps

Used bySize of a marked Dyck path in vertical steps

TheoremSize of a marked Dyck path in vertical steps#✓fully proved

For every marked Dyck path \(P\), the size of \(P\) equals \(N(P) + 2N^*(P)\), where \(N(P)\) and \(N^*(P)\) are the numbers of unmarked and marked vertical steps of \(P\).

theorem MarkedDyckPath.size_eq (P : MarkedDyckPath) :
    P.pathSize = markedDyckCountN P.steps + 2 * markedDyckCountNstar P.steps

Uses 6

Statement usesMarked Dyck path · Size of a marked Dyck path · Steps of a marked Dyck path · Number of unmarked vertical steps · Number of marked vertical steps

Proof usesNumber of horizontal steps in a marked Dyck step sequence

InductiveSteps of a multi-marked Dyck path#✓fully proved

A step of a multi-marked Dyck path is one of the horizontal step \(E = (1, 0)\), the plain vertical step \(N = (0, 1)\), or, for an integer \(t \ge 2\), the marked vertical step \(N^*_t = (0, 1)\) of index \(t\). There are no marked steps of index less than \(2\).

inductive MultiMarkedStep where
  | E : MultiMarkedStep
  | N : MultiMarkedStep
  | marked : (t : Nat) → 2 ≤ t → MultiMarkedStep

Used by 17

Used byMarked tail · Number of horizontal steps in a multi-marked step sequence · Equal horizontal and vertical step counts · Number of marked steps of a given index · Number of plain vertical steps · Number of steps · Number of vertical steps · Multi-marked Dyck path · Multi-marked Dyck paths of a given size · Index sum of a multi-marked step sequence · Vertical steps of a multi-marked Dyck path · Shifted index sum of a multi-marked step sequence · Size of a multi-marked step sequence · Two expressions for the size of a multi-marked Dyck path · Final run of vertical steps · Multi-marked Dyck paths with an unmarked tail · Vertical count plus shifted index sum

DefinitionNumber of horizontal steps in a multi-marked step sequence#✓fully proved

For a finite sequence \(P\) of multi-marked steps (horizontal steps \(E\), plain vertical steps \(N\) and marked vertical steps \(N^*_t\) with index \(t \ge 2\)), \(E(P)\) is the number of horizontal steps \(E\) in \(P\).

def multiMarkedCountE : List MultiMarkedStep → Nat
  | [] => 0
  | .E :: xs => multiMarkedCountE xs + 1
  | .N :: xs => multiMarkedCountE xs
  | .marked _ _ :: xs => multiMarkedCountE xs

Uses 1 · Used by 4

Statement usesSteps of a multi-marked Dyck path

Used byEqual horizontal and vertical step counts · Multi-marked Dyck path · Size of a multi-marked step sequence · Two expressions for the size of a multi-marked Dyck path

DefinitionNumber of plain vertical steps#✓fully proved

For a finite sequence \(P\) of multi-marked steps (horizontal steps \(E\), plain vertical steps \(N\) and marked vertical steps \(N^*_t\) with index \(t \ge 2\)), \(N(P)\) is the number of plain (unmarked) vertical steps \(N\) in \(P\).

def multiMarkedCountPlainN : List MultiMarkedStep → Nat
  | [] => 0
  | .E :: xs => multiMarkedCountPlainN xs
  | .N :: xs => multiMarkedCountPlainN xs + 1
  | .marked _ _ :: xs => multiMarkedCountPlainN xs

Uses 1 · Used by 2

Statement usesSteps of a multi-marked Dyck path

Used byTwo expressions for the size of a multi-marked Dyck path · Vertical count plus shifted index sum

DefinitionNumber of vertical steps#✓fully proved

For a finite sequence \(P\) of multi-marked steps (horizontal steps \(E\), plain vertical steps \(N\) and marked vertical steps \(N^*_t\) with index \(t \ge 2\)), this is the number of vertical steps in \(P\), plain steps \(N\) and marked steps \(N^*_t\) counted together.

def multiMarkedCountVert : List MultiMarkedStep → Nat
  | [] => 0
  | .E :: xs => multiMarkedCountVert xs
  | .N :: xs => multiMarkedCountVert xs + 1
  | .marked _ _ :: xs => multiMarkedCountVert xs + 1

Uses 1 · Used by 4

Statement usesSteps of a multi-marked Dyck path

Used byEqual horizontal and vertical step counts · Multi-marked Dyck path · Two expressions for the size of a multi-marked Dyck path · Vertical count plus shifted index sum

DefinitionNumber of steps#✓fully proved

For a finite sequence \(P\) of multi-marked steps (horizontal steps \(E\), plain vertical steps \(N\) and marked vertical steps \(N^*_t\) with index \(t \ge 2\)), this is the total number of steps in \(P\), that is, the length of \(P\).

def multiMarkedCountTotal : List MultiMarkedStep → Nat
  | [] => 0
  | _ :: xs => multiMarkedCountTotal xs + 1

Uses 1

Statement usesSteps of a multi-marked Dyck path

DefinitionIndex sum of a multi-marked step sequence#✓fully proved

For a finite sequence \(s\) of steps of a multi-marked Dyck path, the index sum of \(s\) is the sum of the indices \(t\) over all occurrences of marked steps \(N^*_t\) in \(s\), each occurrence counted separately; the steps \(E\) and \(N\) contribute nothing.

Grouping the occurrences by index, the index sum equals \(\sum_t t \cdot N^*_t(s)\), where \(N^*_t(s)\) is the number of marked steps of index \(t\) in \(s\).

def multiMarkedIndexSum : List MultiMarkedStep → Nat
  | [] => 0
  | .E :: xs => multiMarkedIndexSum xs
  | .N :: xs => multiMarkedIndexSum xs
  | .marked t _ :: xs => t + multiMarkedIndexSum xs

Uses 1 · Used by 2

Statement usesSteps of a multi-marked Dyck path

Used byTwo expressions for the size of a multi-marked Dyck path · Vertical count plus shifted index sum

DefinitionShifted index sum of a multi-marked step sequence#✓fully proved

For a finite sequence \(s\) of steps of a multi-marked Dyck path, the shifted index sum of \(s\) is the sum of \(t - 1\) over all occurrences of marked steps \(N^*_t\) in \(s\), each occurrence counted separately; the steps \(E\) and \(N\) contribute nothing.

Grouping the occurrences by index, the shifted index sum equals \(\sum_t (t - 1) \cdot N^*_t(s)\), where \(N^*_t(s)\) is the number of marked steps of index \(t\) in \(s\).

def multiMarkedShiftedIndexSum : List MultiMarkedStep → Nat
  | [] => 0
  | .E :: xs => multiMarkedShiftedIndexSum xs
  | .N :: xs => multiMarkedShiftedIndexSum xs
  | .marked t _ :: xs => (t - 1) + multiMarkedShiftedIndexSum xs

Uses 1 · Used by 3

Statement usesSteps of a multi-marked Dyck path

Used bySize of a multi-marked step sequence · Two expressions for the size of a multi-marked Dyck path · Vertical count plus shifted index sum

DefinitionNumber of marked steps of a given index#✓fully proved

For a finite sequence \(P\) of multi-marked steps (horizontal steps \(E\), plain vertical steps \(N\) and marked vertical steps \(N^*_s\) with index \(s \ge 2\)) and a natural number \(t\), \(N^*_t(P)\) is the number of marked steps in \(P\) whose index is exactly \(t\).

def multiMarkedCountMarkedT : List MultiMarkedStep → Nat → Nat
  | [], _ => 0
  | .marked s _ :: xs, t => (if s == t then 1 else 0) + multiMarkedCountMarkedT xs t
  | _ :: xs, t => multiMarkedCountMarkedT xs t

Uses 1

Statement usesSteps of a multi-marked Dyck path

DefinitionSize of a multi-marked step sequence#✓fully proved

The size of a finite sequence \(s\) of steps of a multi-marked Dyck path is \(E(s) + \sum (t - 1)\), where \(E(s)\) is the number of horizontal steps \(E\) in \(s\) and the sum runs over all occurrences of marked steps \(N^*_t\) in \(s\).

def multiMarkedSize (l : List MultiMarkedStep) : Nat :=
  multiMarkedCountE l + multiMarkedShiftedIndexSum l

Uses 3 · Used by 3

Statement usesSteps of a multi-marked Dyck path · Number of horizontal steps in a multi-marked step sequence · Shifted index sum of a multi-marked step sequence

Used byMulti-marked Dyck paths of a given size · Two expressions for the size of a multi-marked Dyck path · Multi-marked Dyck paths with an unmarked tail

StructureMulti-marked Dyck path#✓fully proved

A multi-marked Dyck path is a finite sequence \(P\) of steps, each a horizontal step \(E = (1,0)\), a plain vertical step \(N = (0,1)\) or a marked vertical step \(N^*_t = (0,1)\) carrying an index \(t \ge 2\), such that every prefix of \(P\), including the empty prefix and \(P\) itself, has at most as many vertical steps (plain and marked) as horizontal steps, and \(P\) has exactly as many vertical steps as horizontal steps.

Read as a lattice path from \((0,0)\), \(P\) never rises above the diagonal and ends on it.

structure MultiMarkedDyckPath where
  steps : List MultiMarkedStep
  underdiagonal :
    ∀ k, k ≤ steps.length →
      multiMarkedCountVert (steps.take k) ≤ multiMarkedCountE (steps.take k)
  diagonal_endpoint : multiMarkedCountE steps = multiMarkedCountVert steps

Uses 3 · Used by 6

Statement usesSteps of a multi-marked Dyck path · Number of horizontal steps in a multi-marked step sequence · Number of vertical steps

Used byMarked tail · Unmarked tail · Equal horizontal and vertical step counts · Multi-marked Dyck paths of a given size · Two expressions for the size of a multi-marked Dyck path · Multi-marked Dyck paths with an unmarked tail

TheoremEqual horizontal and vertical step counts#✓fully proved

For every multi-marked Dyck path \(P\), the number \(E(P)\) of horizontal steps of \(P\) equals the number of vertical steps of \(P\), plain steps \(N\) and marked steps \(N^*_t\) counted together.

theorem multiMarkedCountEq (P : MultiMarkedDyckPath) :
    multiMarkedCountE P.steps = multiMarkedCountVert P.steps

Uses 4 · Used by 1

Statement usesMulti-marked Dyck path · Steps of a multi-marked Dyck path · Number of horizontal steps in a multi-marked step sequence · Number of vertical steps

Used byTwo expressions for the size of a multi-marked Dyck path

TheoremVertical count plus shifted index sum#✓fully proved

For every finite sequence \(s\) of steps of a multi-marked Dyck path, the number of vertical steps of \(s\) plus the shifted index sum of \(s\) equals the number of plain vertical steps \(N\) of \(s\) plus the index sum of \(s\).

Each marked step \(N^*_t\) contributes \(1 + (t - 1)\) to the left side and \(t\) to the right side.

theorem multiMarkedVertShifted_eq (l : List MultiMarkedStep) :
    multiMarkedCountVert l + multiMarkedShiftedIndexSum l =
      multiMarkedCountPlainN l + multiMarkedIndexSum l

Uses 5 · Used by 1

Statement usesSteps of a multi-marked Dyck path · Number of plain vertical steps · Number of vertical steps · Index sum of a multi-marked step sequence · Shifted index sum of a multi-marked step sequence

Used byTwo expressions for the size of a multi-marked Dyck path

TheoremTwo expressions for the size of a multi-marked Dyck path#✓fully proved

For every multi-marked Dyck path \(P\), the size \(E(P) + \sum (t - 1)\) of \(P\) equals \(N(P) + \sum t\), where \(E(P)\) is the number of horizontal steps \(E\) of \(P\), \(N(P)\) is the number of plain vertical steps \(N\) of \(P\), and both sums run over all occurrences of marked steps \(N^*_t\) in \(P\).

Grouped by index, this reads \(E(P) + \sum_t (t - 1) N^*_t(P) = N(P) + \sum_t t N^*_t(P)\), where \(N^*_t(P)\) is the number of marked steps of index \(t\) in \(P\).

theorem multiMarkedSizeEq (P : MultiMarkedDyckPath) :
    multiMarkedSize P.steps =
      multiMarkedCountPlainN P.steps + multiMarkedIndexSum P.steps

Uses 10

Statement usesMulti-marked Dyck path · Steps of a multi-marked Dyck path · Number of plain vertical steps · Index sum of a multi-marked step sequence · Size of a multi-marked step sequence

Proof usesNumber of horizontal steps in a multi-marked step sequence · Equal horizontal and vertical step counts · Number of vertical steps · Shifted index sum of a multi-marked step sequence · Vertical count plus shifted index sum

DefinitionVertical steps of a multi-marked Dyck path#✓fully proved

A step of a multi-marked Dyck path is vertical when it is the plain step \(N\) or a marked step \(N^*_t\); the horizontal step \(E\) is not vertical. This test delimits the final run of vertical steps of a step sequence.

def multiMarkedIsVert : MultiMarkedStep → Bool
  | .E => false
  | .N => true
  | .marked _ _ => true

Uses 1 · Used by 1

Statement usesSteps of a multi-marked Dyck path

Used byFinal run of vertical steps

DefinitionFinal run of vertical steps#✓fully proved

The final run of vertical steps of a finite sequence \(s\) of steps of a multi-marked Dyck path is the longest suffix of \(s\) consisting of vertical steps (\(N\) or \(N^*_t\)): the part of \(s\) after its last horizontal step \(E\), or all of \(s\) if \(s\) has no step \(E\).

def multiMarkedTrailingVert (l : List MultiMarkedStep) : List MultiMarkedStep :=
  (l.reverse.takeWhile multiMarkedIsVert).reverse

Uses 2 · Used by 1

Statement usesSteps of a multi-marked Dyck path · Vertical steps of a multi-marked Dyck path

Used byMarked tail

DefinitionMarked tail#✓fully proved

A multi-marked Dyck path \(P\) has a marked tail when its final run of vertical steps (the steps after its last horizontal step \(E\), or all of \(P\) if \(P\) has no step \(E\)) contains a marked vertical step \(N^*_t\) for some index \(t \ge 2\).

def MultiMarkedDyckPath.HasMarkedTail (P : MultiMarkedDyckPath) : Prop :=
  ∃ (t : Nat) (h : 2 ≤ t),
    MultiMarkedStep.marked t h ∈ multiMarkedTrailingVert P.steps

Uses 3 · Used by 1

Statement usesMulti-marked Dyck path · Steps of a multi-marked Dyck path · Final run of vertical steps

Used byUnmarked tail

DefinitionUnmarked tail#✓fully proved

A multi-marked Dyck path \(P\) has an unmarked tail when it does not have a marked tail, that is, when its final run of vertical steps (the steps after its last horizontal step \(E\), or all of \(P\) if \(P\) has no step \(E\)) contains no marked vertical step.

def MultiMarkedDyckPath.HasUnmarkedTail (P : MultiMarkedDyckPath) : Prop :=
  ¬ P.HasMarkedTail

Uses 2 · Used by 1

Statement usesMulti-marked Dyck path · Marked tail

Used byMulti-marked Dyck paths with an unmarked tail

DefinitionMulti-marked Dyck paths of a given size#✓fully proved

For a natural number \(n\), \(\tilde P_n\) is the set of multi-marked Dyck paths \(P\) of size \(n\). Here the size of \(P\) is \(E(P) + \sum (t - 1)\), where \(E(P)\) is the number of horizontal steps of \(P\) and the sum runs over the marked steps \(N^*_t\) of \(P\), each occurrence counted separately.

def MultiMarkedDyckPathOfSize (n : Nat) : Type :=
  { P : MultiMarkedDyckPath // multiMarkedSize P.steps = n }

Uses 3

Statement usesMulti-marked Dyck path · Steps of a multi-marked Dyck path · Size of a multi-marked step sequence

DefinitionMulti-marked Dyck paths with an unmarked tail#✓fully proved

For a natural number \(n\), \(\tilde R_n\) is the set of multi-marked Dyck paths of size \(n\) with an unmarked tail, that is, whose final run of vertical steps contains no marked step.

def MultiMarkedUnmarkedTail (n : Nat) : Type :=
  { P : MultiMarkedDyckPath //
    multiMarkedSize P.steps = n ∧ P.HasUnmarkedTail }

Uses 4

Statement usesMulti-marked Dyck path · Unmarked tail · Steps of a multi-marked Dyck path · Size of a multi-marked step sequence

27 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.