WI_sum_Iab_le

lemma WI_sum_Iab_le {f : ℕ → ℝ} (hpos : 0 ≤ f) {C : ℝ} (hcheby : chebyWith C f) (hb : 0 < b) (hxb : 2 / b < x) :    (∑' n, f n * indicator (Ico a b) 1 (n / x)) / x ≤ C * 2 * b := by  have hb' : 0 < 2 / b := by positivity  have hx : 0 < x := by linarith  have hxb' : 2 < x * b := (div_lt_iff₀ hb).mp hxb  have l1 (i : ℕ) (hi : i ∉ Finset.range ⌈b * x⌉₊) : f i * indicator (Ico a b) 1 (i / x) = 0 := by    simp_all [le_div_iff₀ hx]  have l2 (i : ℕ) (_ : i ∈ Finset.range ⌈b * x⌉₊) : f i * indicator (Ico a b) 1 (i / x) ≤ |f i| := by    rw [abs_eq_self.mpr (hpos _)]    convert_to _ ≤ f i * 1    · ring    apply mul_le_mul_of_nonneg_left ?_ (hpos _)    by_cases hi : (i / x) ∈ (Ico a b) <;> simp [hi]  rw [tsum_eq_sum l1, div_le_iff₀ hx, mul_assoc, mul_assoc]  apply Finset.sum_le_sum l2 |>.trans  have := hcheby ⌈b * x⌉₊ ; simp only [norm_real, norm_eq_abs] at this ; apply this.trans  have : 0 ≤ C := by have := hcheby 1 ; simp only [cumsum, Finset.range_one, norm_real,    Finset.sum_singleton, Nat.cast_one, mul_one] at this ; exact (abs_nonneg _).trans this  refine mul_le_mul_of_nonneg_left ?_ this  apply (Nat.ceil_lt_add_one (by positivity)).le.trans  linarith