internlm/Lean-Github huggingface dataset:
Theorem: hh_integrable_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
this : g =ᶠ[atTop] g₀
⊢ Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
Tactic:
apply Tendsto.congr' this
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
this : g =ᶠ[atTop] g₀
⊢ Tendsto g atTop (𝓝 (a * c / b * (π / 2)))
Theorem: hh_integrable_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
this : g =ᶠ[atTop] g₀
⊢ Tendsto g atTop (𝓝 (a * c / b * (π / 2)))
Tactic:
apply Tendsto.const_mul
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
this : g =ᶠ[atTop] g₀
⊢ Tendsto (fun k => (b * (k / c).log).arctan) atTop (𝓝 (π / 2))
Theorem: hh_integrable_aux
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
this : g =ᶠ[atTop] g₀
⊢ Tendsto (fun k => (b * (k / c).log).arctan) atTop (𝓝 (π / 2))
Tactic:
apply (tendsto_arctan_atTop.mono_right nhdsWithin_le_nhds).comp
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
this : g =ᶠ[atTop] g₀
⊢ Tendsto (fun k => b * (k / c).log) atTop atTop
Theorem: hh_integrable_aux
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
this : g =ᶠ[atTop] g₀
⊢ Tendsto (fun k => b * (k / c).log) atTop atTop
Tactic:
apply Tendsto.const_mul_atTop hb
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
this : g =ᶠ[atTop] g₀
⊢ Tendsto (fun x => (x / c).log) atTop atTop
Theorem: hh_integrable_aux
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
this : g =ᶠ[atTop] g₀
⊢ Tendsto (fun x => (x / c).log) atTop atTop
Tactic:
apply tendsto_log_atTop.comp
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
this : g =ᶠ[atTop] g₀
⊢ Tendsto (fun x => x / c) atTop atTop
Theorem: hh_integrable_aux
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
this : g =ᶠ[atTop] g₀
⊢ Tendsto (fun x => x / c) atTop atTop
Tactic:
apply Tendsto.atTop_div_const hc
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
this : g =ᶠ[atTop] g₀
⊢ Tendsto (fun x => x) atTop atTop
Theorem: hh_integrable_aux
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
this : g =ᶠ[atTop] g₀
⊢ Tendsto (fun x => x) atTop atTop
Tactic:
apply tendsto_id
Proof state after:
no goals
Theorem: hh_integrable_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
⊢ g =ᶠ[atTop] g₀
Tactic:
apply eventually_of_mem (Ioi_mem_atTop 0)
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
⊢ ∀ x ∈ Ioi 0, g x = g₀ x
Theorem: hh_integrable_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
⊢ ∀ x ∈ Ioi 0, g x = g₀ x
Tactic:
intro y (hy : 0 < y)
Proof state after:
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
y : ℝ
hy : 0 < y
⊢ g y = g₀ y
Theorem: hh_integrable_aux
Proof state before:
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
y : ℝ
hy : 0 < y
⊢ g y = g₀ y
Tactic:
simp [g₀, hy.ne.symm]
Proof state after:
no goals
Theorem: hh_integrable_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
⊢ Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
Tactic:
have : g =ᶠ[𝓝[>] 0] g₀ := by
  apply eventually_of_mem self_mem_nhdsWithin
  intro x (hx : 0 < x) ; simp [g₀, hx.ne.symm]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
Theorem: hh_integrable_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
Tactic:
simp only [g₀]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto (fun x => if x = 0 then a * c / b * -(π / 2) else g x) (𝓝[>] 0)
    (𝓝 (if True then a * c / b * -(π / 2) else g 0))
Theorem: hh_integrable_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto (fun x => if x = 0 then a * c / b * -(π / 2) else g x) (𝓝[>] 0)
    (𝓝 (if True then a * c / b * -(π / 2) else g 0))
Tactic:
apply Tendsto.congr' this
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto g (𝓝[>] 0) (𝓝 (if True then a * c / b * -(π / 2) else g 0))
Theorem: hh_integrable_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto g (𝓝[>] 0) (𝓝 (if True then a * c / b * -(π / 2) else g 0))
Tactic:
apply Tendsto.const_mul
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hb : 0 < b
hc : 0 < c
g : ℝ → ℝ := fun x => a * c / b * (b * (x / c).log).arctan
g₀ : ℝ → ℝ := fun x => if x = 0 then a * c / b * -(π / 2) else g x
g' : ℝ → ℝ := fun x => a * (x / c * (1 + (b * (x / c).log) ^ 2))⁻¹
l3 : ∀ (x : ℝ), 0 < x → HasDerivAt Real.log x⁻¹ x
l4 : ∀ (x : ℝ), HasDerivAt (fun t => t / c) (1 / c) x
l2 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun t => (t / c).log) x⁻¹ x
l5 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun y => b * (y / c).log) (b * x⁻¹) x
l1 : ∀ (x : ℝ), 0 < x → HasDerivAt (fun x => (b * (x / c).log).arctan) (1 / (1 + (b * (x / c).log) ^ 2) * (b * x⁻¹)) x
l6 : ∀ (x : ℝ), 0 < x → HasDerivAt g (g' x) x
key : ∀ (x : ℝ), 0 < x → HasDerivAt g₀ (g' x) x
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto (fun k => (b * (k / c).log).arctan) (𝓝[>] 0) (𝓝 (-(π / 2)))