auto_cheby_bootstrap_induction

lemma auto_cheby_bootstrap_induction (hpos : 0 ≤ f)    (h_short : ∃ (ε : ℝ) (C : ℝ), ε > 0 ∧ ε < 1 ∧ C > 0 ∧ ∀ x ≥ 1,      ∑' n, (f n) * (Set.indicator (Set.Ioc ((1 - ε) * x) x) (fun _ ↦ 1) (n : ℝ)) ≤ C * x) :    cheby f := by  obtain ⟨ε, C₀, hε, hε1, hC₀, h_bound⟩ := h_short  let C := C₀ / ε + f 0 + 1  have hf0 : (0 : ℝ) ≤ f 0 := hpos 0  have hdiv : 0 ≤ C₀ / ε := div_nonneg hC₀.le hε.le  have hC : 0 ≤ C := by linarith  refine ⟨C, fun n ↦ ?_⟩  induction n using Nat.strong_induction_on with | h n ih =>  rcases lt_or_ge n 2 with hn | hn  · interval_cases n    · simp [cumsum]    · simp only [cumsum, Finset.sum_range_one, Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg hf0,        Nat.cast_one, mul_one, C]      linarith  let x := (n : ℝ) - 1  have hx : x ≥ 1 := by simp only [x, ge_iff_le, le_sub_iff_add_le]; norm_cast  let m := ⌊(1 - ε) * x⌋₊ + 1  have hm_lt : m < n := by    simp only [m, x]    have h1 : (1 - ε) * (n - 1 : ℝ) < (n - 1 : ℕ) := by      calc (1 - ε) * (↑n - 1) < 1 * (↑n - 1) := by gcongr; linarith        _ = ↑n - 1 := by ring        _ = ↑(n - 1) := by simp [Nat.cast_sub (by omega : 1 ≤ n)]    have h2 : ⌊(1 - ε) * (n - 1 : ℝ)⌋₊ < n - 1 :=      (Nat.floor_lt (mul_nonneg (by linarith) (by linarith : (0 : ℝ) ≤ n - 1))).mpr h1    omega  have hm_gt : (m : ℝ) > (1 - ε) * x := by    simp only [m, Nat.cast_add, Nat.cast_one, gt_iff_lt]    exact Nat.lt_floor_add_one ((1 - ε) * x)  have h_decomp : cumsum (fun k ↦ ‖(f k : ℂ)‖) n = cumsum (fun k ↦ ‖(f k : ℂ)‖) m + ∑ k ∈ Finset.Ico m n, f k := by    simp only [cumsum, Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg (hpos _),      Finset.sum_range_add_sum_Ico _ (by omega : m ≤ n)]  have h_Ico : ∑ k ∈ Finset.Ico m n, f k ≤ C₀ * x := by    calc ∑ k ∈ Finset.Ico m n, f k        = ∑ k ∈ Finset.Ico m n, f k * Set.indicator (Set.Ioc ((1 - ε) * x) x) 1 (k : ℝ) := by          refine Finset.sum_congr rfl fun k hk ↦ ?_          have ⟨hkm, hkn⟩ := Finset.mem_Ico.mp hk          have hk_gt : (k : ℝ) > (1 - ε) * x := by linarith [hm_gt, (Nat.cast_le (α := ℝ)).mpr hkm]          have hk_le : (k : ℝ) ≤ x := by            have h1 : k ≤ n - 1 := Nat.le_pred_of_lt hkn            have h2 : (k : ℝ) ≤ (n - 1 : ℕ) := by exact_mod_cast h1            simp only [Nat.cast_sub (by omega : 1 ≤ n), Nat.cast_one, x] at h2 ⊢; exact h2          simp only [Set.indicator_of_mem (Set.mem_Ioc.mpr ⟨hk_gt, hk_le⟩), Pi.one_apply, mul_one]      _ ≤ ∑' k, f k * Set.indicator (Set.Ioc ((1 - ε) * x) x) 1 (k : ℝ) := by          refine Summable.sum_le_tsum _ (fun k _ ↦ mul_nonneg (hpos k) (Set.indicator_nonneg (by simp) _)) ?_          refine summable_of_hasFiniteSupport <| (Set.finite_le_nat ⌊x⌋₊).subset fun k hk ↦ ?_          simp only [Function.mem_support, ne_eq, mul_eq_zero, not_or, Set.indicator_apply_ne_zero] at hk          exact Nat.le_floor hk.2.1.2      _ ≤ C₀ * x := h_bound x hx  have hm_le : (m : ℝ) ≤ (1 - ε) * x + 1 := by    have hpos' : 0 ≤ (1 - ε) * x := mul_nonneg (by linarith) (by linarith : (0 : ℝ) ≤ x)    simp only [m, Nat.cast_add, Nat.cast_one]    linarith [Nat.floor_le hpos']  have hnorm : ∀ k, ‖(f k : ℂ)‖ = f k := fun k ↦ by simp [abs_of_nonneg (hpos k)]  simp only [hnorm] at h_decomp ih ⊢  calc cumsum f n = cumsum f m + ∑ k ∈ Finset.Ico m n, f k := h_decomp    _ ≤ C * m + C₀ * x := by linarith [ih m hm_lt, h_Ico]    _ ≤ C * ((1 - ε) * x + 1) + C₀ * x := by nlinarith [hC]    _ = (C * (1 - ε) + C₀) * x + C := by ring    _ ≤ C * x + C := by        have : C₀ ≤ C * ε := by          calc C₀ = (C₀ / ε) * ε := by field_simp [ne_of_gt hε]            _ ≤ (C₀ / ε + f 0 + 1) * ε := by gcongr; linarith [hpos 0]            _ = C * ε := by simp only [C]        nlinarith [hε, hε1, hx]    _ ≤ C * n := by simp only [x]; ring_nf; linarith [hC]