Theorem: summable_inv_mul_log_sq (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹
Tactic:
let u (n : ℕ) := (n * (Real.log n) ^ 2)⁻¹
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹
Tactic:
have l7 : ∀ᶠ n : ℕ in atTop, 1 ≤ Real.log n := tendsto_atTop.mp (tendsto_log_atTop.comp tendsto_natCast_atTop_atTop) 1
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹
Tactic:
have l8 : ∀ᶠ n : ℕ in atTop, 1 ≤ n := eventually_ge_atTop 1
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹
Tactic:
have l9 : ∀ᶠ n in atTop, u (n + 1) ≤ u n := by filter_upwards [l7, l8] with n l2 l8 ; dsimp [u] ; gcongr <;> simp
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹
Tactic:
obtain ⟨v, l1, l2, l3⟩ := exists_antitone_of_eventually l9
State after:
case intro.intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹

State before:
case intro.intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹
Tactic:
rw [summable_congr_ae l3.symm]
State after:
case intro.intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
⊢ Summable v

State before:
case intro.intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
⊢ Summable v
Tactic:
have l4 (n : ℕ) : 0 ≤ v n := by obtain ⟨k, hk⟩ := l1 ⟨n, rfl⟩ ; rw [← hk] ; positivity
State after:
case intro.intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
l4 : ∀ (n : ℕ), 0 ≤ v n
⊢ Summable v

State before:
case intro.intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
l4 : ∀ (n : ℕ), 0 ≤ v n
⊢ Summable v
Tactic:
apply (summable_condensed_iff_of_nonneg l4 (fun _ _ _ a ↦ l2 a)).mp
State after:
case intro.intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
l4 : ∀ (n : ℕ), 0 ≤ v n
⊢ Summable fun k => 2 ^ k * v (2 ^ k)

State before:
case intro.intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
l4 : ∀ (n : ℕ), 0 ≤ v n
⊢ Summable fun k => 2 ^ k * v (2 ^ k)
Tactic:
suffices this : ∀ᶠ k : ℕ in atTop, 2 ^ k * v (2 ^ k) = ((k : ℝ) ^ 2)⁻¹ * ((Real.log 2) ^ 2)⁻¹ by
  exact (summable_congr_ae this).mpr <| (Real.summable_nat_pow_inv.mpr one_lt_two).mul_right _
State after:
case intro.intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
l4 : ∀ (n : ℕ), 0 ≤ v n
⊢ ∀ᶠ (k : ℕ) in atTop, 2 ^ k * v (2 ^ k) = (↑k ^ 2)⁻¹ * (Real.log 2 ^ 2)⁻¹

State before:
case intro.intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
l4 : ∀ (n : ℕ), 0 ≤ v n
⊢ ∀ᶠ (k : ℕ) in atTop, 2 ^ k * v (2 ^ k) = (↑k ^ 2)⁻¹ * (Real.log 2 ^ 2)⁻¹
Tactic:
have l5 : ∀ᶠ k in atTop, v (2 ^ k) = u (2 ^ k) := l3.comp_tendsto <| Nat.tendsto_pow_atTop_atTop_of_one_lt Nat.le.refl
State after:
case intro.intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
l4 : ∀ (n : ℕ), 0 ≤ v n
l5 : ∀ᶠ (k : ℕ) in atTop, v (2 ^ k) = u (2 ^ k)
⊢ ∀ᶠ (k : ℕ) in atTop, 2 ^ k * v (2 ^ k) = (↑k ^ 2)⁻¹ * (Real.log 2 ^ 2)⁻¹

State before:
case intro.intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
l4 : ∀ (n : ℕ), 0 ≤ v n
l5 : ∀ᶠ (k : ℕ) in atTop, v (2 ^ k) = u (2 ^ k)
⊢ ∀ᶠ (k : ℕ) in atTop, 2 ^ k * v (2 ^ k) = (↑k ^ 2)⁻¹ * (Real.log 2 ^ 2)⁻¹
Tactic:
filter_upwards [l5, l8] with k l5 l8
State after:
case h
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8✝ : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
l4 : ∀ (n : ℕ), 0 ≤ v n
l5✝ : ∀ᶠ (k : ℕ) in atTop, v (2 ^ k) = u (2 ^ k)
k : ℕ
l5 : v (2 ^ k) = u (2 ^ k)
l8 : 1 ≤ k
⊢ 2 ^ k * v (2 ^ k) = (↑k ^ 2)⁻¹ * (Real.log 2 ^ 2)⁻¹

State before:
case h
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8✝ : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
l4 : ∀ (n : ℕ), 0 ≤ v n
l5✝ : ∀ᶠ (k : ℕ) in atTop, v (2 ^ k) = u (2 ^ k)
k : ℕ
l5 : v (2 ^ k) = u (2 ^ k)
l8 : 1 ≤ k
⊢ 2 ^ k * v (2 ^ k) = (↑k ^ 2)⁻¹ * (Real.log 2 ^ 2)⁻¹
Tactic:
field_simp [u, l5]
State after:
case h
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8✝ : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
l4 : ∀ (n : ℕ), 0 ≤ v n
l5✝ : ∀ᶠ (k : ℕ) in atTop, v (2 ^ k) = u (2 ^ k)
k : ℕ
l5 : v (2 ^ k) = u (2 ^ k)
l8 : 1 ≤ k
⊢ ↑k ^ 2 * Real.log 2 ^ 2 = (↑k * Real.log 2) ^ 2

State before:
case h
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8✝ : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
l4 : ∀ (n : ℕ), 0 ≤ v n
l5✝ : ∀ᶠ (k : ℕ) in atTop, v (2 ^ k) = u (2 ^ k)
k : ℕ
l5 : v (2 ^ k) = u (2 ^ k)
l8 : 1 ≤ k
⊢ ↑k ^ 2 * Real.log 2 ^ 2 = (↑k * Real.log 2) ^ 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 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
⊢ ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
Tactic:
filter_upwards [l7, l8] with n l2 l8
State after:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8✝ : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
n : ℕ
l2 : 1 ≤ (↑n).log
l8 : 1 ≤ n
⊢ u (n + 1) ≤ u n

State before:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8✝ : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
n : ℕ
l2 : 1 ≤ (↑n).log
l8 : 1 ≤ n
⊢ u (n + 1) ≤ u n
Tactic:
dsimp [u]
State after:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8✝ : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
n : ℕ
l2 : 1 ≤ (↑n).log
l8 : 1 ≤ n
⊢ (↑(n + 1) * (↑(n + 1)).log ^ 2)⁻¹ ≤ (↑n * (↑n).log ^ 2)⁻¹

State before:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8✝ : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
n : ℕ
l2 : 1 ≤ (↑n).log
l8 : 1 ≤ n
⊢ (↑(n + 1) * (↑(n + 1)).log ^ 2)⁻¹ ≤ (↑n * (↑n).log ^ 2)⁻¹
Tactic:
gcongr <;> simp
State after:
no goals

State before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
n : ℕ
⊢ 0 ≤ v n
Tactic:
obtain ⟨k, hk⟩ := l1 ⟨n, rfl⟩
State after:
case intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
n k : ℕ
hk : u k = v n
⊢ 0 ≤ v n

State before:
case intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
n k : ℕ
hk : u k = v n
⊢ 0 ≤ v n
Tactic:
rw [← hk]
State after:
case intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
n k : ℕ
hk : u k = v n
⊢ 0 ≤ u k

State before:
case intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
n k : ℕ
hk : u k = v n
⊢ 0 ≤ u k
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
l9 : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
v : ℕ → ℝ
l1 : range v ⊆ range u
l2 : Antitone v
l3 : v =ᶠ[atTop] u
l4 : ∀ (n : ℕ), 0 ≤ v n
this : ∀ᶠ (k : ℕ) in atTop, 2 ^ k * v (2 ^ k) = (↑k ^ 2)⁻¹ * (Real.log 2 ^ 2)⁻¹
⊢ Summable fun k => 2 ^ k * v (2 ^ k)
Tactic:
exact (summable_congr_ae this).mpr <| (Real.summable_nat_pow_inv.mpr one_lt_two).mul_right _
State after:
no goals