English
HasConstantSpeedOnWith f s l is equivalent to LocallyBoundedVariationOn f s together with a precise formula for variationOnFromTo on any pair x,y in s: variationOnFromTo f s x y = l(y−x).
Русский
HasConstantSpeedOnWith f s l эквивалентно LocallyBoundedVariationOn f s и точной формуле для variationOnFromTo на любом паре x,y∈s: variationOnFromTo f s x y = l(y−x).
LaTeX
$$HasConstantSpeedOnWith f s l ⇔ (LocallyBoundedVariationOn f s ∧ ∀ x∈s, y∈s, variationOnFromTo f s x y = l·(y−x))$$
Lean4
theorem hasConstantSpeedOnWith_iff_variationOnFromTo_eq :
HasConstantSpeedOnWith f s l ↔
LocallyBoundedVariationOn f s ∧ ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), variationOnFromTo f s x y = l * (y - x) :=
by
constructor
· rintro h; refine ⟨h.hasLocallyBoundedVariationOn, fun x xs y ys => ?_⟩
rw [hasConstantSpeedOnWith_iff_ordered] at h
rcases le_total x y with (xy | yx)
· rw [variationOnFromTo.eq_of_le f s xy, h xs ys xy]
exact ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr xy))
· rw [variationOnFromTo.eq_of_ge f s yx, h ys xs yx]
have := ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr yx))
simp_all only [NNReal.val_eq_coe]; ring
· rw [hasConstantSpeedOnWith_iff_ordered]
rintro h x xs y ys xy
rw [← h.2 xs ys, variationOnFromTo.eq_of_le f s xy, ENNReal.ofReal_toReal (h.1 x y xs ys)]
