Documentation

TauCeti.MeasureTheory.Function.CurveAction.Polygonal

Polygonal interpolation on a uniform grid and its action #

Given points x 0, x 1, …, x N of a real vector space and the uniform grid t_k = a + k * h with step h > 0, the polygonal interpolation TauCeti.polygonalInterpolation a h N x is the curve that passes through x k at time t_k and is affine on each cell [t_k, t_(k+1)]. It is written as the sum ∑ k ≤ N, φ ((t - t_k) / h) • x k against the hat function φ s = max 0 (1 - |s|). It depends continuously on the points and on the time jointly when addition and real scalar multiplication are continuous.

In a real seminormed space, on the cell [t_k, t_(k+1)] the curve moves at the constant speed ‖x (k + 1) - x k‖ / h, so its p-action over [a, a + N * h], for every real p, is the discrete action

∑ k < N, edist (x k) (x (k + 1)) ^ p * ENNReal.ofReal h ^ (1 - p)

of the points, with powers in ℝ≥0∞. For 1 ≤ p, Hölder's inequality on each cell bounds the discrete action of the samples of an absolutely continuous curve at the grid times by the action of the curve (TauCeti.sum_edist_rpow_mul_rpow_one_sub_le_curveAction). The facts about the interpolation are stated for every curve agreeing with the interpolation on [a, a + N * h], such as its restriction to that interval extended by constants. Interpolating the points of a law on sequences turns it into a law on paths whose expected action is the expected discrete action; this is how laws of random curves are built from couplings at finitely many times, in the superposition principle for absolutely continuous curves of probability measures.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.polygonalInterpolation {E : Type u_1} [AddCommGroup E] [Module ℝ E] (a h : ℝ) (N : ℕ) (x : ℕ → E) (t : ℝ) :
E

The polygonal interpolation of the points x 0, …, x N on the uniform grid a + k * h, defined for every real h as the sum of the x k against the hat functions max 0 (1 - |t - (a + k * h)| / h). For a step h > 0, it is the curve taking the value x k at time a + k * h and affine between consecutive grid times, and outside [a, a + N * h] it decays to 0 within one step.

Instances For
    source
    theorem TauCeti.polygonalInterpolation_def {E : Type u_1} [AddCommGroup E] [Module ℝ E] (a h : ℝ) (N : ℕ) (x : ℕ → E) (t : ℝ) :
    polygonalInterpolation a h N x t = ∑ k ∈ Finset.range (N + 1), max 0 (1 - |t - (a + ↑k * h)| / h) • x k

    The defining formula of the polygonal interpolation, as a sum against hat functions.

    source
    theorem TauCeti.polygonalInterpolation_eq_of_mem_Icc {E : Type u_1} {a h t : ℝ} {N k : ℕ} [AddCommGroup E] [Module ℝ E] (x : ℕ → E) (hh : 0 < h) (hk : k < N) (ht : t ∈ Set.Icc (a + ↑k * h) (a + (↑k + 1) * h)) :
    polygonalInterpolation a h N x t = x k + ((t - (a + ↑k * h)) / h) • (x (k + 1) - x k)

    The affine formula on a cell. On [a + k * h, a + (k + 1) * h], for k < N, the polygonal interpolation is the affine segment from x k to x (k + 1).

    source
    @[simp]
    theorem TauCeti.polygonalInterpolation_apply_grid {E : Type u_1} {a h : ℝ} {N k : ℕ} [AddCommGroup E] [Module ℝ E] (x : ℕ → E) (hh : 0 < h) (hk : k ≤ N) :
    polygonalInterpolation a h N x (a + ↑k * h) = x k

    The interpolation passes through the points. At the grid time a + k * h, for k ≤ N, the polygonal interpolation takes the value x k.

    source
    theorem TauCeti.continuous_polygonalInterpolation {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] (a h : ℝ) (N : ℕ) :
    Continuous fun (q : (ℕ → E) × ℝ) => polygonalInterpolation a h N q.1 q.2

    The polygonal interpolation is jointly continuous in the points and the time.

    source
    theorem TauCeti.isPolygonalOnInterval_of_eqOn_polygonalInterpolation {E : Type u_1} {a h : ℝ} {N : ℕ} [AddCommGroup E] [Module ℝ E] {x : ℕ → E} {f : ℝ → E} (hN : N ≠ 0) (hh : 0 < h) (hf : Set.EqOn f (polygonalInterpolation a h N x) (Set.Icc a (a + ↑N * h))) :
    IsPolygonalOnInterval f a (a + ↑N * h)

    The interpolation is polygonal. For N ≠ 0 and h > 0, a curve that agrees with a polygonal interpolation on [a, a + N * h] is polygonal there, with vertices at the grid times. In a normed space this also implies absolute continuity.

    source
    theorem TauCeti.exists_continuousMap_IccExtend_eqOn_polygonalInterpolation {E : Type u_1} {a h : ℝ} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {b : ℝ} (hab : a ≤ b) (N : ℕ) (hNh : a + ↑N * h = b) :
    ∃ (Φ : C(ℕ → E, C(↑(Set.Icc a b), E))), ∀ (x : ℕ → E), Set.EqOn (Set.IccExtend hab ⇑(Φ x)) (polygonalInterpolation a h N x) (Set.Icc a (a + ↑N * h))

    The polygonal paths through sequences of points, defined on [a, b] where a + N * h = b, depend continuously on the sequence: they are the values of a continuous map C(ℕ → E, C(Icc a b, E)).

    source
    theorem TauCeti.curveAction_eq_sum_edist_rpow_mul_rpow_one_sub_of_eqOn_polygonalInterpolation {E : Type u_1} {a h : ℝ} {N : ℕ} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x : ℕ → E} {f : ℝ → E} {p : ℝ} (hh : 0 < h) (hf : Set.EqOn f (polygonalInterpolation a h N x) (Set.Icc a (a + ↑N * h))) :
    curveAction p f a (a + ↑N * h) = ∑ k ∈ Finset.range N, edist (x k) (x (k + 1)) ^ p * ENNReal.ofReal h ^ (1 - p)

    The action of a polygonal interpolation is the discrete action. For every real p, the p-action over [a, a + N * h] of a curve agreeing there with the polygonal interpolation of x 0, …, x N is ∑ k < N, d(x k, x (k + 1)) ^ p * h ^ (1 - p), with powers in ℝ≥0∞. For negative p, a zero-length edge contributes ∞.