RS.Integ.boundedVariationOn_of_forall_sumAbsDiff_le

lemma boundedVariationOn_of_forall_sumAbsDiff_le    {a b : ℝ} (hab : a < b)    (g : ℝ → ℝ) (K : ℝ)    (hK : ∀ P : RS.IPart.IPartition a b, RS.SumDiff.sumAbsDiff g P ≤ K) :    BoundedVariationOn g (Set.Icc a b) := by -- By definition of BoundedVariationOn, if for all partitions P of [a, b], the sum of absolute differences of g over P is bounded by K, then g has bounded variation on [a, b]. apply ne_of_lt; refine' lt_of_le_of_lt ( iSup_le _ ) _; exact ENNReal.ofReal K; · simp +decide [ edist_dist ];   -- By the properties of the partition, the sum of the absolute differences over the partition P is equal to the sum of the absolute differences of g over the partition P.   have h_sum_eq : ∀ (n : ℕ) (x : Fin (n + 1) → ℝ) (hx : Monotone x) (hx_mem : ∀ i, x i ∈ Set.Icc a b), ∑ i : Fin n, |g (x i.succ) - g (x i.castSucc)| ≤ K := by     exact fun n x hx hx_mem ↦ SumDiff.sum_le_K_of_forall_sumAbsDiff_le hab g K hK n x hx hx_mem;   intro n x hx hx'; specialize h_sum_eq n ( fun i => x i ) ( fun i j hij => hx hij ) ( fun i => hx' i ) ; simp_all +decide [ dist_eq_norm, Finset.sum_range ] ;   simpa only [ ENNReal.ofReal_sum_of_nonneg fun _ _ => abs_nonneg _ ] using ENNReal.ofReal_le_ofReal h_sum_eq; · exact ENNReal.ofReal_lt_top