Gluing absolutely continuous curves

Absolute continuity on adjacent intervals implies absolute continuity on their union in a pseudometric space. This permits splitting and reassembling raw curves with either orientation, and gluing finite subdivisions, including subdivisions into affine cells. In particular a polygonal curve (TauCeti.IsPolygonalOnInterval) is absolutely continuous.

theorem AbsolutelyContinuousOnInterval.trans {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b c : ℝ} (h₁ : AbsolutelyContinuousOnInterval γ a c) (h₂ : AbsolutelyContinuousOnInterval γ c b) : AbsolutelyContinuousOnInterval γ a b

Absolute continuity on two intervals sharing an endpoint implies absolute continuity between their other endpoints, in either orientation.

theorem TauCeti.absolutelyContinuousOnInterval_iff_and {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b c : ℝ} (hc : c ∈ Set.uIcc a b) : AbsolutelyContinuousOnInterval γ a b ↔ AbsolutelyContinuousOnInterval γ a c ∧ AbsolutelyContinuousOnInterval γ c b

Absolute continuity can be checked on the two pieces of a parameter interval.

theorem AbsolutelyContinuousOnInterval.of_subdivision {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {N : ℕ} {s : Fin (N + 1) → ℝ} (h : ∀ (i : Fin N), AbsolutelyContinuousOnInterval γ (s i.castSucc) (s i.succ)) : AbsolutelyContinuousOnInterval γ (s 0) (s (Fin.last N))

Glue absolute continuity on all successive cells of a finite subdivision.

theorem AbsolutelyContinuousOnInterval.of_affine_subdivision {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {N : ℕ} {s : Fin (N + 1) → ℝ} (hs : StrictMono s) (ha : s 0 = a) (hb : s (Fin.last N) = b) (hsegments : ∀ (i : Fin N), ∀ t ∈ Set.Icc (s i.castSucc) (s i.succ), f t = f (s i.castSucc) + ((t - s i.castSucc) / (s i.succ - s i.castSucc)) • (f (s i.succ) - f (s i.castSucc))) : AbsolutelyContinuousOnInterval f a b

A finite increasing subdivision with affine interpolation on every cell gives an absolutely continuous curve. The subdivision may have no cells.

def TauCeti.IsPolygonalOnInterval {F : Type u_1} [AddCommGroup F] [Module ℝ F] (f : ℝ → F) (a b : ℝ) : Prop

A raw curve is polygonal on an interval if a finite increasing subdivision expresses it as the affine interpolation of its successive vertex values on every closed cell.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.IsPolygonalOnInterval.absolutelyContinuousOnInterval {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (h : IsPolygonalOnInterval f a b) : AbsolutelyContinuousOnInterval f a b

A polygonal curve is absolutely continuous: its finitely many affine cells glue together.