CH2.ϕ_pm_deriv_Iic_finite

lemma ϕ_pm_deriv_Iic_finite (ν ε : ℝ) :    eVariationOn (deriv (ϕ_pm ν ε)) (Set.Iic (-1 : ℝ)) ≠ ⊤ := by  set g := deriv (ϕ_pm ν ε)  have hg_zero : ∀ t < -1, g t = 0 := fun t ht ↦ ϕ_pm_deriv_zero_outside ν ε (Or.inl 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.min' hS    have hk_mem : k ∈ S := Finset.min'_mem S hS    have hu_k : u k = -1 := (Finset.mem_filter.mp hk_mem).2    have hu_lt : ∀ i < k, u i < -1 := by      intro i hi      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 (lt_trans hi (Finset.mem_range.mp (Finset.mem_filter.mp hk_mem).1)), h_eq⟩      linarith [S.min'_le i hi_S]    have hk_n : k ≤ n := Nat.le_of_lt_succ (Finset.mem_range.mp (Finset.mem_filter.mp hk_mem).1)    have hu_eq : ∀ i ≥ k, i ≤ n → u i = -1 := fun i hi h_in ↦      le_antisymm (hu_mem i) (hu_k ▸ hu hi)    calc ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u i))      _ = ∑ i ∈ Finset.range n, if i + 1 = 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) = -1 from by rw [h_eq_k, hu_k], hg_zero _ (hu_lt _ (by omega))]        · by_cases h_lt_k : i + 1 < k          · rw [hg_zero _ (hu_lt _ h_lt_k), hg_zero _ (hu_lt _ (by omega)), edist_self]          · rw [show u (i + 1) = -1 from hu_eq _ (by omega) (by omega),                show u i = -1 from hu_eq _ (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 + 1 = 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            omega        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_lt : ∀ 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⟩ : ∃ 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_lt (i + 1) hi_n), hg_zero _ (h_lt i hi_n.le), edist_self]      _ = 0 := by simp      _ ≤ edist (g (-1)) 0 := by positivity