Continuous interpolation of the discrete contour

The time interval is normalized by the actual traversal duration, twice the number of edges. The usual affine interpolation is expressed by the finite sum of triangular hat functions. This also defines the singleton contour as the constant zero function, with no division by zero.

noncomputable def BGW.PlaneTree.contourTime (t : PlaneTree) (i : Fin t.contour.length) : ↑unitInterval

The time of discrete contour visit i, divided by the traversal duration. The denominator is one for the singleton tree, whose only index is zero.

Equations

• t.contourTime i = ⟨↑↑i / ↑(max (t.contour.length - 1) 1), ⋯⟩

noncomputable def BGW.PlaneTree.contourFunction (t : PlaneTree) : C(↑unitInterval, ℝ)

The polygonal contour as a continuous function on the unit interval.

Equations

• t.contourFunction = { toFun := fun (s : ↑unitInterval) => ∑ i : Fin t.contour.length, ↑t.contour[↑i] * max 0 (1 - |↑(t.contour.length - 1) * ↑s - ↑↑i|), continuous_toFun := ⋯ }

theorem BGW.PlaneTree.contourFunction_nonneg (t : PlaneTree) (s : ↑unitInterval) : 0 ≤ t.contourFunction s

theorem BGW.PlaneTree.duration_mul_contourTime (t : PlaneTree) (i : Fin t.contour.length) : ↑(t.contour.length - 1) * ↑(t.contourTime i) = ↑↑i

Multiplying a visit time by the traversal duration recovers its discrete index.

@[simp]

theorem BGW.PlaneTree.contourFunction_contourTime (t : PlaneTree) (i : Fin t.contour.length) : t.contourFunction (t.contourTime i) = ↑t.contour[↑i]

The continuous contour takes exactly the discrete height at every visit time.

theorem BGW.PlaneTree.contourFunction_on_segment (t : PlaneTree) (i : ℕ) (s : ↑unitInterval) (hi : i + 1 < t.contour.length) (hlo : ↑i ≤ ↑(t.contour.length - 1) * ↑s) (hhi : ↑(t.contour.length - 1) * ↑s ≤ ↑i + 1) : have θ := ↑(t.contour.length - 1) * ↑s - ↑i; t.contourFunction s = (1 - θ) * ↑t.contour[i] + θ * ↑t.contour[i + 1]

Between consecutive discrete visit times, the contour is their affine interpolation.

@[simp]

theorem BGW.PlaneTree.contourFunction_zero (t : PlaneTree) : t.contourFunction 0 = 0

@[simp]

theorem BGW.PlaneTree.contourFunction_one (t : PlaneTree) : t.contourFunction 1 = 0