RS_prime.summable_pre413

theorem summable_pre413 {f : ℝ → ℝ} {s : Set ℝ} (hs : Bornology.IsBounded s) (hs_measureable : MeasurableSet s) :  Summable fun (n: ℕ) ↦ ∫ (x : ℝ) in n..(n + 1), f x ∂«θ».Stieltjes.measure.restrict s := by   by_cases s_empty: s = ∅  · rw [summable_congr (g := 0)]    · apply summable_zero    · simp [s_empty, intervalIntegral.integral_of_le]   apply summable_of_hasFiniteSupport  apply Set.Finite.subset (s := Finset.Icc (⌊sInf s⌋₊ - 1) (⌈sSup s⌉₊ + 1))  · apply finite_toSet  · intro a ha    simp only [Function.mem_support, ne_eq] at ha    rw [← ne_eq] at ha    by_contra!    rw [intervalIntegral.integral_zero_ae] at ha    · simp at ha    · rw [MeasureTheory.ae_iff]      rw [Measure.restrict_apply']      · simp only [le_add_iff_nonneg_right, zero_le_one, Set.uIoc_of_le, Set.mem_Ioc,          and_imp, Classical.not_imp]        rw [Set.setOf_and]        rw [Set.setOf_and]        rw [← Set.inter_assoc]        nth_rw 1 [Set.inter_assoc]        rw [Set.inter_comm]        rw [Set.inter_assoc]        apply MeasureTheory.measure_inter_null_of_null_right        · conv =>            arg 1            arg 2            equals ∅ =>              ext c              simp only [Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false,                not_and, not_le]              intro c_mem a_lt              simp only [coe_Icc, Set.mem_Icc, not_and_or] at this              cases this              · rename_i le_a                rw [tsub_le_iff_right, not_le] at le_a                apply Nat.lt_of_lt_floor at le_a                simp at le_a                have := csInf_le (hs.bddBelow) c_mem                linarith              · rename_i a_le                rw [not_le] at a_le                apply LT.lt.le at a_le                rw [Order.add_one_le_iff] at a_le                apply LT.lt.le at a_le                apply Nat.le_of_ceil_le at a_le                grw [le_csSup hs.bddAbove c_mem] at a_lt                linarith          simp      · apply hs_measureable