Documentation

RoughPaths.Sewing.ChainRefine

Chain refinement combinatorics #

List-level machinery for the additive sewing lemma over a linear order: deduplication of monotone chains (dedupChain), and the decomposition of a strict chain as a glued refinement of a coarser strict chain through the same points (refineAlong), giving common refinements of two chains.

Deduplication of monotone chains #

source
def RoughPaths.Sewing.dedupChain {T : Type u} [LinearOrder T] :
List T → List T

Remove adjacent duplicates from a list (of a ≤-chain, producing a <-chain).

Equations
Instances For
    source
    @[simp]
    theorem RoughPaths.Sewing.dedupChain_nil {T : Type u} [LinearOrder T] :
    dedupChain [] = []
    source
    @[simp]
    theorem RoughPaths.Sewing.dedupChain_singleton {T : Type u} [LinearOrder T] (x : T) :
    dedupChain [x] = [x]
    source
    theorem RoughPaths.Sewing.dedupChain_cons_cons {T : Type u} [LinearOrder T] (x y : T) (rest : List T) :
    dedupChain (x :: y :: rest) = if x = y then dedupChain (y :: rest) else x :: dedupChain (y :: rest)
    source
    theorem RoughPaths.Sewing.dedupChain_ne_nil {T : Type u} [LinearOrder T] {l : List T} :
    l ≠ [] → dedupChain l ≠ []
    source
    @[simp]
    theorem RoughPaths.Sewing.mem_dedupChain {T : Type u} [LinearOrder T] {a : T} {l : List T} :
    a ∈ dedupChain l ↔ a ∈ l
    source
    @[simp]
    theorem RoughPaths.Sewing.head?_dedupChain {T : Type u} [LinearOrder T] (l : List T) :
    (dedupChain l).head? = l.head?
    source
    @[simp]
    theorem RoughPaths.Sewing.getLast?_dedupChain {T : Type u} [LinearOrder T] (l : List T) :
    (dedupChain l).getLast? = l.getLast?
    source
    theorem RoughPaths.Sewing.isChain_lt_dedupChain {T : Type u} [LinearOrder T] {l : List T} :
    List.IsChain (fun (x1 x2 : T) => x1 ≤ x2) l → List.IsChain (fun (x1 x2 : T) => x1 < x2) (dedupChain l)

    Deduplicating a ≤-chain yields a <-chain.

    source
    theorem RoughPaths.Sewing.isChain_fine_dedupChain {T : Type u} [LinearOrder T] {ω : Control T} {ε : ENNReal} {l : List T} :
    List.IsChain (fun (a b : T) => a ≤ b ∧ ω.toFun a b ≤ ε) l → List.IsChain (fun (a b : T) => a ≤ b ∧ ω.toFun a b ≤ ε) (dedupChain l)

    Deduplication preserves the fine-chain property.

    source
    theorem RoughPaths.Sewing.pairSum_dedupChain {T : Type u} [LinearOrder T] {E : Type u_1} [AddCommMonoid E] {Ξ : T → T → E} (hdiag : ∀ (t : T), Ξ t t = 0) (l : List T) :
    pairSum Ξ (dedupChain l) = pairSum Ξ l

    Deduplication preserves pair sums when the summand vanishes on the diagonal.

    Strict chains and their extremes #

    source
    theorem RoughPaths.Sewing.head_lt_of_mem_tail {T : Type u} [LinearOrder T] {x : T} {l : List T} (h : List.IsChain (fun (x1 x2 : T) => x1 < x2) (x :: l)) {z : T} (hz : z ∈ l) :
    x < z

    On a strict chain, the head is strictly below every later element.

    source
    theorem RoughPaths.Sewing.head_le_getLast_of_lt {T : Type u} [LinearOrder T] {l : List T} :
    List.IsChain (fun (x1 x2 : T) => x1 < x2) l → ∀ (hl : l ≠ []), l.head hl ≤ l.getLast hl

    On a strict chain, the head is at most the last element.

    source
    theorem RoughPaths.Sewing.lt_getLast_of_mem_dropLast {T : Type u} [LinearOrder T] {l : List T} :
    List.IsChain (fun (x1 x2 : T) => x1 < x2) l → ∀ (hl : l ≠ []), ∀ z ∈ l.dropLast, z < l.getLast hl

    On a strict chain, every element other than the last is below the last.

    Refinement decomposition along a finer chain #

    source
    def RoughPaths.Sewing.refineAlong {T : Type u} [LinearOrder T] (r : List T) :
    List T → List (T × List T)

    Decompose a refinement r along a base chain: for consecutive base points x, y the inserted points are the elements of r strictly between them.

    Equations
    Instances For
      source
      @[simp]
      theorem RoughPaths.Sewing.refineAlong_nil {T : Type u} [LinearOrder T] (r : List T) :
      refineAlong r [] = []
      source
      @[simp]
      theorem RoughPaths.Sewing.refineAlong_singleton {T : Type u} [LinearOrder T] (r : List T) (x : T) :
      refineAlong r [x] = []
      source
      @[simp]
      theorem RoughPaths.Sewing.refineAlong_cons_cons {T : Type u} [LinearOrder T] (r : List T) (x y : T) (rest : List T) :
      refineAlong r (x :: y :: rest) = (x, List.filter (fun (z : T) => decide (x < z) && decide (z < y)) r) :: refineAlong r (y :: rest)
      source
      theorem RoughPaths.Sewing.basePoints_refineAlong {T : Type u} [LinearOrder T] (r mid : List T) (x t : T) :
      basePoints (refineAlong r (x :: (mid ++ [t]))) t = x :: (mid ++ [t])

      refineAlong recovers the base partition.

      source
      theorem RoughPaths.Sewing.glue_refineAlong {T : Type u} [LinearOrder T] (mid : List T) (x t : T) (rtail : List T) :
      List.IsChain (fun (x1 x2 : T) => x1 < x2) (x :: rtail) → List.IsChain (fun (x1 x2 : T) => x1 < x2) (x :: (mid ++ [t])) → (x :: rtail).getLast ⋯ = t → (∀ z ∈ x :: (mid ++ [t]), z ∈ x :: rtail) → glue (refineAlong (x :: rtail) (x :: (mid ++ [t]))) t = x :: rtail

      refineAlong recovers the refinement: if r = x :: rtail is a strict chain ending at t containing all the base points, gluing the decomposition along the base returns r.