CH2.ϕ_pm_deriv_Ici_finite

lemma ϕ_pm_deriv_Ici_finite (ν ε : ℝ) :    eVariationOn (deriv (ϕ_pm ν ε)) (Set.Ici (1 : ℝ)) ≠ ⊤ := by  set g := deriv (ϕ_pm ν ε)  have hg_zero : ∀ t > 1, g t = 0 := fun t ht ↦ ϕ_pm_deriv_zero_outside ν ε (Or.inr ht)  apply ne_top_of_le_ne_top (edist_lt_top (g 1) 0).ne  apply iSup_le; rintro ⟨n, u, hu, hu_mem⟩  by_cases h_any : ∃ i ∈ Finset.range (n + 1), u i = 1  · let S := (Finset.range (n + 1)).filter (fun i ↦ u i = 1)    have hS : S.Nonempty :=      h_any.elim fun i ⟨hi, eq⟩ => ⟨i, Finset.mem_filter.mpr ⟨hi, eq⟩⟩    let k := S.max' hS    have hk_mem : k ∈ S := Finset.max'_mem S hS    have hu_k : u k = 1 := (Finset.mem_filter.mp hk_mem).2    have hu_gt : ∀ i > k, i ≤ n → u i > 1 := by      intro i hi hi_n      apply lt_of_le_of_ne (hu_mem i)      intro h_eq      have hi_S : i ∈ S := Finset.mem_filter.mpr ⟨Finset.mem_range.mpr (Nat.lt_succ_of_le hi_n), h_eq.symm⟩      linarith [S.le_max' i hi_S]    have hu_eq : ∀ i ≤ k, u i = 1 := fun i hi ↦      le_antisymm (hu_k ▸ hu hi) (hu_mem i)    calc ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u i))      _ = ∑ i ∈ Finset.range n, if i = k then edist (g 1) 0 else 0 := by        apply Finset.sum_congr rfl; intro i hi        have hi_n : i < n := Finset.mem_range.mp hi        split_ifs with h_eq_k        · rw [show u i = 1 from by rw [h_eq_k, hu_k], hg_zero _ (hu_gt _ (by omega) (by omega)), edist_comm]        · by_cases h_lt_k : i < k          · rw [show u (i + 1) = 1 from hu_eq _ (by omega), show u i = 1 from hu_eq _ (by omega), edist_self]          · rw [hg_zero _ (hu_gt _ (by omega) (by omega)), hg_zero _ (hu_gt _ (by omega) (by omega)), edist_self]      _ ≤ edist (g 1) 0 := by        rw [Finset.sum_ite]; simp only [Finset.sum_const_zero, add_zero]        let fS := (Finset.range n).filter (fun i ↦ i = k)        have h_card : fS.card ≤ 1 :=          Finset.card_le_one_iff.mpr fun hx hy => by            have hx := (Finset.mem_filter.mp hx).2            have hy := (Finset.mem_filter.mp hy).2            exact hx.trans hy.symm        calc (fS.sum (fun _ ↦ edist (g 1) 0))          _ = fS.card • edist (g 1) 0 := Finset.sum_const _          _ ≤ 1 • edist (g 1) 0 := by gcongr          _ = edist (g 1) 0 := by simp  · have h_gt : ∀ i ≤ n, u i > 1 := fun i hi =>      lt_of_le_of_ne (hu_mem i) fun h_eq =>        absurd (⟨i, Finset.mem_range.mpr (Nat.lt_succ_of_le hi), h_eq.symm⟩ : ∃ i ∈ Finset.range (n + 1), u i = 1) h_any    calc ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u i))      _ = ∑ i ∈ Finset.range n, 0 := by        apply Finset.sum_congr rfl; intro i hi        have hi_n : i < n := Finset.mem_range.mp hi        rw [hg_zero _ (h_gt (i + 1) hi_n), hg_zero _ (h_gt i hi_n.le), edist_self]      _ = 0 := by simp      _ ≤ edist (g 1) 0 := by positivity