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

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 instMeasurableSpace : MeasurableSpace Circle

Equations

• instMeasurableSpace = inferInstanceAs (MeasurableSpace ↥(Submonoid.unitSphere ℂ))

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 * Real.fourierIntegral ψ (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 : Continuous ψ) (hsupp : MeasureTheory.Integrable ψ MeasureTheory.volume) (hσ : 1 < σ') : let ν := (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 : Continuous ψ) (hsupp : MeasureTheory.Integrable ψ MeasureTheory.volume) {x σ' : ℝ} (hx : 0 < x) (hσ : 1 < σ') : ∫ (u : ℝ) in Set.Ici (-Real.log x), ↑(Real.exp (-u * (σ' - 1))) * Real.fourierIntegral ψ (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 decay_bounds_key (f : W21) (u : ℝ) : ‖Real.fourierIntegral 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 : ℝ) : ‖Real.fourierIntegral 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)) : ‖Real.fourierIntegral ψ.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 : ℝ), ‖Real.fourierIntegral ψ.toFun u‖ ≤ C / (1 + u ^ 2)

theorem continuous_FourierIntegral (ψ : W21) : Continuous (Real.fourierIntegral ψ.toFun)

theorem W21.integrable_fourier {c : ℝ} (ψ : W21) (hc : c ≠ 0) : MeasureTheory.Integrable (fun (u : ℝ) => Real.fourierIntegral ψ.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 * Real.fourierIntegral ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x)) - ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Set.Ici (-Real.log x), ↑(Real.exp (-u * (σ' - 1))) * Real.fourierIntegral ψ.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 * Real.fourierIntegral ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x))) (nhdsWithin 1 (Set.Ioi 1)) (nhds (∑' (n : ℕ), f n / ↑n * Real.fourierIntegral ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x))))

theorem limiting_fourier_lim2_aux (x C : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => |x| * (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))) * Real.fourierIntegral ψ.toFun (u / (2 * Real.pi))) (nhdsWithin 1 (Set.Ioi 1)) (nhds (↑A * ∫ (u : ℝ) in Set.Ici (-Real.log x), Real.fourierIntegral ψ.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 * Real.fourierIntegral ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x)) - ↑A * ∫ (u : ℝ) in Set.Ici (-Real.log x), Real.fourierIntegral ψ.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 * Real.fourierIntegral ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x)) - ↑A * ∫ (u : ℝ) in Set.Ici (-Real.log x), Real.fourierIntegral ψ.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

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

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 {f : ℕ → ℂ} (x : ℝ) (hx : 0 < x) (ψ : W21) (hcheby : cheby f) : Summable fun (i : ℕ) => ‖f i / ↑i * Real.fourierIntegral ψ.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 * Real.fourierIntegral ψ.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 * Real.fourierIntegral ψ.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), Real.fourierIntegral ψ.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 * Real.fourierIntegral ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x)) - A * ∫ (u : ℝ) in Set.Ici (-Real.log x), Real.fourierIntegral ψ.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 * Real.fourierIntegral ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x)) - ↑A * ∫ (u : ℝ) in Set.Ici (-Real.log x), Real.fourierIntegral ψ.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 * Real.fourierIntegral (⇑ψ) (1 / (2 * Real.pi) * Real.log (↑n / x)) - ↑A * ∫ (u : ℝ) in Set.Ici (-Real.log x), Real.fourierIntegral (⇑ψ) (u / (2 * Real.pi))) Filter.atTop (nhds 0)

theorem fourier_surjection_on_schwartz (f : SchwartzMap ℝ ℂ) : ∃ (g : SchwartzMap ℝ ℂ), Real.fourierIntegral ⇑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))

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 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 ≤ (Real.fourierIntegral ψ.toFun y).re ∧ (Real.fourierIntegral ψ.toFun y).im = 0) (hx : 1 ≤ x) : ∑' (n : ℕ), ↑(f n) / ↑n * Real.fourierIntegral ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x)) - ↑A * ∫ (u : ℝ) in Set.Ici (-Real.log x), Real.fourierIntegral ψ.toFun (u / (2 * Real.pi)) = ∫ (t : ℝ), G (1 + ↑t * Complex.I) * ψ.toFun t * ↑x ^ (↑t * Complex.I)

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 ≤ (Real.fourierIntegral ψ.toFun y).re ∧ (Real.fourierIntegral ψ.toFun y).im = 0) : ∃ (B : ℝ), ∀ (x : ℝ), 0 < x → ‖∑' (n : ℕ), ↑(f n) / ↑n * Real.fourierIntegral ψ.toFun (1 / (2 * Real.pi) * Real.log (↑n / x))‖ ≤ B

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 : ℝ} {F : ℂ → ℂ} {f : ℕ → ℝ} (hpos : 0 ≤ f) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun (n : ℕ) => ↑(f n)) σ')) (hG : ContinuousOn F {s : ℂ | 1 ≤ s.re}) (hG' : Set.EqOn F (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