internlm/Lean-Github huggingface dataset:
Theorem: summable_inv_mul_log_sq
Proof 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
Proof 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)⁻¹
Theorem: summable_inv_mul_log_sq
Proof 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
Proof 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)⁻¹
Theorem: summable_inv_mul_log_sq
Proof 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]
Proof 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
Theorem: summable_inv_mul_log_sq
Proof 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
Proof 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
Theorem: summable_inv_mul_log_sq
Proof 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
Proof 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)
Theorem: summable_inv_mul_log_sq
Proof 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 _
Proof 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)⁻¹
Theorem: summable_inv_mul_log_sq
Proof 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
Proof 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)⁻¹
Theorem: summable_inv_mul_log_sq
Proof 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
Proof 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)⁻¹
Theorem: summable_inv_mul_log_sq
Proof 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]
Proof 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
Theorem: summable_inv_mul_log_sq
Proof 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
Proof state after:
no goals
Theorem: summable_inv_mul_log_sq
Proof 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
Proof 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
Theorem: summable_inv_mul_log_sq
Proof 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]
Proof 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)⁻¹
Theorem: summable_inv_mul_log_sq
Proof 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
Proof state after:
no goals
Theorem: summable_inv_mul_log_sq
Proof 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⟩
Proof 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
Theorem: summable_inv_mul_log_sq
Proof 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]
Proof 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
Theorem: summable_inv_mul_log_sq
Proof 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
Proof state after:
no goals
Theorem: summable_inv_mul_log_sq
Proof 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 _
Proof state after:
no goals
Theorem: isLittleO_const_of_tendsto_atTop
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
α : Type u_1
inst✝ : Preorder α
a : ℝ
f : α → ℝ
hf : Tendsto f atTop atTop
⊢ (fun x => a) =o[atTop] f
Tactic:
simp [tendsto_norm_atTop_atTop.comp hf]
Proof state after:
no goals
Theorem: isBigO_pow_pow_of_le
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
m n : ℕ
h : m ≤ n
⊢ (fun x => x ^ m) =O[atTop] fun x => x ^ n
Tactic:
apply IsBigO.of_bound 1
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
m n : ℕ
h : m ≤ n
⊢ ∀ᶠ (x : ℝ) in atTop, ‖x ^ m‖ ≤ 1 * ‖x ^ n‖
Theorem: isBigO_pow_pow_of_le
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
m n : ℕ
h : m ≤ n
⊢ ∀ᶠ (x : ℝ) in atTop, ‖x ^ m‖ ≤ 1 * ‖x ^ n‖
Tactic:
filter_upwards [eventually_ge_atTop 1] with x l1
Proof state after:
case h
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
m n : ℕ
h : m ≤ n
x : ℝ
l1 : 1 ≤ x
⊢ ‖x ^ m‖ ≤ 1 * ‖x ^ n‖
Theorem: isBigO_pow_pow_of_le
Proof state before:
case h
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
m n : ℕ
h : m ≤ n
x : ℝ
l1 : 1 ≤ x
⊢ ‖x ^ m‖ ≤ 1 * ‖x ^ n‖
Tactic:
simpa [abs_eq_self.mpr (zero_le_one.trans l1)] using pow_le_pow_right l1 h
Proof state after:
no goals
Theorem: isLittleO_mul_add_sq
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => a * x + b) =o[atTop] fun x => x ^ 2
Tactic:
apply IsLittleO.add
Proof state after:
case h₁
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => a * x) =o[atTop] fun x => x ^ 2

case h₂
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => b) =o[atTop] fun x => x ^ 2
Theorem: isLittleO_mul_add_sq
Proof state before:
case h₁
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => a * x) =o[atTop] fun x => x ^ 2
Tactic:
apply IsLittleO.const_mul_left
Proof state after:
case h₁.h
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => x) =o[atTop] fun x => x ^ 2
Theorem: isLittleO_mul_add_sq
Proof state before:
case h₁.h
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => x) =o[atTop] fun x => x ^ 2
Tactic:
simpa using isLittleO_pow_pow_atTop_of_lt (𝕜 := ℝ) one_lt_two
Proof state after:
no goals
Theorem: isLittleO_mul_add_sq
Proof state before:
case h₂
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ (fun x => b) =o[atTop] fun x => x ^ 2
Tactic:
apply isLittleO_const_of_tendsto_atTop _ <| tendsto_pow_atTop (by linarith)
Proof state after:
no goals
Theorem: isLittleO_mul_add_sq
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
⊢ 2 ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: log_mul_add_isBigO_log
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
⊢ (fun x => (a * x + b).log) =O[atTop] Real.log
Tactic:
apply IsBigO.of_bound (2 : ℕ)
Proof state after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Theorem: log_mul_add_isBigO_log
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Tactic:
have l2 : ∀ᶠ x : ℝ in atTop, 0 ≤ log x := tendsto_atTop.mp tendsto_log_atTop 0
Proof state after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Theorem: log_mul_add_isBigO_log
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Tactic:
have l3 : ∀ᶠ x : ℝ in atTop, 0 ≤ log (a * x + b) :=
  tendsto_atTop.mp (tendsto_log_atTop.comp (tendsto_mul_add_atTop ha b)) 0
Proof state after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Theorem: log_mul_add_isBigO_log
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Tactic:
have l5 : ∀ᶠ x : ℝ in atTop, 1 ≤ a * x + b := tendsto_atTop.mp (tendsto_mul_add_atTop ha b) 1
Proof state after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5 : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Theorem: log_mul_add_isBigO_log
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5 : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Tactic:
have l1 : ∀ᶠ x : ℝ in atTop, a * x + b ≤ x ^ 2 := by
  filter_upwards [(isLittleO_mul_add_sq a b).eventuallyLE, l5] with x r2 l5
  simpa [abs_eq_self.mpr (zero_le_one.trans l5)] using r2
Proof state after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5 : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
l1 : ∀ᶠ (x : ℝ) in atTop, a * x + b ≤ x ^ 2
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Theorem: log_mul_add_isBigO_log
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5 : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
l1 : ∀ᶠ (x : ℝ) in atTop, a * x + b ≤ x ^ 2
⊢ ∀ᶠ (x : ℝ) in atTop, ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Tactic:
filter_upwards [l1, l2, l3, l5] with x l1 l2 l3 l5
Proof state after:
case h
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5✝ : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
l1✝ : ∀ᶠ (x : ℝ) in atTop, a * x + b ≤ x ^ 2
x : ℝ
l1 : a * x + b ≤ x ^ 2
l2 : 0 ≤ x.log
l3 : 0 ≤ (a * x + b).log
l5 : 1 ≤ a * x + b
⊢ ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Theorem: log_mul_add_isBigO_log
Proof state before:
case h
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5✝ : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
l1✝ : ∀ᶠ (x : ℝ) in atTop, a * x + b ≤ x ^ 2
x : ℝ
l1 : a * x + b ≤ x ^ 2
l2 : 0 ≤ x.log
l3 : 0 ≤ (a * x + b).log
l5 : 1 ≤ a * x + b
⊢ ‖(a * x + b).log‖ ≤ ↑2 * ‖x.log‖
Tactic:
simpa [abs_eq_self.mpr l2, abs_eq_self.mpr l3, Real.log_pow] using Real.log_le_log (by linarith) l1
Proof state after:
no goals
Theorem: log_mul_add_isBigO_log
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5 : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
⊢ ∀ᶠ (x : ℝ) in atTop, a * x + b ≤ x ^ 2
Tactic:
filter_upwards [(isLittleO_mul_add_sq a b).eventuallyLE, l5] with x r2 l5
Proof state after:
case h
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5✝ : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
x : ℝ
r2 : ‖a * x + b‖ ≤ ‖x ^ 2‖
l5 : 1 ≤ a * x + b
⊢ a * x + b ≤ x ^ 2
Theorem: log_mul_add_isBigO_log
Proof state before:
case h
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5✝ : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
x : ℝ
r2 : ‖a * x + b‖ ≤ ‖x ^ 2‖
l5 : 1 ≤ a * x + b
⊢ a * x + b ≤ x ^ 2
Tactic:
simpa [abs_eq_self.mpr (zero_le_one.trans l5)] using r2
Proof state after:
no goals
Theorem: log_mul_add_isBigO_log
Proof state before:
n : ℕ
A a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
l2✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ x.log
l3✝ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ (a * x + b).log
l5✝ : ∀ᶠ (x : ℝ) in atTop, 1 ≤ a * x + b
l1✝ : ∀ᶠ (x : ℝ) in atTop, a * x + b ≤ x ^ 2
x : ℝ
l1 : a * x + b ≤ x ^ 2
l2 : 0 ≤ x.log
l3 : 0 ≤ (a * x + b).log
l5 : 1 ≤ a * x + b
⊢ 0 < a * x + b
Tactic:
linarith
Proof state after:
no goals
Theorem: isBigO_log_mul_add
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
⊢ Real.log =O[atTop] fun x => (a * x + b).log
Tactic:
convert (log_mul_add_isBigO_log (b := -b / a) (inv_pos.mpr ha)).comp_tendsto (tendsto_mul_add_atTop (b := b) ha) using 1
Proof state after:
case h.e'_7
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : 0 < a
b : ℝ
⊢ Real.log = (fun x => (a⁻¹ * x + -b / a).log) ∘ fun x => a * x + b