crude_upper_bound

@[blueprint "crude-upper-bound"  (title := "crude-upper-bound")  (statement := /--    If $\psi: \R \to \C$ is $C^2$ and compactly supported with $f$ and $\hat \psi$ non-negative, then there exists a constant $B$ such that  $$ |\sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} )| \leq B$$  for all $x > 0$.  -/)  (proof := /-- This readily follows from the previous lemma and the triangle inequality. -/)  (proofUses := ["limiting-fourier-variant"])  (latexEnv := "corollary")]lemma crude_upper_bound    (hpos : 0 ≤ f)    (hG : ContinuousOn G {s | 1 ≤ s.re})    (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re})    (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ'))    (ψ : CS 2 ℂ)    (hψpos : ∀ y, 0 ≤ (𝓕 (ψ : ℝ → ℂ) y).re ∧ (𝓕 (ψ : ℝ → ℂ) y).im = 0) :    ∃ B : ℝ, ∀ x : ℝ, 0 < x → ‖∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * log (n / x))‖ ≤ B := by   -- Integrability of ψ  have hψ_int : MeasureTheory.Integrable (ψ : ℝ → ℂ) := by    simpa using (ψ.h1.continuous.integrable_of_hasCompactSupport ψ.h2)  have hψ_norm_int : MeasureTheory.Integrable (fun t : ℝ => ‖(ψ : ℝ → ℂ) t‖) :=    hψ_int.norm  have hψ_meas : MeasureTheory.AEStronglyMeasurable (ψ : ℝ → ℂ) :=    hψ_int.aestronglyMeasurable   -- Uniform bound K for ‖G(1+it)‖ on support ψ  rcases exists_bound_norm_G_on_tsupport (G := G) hG ψ with ⟨K, hK_ts⟩  have hK_support :      ∀ t : ℝ, t ∈ Function.support (ψ : ℝ → ℂ) → ‖G (1 + t * Complex.I)‖ ≤ K := by    have hbnG (hKts : ∀ t : ℝ, t ∈ tsupport ψ → ‖G (1 + t * Complex.I)‖ ≤ K) :      ∀ t : ℝ, t ∈ Function.support ψ → ‖G (1 + t * Complex.I)‖ ≤ K := by      intro t ht      exact hKts t ((subset_tsupport ψ) ht)    exact hbnG hK_ts   -- Measurability of the line restriction t ↦ G(1 + t I) from continuity-on  have hGline_meas : Measurable (fun t : ℝ => G (1 + t * Complex.I)) := by    have hline_cont : Continuous (fun t : ℝ => (1 : ℂ) + t * Complex.I) := by      continuity    have hmem : ∀ t : ℝ, ((1 : ℂ) + t * Complex.I) ∈ {s : ℂ | 1 ≤ s.re} := by      intro t      simp    have hcont : Continuous (G ∘ fun t : ℝ => (1 : ℂ) + t * Complex.I) :=      hG.comp_continuous hline_cont hmem    simpa [Function.comp] using! hcont.measurable   -- L¹ bound for the scaled Fourier transform norm  have hF_norm_int :      MeasureTheory.Integrable (fun u : ℝ => ‖𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))‖) :=    integrable_norm_fourier_scaled_of_CS2 ψ  have hF_meas :      MeasureTheory.AEStronglyMeasurable        (fun u : ℝ => 𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))) := by    have hcont : Continuous fun u : ℝ => 𝓕 (ψ : ℝ → ℂ) u := by      simpa using! continuous_FourierIntegral (ψ : W21)    have hcont_scaled : Continuous fun u : ℝ => 𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi)) :=      hcont.comp (by continuity)    exact hcont_scaled.aestronglyMeasurable  have hF_int :      MeasureTheory.Integrable (fun u : ℝ => 𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))) :=    by      have hfin_norm :          MeasureTheory.HasFiniteIntegral            (fun u : ℝ => ‖𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))‖) :=        hF_norm_int.hasFiniteIntegral      have hfin :          MeasureTheory.HasFiniteIntegral            (fun u : ℝ => 𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))) := by        simpa [MeasureTheory.hasFiniteIntegral_iff_norm] using hfin_norm      exact ⟨hF_meas, hfin⟩  refine ⟨K * (∫ t : ℝ, ‖(ψ : ℝ → ℂ) t‖)            + ‖A‖ * (∫ u : ℝ, ‖𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))‖), ?_⟩  intro x hx  set I : ℂ := ∫ u in Set.Ici (-Real.log x), 𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi)) with hI   -- Lemma 12  have hlim :=    limiting_fourier_variant (f := f) (A := A) (G := G)      hpos hG hG' hf ψ hψpos hx  have hlim' :      (∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * Real.pi) * Real.log (n / x)))        - A * I      = ∫ (t : ℝ), (G (1 + t * Complex.I)) * (ψ t) * x ^ (t * Complex.I) := by    simpa [hI] using hlim   -- express the tsum as RHS + A*I  have htsum :      (∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * Real.pi) * Real.log (n / x)))      = (∫ (t : ℝ), (G (1 + t * Complex.I)) * (ψ t) * x ^ (t * Complex.I)) + A * I := by    have h' :        (∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * Real.pi) * Real.log (n / x)))          = (∫ (t : ℝ), (G (1 + t * Complex.I)) * (ψ t) * x ^ (t * Complex.I)) + A * I :=      eq_add_of_sub_eq hlim'    simpa [add_comm, mul_comm, mul_left_comm, mul_assoc] using h'   -- bound the RHS integral  have hRHS_bound :      ‖∫ (t : ℝ), (G (1 + t * Complex.I)) * (ψ t) * x ^ (t * Complex.I)‖        ≤ K * (∫ t : ℝ, ‖(ψ : ℝ → ℂ) t‖) :=    norm_error_integral_le (G := G) (ψ := (ψ : ℝ → ℂ)) (x := x) (K := K)      hGline_meas hψ_meas hx hK_support hψ_norm_int   -- bound the A * I term  have hA_bound :      ‖A * I‖ ≤ ‖A‖ * (∫ u : ℝ, ‖𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))‖) := by    have hF_on : MeasureTheory.IntegrableOn        (fun u : ℝ => 𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi)))        (Set.Ici (-Real.log x)) :=      hF_int.integrableOn    simpa [hI] using      norm_mul_integral_Ici_le_integral_norm (A := A)        (F := fun u : ℝ => 𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi)))        (a := -Real.log x) hF_on hF_norm_int   -- combine bounds  have htsum_std :      (∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * Real.pi) * Real.log ((n : ℝ) / x)))        = (∫ (t : ℝ), (G (1 + t * Complex.I)) * (ψ t) * x ^ (t * Complex.I)) + A * I := by    simpa [one_div, mul_comm, mul_left_comm, mul_assoc] using htsum   -- bound in the normalized form  have hbound :      ‖∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ)          (1 / (2 * Real.pi) * Real.log ((n : ℝ) / x))‖        ≤ K * (∫ t : ℝ, ‖(ψ : ℝ → ℂ) t‖)          + ‖A‖ * (∫ u : ℝ, ‖𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))‖) := by    have hnorm :        ‖∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ)            (1 / (2 * Real.pi) * Real.log ((n : ℝ) / x))‖ =          ‖(∫ (t : ℝ), (G (1 + t * Complex.I)) * (ψ t) * x ^ (t * Complex.I)) + A * I‖ :=      congrArg norm htsum_std    calc      ‖∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ)          (1 / (2 * Real.pi) * Real.log ((n : ℝ) / x))‖          = ‖(∫ (t : ℝ), (G (1 + t * Complex.I)) * (ψ t) * x ^ (t * Complex.I)) + A * I‖ := hnorm      _ ≤ ‖∫ (t : ℝ), (G (1 + t * Complex.I)) * (ψ t) * x ^ (t * Complex.I)‖ + ‖A * I‖ :=            norm_add_le _ _      _ ≤ K * (∫ t : ℝ, ‖(ψ : ℝ → ℂ) t‖)          + ‖A‖ * (∫ u : ℝ, ‖𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))‖) :=            add_le_add hRHS_bound hA_bound  exact hbound