noncomputable def nterm (f : ℕ → ℂ) (σ' : ℝ) (n : ℕ) : ℝ

Equations

• nterm f σ' n = if n = 0 then 0 else ‖f n‖ / ↑n ^ σ'

theorem nterm_eq_norm_term {n : ℕ} {σ' : ℝ} {f : ℕ → ℂ} : nterm f σ' n = ‖LSeries.term f (↑σ') n‖

theorem norm_term_eq_nterm_re {n : ℕ} {f : ℕ → ℂ} (s : ℂ) : ‖LSeries.term f s n‖ = nterm f s.re n

theorem hf_coe1 {σ' : ℝ} {f : ℕ → ℂ} (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hσ : 1 < σ') : ∑' (i : ℕ), ↑‖LSeries.term f (↑σ') i‖₊ ≠ ⊤

@[instance_reducible]

instance instMeasurableSpace : MeasurableSpace Circle

Equations

• instMeasurableSpace = { MeasurableSet' := instMeasurableSpace._aux_1, measurableSet_empty := instMeasurableSpace._proof_3, measurableSet_compl := instMeasurableSpace._proof_4, measurableSet_iUnion := instMeasurableSpace._proof_5 }

instance instBorelSpace : BorelSpace Circle

theorem first_fourier_aux1 {ψ : ℝ → ℂ} (hψ : AEMeasurable ψ MeasureTheory.volume) {x : ℝ} (n : ℕ) : AEMeasurable (fun (u : ℝ) => ‖Real.fourierChar (-(u * (1 / (2 * Real.pi) * Real.log (↑n / x)))) • ψ u‖ₑ) MeasureTheory.volume

theorem first_fourier_aux2a {n : ℕ} {x y : ℝ} : 2 * ↑Real.pi * -(↑y * (1 / (2 * ↑Real.pi) * ↑(Real.log (↑n / x)))) = -(↑y * ↑(Real.log (↑n / x)))

theorem first_fourier_aux2 {x y σ' : ℝ} {ψ : ℝ → ℂ} {f : ℕ → ℂ} (hx : 0 < x) (n : ℕ) : LSeries.term f (↑σ') n * Real.fourierChar (-(y * (1 / (2 * Real.pi) * Real.log (↑n / x)))) • ψ y = LSeries.term f (↑σ' + ↑y * Complex.I) n • (ψ y * ↑x ^ (↑y * Complex.I))

theorem first_fourier {x σ' : ℝ} {ψ : ℝ → ℂ} {f : ℕ → ℂ} (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hsupp : MeasureTheory.Integrable ψ MeasureTheory.volume) (hx : 0 < x) (hσ : 1 < σ') : ∑' (n : ℕ), LSeries.term f (↑σ') n * FourierTransform.fourier ψ (1 / (2 * Real.pi) * Real.log (↑n / x)) = ∫ (t : ℝ), LSeries f (↑σ' + ↑t * Complex.I) * ψ t * ↑x ^ (↑t * Complex.I)

theorem continuous_multiplicative_ofAdd : Continuous ⇑Multiplicative.ofAdd

theorem second_fourier_integrable_aux1a {x σ' : ℝ} (hσ : 1 < σ') : MeasureTheory.IntegrableOn (fun (x : ℝ) => Complex.exp (-(↑x * (↑σ' - 1)))) (Set.Ici (-Real.log x)) MeasureTheory.volume

theorem second_fourier_integrable_aux1 {x σ' : ℝ} {ψ : ℝ → ℂ} (hcont : Measurable ψ) (hsupp : MeasureTheory.Integrable ψ MeasureTheory.volume) (hσ : 1 < σ') : have ν := (MeasureTheory.volume.restrict (Set.Ici (-Real.log x))).prod MeasureTheory.volume; MeasureTheory.Integrable (Function.uncurry fun (u a : ℝ) => ↑(Real.exp (-u * (σ' - 1))) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * (u / (2 * Real.pi)))))) • ψ a) ν

theorem second_fourier_integrable_aux2 {x t σ' : ℝ} (hσ : 1 < σ') : MeasureTheory.IntegrableOn (fun (u : ℝ) => Complex.exp ((1 - ↑σ' - ↑t * Complex.I) * ↑u)) (Set.Ioi (-Real.log x)) MeasureTheory.volume

theorem second_fourier_aux {x t σ' : ℝ} (hx : 0 < x) : -(Complex.exp (-((1 - ↑σ' - ↑t * Complex.I) * ↑(Real.log x))) / (1 - ↑σ' - ↑t * Complex.I)) = ↑(x ^ (σ' - 1)) * (↑σ' + ↑t * Complex.I - 1)⁻¹ * ↑x ^ (↑t * Complex.I)

theorem second_fourier {ψ : ℝ → ℂ} (hcont : Measurable ψ) (hsupp : MeasureTheory.Integrable ψ MeasureTheory.volume) {x σ' : ℝ} (hx : 0 < x) (hσ : 1 < σ') : ∫ (u : ℝ) in Set.Ici (-Real.log x), ↑(Real.exp (-u * (σ' - 1))) * FourierTransform.fourier ψ (u / (2 * Real.pi)) = ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * Complex.I - 1) * ψ t * ↑x ^ (↑t * Complex.I)

theorem one_add_sq_pos (u : ℝ) : 0 < 1 + u ^ 2

theorem prelim_decay (ψ : ℝ → ℂ) (u : ℝ) : ‖FourierTransform.fourier ψ u‖ ≤ ∫ (t : ℝ), ‖ψ t‖

The upstream file also contains three unused alternate Fourier-decay declarations (prelim_decay_2, prelim_decay_3, and decay_alt). Two of those declarations are unfinished upstream and none lies in the dependency closure of WeakPNT. They are intentionally omitted from this minimal, zero-sorry port; see UPSTREAM.md.

theorem decay_bounds_key (f : W21) (u : ℝ) : ‖FourierTransform.fourier f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹

theorem decay_bounds_aux {A : ℝ} {f : ℝ → ℂ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (h : ∀ (t : ℝ), ‖f t‖ ≤ A * (1 + t ^ 2)⁻¹) : ∫ (t : ℝ), ‖f t‖ ≤ Real.pi * A

theorem decay_bounds_W21 {A : ℝ} (f : W21) (hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)) (hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)) (u : ℝ) : ‖FourierTransform.fourier f.toFun u‖ ≤ (Real.pi + 1 / (4 * Real.pi)) * A / (1 + u ^ 2)

theorem decay_bounds {A u : ℝ} (ψ : CS 2 ℂ) (hA : ∀ (t : ℝ), ‖ψ.toFun t‖ ≤ A / (1 + t ^ 2)) (hA' : ∀ (t : ℝ), ‖deriv^[2] ψ.toFun t‖ ≤ A / (1 + t ^ 2)) : ‖FourierTransform.fourier ψ.toFun u‖ ≤ (Real.pi + 1 / (4 * Real.pi)) * A / (1 + u ^ 2)

theorem decay_bounds_cor_aux (ψ : CS 2 ℂ) : ∃ (C : ℝ), ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)

theorem decay_bounds_cor (ψ : W21) : ∃ (C : ℝ), ∀ (u : ℝ), ‖FourierTransform.fourier ψ.toFun u‖ ≤ C / (1 + u ^ 2)

theorem continuous_FourierIntegral (ψ : W21) : Continuous (FourierTransform.fourier ψ.toFun)

theorem W21.integrable_fourier {c : ℝ} (ψ : W21) (hc : c ≠ 0) : MeasureTheory.Integrable (fun (u : ℝ) => FourierTransform.fourier ψ.toFun (u / c)) MeasureTheory.volume

theorem continuous_LSeries_aux {σ' : ℝ} {f : ℕ → ℂ} (hf : Summable (nterm f σ')) : Continuous fun (x : ℝ) => LSeries f (↑σ' + ↑x * Complex.I)

theorem limiting_fourier_aux {A x : ℝ} {G : ℂ → ℂ} {f : ℕ → ℂ} (hG' : Set.EqOn G (fun (s : ℂ) => LSeries f s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (ψ : CS 2 ℂ) (hx : 1 ≤ x) (σ' : ℝ) (hσ' : 1 < σ') : ∑' (n : ℕ), LSeries.term f (↑σ') n * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x)) - ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Set.Ici (-Real.log x), ↑(Real.exp (-u * (σ' - 1))) * FourierTransform.fourier ψ.toFun (u / (2 * Real.pi)) = ∫ (t : ℝ), G (↑σ' + ↑t * Complex.I) * ψ.toFun t * ↑x ^ (↑t * Complex.I)

def cumsum {E : Type u_2} [AddCommMonoid E] (u : ℕ → E) (n : ℕ) : E

Equations

• cumsum u n = ∑ i ∈ Finset.range n, u i

def nabla {α : Type u_1} {E : Type u_2} [OfNat α 1] [Add α] [Sub E] (u : α → E) (n : α) : E

Equations

• nabla u n = u (n + 1) - u n

def nnabla {α : Type u_1} {E : Type u_2} [OfNat α 1] [Add α] [Sub E] (u : α → E) (n : α) : E

Equations

• nnabla u n = u n - u (n + 1)

def shift {α : Type u_1} {E : Type u_2} [OfNat α 1] [Add α] (u : α → E) (n : α) : E

Equations

• shift u n = u (n + 1)

@[simp]

theorem cumsum_zero {E : Type u_2} [AddCommMonoid E] {u : ℕ → E} : cumsum u 0 = 0

theorem cumsum_succ {E : Type u_2} [AddCommMonoid E] {u : ℕ → E} (n : ℕ) : cumsum u (n + 1) = cumsum u n + u n

@[simp]

theorem nabla_cumsum {E : Type u_2} [AddCommGroup E] {u : ℕ → E} : nabla (cumsum u) = u

theorem neg_cumsum {E : Type u_2} [AddCommGroup E] {u : ℕ → E} : -cumsum u = cumsum (-u)

theorem cumsum_nonneg {u : ℕ → ℝ} (hu : 0 ≤ u) : 0 ≤ cumsum u

theorem neg_nabla {α : Type u_1} {E : Type u_2} [OfNat α 1] [Add α] [Ring E] {u : α → E} : -nabla u = nnabla u

@[simp]

theorem nabla_mul {α : Type u_1} {E : Type u_2} [OfNat α 1] [Add α] [Ring E] {u : α → E} {c : E} : (nabla fun (n : α) => c * u n) = c • nabla u

@[simp]

theorem nnabla_mul {α : Type u_1} {E : Type u_2} [OfNat α 1] [Add α] [Ring E] {u : α → E} {c : E} : (nnabla fun (n : α) => c * u n) = c • nnabla u

theorem nnabla_cast {E : Type u_2} (u : ℝ → E) [Sub E] : nnabla u ∘ Nat.cast = nnabla (u ∘ Nat.cast)

theorem Finset.sum_shift_front {E : Type u_1} [Ring E] {u : ℕ → E} {n : ℕ} : cumsum u (n + 1) = u 0 + cumsum (shift u) n

theorem Finset.sum_shift_front' {E : Type u_1} [Ring E] {u : ℕ → E} : shift (cumsum u) = (fun (x : ℕ) => u 0) + cumsum (shift u)

theorem Finset.sum_shift_back {E : Type u_1} [Ring E] {u : ℕ → E} {n : ℕ} : cumsum u (n + 1) = cumsum u n + u n

theorem Finset.sum_shift_back' {E : Type u_1} [Ring E] {u : ℕ → E} : shift (cumsum u) = cumsum u + u

theorem summation_by_parts {E : Type u_1} [Ring E] {a A b : ℕ → E} (ha : a = nabla A) {n : ℕ} : cumsum (a * b) (n + 1) = A (n + 1) * b n - A 0 * b 0 - cumsum (shift A * fun (i : ℕ) => b (i + 1) - b i) n

theorem summation_by_parts' {E : Type u_1} [Ring E] {a b : ℕ → E} {n : ℕ} : cumsum (a * b) (n + 1) = cumsum a (n + 1) * b n - cumsum (shift (cumsum a) * nabla b) n

theorem summation_by_parts'' {E : Type u_1} [Ring E] {a b : ℕ → E} : shift (cumsum (a * b)) = shift (cumsum a) * b - cumsum (shift (cumsum a) * nabla b)

theorem summable_iff_bounded {u : ℕ → ℝ} (hu : 0 ≤ u) : Summable u ↔ Filter.atTop.BoundedAtFilter (cumsum u)

theorem Filter.EventuallyEq.summable {u v : ℕ → ℝ} (h : u =ᶠ[atTop] v) (hu : Summable v) : Summable u

theorem summable_congr_ae {u v : ℕ → ℝ} (huv : u =ᶠ[Filter.atTop] v) : Summable u ↔ Summable v

theorem BoundedAtFilter.add_const {u : ℕ → ℝ} {c : ℝ} : (Filter.atTop.BoundedAtFilter fun (n : ℕ) => u n + c) ↔ Filter.atTop.BoundedAtFilter u

theorem BoundedAtFilter.comp_add {u : ℕ → ℝ} {N : ℕ} : (Filter.atTop.BoundedAtFilter fun (n : ℕ) => u (n + N)) ↔ Filter.atTop.BoundedAtFilter u

theorem summable_iff_bounded' {u : ℕ → ℝ} (hu : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ u n) : Summable u ↔ Filter.atTop.BoundedAtFilter (cumsum u)

theorem bounded_of_shift {u : ℕ → ℝ} (h : Filter.atTop.BoundedAtFilter (shift u)) : Filter.atTop.BoundedAtFilter u

theorem dirichlet_test' {a b : ℕ → ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hAb : Filter.atTop.BoundedAtFilter (shift (cumsum a) * b)) (hbb : ∀ᶠ (n : ℕ) in Filter.atTop, b (n + 1) ≤ b n) (h : Summable (shift (cumsum a) * nnabla b)) : Summable (a * b)

theorem exists_antitone_of_eventually {u : ℕ → ℝ} (hu : ∀ᶠ (n : ℕ) in Filter.atTop, u (n + 1) ≤ u n) : ∃ (v : ℕ → ℝ), Set.range v ⊆ Set.range u ∧ Antitone v ∧ v =ᶠ[Filter.atTop] u

theorem summable_inv_mul_log_sq : Summable fun (n : ℕ) => (↑n * Real.log ↑n ^ 2)⁻¹

theorem tendsto_mul_add_atTop {a : ℝ} (ha : 0 < a) (b : ℝ) : Filter.Tendsto (fun (x : ℝ) => a * x + b) Filter.atTop Filter.atTop

theorem isLittleO_const_of_tendsto_atTop {α : Type u_1} [Preorder α] (a : ℝ) {f : α → ℝ} (hf : Filter.Tendsto f Filter.atTop Filter.atTop) : (fun (x : α) => a) =o[Filter.atTop] f

theorem isBigO_pow_pow_of_le {m n : ℕ} (h : m ≤ n) : (fun (x : ℝ) => x ^ m) =O[Filter.atTop] fun (x : ℝ) => x ^ n

theorem isLittleO_mul_add_sq (a b : ℝ) : (fun (x : ℝ) => a * x + b) =o[Filter.atTop] fun (x : ℝ) => x ^ 2

theorem log_mul_add_isBigO_log {a : ℝ} (ha : 0 < a) (b : ℝ) : (fun (x : ℝ) => Real.log (a * x + b)) =O[Filter.atTop] Real.log

theorem isBigO_log_mul_add {a : ℝ} (ha : 0 < a) (b : ℝ) : Real.log =O[Filter.atTop] fun (x : ℝ) => Real.log (a * x + b)

theorem log_isbigo_log_div {d : ℝ} (hb : 0 < d) : (fun (n : ℝ) => Real.log n) =O[Filter.atTop] fun (n : ℝ) => Real.log (n / d)

theorem Asymptotics.IsBigO.add_isLittleO_right {f g : ℝ → ℝ} (h : g =o[Filter.atTop] f) : f =O[Filter.atTop] (f + g)

theorem Asymptotics.IsBigO.sq {α : Type u_1} [Preorder α] {f g : α → ℝ} (h : f =O[Filter.atTop] g) : (fun (n : α) => f n ^ 2) =O[Filter.atTop] fun (n : α) => g n ^ 2

theorem log_sq_isbigo_mul {a b : ℝ} (hb : 0 < b) : (fun (x : ℝ) => Real.log x ^ 2) =O[Filter.atTop] fun (x : ℝ) => a + Real.log (x / b) ^ 2

theorem log_add_div_isBigO_log (a : ℝ) {b : ℝ} (hb : 0 < b) : (fun (x : ℝ) => Real.log ((x + a) / b)) =O[Filter.atTop] fun (x : ℝ) => Real.log x

theorem log_add_one_sub_log_le {x : ℝ} (hx : 0 < x) : nabla Real.log x ≤ x⁻¹

theorem nabla_log_main : nabla Real.log =O[Filter.atTop] fun (x : ℝ) => 1 / x

theorem nabla_log {b : ℝ} (hb : 0 < b) : (nabla fun (x : ℝ) => Real.log (x / b)) =O[Filter.atTop] fun (x : ℝ) => 1 / x

theorem nnabla_mul_log_sq (a : ℝ) {b : ℝ} (hb : 0 < b) : (nabla fun (x : ℝ) => x * (a + Real.log (x / b) ^ 2)) =O[Filter.atTop] fun (x : ℝ) => Real.log x ^ 2

theorem nnabla_bound_aux1 (a : ℝ) {b : ℝ} (hb : 0 < b) : Filter.Tendsto (fun (x : ℝ) => x * (a + Real.log (x / b) ^ 2)) Filter.atTop Filter.atTop

theorem nnabla_bound_aux2 (a : ℝ) {b : ℝ} (hb : 0 < b) : ∀ᶠ (x : ℝ) in Filter.atTop, 0 < x * (a + Real.log (x / b) ^ 2)

theorem Real.log_eventually_gt_atTop (a : ℝ) : ∀ᶠ (x : ℝ) in Filter.atTop, a < log x

theorem norm_lt_norm_of_nonneg (x y : ℝ) (hx : 0 ≤ x) (hxy : x ≤ y) : ‖x‖ ≤ ‖y‖

Should this be a gcongr lemma?

theorem nnabla_bound_aux {x : ℝ} (hx : 0 < x) : (nnabla fun (n : ℝ) => 1 / (n * ((2 * Real.pi) ^ 2 + Real.log (n / x) ^ 2))) =O[Filter.atTop] fun (n : ℝ) => 1 / (Real.log n ^ 2 * n ^ 2)

theorem nnabla_bound (C : ℝ) {x : ℝ} (hx : 0 < x) : (nnabla fun (n : ℝ) => C / (1 + (Real.log (n / x) / (2 * Real.pi)) ^ 2) / n) =O[Filter.atTop] fun (n : ℝ) => (n ^ 2 * Real.log n ^ 2)⁻¹

def chebyWith (C : ℝ) (f : ℕ → ℂ) : Prop

Equations

• chebyWith C f = ∀ (n : ℕ), cumsum (fun (x : ℕ) => ‖f x‖) n ≤ C * ↑n

def cheby (f : ℕ → ℂ) : Prop

Equations

• cheby f = ∃ (C : ℝ), chebyWith C f

theorem cheby.bigO {f : ℕ → ℂ} (h : cheby f) : (cumsum fun (x : ℕ) => ‖f x‖) =O[Filter.atTop] Nat.cast

theorem limiting_fourier_lim1_aux {x : ℝ} {f : ℕ → ℂ} (hcheby : cheby f) (hx : 0 < x) (C : ℝ) (hC : 0 ≤ C) : Summable fun (n : ℕ) => ‖f n‖ / ↑n * (C / (1 + (1 / (2 * Real.pi) * Real.log (↑n / x)) ^ 2))

theorem limiting_fourier_lim1 {x : ℝ} {f : ℕ → ℂ} (hcheby : cheby f) (ψ : W21) (hx : 0 < x) : Filter.Tendsto (fun (σ' : ℝ) => ∑' (n : ℕ), LSeries.term f (↑σ') n * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x))) (nhdsWithin 1 (Set.Ioi 1)) (nhds (∑' (n : ℕ), f n / ↑n * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x))))

theorem limiting_fourier_lim2_aux (x C : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => max |x| 1 * (C / (1 + (t / (2 * Real.pi)) ^ 2))) (MeasureTheory.volume.restrict (Set.Ici (-Real.log x)))

theorem limiting_fourier_lim2 {x : ℝ} (A : ℝ) (ψ : W21) (hx : 1 ≤ x) : Filter.Tendsto (fun (σ' : ℝ) => ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Set.Ici (-Real.log x), ↑(Real.exp (-u * (σ' - 1))) * FourierTransform.fourier ψ.toFun (u / (2 * Real.pi))) (nhdsWithin 1 (Set.Ioi 1)) (nhds (↑A * ∫ (u : ℝ) in Set.Ici (-Real.log x), FourierTransform.fourier ψ.toFun (u / (2 * Real.pi))))

theorem limiting_fourier_lim3 {x : ℝ} {G : ℂ → ℂ} (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (ψ : CS 2 ℂ) (hx : 1 ≤ x) : Filter.Tendsto (fun (σ' : ℝ) => ∫ (t : ℝ), G (↑σ' + ↑t * Complex.I) * ψ.toFun t * ↑x ^ (↑t * Complex.I)) (nhdsWithin 1 (Set.Ioi 1)) (nhds (∫ (t : ℝ), G (1 + ↑t * Complex.I) * ψ.toFun t * ↑x ^ (↑t * Complex.I)))

theorem limiting_fourier {A x : ℝ} {G : ℂ → ℂ} {f : ℕ → ℂ} (hcheby : cheby 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 ℂ) (hx : 1 ≤ x) : ∑' (n : ℕ), f n / ↑n * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x)) - ↑A * ∫ (u : ℝ) in Set.Ici (-Real.log x), FourierTransform.fourier ψ.toFun (u / (2 * Real.pi)) = ∫ (t : ℝ), G (1 + ↑t * Complex.I) * ψ.toFun t * ↑x ^ (↑t * Complex.I)

theorem limiting_cor_aux {f : ℝ → ℂ} : Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ), f t * ↑x ^ (↑t * Complex.I)) Filter.atTop (nhds 0)

theorem limiting_cor {A : ℝ} {G : ℂ → ℂ} {f : ℕ → ℂ} (ψ : CS 2 ℂ) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hcheby : cheby f) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries f s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) : Filter.Tendsto (fun (x : ℝ) => ∑' (n : ℕ), f n / ↑n * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x)) - ↑A * ∫ (u : ℝ) in Set.Ici (-Real.log x), FourierTransform.fourier ψ.toFun (u / (2 * Real.pi))) Filter.atTop (nhds 0)

theorem smooth_urysohn (a b c d : ℝ) (h1 : a < b) (h3 : c < d) : ∃ (Ψ : ℝ → ℝ), ContDiff ℝ (↑⊤) Ψ ∧ HasCompactSupport Ψ ∧ (Set.Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Set.Ioo a d).indicator 1

noncomputable def exists_trunc : trunc

Equations

• exists_trunc = (fun (ψ : ℝ → ℝ) (x : ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ (Set.Icc (-1) 1).indicator 1 ≤ ψ ∧ ψ ≤ (Set.Ioo (-2) 2).indicator 1) => { toFun := ψ, h1 := ⋯, h2 := ⋯, h3 := ⋯, h4 := ⋯ }) (Classical.choose exists_trunc._proof_6) exists_trunc._proof_7

theorem one_div_sub_one (n : ℕ) : 1 / ↑(n - 1) ≤ 2 / ↑n

theorem quadratic_pos (a b c x : ℝ) (ha : 0 < a) (hΔ : discrim a b c < 0) : 0 < a * x ^ 2 + b * x + c

noncomputable def pp (a x : ℝ) : ℝ

Equations

• pp a x = a ^ 2 * (x + 1) ^ 2 + (1 - a) * (1 + a)

noncomputable def pp' (a x : ℝ) : ℝ

Equations

• pp' a x = a ^ 2 * (2 * (x + 1))

theorem pp_pos {a : ℝ} (ha : a ∈ Set.Ioo (-1) 1) (x : ℝ) : 0 < pp a x

theorem pp_deriv (a x : ℝ) : HasDerivAt (pp a) (pp' a x) x

theorem pp_deriv_eq (a : ℝ) : deriv (pp a) = pp' a

theorem pp'_deriv (a x : ℝ) : HasDerivAt (pp' a) (a ^ 2 * 2) x

theorem pp'_deriv_eq (a : ℝ) : deriv (pp' a) = fun (x : ℝ) => a ^ 2 * 2

noncomputable def hh (a t : ℝ) : ℝ

Equations

• hh a t = (t * (1 + (a * Real.log t) ^ 2))⁻¹

noncomputable def hh' (a t : ℝ) : ℝ

Equations

• hh' a t = -pp a (Real.log t) * hh a t ^ 2

theorem hh_nonneg (a : ℝ) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ hh a t

theorem hh_le (a t : ℝ) (ht : 0 ≤ t) : |hh a t| ≤ t⁻¹

theorem hh_deriv (a : ℝ) {t : ℝ} (ht : t ≠ 0) : HasDerivAt (hh a) (hh' a t) t

theorem hh_continuous (a : ℝ) : ContinuousOn (hh a) (Set.Ioi 0)

theorem hh'_nonpos {a x : ℝ} (ha : a ∈ Set.Ioo (-1) 1) : hh' a x ≤ 0

theorem hh_antitone {a : ℝ} (ha : a ∈ Set.Ioo (-1) 1) : AntitoneOn (hh a) (Set.Ioi 0)

noncomputable def gg (x i : ℝ) : ℝ

Equations

• gg x i = 1 / i * (1 + (1 / (2 * Real.pi) * Real.log (i / x)) ^ 2)⁻¹

theorem gg_of_hh {x : ℝ} (hx : x ≠ 0) (i : ℝ) : gg x i = x⁻¹ * hh (1 / (2 * Real.pi)) (i / x)

theorem gg_l1 {x : ℝ} (hx : 0 < x) (n : ℕ) : |gg x ↑n| ≤ 1 / ↑n

theorem gg_le_one {x : ℝ} (i : ℕ) : gg x ↑i ≤ 1

theorem one_div_two_pi_mem_Ioo : 1 / (2 * Real.pi) ∈ Set.Ioo (-1) 1

theorem sum_telescopic (a : ℕ → ℝ) (n : ℕ) : ∑ i ∈ Finset.range n, (a (i + 1) - a i) = a n - a 0

theorem cancel_aux {C : ℝ} {f g : ℕ → ℝ} (hf : 0 ≤ f) (hg : 0 ≤ g) (hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n) (hg' : Antitone g) (n : ℕ) : ∑ i ∈ Finset.range n, f i * g i ≤ g (n - 1) * (C * ↑n) + (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) - ((n - 1 - 1) • (C * g 0) - ∑ x ∈ Finset.range (n - 1 - 1), C * g (x + 1)))

theorem sum_range_succ (a : ℕ → ℝ) (n : ℕ) : ∑ i ∈ Finset.range n, a (i + 1) = ∑ i ∈ Finset.range (n + 1), a i - a 0

theorem cancel_aux' {C : ℝ} {f g : ℕ → ℝ} (hf : 0 ≤ f) (hg : 0 ≤ g) (hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n) (hg' : Antitone g) (n : ℕ) : ∑ i ∈ Finset.range n, f i * g i ≤ C * ↑n * g (n - 1) + C * cumsum g (n - 1 - 1 + 1) - C * (↑(n - 1 - 1) + 1) * g (n - 1)

theorem cancel_main {C : ℝ} {f g : ℕ → ℝ} (hf : 0 ≤ f) (hg : 0 ≤ g) (hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n) (hg' : Antitone g) (n : ℕ) (hn : 2 ≤ n) : cumsum (f * g) n ≤ C * cumsum g n

theorem cancel_main' {C : ℝ} {f g : ℕ → ℝ} (hf : 0 ≤ f) (hf0 : f 0 = 0) (hg : 0 ≤ g) (hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n) (hg' : Antitone g) (n : ℕ) : cumsum (f * g) n ≤ C * cumsum g n

theorem sum_le_integral {x₀ : ℝ} {f : ℝ → ℝ} {n : ℕ} (hf : AntitoneOn f (Set.Ioc x₀ (x₀ + ↑n))) (hfi : MeasureTheory.IntegrableOn f (Set.Icc x₀ (x₀ + ↑n)) MeasureTheory.volume) : ∑ i ∈ Finset.range n, f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑n, f x

theorem hh_integrable_aux {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : MeasureTheory.IntegrableOn (fun (t : ℝ) => a * hh b (t / c)) (Set.Ici 0) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Ioi 0, a * hh b (t / c) = a * c / b * Real.pi

theorem hh_integrable {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : MeasureTheory.IntegrableOn (fun (t : ℝ) => a * hh b (t / c)) (Set.Ici 0) MeasureTheory.volume

theorem hh_integral {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : ∫ (t : ℝ) in Set.Ioi 0, a * hh b (t / c) = a * c / b * Real.pi

theorem hh_integral' : ∫ (t : ℝ) in Set.Ioi 0, hh (1 / (2 * Real.pi)) t = 2 * Real.pi ^ 2

theorem bound_sum_log {f : ℕ → ℂ} {C : ℝ} (hf0 : f 0 = 0) (hf : chebyWith C f) {x : ℝ} (hx : 1 ≤ x) : ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * Real.pi) * Real.log (↑i / x)) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Set.Ioi 0, hh (1 / (2 * Real.pi)) t)

theorem bound_sum_log0 {f : ℕ → ℂ} {C : ℝ} (hf : chebyWith C f) {x : ℝ} (hx : 1 ≤ x) : ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * Real.pi) * Real.log (↑i / x)) ^ 2)⁻¹ ≤ C * (1 + ∫ (t : ℝ) in Set.Ioi 0, hh (1 / (2 * Real.pi)) t)

theorem bound_sum_log' {f : ℕ → ℂ} {C : ℝ} (hf : chebyWith C f) {x : ℝ} (hx : 1 ≤ x) : ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * Real.pi) * Real.log (↑i / x)) ^ 2)⁻¹ ≤ C * (1 + 2 * Real.pi ^ 2)

theorem summable_fourier_aux (x : ℝ) (f : ℕ → ℂ) (ψ : W21) (i : ℕ) : ‖f i / ↑i * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑i / x))‖ ≤ W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * Real.pi) * Real.log (↑i / x)) ^ 2)⁻¹)

theorem summable_fourier {f : ℕ → ℂ} (x : ℝ) (hx : 0 < x) (ψ : W21) (hcheby : cheby f) : Summable fun (i : ℕ) => ‖f i / ↑i * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑i / x))‖

theorem bound_I1 {f : ℕ → ℂ} (x : ℝ) (hx : 0 < x) (ψ : W21) (hcheby : cheby f) : ‖∑' (n : ℕ), f n / ↑n * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x))‖ ≤ W21.norm ψ.toFun • ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * Real.pi) * Real.log (↑i / x)) ^ 2)⁻¹

theorem bound_I1' {f : ℕ → ℂ} {C : ℝ} (x : ℝ) (hx : 1 ≤ x) (ψ : W21) (hcheby : chebyWith C f) : ‖∑' (n : ℕ), f n / ↑n * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x))‖ ≤ W21.norm ψ.toFun * C * (1 + 2 * Real.pi ^ 2)

theorem bound_I2 (x : ℝ) (ψ : W21) : ‖∫ (u : ℝ) in Set.Ici (-Real.log x), FourierTransform.fourier ψ.toFun (u / (2 * Real.pi))‖ ≤ W21.norm ψ.toFun * (2 * Real.pi ^ 2)

theorem bound_main {f : ℕ → ℂ} {C : ℝ} (A : ℂ) (x : ℝ) (hx : 1 ≤ x) (ψ : W21) (hcheby : chebyWith C f) : ‖∑' (n : ℕ), f n / ↑n * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x)) - A * ∫ (u : ℝ) in Set.Ici (-Real.log x), FourierTransform.fourier ψ.toFun (u / (2 * Real.pi))‖ ≤ W21.norm ψ.toFun * (C * (1 + 2 * Real.pi ^ 2) + ‖A‖ * (2 * Real.pi ^ 2))

theorem limiting_cor_W21 {A : ℝ} {G : ℂ → ℂ} {f : ℕ → ℂ} (ψ : W21) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hcheby : cheby f) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries f s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) : Filter.Tendsto (fun (x : ℝ) => ∑' (n : ℕ), f n / ↑n * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x)) - ↑A * ∫ (u : ℝ) in Set.Ici (-Real.log x), FourierTransform.fourier ψ.toFun (u / (2 * Real.pi))) Filter.atTop (nhds 0)

theorem limiting_cor_schwartz {A : ℝ} {G : ℂ → ℂ} {f : ℕ → ℂ} (ψ : SchwartzMap ℝ ℂ) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hcheby : cheby f) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries f s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) : Filter.Tendsto (fun (x : ℝ) => ∑' (n : ℕ), f n / ↑n * FourierTransform.fourier (⇑ψ) (1 / (2 * Real.pi) * Real.log (↑n / x)) - ↑A * ∫ (u : ℝ) in Set.Ici (-Real.log x), FourierTransform.fourier (⇑ψ) (u / (2 * Real.pi))) Filter.atTop (nhds 0)

theorem fourier_surjection_on_schwartz (f : SchwartzMap ℝ ℂ) : ∃ (g : SchwartzMap ℝ ℂ), FourierTransform.fourier g = f

noncomputable def toSchwartz (f : ℝ → ℂ) (h1 : ContDiff ℝ (↑⊤) f) (h2 : HasCompactSupport f) : SchwartzMap ℝ ℂ

Equations

• toSchwartz f h1 h2 = { toFun := f, smooth' := h1, decay' := ⋯ }

@[simp]

theorem toSchwartz_apply (f : ℝ → ℂ) {h1 : ContDiff ℝ (↑⊤) f} {h2 : ∀ (k n : ℕ), ∃ (C : ℝ), ∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C} {x : ℝ} : { toFun := f, smooth' := h1, decay' := h2 } x = f x

theorem comp_exp_support0 {Ψ : ℝ → ℂ} (hplus : closure (Function.support Ψ) ⊆ Set.Ioi 0) : ∀ᶠ (x : ℝ) in nhds 0, Ψ x = 0

theorem comp_exp_support1 {Ψ : ℝ → ℂ} (hplus : closure (Function.support Ψ) ⊆ Set.Ioi 0) : ∀ᶠ (x : ℝ) in Filter.atBot, Ψ (Real.exp x) = 0

theorem comp_exp_support2 {Ψ : ℝ → ℂ} (hsupp : HasCompactSupport Ψ) : ∀ᶠ (x : ℝ) in Filter.atTop, (Ψ ∘ Real.exp) x = 0

theorem comp_exp_support {Ψ : ℝ → ℂ} (hsupp : HasCompactSupport Ψ) (hplus : closure (Function.support Ψ) ⊆ Set.Ioi 0) : HasCompactSupport (Ψ ∘ Real.exp)

theorem wiener_ikehara_smooth_aux {Ψ : ℝ → ℂ} (l0 : Continuous Ψ) (hsupp : HasCompactSupport Ψ) (hplus : closure (Function.support Ψ) ⊆ Set.Ioi 0) (x : ℝ) (hx : 0 < x) : ∫ (u : ℝ) in Set.Ioi (-Real.log x), ↑(Real.exp u) * Ψ (Real.exp u) = ∫ (y : ℝ) in Set.Ioi (1 / x), Ψ y

theorem wiener_ikehara_smooth_sub {A : ℝ} {Ψ : ℝ → ℂ} (h1 : MeasureTheory.Integrable Ψ MeasureTheory.volume) (hplus : closure (Function.support Ψ) ⊆ Set.Ioi 0) : Filter.Tendsto (fun (x : ℝ) => (↑A * ∫ (y : ℝ) in Set.Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Set.Ioi 0, Ψ y) Filter.atTop (nhds 0)

theorem wiener_ikehara_smooth {A : ℝ} {Ψ : ℝ → ℂ} {G : ℂ → ℂ} {f : ℕ → ℂ} (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hcheby : cheby f) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries f s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (hsmooth : ContDiff ℝ (↑⊤) Ψ) (hsupp : HasCompactSupport Ψ) (hplus : closure (Function.support Ψ) ⊆ Set.Ioi 0) : Filter.Tendsto (fun (x : ℝ) => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Set.Ioi 0, Ψ y) Filter.atTop (nhds 0)

theorem wiener_ikehara_smooth' {A : ℝ} {Ψ : ℝ → ℂ} {G : ℂ → ℂ} {f : ℕ → ℂ} (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hcheby : cheby f) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries f s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (hsmooth : ContDiff ℝ (↑⊤) Ψ) (hsupp : HasCompactSupport Ψ) (hplus : closure (Function.support Ψ) ⊆ Set.Ioi 0) : Filter.Tendsto (fun (x : ℝ) => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x) Filter.atTop (nhds (↑A * ∫ (y : ℝ) in Set.Ioi 0, Ψ y))

@[instance_reducible]

def instCoeForallRealForallComplex_primeNumberTheoremAnd_1 {E : Type u_1} : Coe (E → ℝ) (E → ℂ)

Equations

• instCoeForallRealForallComplex_primeNumberTheoremAnd_1 = { coe := fun (f : E → ℝ) (n : E) => ↑(f n) }

theorem set_integral_ofReal {f : ℝ → ℝ} {s : Set ℝ} : ∫ (x : ℝ) in s, ↑(f x) = ↑(∫ (x : ℝ) in s, f x)

theorem wiener_ikehara_smooth_real {A : ℝ} {G : ℂ → ℂ} {f : ℕ → ℝ} {Ψ : ℝ → ℝ} (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (hcheby : cheby fun (n : ℕ) => ↑(f n)) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (hsmooth : ContDiff ℝ (↑⊤) Ψ) (hsupp : HasCompactSupport Ψ) (hplus : closure (Function.support Ψ) ⊆ Set.Ioi 0) : Filter.Tendsto (fun (x : ℝ) => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) Filter.atTop (nhds (A * ∫ (y : ℝ) in Set.Ioi 0, Ψ y))

theorem interval_approx_inf {a b : ℝ} (ha : 0 < a) (hab : a < b) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∃ (ψ : ℝ → ℝ), ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ closure (Function.support ψ) ⊆ Set.Ioi 0 ∧ ψ ≤ (Set.Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Set.Ioi 0, ψ y

theorem interval_approx_sup {a b : ℝ} (ha : 0 < a) (hab : a < b) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∃ (ψ : ℝ → ℝ), ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ closure (Function.support ψ) ⊆ Set.Ioi 0 ∧ (Set.Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Set.Ioi 0, ψ y ≤ b - a + ε

theorem WI_summable {x : ℝ} {f : ℕ → ℝ} {g : ℝ → ℝ} (hg : HasCompactSupport g) (hx : 0 < x) : Summable fun (n : ℕ) => f n * g (↑n / x)

theorem WI_sum_le {x : ℝ} {f : ℕ → ℝ} {g₁ g₂ : ℝ → ℝ} (hf : 0 ≤ f) (hg : g₁ ≤ g₂) (hx : 0 < x) (hg₁ : HasCompactSupport g₁) (hg₂ : HasCompactSupport g₂) : (∑' (n : ℕ), f n * g₁ (↑n / x)) / x ≤ (∑' (n : ℕ), f n * g₂ (↑n / x)) / x

theorem WI_sum_Iab_le {a b x : ℝ} {f : ℕ → ℝ} (hpos : 0 ≤ f) {C : ℝ} (hcheby : chebyWith C fun (n : ℕ) => ↑(f n)) (hb : 0 < b) (hxb : 2 / b < x) : (∑' (n : ℕ), f n * (Set.Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b

theorem WI_sum_Iab_le' {a b : ℝ} {f : ℕ → ℝ} (hpos : 0 ≤ f) {C : ℝ} (hcheby : chebyWith C fun (n : ℕ) => ↑(f n)) (hb : 0 < b) : ∀ᶠ (x : ℝ) in Filter.atTop, (∑' (n : ℕ), f n * (Set.Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b

theorem le_of_eventually_nhdsWithin {a b : ℝ} (h : ∀ᶠ (c : ℝ) in nhdsWithin b (Set.Ioi b), a ≤ c) : a ≤ b

theorem ge_of_eventually_nhdsWithin {a b : ℝ} (h : ∀ᶠ (c : ℝ) in nhdsWithin b (Set.Iio b), c ≤ a) : b ≤ a

theorem WI_tendsto_aux (a b : ℝ) {A : ℝ} (hA : 0 < A) : Filter.Tendsto (fun (c : ℝ) => c / A - (b - a)) (nhdsWithin (A * (b - a)) (Set.Ioi (A * (b - a)))) (nhdsWithin 0 (Set.Ioi 0))

theorem WI_tendsto_aux' (a b : ℝ) {A : ℝ} (hA : 0 < A) : Filter.Tendsto (fun (c : ℝ) => b - a - c / A) (nhdsWithin (A * (b - a)) (Set.Iio (A * (b - a)))) (nhdsWithin 0 (Set.Ioi 0))

theorem residue_nonneg {A : ℝ} {G : ℂ → ℂ} {f : ℕ → ℝ} (hpos : 0 ≤ f) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (hcheby : cheby fun (n : ℕ) => ↑(f n)) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) : 0 ≤ A

theorem WienerIkeharaInterval {A a b : ℝ} {G : ℂ → ℂ} {f : ℕ → ℝ} (hpos : 0 ≤ f) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (hcheby : cheby fun (n : ℕ) => ↑(f n)) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (ha : 0 < a) (hb : a ≤ b) : Filter.Tendsto (fun (x : ℝ) => (∑' (n : ℕ), f n * (Set.Ico a b).indicator 1 (↑n / x)) / x) Filter.atTop (nhds (A * (b - a)))

theorem le_floor_mul_iff {n : ℕ} {b x : ℝ} (hb : 0 ≤ b) (hx : 0 < x) : n ≤ ⌊b * x⌋₊ ↔ ↑n / x ≤ b

theorem lt_ceil_mul_iff {n : ℕ} {b x : ℝ} (hx : 0 < x) : n < ⌈b * x⌉₊ ↔ ↑n / x < b

theorem ceil_mul_le_iff {n : ℕ} {a x : ℝ} (hx : 0 < x) : ⌈a * x⌉₊ ≤ n ↔ a ≤ ↑n / x

theorem mem_Icc_iff_div {n : ℕ} {a b x : ℝ} (hb : 0 ≤ b) (hx : 0 < x) : n ∈ Finset.Icc ⌈a * x⌉₊ ⌊b * x⌋₊ ↔ ↑n / x ∈ Set.Icc a b

theorem mem_Ico_iff_div {n : ℕ} {a b x : ℝ} (hx : 0 < x) : n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊ ↔ ↑n / x ∈ Set.Ico a b

theorem tsum_indicator {a b x : ℝ} {f : ℕ → ℝ} (hx : 0 < x) : ∑' (n : ℕ), f n * (Set.Ico a b).indicator 1 (↑n / x) = ∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n

theorem WienerIkeharaInterval_discrete {A a b : ℝ} {G : ℂ → ℂ} {f : ℕ → ℝ} (hpos : 0 ≤ f) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (hcheby : cheby fun (n : ℕ) => ↑(f n)) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (ha : 0 < a) (hb : a ≤ b) : Filter.Tendsto (fun (x : ℝ) => (∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n) / x) Filter.atTop (nhds (A * (b - a)))

theorem WienerIkeharaInterval_discrete' {A a b : ℝ} {G : ℂ → ℂ} {f : ℕ → ℝ} (hpos : 0 ≤ f) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (hcheby : cheby fun (n : ℕ) => ↑(f n)) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (ha : 0 < a) (hb : a ≤ b) : Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.Ico ⌈a * ↑N⌉₊ ⌈b * ↑N⌉₊, f n) / ↑N) Filter.atTop (nhds (A * (b - a)))

theorem tendsto_mul_ceil_div : Filter.Tendsto (fun (p : ℝ × ℕ) => ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2) (nhdsWithin 0 (Set.Ioi 0) ×ˢ Filter.atTop) (nhds 0)

A version of the Wiener-Ikehara Tauberian Theorem: If f is a nonnegative arithmetic function whose L-series has a simple pole at s = 1 with residue A and otherwise extends continuously to the closed half-plane re s ≥ 1, then ∑ n < N, f n is asymptotic to A*N.

noncomputable def S {𝕜 : Type} [RCLike 𝕜] (f : ℕ → 𝕜) (ε : ℝ) (N : ℕ) : 𝕜

Equations

• S f ε N = (∑ n ∈ Finset.Ico ⌈ε * ↑N⌉₊ N, f n) / ↑N

theorem S_sub_S {𝕜 : Type} [RCLike 𝕜] {f : ℕ → 𝕜} {ε : ℝ} {N : ℕ} (hε : ε ≤ 1) : S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N

theorem tendsto_S_S_zero {f : ℕ → ℝ} (hpos : 0 ≤ f) (hcheby : cheby fun (n : ℕ) => ↑(f n)) : TendstoUniformlyOnFilter (S f) (S f 0) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

theorem WienerIkeharaTheorem' {A : ℝ} {G : ℂ → ℂ} {f : ℕ → ℝ} (hpos : 0 ≤ f) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (hcheby : cheby fun (n : ℕ) => ↑(f n)) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) : Filter.Tendsto (fun (N : ℕ) => cumsum f N / ↑N) Filter.atTop (nhds A)

theorem vonMangoldt_cheby : cheby fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n)

theorem WeakPNT : Filter.Tendsto (fun (N : ℕ) => cumsum (⇑ArithmeticFunction.vonMangoldt) N / ↑N) Filter.atTop (nhds 1)

theorem norm_x_cpow_it (x t : ℝ) (hx : 0 < x) : ‖↑x ^ (↑t * Complex.I)‖ = 1

theorem limiting_fourier_aux_gt_zero {A x : ℝ} {G : ℂ → ℂ} {f : ℕ → ℝ} (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (ψ : CS 2 ℂ) (hx : 0 < x) (σ' : ℝ) (hσ' : 1 < σ') : ∑' (n : ℕ), LSeries.term (fun (n : ℕ) => ↑(f n)) (↑σ') n * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x)) - ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Set.Ici (-Real.log x), ↑(Real.exp (-u * (σ' - 1))) * FourierTransform.fourier ψ.toFun (u / (2 * Real.pi)) = ∫ (t : ℝ), G (↑σ' + ↑t * Complex.I) * ψ.toFun t * ↑x ^ (↑t * Complex.I)

theorem limiting_fourier_lim2_gt_zero {x : ℝ} (A : ℝ) (ψ : W21) (hx : 0 < x) : Filter.Tendsto (fun (σ' : ℝ) => ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Set.Ici (-Real.log x), ↑(Real.exp (-u * (σ' - 1))) * FourierTransform.fourier ψ.toFun (u / (2 * Real.pi))) (nhdsWithin 1 (Set.Ioi 1)) (nhds (↑A * ∫ (u : ℝ) in Set.Ici (-Real.log x), FourierTransform.fourier ψ.toFun (u / (2 * Real.pi))))

theorem limiting_fourier_lim3_gt_zero {x : ℝ} {G : ℂ → ℂ} (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (ψ : CS 2 ℂ) (hx : 0 < x) : Filter.Tendsto (fun (σ' : ℝ) => ∫ (t : ℝ), G (↑σ' + ↑t * Complex.I) * ψ.toFun t * ↑x ^ (↑t * Complex.I)) (nhdsWithin 1 (Set.Ioi 1)) (nhds (∫ (t : ℝ), G (1 + ↑t * Complex.I) * ψ.toFun t * ↑x ^ (↑t * Complex.I)))

theorem tendsto_tsum_of_monotone_convergence {β : Type u_1} {f : ℕ → β → ENNReal} {g : β → ENNReal} (hmono : ∀ (k : β), Monotone fun (n : ℕ) => f n k) (hlim : ∀ (k : β), Filter.Tendsto (fun (n : ℕ) => f n k) Filter.atTop (nhds (g k))) : Filter.Tendsto (fun (n : ℕ) => ∑' (k : β), f n k) Filter.atTop (nhds (∑' (k : β), g k))

theorem tendsto_tsum_of_monotone_convergence_nhdsGT_one {F : ℝ → ℕ → ℝ} (hF_nonneg : ∀ (σ : ℝ) (n : ℕ), 0 ≤ F σ n) (hF_antitone : ∀ (n : ℕ), AntitoneOn (fun (σ : ℝ) => F σ n) (Set.Ioi 1)) (hF_tend : ∀ (n : ℕ), Filter.Tendsto (fun (σ : ℝ) => F σ n) (nhdsWithin 1 (Set.Ioi 1)) (nhds (F 1 n))) (hSumm : ∀ (σ : ℝ), 1 < σ → Summable fun (n : ℕ) => F σ n) (hbounded : (nhdsWithin 1 (Set.Ioi 1)).BoundedAtFilter fun (σ : ℝ) => ∑' (n : ℕ), F σ n) : Filter.Tendsto (fun (σ : ℝ) => ∑' (n : ℕ), F σ n) (nhdsWithin 1 (Set.Ioi 1)) (nhds (∑' (n : ℕ), F 1 n))

theorem limiting_fourier_variant_lim1_aux {f : ℕ → ℝ} {x : ℝ} (ψ : CS 2 ℂ) (hpos : 0 ≤ f) (hf : ∀ (σ : ℝ), 1 < σ → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ)) (hψpos : ∀ (y : ℝ), 0 ≤ (FourierTransform.fourier ψ.toFun y).re ∧ (FourierTransform.fourier ψ.toFun y).im = 0) (σ : ℝ) : 1 < σ → Summable fun (n : ℕ) => (if n = 0 then 0 else f n / ↑n ^ σ) * (FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x))).re

theorem limiting_fourier_variant_lim1 {f : ℕ → ℝ} {x : ℝ} {ψ : CS 2 ℂ} (hpos : 0 ≤ f) (hψpos : ∀ (y : ℝ), 0 ≤ (FourierTransform.fourier ψ.toFun y).re ∧ (FourierTransform.fourier ψ.toFun y).im = 0) (S : ℝ → ℂ) (hSdef : ∀ (σ' : ℝ), S σ' = ∑' (n : ℕ), LSeries.term (fun (n : ℕ) => ↑(f n)) (↑σ') n * FourierTransform.fourier ψ.toFun (Real.pi⁻¹ * 2⁻¹ * Real.log (↑n / x))) (hbounded : (nhdsWithin 1 (Set.Ioi 1)).BoundedAtFilter fun (σ' : ℝ) => ‖S σ'‖) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) : Filter.Tendsto (fun (σ' : ℝ) => ∑' (n : ℕ), LSeries.term (fun (n : ℕ) => ↑(f n)) (↑σ') n * FourierTransform.fourier ψ.toFun (Real.pi⁻¹ * 2⁻¹ * Real.log (↑n / x))) (nhdsWithin 1 (Set.Ioi 1)) (nhds (∑' (n : ℕ), ↑(f n) / ↑n * FourierTransform.fourier ψ.toFun (Real.pi⁻¹ * 2⁻¹ * Real.log (↑n / x))))

theorem limiting_fourier_variant {A x : ℝ} {G : ℂ → ℂ} {f : ℕ → ℝ} (hpos : 0 ≤ f) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (ψ : CS 2 ℂ) (hψpos : ∀ (y : ℝ), 0 ≤ (FourierTransform.fourier ψ.toFun y).re ∧ (FourierTransform.fourier ψ.toFun y).im = 0) (hx : 0 < x) : ∑' (n : ℕ), ↑(f n) / ↑n * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x)) - ↑A * ∫ (u : ℝ) in Set.Ici (-Real.log x), FourierTransform.fourier ψ.toFun (u / (2 * Real.pi)) = ∫ (t : ℝ), G (1 + ↑t * Complex.I) * ψ.toFun t * ↑x ^ (↑t * Complex.I)

theorem norm_mul_integral_Ici_le_integral_norm (A : ℂ) (F : ℝ → ℂ) (a : ℝ) (_hF : MeasureTheory.IntegrableOn F (Set.Ici a) MeasureTheory.volume) (hnorm : MeasureTheory.Integrable (fun (u : ℝ) => ‖F u‖) MeasureTheory.volume) : ‖A * ∫ (u : ℝ) in Set.Ici a, F u‖ ≤ ‖A‖ * ∫ (u : ℝ), ‖F u‖

theorem fourier_decay_of_CS2 (ψ : CS 2 ℂ) : ∃ (C : ℝ), ∀ (u : ℝ), ‖FourierTransform.fourier ψ.toFun u‖ ≤ C / (1 + u ^ 2)

theorem integrable_norm_fourier_scaled_of_CS2 (ψ : CS 2 ℂ) : MeasureTheory.Integrable (fun (u : ℝ) => ‖FourierTransform.fourier ψ.toFun (u / (2 * Real.pi))‖) MeasureTheory.volume

theorem exists_bound_norm_G_on_tsupport {G : ℂ → ℂ} (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (ψ : CS 2 ℂ) : ∃ (K : ℝ), ∀ t ∈ tsupport ψ.toFun, ‖G (1 + ↑t * Complex.I)‖ ≤ K

theorem norm_integrand_le_K_mul_norm_psi {ψ : ℝ → ℂ} {G : ℂ → ℂ} {x K : ℝ} (hx : 0 < x) (hK : ∀ t ∈ Function.support ψ, ‖G (1 + ↑t * Complex.I)‖ ≤ K) (t : ℝ) : ‖G (1 + ↑t * Complex.I) * ψ t * ↑x ^ (↑t * Complex.I)‖ ≤ K * ‖ψ t‖

theorem norm_error_integral_le {G : ℂ → ℂ} (ψ : ℝ → ℂ) (x K : ℝ) (hGline_meas : Measurable fun (t : ℝ) => G (1 + ↑t * Complex.I)) (hψ_meas : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume) (hx : 0 < x) (hK : ∀ t ∈ Function.support ψ, ‖G (1 + ↑t * Complex.I)‖ ≤ K) (hψ : MeasureTheory.Integrable (fun (t : ℝ) => ‖ψ t‖) MeasureTheory.volume) : ‖∫ (t : ℝ), G (1 + ↑t * Complex.I) * ψ t * ↑x ^ (↑t * Complex.I)‖ ≤ K * ∫ (t : ℝ), ‖ψ t‖

theorem crude_upper_bound {A : ℝ} {G : ℂ → ℂ} {f : ℕ → ℝ} (hpos : 0 ≤ f) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (ψ : CS 2 ℂ) (hψpos : ∀ (y : ℝ), 0 ≤ (FourierTransform.fourier ψ.toFun y).re ∧ (FourierTransform.fourier ψ.toFun y).im = 0) : ∃ (B : ℝ), ∀ (x : ℝ), 0 < x → ‖∑' (n : ℕ), ↑(f n) / ↑n * FourierTransform.fourier ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x))‖ ≤ B

theorem Real.fourierIntegral_convolution {f g : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : FourierTransform.fourier (MeasureTheory.convolution f g (ContinuousLinearMap.mul ℂ ℂ) MeasureTheory.volume) = FourierTransform.fourier f * FourierTransform.fourier g

theorem Real.fourierIntegral_conj_neg {f : ℝ → ℂ} (y : ℝ) : FourierTransform.fourier (fun (x : ℝ) => (starRingEnd ℂ) (f (-x))) y = (starRingEnd ℂ) (FourierTransform.fourier f y)

theorem auto_cheby_exists_smooth_nonneg_fourier_kernel : ∃ (ψ : ℝ → ℂ), ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ (∀ (y : ℝ), 0 ≤ (FourierTransform.fourier ψ y).re ∧ (FourierTransform.fourier ψ y).im = 0) ∧ 0 < (FourierTransform.fourier ψ 0).re

Smooth compactly supported function with non-negative Fourier transform via self-convolution.

theorem auto_cheby_fourier_summable {A : ℝ} {G : ℂ → ℂ} {f : ℕ → ℝ} (hpos : 0 ≤ f) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (ψ : ℝ → ℂ) (hψSmooth : ContDiff ℝ (↑⊤) ψ) (hψCompact : HasCompactSupport ψ) (hψpos : ∀ (y : ℝ), 0 ≤ (FourierTransform.fourier ψ y).re ∧ (FourierTransform.fourier ψ y).im = 0) (x : ℝ) (hx : 1 ≤ x) : Summable fun (n : ℕ) => ↑(f n) / ↑n * FourierTransform.fourier ψ (1 / (2 * Real.pi) * Real.log (↑n / x))

The series ∑ f(n)/n · 𝓕ψ(log(n/x)/(2π)) is summable for x ≥ 1.

theorem auto_cheby_short_interval_bound {A : ℝ} {G : ℂ → ℂ} {f : ℕ → ℝ} (hpos : 0 ≤ f) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) (B : ℝ) (ψ : ℝ → ℂ) (hψSmooth : ContDiff ℝ (↑⊤) ψ) (hψCompact : HasCompactSupport ψ) (hψpos : ∀ (y : ℝ), 0 ≤ (FourierTransform.fourier ψ y).re ∧ (FourierTransform.fourier ψ y).im = 0) (hψ0 : 0 < (FourierTransform.fourier ψ 0).re) (hB_bound : ∀ x ≥ 1, ‖∑' (n : ℕ), ↑(f n) / ↑n * FourierTransform.fourier ψ (1 / (2 * Real.pi) * Real.log (↑n / x))‖ ≤ B) : ∃ (ε : ℝ) (C : ℝ), ε > 0 ∧ ε < 1 ∧ C > 0 ∧ ∀ x ≥ 1, ∑' (n : ℕ), f n * (Set.Ioc ((1 - ε) * x) x).indicator (fun (x : ℝ) => 1) ↑n ≤ C * x

Short interval bound from global filtered bound: if ∑ f(n)/n · 𝓕ψ(log(n/x)) ≤ B, then ∑_{(1-ε)x < n ≤ x} f(n) ≤ Cx for some ε, C > 0.

theorem auto_cheby_bootstrap_induction {f : ℕ → ℝ} (hpos : 0 ≤ f) (h_short : ∃ (ε : ℝ) (C : ℝ), ε > 0 ∧ ε < 1 ∧ C > 0 ∧ ∀ x ≥ 1, ∑' (n : ℕ), f n * (Set.Ioc ((1 - ε) * x) x).indicator (fun (x : ℝ) => 1) ↑n ≤ C * x) : cheby fun (n : ℕ) => ↑(f n)

Bootstraps short interval bounds to global Chebyshev bound via strong induction. If ∑_{(1-ε)x < n ≤ x} f(n) ≤ Cx for all x ≥ 1, then ∑_{n ≤ x} f(n) = O(x).

theorem auto_cheby {A : ℝ} {G : ℂ → ℂ} {f : ℕ → ℝ} (hpos : 0 ≤ f) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) : cheby fun (n : ℕ) => ↑(f n)

theorem WienerIkeharaTheorem'' {A : ℝ} {G : ℂ → ℂ} {f : ℕ → ℝ} (hpos : 0 ≤ f) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (hG : ContinuousOn G {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => ↑(f n)) s - ↑A / (s - 1)) {s : ℂ | 1 < s.re}) : Filter.Tendsto (fun (N : ℕ) => cumsum f N / ↑N) Filter.atTop (nhds A)

theorem WeakPNT_character {q a : ℕ} (hq : q ≥ 1) (ha : a.Coprime q) (ha' : a < q) {s : ℂ} (hs : 1 < s.re) : LSeries (fun (n : ℕ) => if n % q = a then ↑(ArithmeticFunction.vonMangoldt n) else 0) s = (-∑' (χ : DirichletCharacter ℂ q), (starRingEnd ℂ) (χ ↑a) * deriv (LSeries fun (n : ℕ) => χ ↑n) s / LSeries (fun (n : ℕ) => χ ↑n) s) / ↑q.totient

theorem WeakPNT_AP_prelim {q a : ℕ} (hq : q ≥ 1) (ha : a.Coprime q) (ha' : a < q) : ∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | 1 ≤ s.re} ∧ Set.EqOn G (fun (s : ℂ) => LSeries (fun (n : ℕ) => if n % q = a then ↑(ArithmeticFunction.vonMangoldt n) else 0) s - 1 / (↑q.totient * (s - 1))) {s : ℂ | 1 < s.re}

theorem summable_vonMangoldt_div_rpow {s : ℝ} (hs : 1 < s) : Summable fun (n : ℕ) => ArithmeticFunction.vonMangoldt n / ↑n ^ s

The von Mangoldt function divided by n ^ s is summable for s > 1.

theorem WeakPNT_AP {q a : ℕ} (hq : q ≥ 1) (ha : a.Coprime q) (ha' : a < q) : Filter.Tendsto (fun (N : ℕ) => cumsum (fun (n : ℕ) => if n % q = a then ArithmeticFunction.vonMangoldt n else 0) N / ↑N) Filter.atTop (nhds (1 / ↑q.totient))