Polygonal approximation of absolutely continuous curves

Absolutely continuous curves in finite-dimensional real normed spaces admit polygonal approximations with the same endpoints, converging uniformly and with their derivatives in L¹. The construction integrates finite interval step functions and corrects their average velocity.

theorem AbsolutelyContinuousOnInterval.exists_polygonal_approximation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [FiniteDimensional ℝ E] {γ : ℝ → E} (hγ : AbsolutelyContinuousOnInterval γ a b) (hab : a < b) : ∃ (γn : ℕ → ℝ → E), (∀ (n : ℕ), TauCeti.IsPolygonalOnInterval (γn n) a b ∧ γn n a = γ a ∧ γn n b = γ b) ∧ TendstoUniformlyOn γn γ Filter.atTop (Set.Icc a b) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ) in a..b, ‖deriv (γn n) t - deriv γ t‖) Filter.atTop (nhds 0)

Every absolutely continuous curve in a finite-dimensional real normed space admits polygonal approximations with the same endpoints, converging uniformly and with their derivatives in L¹.