English
If f has constant speed on s and on t with the same rate l, and x is the greatest point of s and the least point of t, then f has constant speed on s∪t with the same rate.
Русский
Если функция имеет одинаковую скорость на двух участках s и t и x является максимальным элементом s и минимальным элементом t, то на объединении s∪t функция имеет ту же скорость.
LaTeX
$$HasConstantSpeedOnWith f s l → HasConstantSpeedOnWith f t l → IsGreatest s x → IsLeast t x → HasConstantSpeedOnWith f (s ∪ t) l$$
Lean4
theorem union {t : Set ℝ} (hfs : HasConstantSpeedOnWith f s l) (hft : HasConstantSpeedOnWith f t l) {x : ℝ}
(hs : IsGreatest s x) (ht : IsLeast t x) : HasConstantSpeedOnWith f (s ∪ t) l :=
by
rw [hasConstantSpeedOnWith_iff_ordered] at hfs hft ⊢
rintro z (zs | zt) y (ys | yt) zy
· have : (s ∪ t) ∩ Icc z y = s ∩ Icc z y := by
ext w; constructor
· rintro ⟨ws | wt, zw, wy⟩
· exact ⟨ws, zw, wy⟩
· exact ⟨(le_antisymm (wy.trans (hs.2 ys)) (ht.2 wt)).symm ▸ hs.1, zw, wy⟩
· rintro ⟨ws, zwy⟩; exact ⟨Or.inl ws, zwy⟩
rw [this, hfs zs ys zy]
· have : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y :=
by
ext w; constructor
· rintro ⟨ws | wt, zw, wy⟩
exacts [Or.inl ⟨ws, zw, hs.2 ws⟩, Or.inr ⟨wt, ht.2 wt, wy⟩]
· rintro (⟨ws, zw, wx⟩ | ⟨wt, xw, wy⟩)
exacts [⟨Or.inl ws, zw, wx.trans (ht.2 yt)⟩, ⟨Or.inr wt, (hs.2 zs).trans xw, wy⟩]
rw [this, @eVariationOn.union _ _ _ _ f _ _ x, hfs zs hs.1 (hs.2 zs), hft ht.1 yt (ht.2 yt)]
· have q :=
ENNReal.ofReal_add (mul_nonneg l.prop (sub_nonneg.mpr (hs.2 zs))) (mul_nonneg l.prop (sub_nonneg.mpr (ht.2 yt)))
simp only [NNReal.val_eq_coe] at q
rw [← q]
ring_nf
exacts [⟨⟨hs.1, hs.2 zs, le_rfl⟩, fun w ⟨_, _, wx⟩ => wx⟩, ⟨⟨ht.1, le_rfl, ht.2 yt⟩, fun w ⟨_, xw, _⟩ => xw⟩]
· cases le_antisymm zy ((hs.2 ys).trans (ht.2 zt))
simp only [Icc_self, sub_self, mul_zero, ENNReal.ofReal_zero]
exact eVariationOn.subsingleton _ fun _ ⟨_, uz⟩ _ ⟨_, vz⟩ => uz.trans vz.symm
· have : (s ∪ t) ∩ Icc z y = t ∩ Icc z y := by
ext w; constructor
· rintro ⟨ws | wt, zw, wy⟩
· exact ⟨le_antisymm ((ht.2 zt).trans zw) (hs.2 ws) ▸ ht.1, zw, wy⟩
· exact ⟨wt, zw, wy⟩
· rintro ⟨wt, zwy⟩; exact ⟨Or.inr wt, zwy⟩
rw [this, hft zt yt zy]
