English
For any f and any s, edist(f x, f y) ≤ eVariationOn f s whenever x,y ∈ s.
Русский
Для любых f и s, если x,y ∈ s, то edist(f x, f y) ≤ eVariationOn f s.
LaTeX
$$$\forall f:α\to E,\; s, x,y\in s\Rightarrow edist(f x, f y) \le eVariationOn f s$$
Lean4
/-- The variation of a function on the union of two sets `s` and `t`, with `s` to the left of `t`,
bounds the sum of the variations along `s` and `t`. -/
theorem add_le_union (f : α → E) {s t : Set α} (h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y) :
eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t) :=
by
by_cases hs : s = ∅
· simp [hs]
have : Nonempty { u // Monotone u ∧ ∀ i : ℕ, u i ∈ s } := nonempty_monotone_mem (nonempty_iff_ne_empty.2 hs)
by_cases ht : t = ∅
· simp [ht]
have : Nonempty { u // Monotone u ∧ ∀ i : ℕ, u i ∈ t } := nonempty_monotone_mem (nonempty_iff_ne_empty.2 ht)
refine
ENNReal.iSup_add_iSup_le
?_
/- We start from two sequences `u` and `v` along `s` and `t` respectively, and we build a new
sequence `w` along `s ∪ t` by juxtaposing them. Its variation is larger than the sum of the
variations. -/
rintro ⟨n, ⟨u, hu, us⟩⟩ ⟨m, ⟨v, hv, vt⟩⟩
let w i := if i ≤ n then u i else v (i - (n + 1))
have wst : ∀ i, w i ∈ s ∪ t := by
intro i
by_cases hi : i ≤ n
· simp [w, hi, us]
· simp [w, hi, vt]
have hw : Monotone w := by
intro i j hij
dsimp only [w]
split_ifs with h_1 h_2 h_2
· exact hu hij
· apply h _ (us _) _ (vt _)
· exfalso; exact h_1 (hij.trans h_2)
· apply hv (tsub_le_tsub hij le_rfl)
calc
((∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) + ∑ i ∈ Finset.range m, edist (f (v (i + 1))) (f (v i))) =
(∑ i ∈ Finset.range n, edist (f (w (i + 1))) (f (w i))) +
∑ i ∈ Finset.range m, edist (f (w (n + 1 + i + 1))) (f (w (n + 1 + i))) :=
by
dsimp only [w]
congr 1
· grind [Finset.sum_congr]
· grind
_ =
(∑ i ∈ Finset.range n, edist (f (w (i + 1))) (f (w i))) +
∑ i ∈ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (i + 1))) (f (w i)) :=
by
congr 1
rw [Finset.range_eq_Ico]
convert Finset.sum_Ico_add (fun i : ℕ => edist (f (w (i + 1))) (f (w i))) 0 m (n + 1) using 3 <;> abel
_ ≤ ∑ i ∈ Finset.range (n + 1 + m), edist (f (w (i + 1))) (f (w i)) :=
by
rw [← Finset.sum_union]
· gcongr
rintro i hi
simp only [Finset.mem_union, Finset.mem_range, Finset.mem_Ico] at hi ⊢
cutsat
· refine Finset.disjoint_left.2 fun i hi h'i => ?_
simp only [Finset.mem_Ico, Finset.mem_range] at hi h'i
exact hi.not_gt (Nat.lt_of_succ_le h'i.left)
_ ≤ eVariationOn f (s ∪ t) := sum_le f _ hw wst
