auto_cheby_short_interval_bound

lemma auto_cheby_short_interval_bound (hpos : 0 ≤ f)    (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ'))    (hG : ContinuousOn G {s | 1 ≤ s.re})    (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re})    (B : ℝ) (ψ : ℝ → ℂ) (hψSmooth : ContDiff ℝ ∞ ψ) (hψCompact : HasCompactSupport ψ)    (hψpos : ∀ y, 0 ≤ (𝓕 ψ y).re ∧ (𝓕 ψ y).im = 0) (hψ0 : 0 < (𝓕 ψ 0).re)    (hB_bound : ∀ x ≥ 1, ‖∑' n, f n / n * 𝓕 ψ (1 / (2 * Real.pi) * Real.log (n / x))‖ ≤ B) :    ∃ (ε : ℝ) (C : ℝ), ε > 0 ∧ ε < 1 ∧ C > 0 ∧ ∀ x ≥ 1,      ∑' n, (f n) * (Set.indicator (Set.Ioc ((1 - ε) * x) x) (fun _ ↦ 1) (n : ℝ)) ≤ C * x := by  have hF : Continuous (𝓕 ψ) := VectorFourier.fourierIntegral_continuous Real.continuous_fourierChar    (by continuity) (hψSmooth.continuous.integrable_of_hasCompactSupport hψCompact)  have hg : Continuous fun y ↦ (𝓕 ψ y).re := Complex.continuous_re.comp hF  obtain ⟨δ, hδpos, hball⟩ := Metric.mem_nhds_iff.1 <|    hg.continuousAt.preimage_mem_nhds (IsOpen.mem_nhds isOpen_Ioi (half_lt_self hψ0))  let c := (𝓕 ψ 0).re / 2  have hcpos : 0 < c := by dsimp only [c]; linarith  have h_psi_ge_c : ∀ y, |y| < δ → c ≤ (𝓕 ψ y).re := fun y hy ↦ (hball (mem_ball_zero_iff.mpr hy)).le  let ε := 1 - Real.exp (-2 * π * δ)  have hε : 0 < ε ∧ ε < 1 := by    have h1 : Real.exp (-2 * π * δ) < 1 := Real.exp_lt_one_iff.mpr (by nlinarith [Real.pi_pos])    exact ⟨by simp only [ε]; linarith, by simp only [ε]; linarith [Real.exp_pos (-2 * π * δ)]⟩  have hB_nonneg : 0 ≤ B := (norm_nonneg _).trans (hB_bound 1 le_rfl)  refine ⟨ε, B / c + 1, hε.1, hε.2, by positivity, fun x hx ↦ ?_⟩  have h_summable : Summable fun n ↦ (f n : ℂ) / n * 𝓕 ψ (1 / (2 * π) * Real.log (n / x)) :=    auto_cheby_fourier_summable hpos hf hG hG' ψ hψSmooth hψCompact hψpos x hx  have hx_pos : 0 < x := by linarith  have h_sum_lower : c / x * ∑' n, f n * Set.indicator (Set.Ioc ((1 - ε) * x) x) 1 (n : ℝ)      ≤ ∑' n, f n / n * (𝓕 ψ (1 / (2 * π) * Real.log (n / x))).re := by    rw [← tsum_mul_left]    refine Summable.tsum_le_tsum (fun n ↦ ?_) ?_ ?_    · by_cases hn : (n : ℝ) ∈ Set.Ioc ((1 - ε) * x) x      · rw [Set.indicator_of_mem hn, Pi.one_apply, mul_one]        have hn_pos : 0 < (n : ℝ) := by nlinarith [hn.1, hε.2]        let y := (1 / (2 * π)) * Real.log (n / x)        have h_arg_small : |y| < δ := by          have h2pi : 0 < 2 * π := by linarith [Real.pi_pos]          simp only [y, abs_mul, abs_div, abs_one, abs_of_pos h2pi]          field_simp [ne_of_gt h2pi]; rw [mul_comm, abs_lt]          have h_log_lower : -2 * π * δ < Real.log (n / x) := by            rw [← Real.log_exp (-2 * π * δ), Real.log_lt_log_iff (Real.exp_pos _) (by positivity)]            have : Real.exp (-2 * π * δ) = 1 - ε := by simp only [ε]; ring            rw [this]; field_simp; exact hn.1          have h_log_upper : Real.log (n / x) ≤ 0 :=            Real.log_nonpos (by positivity) (div_le_one_of_le₀ hn.2 hx_pos.le)          constructor <;> nlinarith [Real.pi_pos]        have h1 : x⁻¹ ≤ (n : ℝ)⁻¹ := by rw [inv_le_inv₀ hx_pos hn_pos]; exact hn.2        have h2 : c ≤ (𝓕 ψ y).re := h_psi_ge_c y h_arg_small        have hfn : 0 ≤ f n := hpos n        have hre : 0 ≤ (𝓕 ψ y).re := (hψpos y).1        have hn_inv : 0 ≤ (n : ℝ)⁻¹ := inv_nonneg.mpr hn_pos.le        calc c / x * f n = c * x⁻¹ * f n := by rw [div_eq_mul_inv]          _ ≤ c * (n : ℝ)⁻¹ * f n := by gcongr          _ ≤ (𝓕 ψ y).re * (n : ℝ)⁻¹ * f n := by gcongr          _ = (n : ℝ)⁻¹ * (𝓕 ψ y).re * f n := by ring          _ = f n / n * (𝓕 ψ y).re := by ring      · rw [Set.indicator_of_notMem hn, mul_zero, mul_zero]        exact mul_nonneg (div_nonneg (hpos n) (Nat.cast_nonneg n)) (hψpos _).1    · refine summable_of_hasFiniteSupport <| (Set.finite_le_nat ⌊x⌋₊).subset fun n hn ↦ ?_      simp only [Function.mem_support, ne_eq, mul_eq_zero, not_or, Set.indicator_apply_ne_zero] at hn      exact Nat.le_floor hn.2.2.1.2    · rw [← Complex.summable_ofReal]; convert h_summable using 1; ext n      rw [Complex.ofReal_mul, Complex.ofReal_div]      norm_cast      rw [Complex.ofReal_mul]      congr 1      apply Complex.ext      · simp only [Complex.ofReal_re]      · simp only [Complex.ofReal_im]; exact (hψpos _).2.symm  have h_real_eq : ∑' n, f n / n * (𝓕 ψ (1 / (2 * π) * Real.log (n / x))).re =      (∑' n, (f n : ℂ) / n * 𝓕 ψ (1 / (2 * π) * Real.log (n / x))).re := by    rw [Complex.re_tsum h_summable]; congr with n    rw [Complex.mul_re]; norm_cast; simp only [zero_mul, sub_zero]  calc ∑' n, f n * Set.indicator (Set.Ioc ((1 - ε) * x) x) 1 (n : ℝ)      = x / c * (c / x * ∑' n, f n * Set.indicator (Set.Ioc ((1 - ε) * x) x) 1 (n : ℝ)) := by        field_simp [ne_of_gt hcpos, ne_of_gt hx_pos]    _ ≤ x / c * B := by        gcongr; rw [h_real_eq] at h_sum_lower        exact h_sum_lower.trans ((Complex.re_le_norm _).trans (hB_bound x hx))    _ = (B / c) * x := by field_simp [ne_of_gt hcpos]    _ ≤ (B / c + 1) * x := by nlinarith