Documentation

LeanPool.MooreBound.PrimeNumberTheoremAnd.Wiener

Ported for Lean Pool from PrimeNumberTheoremAnd commit 0c7abf7be7765dc5ffd21afc1c37b018199ec3c9, via wewantmoore commit d59bd80ea93fabb9faf769e790ab47692645e022 (both Apache-2.0). The port adds the MooreBound namespace and updates Mathlib APIs and proof style. Wiener and Consequences retain the PNT and prime-interval dependency closure; unrelated later developments and LeanArchitect annotations are omitted.

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

The nonnegative absolute Dirichlet-series term, defined to be zero at n=0.

Equations

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

Instances For

theorem MooreBound.nterm_eq_norm_term {n : ℕ} {σ' : ℝ} {f : ℕ → ℂ} :

nterm f σ' n = ‖LSeries.term f (↑σ') n‖

theorem MooreBound.norm_term_eq_nterm_re {n : ℕ} {f : ℕ → ℂ} (s : ℂ) :

‖LSeries.term f s n‖ = nterm f s.re n

theorem MooreBound.hf_coe1 {σ' : ℝ} {f : ℕ → ℂ} (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hσ : 1 < σ') :

∑' (i : ℕ), ↑‖LSeries.term f (↑σ') i‖₊ ≠ ⊤

@[instance_reducible]

instance MooreBound.instMeasurableSpace :

MeasurableSpace Circle

Equations

One or more equations did not get rendered due to their size.

instance MooreBound.instBorelSpace :

BorelSpace Circle

theorem MooreBound.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 MooreBound.first_fourier_aux2a {n : ℕ} {x y : ℝ} :

2 * ↑Real.pi * -(↑y * (1 / (2 * ↑Real.pi) * ↑(Real.log (↑n / x)))) = -(↑y * ↑(Real.log (↑n / x)))

theorem MooreBound.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 MooreBound.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 MooreBound.continuous_multiplicative_ofAdd :

Continuous ⇑Multiplicative.ofAdd

theorem MooreBound.second_fourier_integrable_aux1a {x σ' : ℝ} (hσ : 1 < σ') :

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

theorem MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.one_add_sq_pos (u : ℝ) :

0 < 1 + u ^ 2

theorem MooreBound.prelim_decay (ψ : ℝ → ℂ) (u : ℝ) :

‖FourierTransform.fourier ψ u‖ ≤ ∫ (t : ℝ), ‖ψ t‖

theorem MooreBound.decay_bounds_key (f : W21) (u : ℝ) :

‖FourierTransform.fourier f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹

theorem MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.decay_bounds_cor_aux (ψ : CS 2 ℂ) :

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

theorem MooreBound.decay_bounds_cor (ψ : W21) :

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

theorem MooreBound.continuous_FourierIntegral (ψ : W21) :

Continuous (FourierTransform.fourier ψ.toFun)

theorem MooreBound.W21.integrable_fourier {c : ℝ} (ψ : W21) (hc : c ≠ 0) :

MeasureTheory.Integrable (fun (u : ℝ) => FourierTransform.fourier ψ.toFun (u / c)) MeasureTheory.volume

theorem MooreBound.continuous_LSeries_aux {σ' : ℝ} {f : ℕ → ℂ} (hf : Summable (nterm f σ')) :

Continuous fun (x : ℝ) => LSeries f (↑σ' + ↑x * Complex.I)

theorem MooreBound.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 MooreBound.cumsum {E : Type u_2} [AddCommMonoid E] (u : ℕ → E) (n : ℕ) :

E

The sum of the sequence over indices strictly below n.

Equations

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

Instances For

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

E

The forward difference u(n+1)-u(n).

Equations

MooreBound.nabla u n = u (n + 1) - u n

Instances For

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

E

The oppositely oriented difference u(n)-u(n+1).

Equations

MooreBound.nnabla u n = u n - u (n + 1)

Instances For

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

E

Shift the argument of a sequence forward by one.

Equations

MooreBound.shift u n = u (n + 1)

Instances For

@[simp]

theorem MooreBound.cumsum_zero {E : Type u_2} [AddCommMonoid E] {u : ℕ → E} :

cumsum u 0 = 0

theorem MooreBound.cumsum_succ {E : Type u_2} [AddCommMonoid E] {u : ℕ → E} (n : ℕ) :

cumsum u (n + 1) = cumsum u n + u n

@[simp]

theorem MooreBound.nabla_cumsum {E : Type u_2} [AddCommGroup E] {u : ℕ → E} :

nabla (cumsum u) = u

theorem MooreBound.neg_cumsum {E : Type u_2} [AddCommGroup E] {u : ℕ → E} :

-cumsum u = cumsum (-u)

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

theorem MooreBound.neg_nabla {α : Type u_1} {E : Type u_2} [OfNat α 1] [Add α] [Ring E] {u : α → E} :

-nabla u = nnabla u

@[simp]

theorem MooreBound.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 MooreBound.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 MooreBound.nnabla_cast {E : Type u_2} (u : ℝ → E) [Sub E] :

nnabla u ∘ Nat.cast = nnabla (u ∘ Nat.cast)

theorem Finset.mooreBoundSumShiftFront {E : Type u_1} [Ring E] {u : ℕ → E} {n : ℕ} :

MooreBound.cumsum u (n + 1) = u 0 + MooreBound.cumsum (MooreBound.shift u) n

theorem Finset.mooreBoundSumShiftFront' {E : Type u_1} [Ring E] {u : ℕ → E} :

MooreBound.shift (MooreBound.cumsum u) = (fun (x : ℕ) => u 0) + MooreBound.cumsum (MooreBound.shift u)

theorem MooreBound.Finset.sum_shift_back {E : Type u_1} [Ring E] {u : ℕ → E} {n : ℕ} :

cumsum u (n + 1) = cumsum u n + u n

theorem MooreBound.Finset.sum_shift_back' {E : Type u_1} [Ring E] {u : ℕ → E} :

shift (cumsum u) = cumsum u + u

theorem MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.summable_iff_bounded {u : ℕ → ℝ} (hu : 0 ≤ u) :

Summable u ↔ Filter.atTop.BoundedAtFilter (cumsum u)

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

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

Summable u ↔ Summable v

theorem MooreBound.BoundedAtFilter.add_const {u : ℕ → ℝ} {c : ℝ} :

(Filter.atTop.BoundedAtFilter fun (n : ℕ) => u n + c) ↔ Filter.atTop.BoundedAtFilter u

theorem MooreBound.BoundedAtFilter.comp_add {u : ℕ → ℝ} {N : ℕ} :

(Filter.atTop.BoundedAtFilter fun (n : ℕ) => u (n + N)) ↔ Filter.atTop.BoundedAtFilter u

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

Summable u ↔ Filter.atTop.BoundedAtFilter (cumsum u)

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

Filter.atTop.BoundedAtFilter u

theorem MooreBound.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 MooreBound.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 MooreBound.summable_inv_mul_log_sq :

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

theorem MooreBound.tendsto_mul_add_atTop {a : ℝ} (ha : 0 < a) (b : ℝ) :

Filter.Tendsto (fun (x : ℝ) => a * x + b) Filter.atTop Filter.atTop

theorem MooreBound.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 MooreBound.isBigO_pow_pow_of_le {m n : ℕ} (h : m ≤ n) :

(fun (x : ℝ) => x ^ m) =O[Filter.atTop ] fun (x : ℝ) => x ^ n

theorem MooreBound.isLittleO_mul_add_sq (a b : ℝ) :

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

theorem MooreBound.log_mul_add_isBigO_log {a : ℝ} (ha : 0 < a) (b : ℝ) :

(fun (x : ℝ) => Real.log (a * x + b)) =O[Filter.atTop ] Real.log

theorem MooreBound.isBigO_log_mul_add {a : ℝ} (ha : 0 < a) (b : ℝ) :

Real.log =O[Filter.atTop ] fun (x : ℝ) => Real.log (a * x + b)

theorem MooreBound.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.mooreBoundAddIsLittleORight {f g : ℝ → ℝ} (h : g =o[Filter.atTop ] f) :

f =O[Filter.atTop ] (f + g)

theorem Asymptotics.IsBigO.mooreBoundSq {α : 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 MooreBound.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 MooreBound.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 MooreBound.log_add_one_sub_log_le {x : ℝ} (hx : 0 < x) :

nabla Real.log x ≤ x⁻¹

theorem MooreBound.nabla_log_main :

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

theorem MooreBound.nabla_log {b : ℝ} (hb : 0 < b) :

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

theorem MooreBound.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 MooreBound.nnabla_bound_aux1 (a : ℝ) {b : ℝ} (hb : 0 < b) :

Filter.Tendsto (fun (x : ℝ) => x * (a + Real.log (x / b) ^ 2)) Filter.atTop Filter.atTop

theorem MooreBound.nnabla_bound_aux2 (a : ℝ) {b : ℝ} (hb : 0 < b) :

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

theorem MooreBound.Real.log_eventually_gt_atTop (a : ℝ) :

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

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

‖x‖ ≤ ‖y‖

Should this be a gcongr lemma?

theorem MooreBound.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 MooreBound.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 MooreBound.chebyWith (C : ℝ) (f : ℕ → ℂ) :

A linear upper bound, with constant C, on sums of absolute coefficients.

Equations

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

Instances For

def MooreBound.cheby (f : ℕ → ℂ) :

Existence of a linear upper bound on sums of absolute coefficients.

Equations

MooreBound.cheby f = ∃ (C : ℝ), MooreBound.chebyWith C f

Instances For

theorem MooreBound.cheby.bigO {f : ℕ → ℂ} (h : cheby f) :

(cumsum fun (x : ℕ) => ‖f x‖) =O[Filter.atTop ] Nat.cast

theorem MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.limiting_cor_aux {f : ℝ → ℂ} :

Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ), f t * ↑x ^ (↑t * Complex.I)) Filter.atTop (nhds 0)

theorem MooreBound.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 MooreBound.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 MooreBound.chosenTrunc :

A chosen smooth cutoff with the support and plateau required by trunc.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem MooreBound.one_div_sub_one (n : ℕ) :

1 / ↑(n - 1) ≤ 2 / ↑n

theorem MooreBound.quadratic_pos (a b c x : ℝ) (ha : 0 < a) (hΔ : discrim a b c < 0) :

0 < a * x ^ 2 + b * x + c

noncomputable def MooreBound.pp (a x : ℝ) :

The quadratic numerator used to control the derivative of the decay kernel.

Equations

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

Instances For

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

The derivative of the quadratic numerator with respect to x.

Equations

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

Instances For

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

0 < pp a x

theorem MooreBound.pp_deriv (a x : ℝ) :

HasDerivAt (pp a) (pp' a x) x

theorem MooreBound.pp_deriv_eq (a : ℝ) :

deriv (pp a) = pp' a

theorem MooreBound.pp'_deriv (a x : ℝ) :

HasDerivAt (pp' a) (a ^ 2 * 2) x

theorem MooreBound.pp'_deriv_eq (a : ℝ) :

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

noncomputable def MooreBound.hh (a t : ℝ) :

The integrable logarithmic decay kernel 1/(t(1+(a log t)²)).

Equations

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

Instances For

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

The derivative of the logarithmic decay kernel with respect to t.

Equations

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

Instances For

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

0 ≤ hh a t

theorem MooreBound.hh_le (a t : ℝ) (ht : 0 ≤ t) :

|hh a t| ≤ t⁻¹

theorem MooreBound.hh_deriv (a : ℝ) {t : ℝ} (ht : t ≠ 0) :

HasDerivAt (hh a) (hh' a t) t

theorem MooreBound.hh_continuous (a : ℝ) :

ContinuousOn (hh a) (Set.Ioi 0)

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

hh' a x ≤ 0

theorem MooreBound.hh_antitone {a : ℝ} (ha : a ∈ Set.Ioo (-1) 1) :

AntitoneOn (hh a) (Set.Ioi 0)

noncomputable def MooreBound.gg (x i : ℝ) :

The rescaled logarithmic kernel used to bound Fourier tails.

Equations

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

Instances For

theorem MooreBound.gg_of_hh {x : ℝ} (hx : x ≠ 0) (i : ℝ) :

gg x i = x⁻¹ * hh (1 / (2 * Real.pi)) (i / x)

theorem MooreBound.gg_l1 {x : ℝ} (hx : 0 < x) (n : ℕ) :

|gg x ↑n| ≤ 1 / ↑n

theorem MooreBound.gg_le_one {x : ℝ} (i : ℕ) :

gg x ↑i ≤ 1

theorem MooreBound.one_div_two_pi_mem_Ioo :

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

theorem MooreBound.sum_telescopic (a : ℕ → ℝ) (n : ℕ) :

∑ i ∈ Finset.range n, (a (i + 1) - a i) = a n - a 0

theorem MooreBound.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 MooreBound.sum_range_succ (a : ℕ → ℝ) (n : ℕ) :

∑ i ∈ Finset.range n, a (i + 1) = ∑ i ∈ Finset.range (n + 1), a i - a 0

theorem MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.hh_integral' :

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

theorem MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.fourier_surjection_on_schwartz (f : SchwartzMap ℝ ℂ) :

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

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

SchwartzMap ℝ ℂ

Turn a compactly supported smooth complex function into a Schwartz function.

Equations

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

Instances For

@[simp]

theorem MooreBound.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 MooreBound.comp_exp_support0 {Ψ : ℝ → ℂ} (hplus : closure (Function.support Ψ) ⊆ Set.Ioi 0) :

∀ᶠ (x : ℝ) in nhds 0, Ψ x = 0

theorem MooreBound.comp_exp_support1 {Ψ : ℝ → ℂ} (hplus : closure (Function.support Ψ) ⊆ Set.Ioi 0) :

∀ᶠ (x : ℝ) in Filter.atBot , Ψ (Real.exp x) = 0

theorem MooreBound.comp_exp_support2 {Ψ : ℝ → ℂ} (hsupp : HasCompactSupport Ψ) :

∀ᶠ (x : ℝ) in Filter.atTop , (Ψ ∘ Real.exp) x = 0

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

HasCompactSupport (Ψ ∘ Real.exp)

theorem MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.realFunctionComplexCoeWiener {E : Type u_1} :

Coe (E → ℝ) (E → ℂ)

Pointwise complexification, local to the real Wiener-Ikehara argument.

Equations

MooreBound.realFunctionComplexCoeWiener = { coe := fun (f : E → ℝ) (n : E) => ↑(f n) }

Instances For

theorem MooreBound.set_integral_ofReal {f : ℝ → ℝ} {s : Set ℝ} :

∫ (x : ℝ) in s, ↑(f x) = ↑(∫ (x : ℝ) in s, f x)

theorem MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.WI_summable {x : ℝ} {f : ℕ → ℝ} {g : ℝ → ℝ} (hg : HasCompactSupport g) (hx : 0 < x) :

Summable fun (n : ℕ) => f n * g (↑n / x)

theorem MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.le_of_eventually_nhdsWithin {a b : ℝ} (h : ∀ᶠ (c : ℝ) in nhdsWithin b (Set.Ioi b), a ≤ c) :

a ≤ b

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

b ≤ a

theorem MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.le_floor_mul_iff {n : ℕ} {b x : ℝ} (hb : 0 ≤ b) (hx : 0 < x) :

n ≤ ⌊b * x⌋₊ ↔ ↑n / x ≤ b

theorem MooreBound.lt_ceil_mul_iff {n : ℕ} {b x : ℝ} (hx : 0 < x) :

n < ⌈b * x⌉₊ ↔ ↑n / x < b

theorem MooreBound.ceil_mul_le_iff {n : ℕ} {a x : ℝ} (hx : 0 < x) :

⌈a * x⌉₊ ≤ n ↔ a ≤ ↑n / x

theorem MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.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 MooreBound.S {𝕜 : Type} [RCLike 𝕜] (f : ℕ → 𝕜) (ε : ℝ) (N : ℕ) :

𝕜

Normalize a coefficient sum over the interval from ceil(epsilon*N) to N-1.

Equations

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

Instances For

theorem MooreBound.S_sub_S {𝕜 : Type} [RCLike 𝕜] {f : ℕ → 𝕜} {ε : ℝ} {N : ℕ} (hε : ε ≤ 1) :

S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N

theorem MooreBound.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 MooreBound.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 MooreBound.vonMangoldt_cheby :

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

theorem MooreBound.WeakPNT :

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