Lean4
/-- Consider a monotone function `u` parameterizing some points of a set `s`. Given `x ∈ s`, then
one can find another monotone function `v` parameterizing the same points as `u`, with `x` added.
In particular, the variation of a function along `u` is bounded by its variation along `v`. -/
theorem add_point (f : α → E) {s : Set α} {x : α} (hx : x ∈ s) (u : ℕ → α) (hu : Monotone u) (us : ∀ i, u i ∈ s)
(n : ℕ) :
∃ (v : ℕ → α) (m : ℕ),
Monotone v ∧
(∀ i, v i ∈ s) ∧
x ∈ v '' Iio m ∧
(∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) ≤
∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j)) :=
by
rcases le_or_gt (u n) x with (h | h)
· let v i := if i ≤ n then u i else x
have vs : ∀ i, v i ∈ s := fun i ↦ by
simp only [v]
split_ifs
· exact us i
· exact hx
have hv : Monotone v := by
refine monotone_nat_of_le_succ fun i => ?_
simp only [v]
rcases lt_trichotomy i n with (hi | rfl | hi)
· have : i + 1 ≤ n := Nat.succ_le_of_lt hi
simp only [hi.le, this, if_true]
exact hu (Nat.le_succ i)
· simp only [le_refl, if_true, add_le_iff_nonpos_right, Nat.le_zero, Nat.one_ne_zero, if_false, h]
· have A : ¬i ≤ n := hi.not_ge
have B : ¬i + 1 ≤ n := fun h => A (i.le_succ.trans h)
simp only [A, B, if_false, le_rfl]
refine ⟨v, n + 2, hv, vs, (mem_image _ _ _).2 ⟨n + 1, ?_, ?_⟩, ?_⟩
· rw [mem_Iio]; exact Nat.lt_succ_self (n + 1)
· have : ¬n + 1 ≤ n := Nat.not_succ_le_self n
simp only [v, this, ite_eq_right_iff, IsEmpty.forall_iff]
·
calc
(∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) :=
by
apply Finset.sum_congr rfl fun i hi => ?_
simp only [Finset.mem_range] at hi
have : i + 1 ≤ n := Nat.succ_le_of_lt hi
simp only [v, hi.le, this, if_true]
_ ≤ ∑ j ∈ Finset.range (n + 2), edist (f (v (j + 1))) (f (v j)) :=
by
gcongr
apply Nat.le_add_right
have exists_N : ∃ N, N ≤ n ∧ x < u N := ⟨n, le_rfl, h⟩
let N := Nat.find exists_N
have hN : N ≤ n ∧ x < u N := Nat.find_spec exists_N
let w : ℕ → α := fun i => if i < N then u i else if i = N then x else u (i - 1)
have ws : ∀ i, w i ∈ s := by grind
have hw : Monotone w := by
apply monotone_nat_of_le_succ fun i => ?_
dsimp only [w]
rcases lt_trichotomy (i + 1) N with (hi | hi | hi)
· have : i < N := Nat.lt_of_le_of_lt (Nat.le_succ i) hi
simp only [hi, this, if_true]
exact hu (Nat.le_succ _)
· have A : i < N := hi ▸ i.lt_succ_self
have B : ¬i + 1 < N := by rw [← hi]; exact fun h => h.ne rfl
rw [if_pos A, if_neg B, if_pos hi]
have T := Nat.find_min exists_N A
push_neg at T
exact T (A.le.trans hN.1)
· have A : ¬i < N := (Nat.lt_succ_iff.mp hi).not_gt
have B : ¬i + 1 < N := hi.not_gt
have C : ¬i + 1 = N := hi.ne.symm
have D : i + 1 - 1 = i := Nat.pred_succ i
rw [if_neg A, if_neg B, if_neg C, D]
split_ifs
· exact hN.2.le.trans (hu (le_of_not_gt A))
· exact hu (Nat.pred_le _)
refine ⟨w, n + 1, hw, ws, (mem_image _ _ _).2 ⟨N, hN.1.trans_lt (Nat.lt_succ_self n), ?_⟩, ?_⟩
· dsimp only [w]; rw [if_neg (lt_irrefl N), if_pos rfl]
rcases eq_or_lt_of_le (zero_le N) with (Npos | Npos)
·
calc
(∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
∑ i ∈ Finset.range n, edist (f (w (1 + i + 1))) (f (w (1 + i))) :=
by grind
_ = ∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)) :=
by
rw [Finset.range_eq_Ico]
exact Finset.sum_Ico_add (fun i => edist (f (w (i + 1))) (f (w i))) 0 n 1
_ ≤ ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)) :=
by
rw [Finset.range_eq_Ico]
gcongr
exact zero_le_one
·
calc
(∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
((∑ i ∈ Finset.Ico 0 (N - 1), edist (f (u (i + 1))) (f (u i))) +
∑ i ∈ Finset.Ico (N - 1) N, edist (f (u (i + 1))) (f (u i))) +
∑ i ∈ Finset.Ico N n, edist (f (u (i + 1))) (f (u i)) :=
by
rw [Finset.sum_Ico_consecutive, Finset.sum_Ico_consecutive, Finset.range_eq_Ico]
· exact zero_le _
· exact hN.1
· exact zero_le _
· exact Nat.pred_le _
_ =
(∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i))) + edist (f (u N)) (f (u (N - 1))) +
∑ i ∈ Finset.Ico N n, edist (f (w (1 + i + 1))) (f (w (1 + i))) :=
by
congr 1
· congr 1
· grind [Finset.mem_Ico, Finset.sum_congr]
· have A : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
have : Finset.Ico (N - 1) N = {N - 1} := by rw [← Nat.Ico_succ_singleton, A]
simp only [this, A, Finset.sum_singleton]
· grind [Finset.sum_congr, Finset.mem_Ico]
_ =
(∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i))) + edist (f (w (N + 1))) (f (w (N - 1))) +
∑ i ∈ Finset.Ico (N + 1) (n + 1), edist (f (w (i + 1))) (f (w i)) :=
by
congr 1
· grind
· exact Finset.sum_Ico_add (fun i => edist (f (w (i + 1))) (f (w i))) N n 1
_ ≤
((∑ i ∈ Finset.Ico 0 (N - 1), edist (f (w (i + 1))) (f (w i))) +
∑ i ∈ Finset.Ico (N - 1) (N + 1), edist (f (w (i + 1))) (f (w i))) +
∑ i ∈ Finset.Ico (N + 1) (n + 1), edist (f (w (i + 1))) (f (w i)) :=
by
refine add_le_add (add_le_add le_rfl ?_) le_rfl
have A : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
have B : N - 1 + 1 < N + 1 := A.symm ▸ N.lt_succ_self
have C : N - 1 < N + 1 := lt_of_le_of_lt N.pred_le N.lt_succ_self
rw [Finset.sum_eq_sum_Ico_succ_bot C, Finset.sum_eq_sum_Ico_succ_bot B, A, Finset.Ico_self, Finset.sum_empty,
add_zero, add_comm (edist _ _)]
exact edist_triangle _ _ _
_ = ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)) :=
by
rw [Finset.sum_Ico_consecutive, Finset.sum_Ico_consecutive, Finset.range_eq_Ico]
· exact zero_le _
· exact Nat.succ_le_succ hN.left
· exact zero_le _
· exact N.pred_le.trans N.le_succ
