theorem ContinuousAt.boundedAtFilter {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [SeminormedAddCommGroup Y] (f : X → Y) (x : X) (hf : ContinuousAt f x) : (nhds x).BoundedAtFilter f

theorem MellinOfPsi_better {σ₁ σ₂ : ℝ} (hσ₂ : 0 ≤ σ₂) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : ∃ C > 0, ∀ (s : ℂ), s ≠ 0 → σ₁ ≤ s.re → s.re ≤ σ₂ → ‖mellin (fun (x : ℝ) => ↑(ν x)) s‖ ≤ C * ‖s‖⁻¹

Variant of MellinOfPsi on aribtrary vertial strips. hσ₂ is unnecessary but harmless.

theorem MellinOfPsi_filter {σ₁ σ₂ : ℝ} (hσ₂ : 0 ≤ σ₂) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : (mellin fun (x : ℝ) => ↑(ν x)) =O[Filter.principal {s : ℂ | σ₁ ≤ s.re ∧ s.re ≤ σ₂ ∧ s ≠ 0}] fun (s : ℂ) => s⁻¹

theorem mellin_bump_differentiable {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : Differentiable ℂ (mellin fun (x : ℝ) => ↑(ν x))

theorem Complex.inv_isBigO_one {r : ℝ} (hr : 0 < r) : (fun (s : ℂ) => s⁻¹) =O[Filter.principal {z : ℂ | r ≤ ‖z‖}] fun (x : ℂ) => 1

theorem exists_radius_eventually_of_nhds {X : Type u_1} {x : X} [PseudoMetricSpace X] {P : X → Prop} (hP : ∀ᶠ (s : X) in nhds x, P s) : ∃ r > 0, ∀ᶠ (s : X) in Filter.principal {s : X | dist s x < r}, P s

theorem eventually_principal_of_nhds {X : Type u_1} [PseudoMetricSpace X] {x : X} {P : X → Prop} (hP : ∀ᶠ (s : X) in nhds x, P s) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᶠ (s : X) in Filter.principal {s : X | dist s x < r}, P s

theorem isBigO_nhds_eventually_principal {X : Type u_1} {E : Type u_2} {F : Type u_3} [PseudoMetricSpace X] [Norm E] [Norm F] {f : X → E} {g : X → F} {x : X} (h : f =O[nhds x] g) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), f =O[Filter.principal {s : X | dist s x < r}] g

theorem mellin_bump_bounded_aux {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : (fun (s : ℂ) => mellin (fun (x : ℝ) => ↑(ν x)) s) =O[nhds 0] fun (x : ℂ) => 1

theorem mellin_bump_bounded {σ₁ σ₂ : ℝ} (hσ₂ : 0 ≤ σ₂) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : (mellin fun (x : ℝ) => ↑(ν x)) =O[Filter.principal {s : ℂ | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun (x : ℂ) => 1

theorem mellin_smooth1_bound {ε σ₂ : ℝ} (hε : 0 < ε) (hσ₂ : 0 ≤ σ₂) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : (mellin fun (x : ℝ) => ↑(Smooth1 ν ε x)) =O[Filter.principal {s : ℂ | 0 < s.re ∧ s.re ≤ σ₂}] fun (s : ℂ) => s⁻¹

theorem mellin_smooth1_bound' {σ₂ : ℝ} (hσ₂ : 0 ≤ σ₂) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : ∃ (C : NNReal), ∀ (ε : ℝ), 0 < ε → ε ≤ 1 → ∀ (s : ℂ), 0 < s.re → s.re ≤ σ₂ → ‖mellin (fun (x : ℝ) => ↑(Smooth1 ν ε x)) s‖ ≤ ↑C * ‖s⁻¹‖

theorem mellin_partial_int {σ₁ σ₂ : ℝ} {ν : ℝ → ℝ} {k : ℕ} (diffν : ContDiff ℝ (↑k) ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (s : ℂ) : mellin (fun (x : ℝ) => ↑(ν x)) s = s⁻¹ * mellin (fun (x : ℝ) => ↑(deriv ν x)) (s + 1)

theorem mellin_isBigO_pow {σ₁ σ₂ : ℝ} {ν : ℝ → ℝ} {k : ℕ} (diffν : ContDiff ℝ (↑k) ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : (mellin fun (x : ℝ) => ↑(ν x)) =O[Filter.principal (Complex.re ⁻¹' Set.Icc σ₁ σ₂)] fun (s : ℂ) => (1 + ‖s‖) ^ k

theorem Smooth1_verticalIntegrable {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) {ε : ℝ} (εpos : 0 < ε) (ε_lt_one : ε < 1) {σ : ℝ} (σ_pos : 0 < σ) (σ_le : σ ≤ 2) : Complex.VerticalIntegrable (mellin fun (x : ℝ) => ↑(Smooth1 ν ε x)) σ MeasureTheory.volume

Written by Claude:

In case the comments don't give it away, this lemma is written by claude. It's adapting a result that was implicit in MediumPNT.

The Mellin transform of the smoothed indicator Smooth1 ν ε is vertically integrable along the line Re s = σ, for any 0 < σ ≤ 2. The integrand is O(1/(σ² + t²)) by MellinOfSmooth1b, and t ↦ (σ² + t²)⁻¹ is integrable since σ ≠ 0. (This is the content of SmoothedChebyshevDirichlet_aux_integrable in MediumPNT, generalised from 1 < σ to 0 < σ.)

theorem Smooth1_mellinInv_mellin_eq {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) {ε : ℝ} (εpos : 0 < ε) (ε_lt_one : ε < 1) {σ : ℝ} (σ_pos : 0 < σ) (σ_le : σ ≤ 2) {x : ℝ} (hx : 0 < x) : mellinInv σ (mellin fun (x : ℝ) => ↑(Smooth1 ν ε x)) x = ↑(Smooth1 ν ε x)

In case the comments don't give it away, this lemma is written by claude. It's adapting a result that was implicit in MediumPNT

The smoothed indicator Smooth1 ν ε equals the inverse Mellin transform of its own Mellin transform — equation (*) of notes/theorem26_6_smooth.md. This is the specialization of mellinInv_mellin_eq to f = fun x ↦ (Smooth1 ν ε x : ℂ), proved implicitly inside SmoothedChebyshevDirichlet in PrimeNumberTheoremAnd.MediumPNT. The vertical integrability of the Mellin transform is established inline (as in SmoothedChebyshevDirichlet_aux_integrable) from the O(1/‖s‖²) decay of MellinOfSmooth1b, valid for any 0 < σ ≤ 2.