English
HasConstantSpeedOnWith f s l is equivalent to a crest of conditions with order: for all x∈s, y∈s, if x ≤ y then a variation formula holds.
Русский
HasConstantSpeedOnWith f s l эквивалентно совокупности условий порядка: для всех x,y∈s, если x ≤ y, тогда выполняется формула вариации.
LaTeX
$$HasConstantSpeedOnWith f s l ⇔ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal(l(y−x))$$
Lean4
/-- If both `f` and `f ∘ φ` have unit speed (on `Icc 0 t` and `Icc 0 s` respectively)
and `φ` monotonically maps `Icc 0 s` onto `Icc 0 t`, then `φ` is the identity on `Icc 0 s`
-/
theorem unique_unit_speed_on_Icc_zero {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) {φ : ℝ → ℝ} (φm : MonotoneOn φ <| Icc 0 s)
(φst : φ '' Icc 0 s = Icc 0 t) (hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)) (hf : HasUnitSpeedOn f (Icc 0 t)) :
EqOn φ id (Icc 0 s) := by
rw [← φst] at hf
convert unique_unit_speed φm hfφ hf ⟨le_rfl, hs⟩ using 1
have : φ 0 = 0 := by
have hm : 0 ∈ φ '' Icc 0 s := by simp only [φst, ht, mem_Icc, le_refl, and_self]
obtain ⟨x, xs, hx⟩ := hm
apply le_antisymm ((φm ⟨le_rfl, hs⟩ xs xs.1).trans_eq hx) _
have := φst ▸ mapsTo_image φ (Icc 0 s)
exact (mem_Icc.mp (@this 0 (by rw [mem_Icc]; exact ⟨le_rfl, hs⟩))).1
simp only [tsub_zero, this, add_zero]
rfl
