English
Let f be a function with locally bounded variation on a subset s of a linear ordered domain. For any a ∈ s, the natural parameterization of f on s at a is a unit-speed curve whose image is the variation set variationOnFromTo f s a '' s.
Русский
Пусть f имеет локально ограниченную вариацию на подмножества s. Для произвольного a ∈ s естественная параметризация f на s в точке a является траекторией с единичной скоростью, чье изображение равно множество вариаций variationOnFromTo f s a '' s.
LaTeX
$$$\HasUnitSpeedOn(\mathrm{naturalParameterization}\,f\,s\,a,\ \mathrm{variationOnFromTo}\,f\,s\,a''s)$$$
Lean4
theorem has_unit_speed_naturalParameterization (f : α → E) {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α}
(as : a ∈ s) : HasUnitSpeedOn (naturalParameterization f s a) (variationOnFromTo f s a '' s) :=
by
dsimp only [HasUnitSpeedOn]
rw [hasConstantSpeedOnWith_iff_ordered]
rintro _ ⟨b, bs, rfl⟩ _ ⟨c, cs, rfl⟩ h
rcases le_total c b with (cb | bc)
· rw [NNReal.coe_one, one_mul, le_antisymm h (variationOnFromTo.monotoneOn hf as cs bs cb), sub_self,
ENNReal.ofReal_zero, Icc_self, eVariationOn.subsingleton]
exact fun x hx y hy => hx.2.trans hy.2.symm
· rw [NNReal.coe_one, one_mul, sub_eq_add_neg, variationOnFromTo.eq_neg_swap, neg_neg, add_comm,
variationOnFromTo.add hf bs as cs, ← variationOnFromTo.eq_neg_swap f]
rw [←
eVariationOn.comp_inter_Icc_eq_of_monotoneOn (naturalParameterization f s a) _
(variationOnFromTo.monotoneOn hf as) bs cs]
rw [@eVariationOn.eq_of_edist_zero_on _ _ _ _ _ f]
· rw [variationOnFromTo.eq_of_le _ _ bc, ENNReal.ofReal_toReal (hf b c bs cs)]
· rintro x ⟨xs, _, _⟩
exact edist_naturalParameterization_eq_zero hf as xs
