internlm/Lean-Github huggingface dataset:
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
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto (fun k => (b * (k / c).log).arctan) (𝓝[>] 0) (𝓝 (-(π / 2)))
Tactic:
apply (tendsto_arctan_atBot.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
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto (fun k => b * (k / c).log) (𝓝[>] 0) atBot
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
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto (fun k => b * (k / c).log) (𝓝[>] 0) atBot
Tactic:
apply Tendsto.const_mul_atBot 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
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto (fun x => (x / c).log) (𝓝[>] 0) atBot
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
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto (fun x => (x / c).log) (𝓝[>] 0) atBot
Tactic:
apply tendsto_log_nhdsWithin_zero_right.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
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto (fun x => x / c) (𝓝[>] 0) (𝓝[>] 0)
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
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ Tendsto (fun x => x / c) (𝓝[>] 0) (𝓝[>] 0)
Tactic:
rw [Metric.tendsto_nhdsWithin_nhdsWithin]
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₀
⊢ ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → x / c ∈ Ioi 0 ∧ dist (x / c) 0 < ε
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
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
⊢ ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → x / c ∈ Ioi 0 ∧ dist (x / c) 0 < ε
Tactic:
intro ε hε
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₀
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → x / c ∈ Ioi 0 ∧ dist (x / c) 0 < ε
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
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
this : g =ᶠ[𝓝[>] 0] g₀
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → x / c ∈ Ioi 0 ∧ dist (x / c) 0 < ε
Tactic:
refine ⟨c * ε, by positivity, fun hx1 hx2 => ⟨?_, ?_⟩⟩
Proof state after:
case h.refine_1
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₀
ε : ℝ
hε : ε > 0
x✝ : ℝ
hx1 : x✝ ∈ Ioi 0
hx2 : dist x✝ 0 < c * ε
⊢ x✝ / c ∈ Ioi 0

case h.refine_2
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₀
ε : ℝ
hε : ε > 0
x✝ : ℝ
hx1 : x✝ ∈ Ioi 0
hx2 : dist x✝ 0 < c * ε
⊢ dist (x✝ / c) 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)))
⊢ g =ᶠ[𝓝[>] 0] g₀
Tactic:
apply eventually_of_mem self_mem_nhdsWithin
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)))
⊢ ∀ 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
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
⊢ ∀ x ∈ Ioi 0, g x = g₀ x
Tactic:
intro x (hx : 0 < x)
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)))
x : ℝ
hx : 0 < x
⊢ 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
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
x : ℝ
hx : 0 < x
⊢ g x = g₀ x
Tactic:
simp [g₀, hx.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)))
this : g =ᶠ[𝓝[>] 0] g₀
ε : ℝ
hε : ε > 0
⊢ c * ε > 0
Tactic:
positivity
Proof state after:
no goals
Theorem: hh_integrable_aux
Proof state before:
case h.refine_1
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₀
ε : ℝ
hε : ε > 0
x✝ : ℝ
hx1 : x✝ ∈ Ioi 0
hx2 : dist x✝ 0 < c * ε
⊢ x✝ / c ∈ Ioi 0
Tactic:
simp at hx1 ⊢
Proof state after:
case h.refine_1
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₀
ε : ℝ
hε : ε > 0
x✝ : ℝ
hx2 : dist x✝ 0 < c * ε
hx1 : 0 < x✝
⊢ 0 < x✝ / c
Theorem: hh_integrable_aux
Proof state before:
case h.refine_1
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₀
ε : ℝ
hε : ε > 0
x✝ : ℝ
hx2 : dist x✝ 0 < c * ε
hx1 : 0 < x✝
⊢ 0 < x✝ / c
Tactic:
positivity
Proof state after:
no goals
Theorem: hh_integrable_aux
Proof state before:
case h.refine_2
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₀
ε : ℝ
hε : ε > 0
x✝ : ℝ
hx1 : x✝ ∈ Ioi 0
hx2 : dist x✝ 0 < c * ε
⊢ dist (x✝ / c) 0 < ε
Tactic:
simp [abs_eq_self.mpr hc.le] at hx2 ⊢
Proof state after:
case h.refine_2
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₀
ε : ℝ
hε : ε > 0
x✝ : ℝ
hx1 : x✝ ∈ Ioi 0
hx2 : |x✝| < c * ε
⊢ |x✝| / c < ε
Theorem: hh_integrable_aux
Proof state before:
case h.refine_2
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₀
ε : ℝ
hε : ε > 0
x✝ : ℝ
hx1 : x✝ ∈ Ioi 0
hx2 : |x✝| < c * ε
⊢ |x✝| / c < ε
Tactic:
rwa [div_lt_iff hc, mul_comm]
Proof state after:
no goals