Theorem: bound_I1 (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤
    W21.norm ψ.toFun • ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
Tactic:
have l5 : Summable fun i ↦ ‖f i‖ / ↑i * ((1 + (1 / (2 * ↑π) * ↑(Real.log (↑i / x))) ^ 2)⁻¹) := by
  simpa using limiting_fourier_lim1_aux hcheby hx 1 zero_le_one
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤
    W21.norm ψ.toFun • ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
l6 :
  ∀ (i : ℕ),
    ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ ≤
      W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤
    W21.norm ψ.toFun • ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
Tactic:
have l1 : Summable fun i ↦ ‖f i / ↑i * 𝓕 ψ (1 / (2 * π) * Real.log (↑i / x))‖ := by
  exact summable_fourier x hx ψ hcheby
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
l6 :
  ∀ (i : ℕ),
    ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ ≤
      W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
l1 : Summable fun i => ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤
    W21.norm ψ.toFun • ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
l6 :
  ∀ (i : ℕ),
    ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ ≤
      W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
l1 : Summable fun i => ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤
    W21.norm ψ.toFun • ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
Tactic:
apply (norm_tsum_le_tsum_norm l1).trans
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
l6 :
  ∀ (i : ℕ),
    ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ ≤
      W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
l1 : Summable fun i => ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖
⊢ ∑' (i : ℕ), ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ ≤
    W21.norm ψ.toFun • ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
l6 :
  ∀ (i : ℕ),
    ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ ≤
      W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
l1 : Summable fun i => ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖
⊢ ∑' (i : ℕ), ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ ≤
    W21.norm ψ.toFun • ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
Tactic:
simpa only [← tsum_const_smul _ l5] using tsum_mono l1 (by simpa using l5.const_smul (W21.norm ψ)) l6
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
⊢ Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
Tactic:
simpa using limiting_fourier_lim1_aux hcheby hx 1 zero_le_one
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ ≤
    W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
Tactic:
convert mul_le_mul_of_nonneg_left (decay_bounds_key ψ (1 / (2 * π) * log (i / x))) (norm_nonneg (f i / i)) using 1
State after:
case h.e'_3
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ = ‖f i / ↑i‖ * ‖𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖

case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹) =
    ‖f i / ↑i‖ * (‖ψ‖ * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)

State before:
case h.e'_3
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ = ‖f i / ↑i‖ * ‖𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖
Tactic:
simp [norm_mul]
State after:
no goals

State before:
case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹) =
    ‖f i / ↑i‖ * (‖ψ‖ * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
Tactic:
change _ = _ * (W21.norm ψ * _)
State after:
case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹) =
    ‖f i / ↑i‖ * (W21.norm ψ.toFun * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)

State before:
case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹) =
    ‖f i / ↑i‖ * (W21.norm ψ.toFun * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
Tactic:
simp [W21.norm]
State after:
case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ ((∫ (v : ℝ), Complex.abs (ψ.toFun v)) + (π ^ 2)⁻¹ * 4⁻¹ * ∫ (v : ℝ), Complex.abs (deriv (deriv ψ.toFun) v)) *
      (Complex.abs (f i) / ↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹) =
    Complex.abs (f i) / ↑i *
      (((∫ (v : ℝ), Complex.abs (ψ.toFun v)) + (π ^ 2)⁻¹ * 4⁻¹ * ∫ (v : ℝ), Complex.abs (deriv (deriv ψ.toFun) v)) *
        (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹)

State before:
case h.e'_4
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
i : ℕ
⊢ ((∫ (v : ℝ), Complex.abs (ψ.toFun v)) + (π ^ 2)⁻¹ * 4⁻¹ * ∫ (v : ℝ), Complex.abs (deriv (deriv ψ.toFun) v)) *
      (Complex.abs (f i) / ↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹) =
    Complex.abs (f i) / ↑i *
      (((∫ (v : ℝ), Complex.abs (ψ.toFun v)) + (π ^ 2)⁻¹ * 4⁻¹ * ∫ (v : ℝ), Complex.abs (deriv (deriv ψ.toFun) v)) *
        (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹)
Tactic:
ring
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
l6 :
  ∀ (i : ℕ),
    ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ ≤
      W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
⊢ Summable fun i => ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖
Tactic:
exact summable_fourier x hx ψ hcheby
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
ψ : W21
hcheby : cheby f
l5 : Summable fun i => ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
l6 :
  ∀ (i : ℕ),
    ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖ ≤
      W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
l1 : Summable fun i => ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖
⊢ Summable fun i => W21.norm ψ.toFun * (‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹)
Tactic:
simpa using l5.const_smul (W21.norm ψ)
State after:
no goals