English
Given two speeds l and l', with l' ≠ 0, and a monotone φ mapping s to itself, if f∘φ has speed l on s and f has speed l' on φ(s), then φ is affine with slope l/l' on s, i.e., φ(y) = φ(x) + (l/l')(y−x) for all y in s given x in s.
Русский
Дано две скорости l и l', с l' ≠ 0, и монотонное отображение φ, переводящее s в s. Если f∘φ имеет скорость l на s, а f имеет скорость l' на φ(s), то φ на s является афинной: φ(y) = φ(x) + (l/l')(y−x) для всех y∈s и фиксированного x.
LaTeX
$$ratio {l' : ℝ≥0} (hl' : l' ≠ 0) {φ : ℝ → ℝ} (φm : MonotoneOn φ s) (hfφ : HasConstantSpeedOnWith (f ∘ φ) s l) (hf : HasConstantSpeedOnWith f (φ '' s) l') ⦃x : Real⦄ (xs : x ∈ s) : EqOn φ (fun y => l / l' * (y - x) + φ x) s$$
Lean4
theorem ratio {l' : ℝ≥0} (hl' : l' ≠ 0) {φ : ℝ → ℝ} (φm : MonotoneOn φ s) (hfφ : HasConstantSpeedOnWith (f ∘ φ) s l)
(hf : HasConstantSpeedOnWith f (φ '' s) l') ⦃x : ℝ⦄ (xs : x ∈ s) : EqOn φ (fun y => l / l' * (y - x) + φ x) s :=
by
rintro y ys
rw [← sub_eq_iff_eq_add, mul_comm, ← mul_div_assoc, eq_div_iff (NNReal.coe_ne_zero.mpr hl')]
rw [hasConstantSpeedOnWith_iff_variationOnFromTo_eq] at hf
rw [hasConstantSpeedOnWith_iff_variationOnFromTo_eq] at hfφ
symm
calc
(y - x) * l = l * (y - x) := by rw [mul_comm]
_ = variationOnFromTo (f ∘ φ) s x y := (hfφ.2 xs ys).symm
_ = variationOnFromTo f (φ '' s) (φ x) (φ y) := (variationOnFromTo.comp_eq_of_monotoneOn f φ φm xs ys)
_ = l' * (φ y - φ x) := (hf.2 ⟨x, xs, rfl⟩ ⟨y, ys, rfl⟩)
_ = (φ y - φ x) * l' := by rw [mul_comm]
