internlm/Lean-Github huggingface dataset:
Theorem: bound_I1
Proof 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
Proof 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)⁻¹
Theorem: bound_I1
Proof 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
Proof 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)⁻¹
Theorem: bound_I1
Proof 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
Proof 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)⁻¹
Theorem: bound_I1
Proof 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
Proof state after:
no goals
Theorem: bound_I1
Proof 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
Proof state after:
no goals
Theorem: bound_I1
Proof 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
Proof 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)⁻¹)
Theorem: bound_I1
Proof 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]
Proof state after:
no goals
Theorem: bound_I1
Proof 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 ψ * _)
Proof 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)⁻¹)
Theorem: bound_I1
Proof 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]
Proof 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)⁻¹)
Theorem: bound_I1
Proof 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
Proof state after:
no goals
Theorem: bound_I1
Proof 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
Proof state after:
no goals
Theorem: bound_I1
Proof 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 ψ)
Proof state after:
no goals
Theorem: bound_I1'
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ ‖∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log)‖ ≤ W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
Tactic:
apply bound_I1 x (by linarith) ψ ⟨_, hcheby⟩ |>.trans
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ W21.norm ψ.toFun • ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤
    W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
Theorem: bound_I1'
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ W21.norm ψ.toFun • ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤
    W21.norm ψ.toFun * C * (1 + 2 * π ^ 2)
Tactic:
rw [smul_eq_mul, mul_assoc]
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ W21.norm ψ.toFun * ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤
    W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2))
Theorem: bound_I1'
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ W21.norm ψ.toFun * ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹ ≤
    W21.norm ψ.toFun * (C * (1 + 2 * π ^ 2))
Tactic:
apply mul_le_mul le_rfl (bound_sum_log' hcheby hx) ?_ W21.norm_nonneg
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ 0 ≤ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
Theorem: bound_I1'
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ 0 ≤ ∑' (i : ℕ), ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
Tactic:
apply tsum_nonneg (fun i => by positivity)
Proof state after:
no goals
Theorem: bound_I1'
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
⊢ 0 < x
Tactic:
linarith
Proof state after:
no goals
Theorem: bound_I1'
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C x : ℝ
hx : 1 ≤ x
ψ : W21
hcheby : chebyWith C f
i : ℕ
⊢ 0 ≤ ‖f i‖ / ↑i * (1 + (1 / (2 * π) * (↑i / x).log) ^ 2)⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: bound_I2
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
have key a : ‖𝓕 ψ (a / (2 * π))‖ ≤ W21.norm ψ * (1 + (a / (2 * π)) ^ 2)⁻¹ := decay_bounds_key ψ _
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Theorem: bound_I2
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
have twopi : 0 ≤ 2 * π := by simp [pi_nonneg]
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Theorem: bound_I2
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
have l3 : Integrable (fun a ↦ (1 + (a / (2 * π)) ^ 2)⁻¹) := integrable_inv_one_add_sq.comp_div (by norm_num [pi_ne_zero])
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Theorem: bound_I2
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
have l2 : IntegrableOn (fun i ↦ W21.norm ψ * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-Real.log x)) := by
  exact (l3.const_mul _).integrableOn
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Theorem: bound_I2
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
have l5 : 0 ≤ᵐ[volume] fun a ↦ (1 + (a / (2 * π)) ^ 2)⁻¹ := by apply eventually_of_forall ; intro x ; positivity
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Theorem: bound_I2
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
refine (norm_integral_le_integral_norm _).trans <| (setIntegral_mono l1 l2 key).trans ?_
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ∫ (x : ℝ) in Ici (-x.log), W21.norm ψ.toFun * (1 + (x / (2 * π)) ^ 2)⁻¹ ∂volume ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Theorem: bound_I2
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ∫ (x : ℝ) in Ici (-x.log), W21.norm ψ.toFun * (1 + (x / (2 * π)) ^ 2)⁻¹ ∂volume ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
rw [integral_mul_left]
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ W21.norm ψ.toFun * ∫ (a : ℝ) in Ici (-x.log), (1 + (a / (2 * π)) ^ 2)⁻¹ ∂volume ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Theorem: bound_I2
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ W21.norm ψ.toFun * ∫ (a : ℝ) in Ici (-x.log), (1 + (a / (2 * π)) ^ 2)⁻¹ ∂volume ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
gcongr
Proof state after:
case a0
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ 0 ≤ W21.norm ψ.toFun

case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ∫ (a : ℝ) in Ici (-x.log), (1 + (a / (2 * π)) ^ 2)⁻¹ ∂volume ≤ 2 * π ^ 2
Theorem: bound_I2
Proof state before:
case a0
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ 0 ≤ W21.norm ψ.toFun

case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ∫ (a : ℝ) in Ici (-x.log), (1 + (a / (2 * π)) ^ 2)⁻¹ ∂volume ≤ 2 * π ^ 2
Tactic:
apply W21.norm_nonneg
Proof state after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ∫ (a : ℝ) in Ici (-x.log), (1 + (a / (2 * π)) ^ 2)⁻¹ ∂volume ≤ 2 * π ^ 2