auto_cheby

@[blueprint "auto-cheby"  (title := "auto-cheby")  (statement := /-- One has $$ \sum_{n \leq x} f(n) = O(x)$$ for all $x \geq 1$. -/)  (proof := /--  By applying Corollary \ref{crude-upper-bound} for a specific compactly supported function $\psi$,  one can obtain a bound of the form $\sum_{(1-\varepsilon)x < n \leq x} f(n) = O(x)$ for all $x$  and some absolute constant $\varepsilon$ (which can be made explicit).   If $C$ is a sufficiently large constant, the claim $|\sum_{n \leq x} f(n)| \leq Cx$ can now be  proven by strong induction on $x$, as the claim for $(1-\varepsilon)x$ implies the claim for $x$  by the triangle inequality (and the claim is trivial for $x < 1$).  -/)  (proofUses := ["crude-upper-bound", "WienerIkehara"])  (latexEnv := "corollary")]lemma auto_cheby (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}) : cheby f := by  obtain ⟨ψ_fun, hψSmooth, hψCompact, hψpos, hψ0⟩ := auto_cheby_exists_smooth_nonneg_fourier_kernel  obtain ⟨B, hB⟩ := crude_upper_bound hpos hG hG' hf ⟨ψ_fun, hψSmooth.of_le ENat.LEInfty.out, hψCompact⟩ hψpos  exact auto_cheby_bootstrap_induction hpos <| auto_cheby_short_interval_bound hpos hf hG hG' B ψ_fun    hψSmooth hψCompact hψpos hψ0 fun x hx ↦ hB x (by linarith)