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
k1 : Tendsto g₀ atTop (𝓝 (a * c / b * (π / 2)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
⊢ ContinuousWithinAt g₀ (Ici 0) 0
Tactic:
rw [Metric.continuousWithinAt_iff]
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)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
⊢ ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ici 0 → dist x 0 < δ → dist (g₀ x) (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)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
⊢ ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ici 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
Tactic:
rw [Metric.tendsto_nhdsWithin_nhds] at k2
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)))
k2 : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
⊢ ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ici 0 → dist x 0 < δ → dist (g₀ x) (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)))
k2 : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
⊢ ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ici 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
Tactic:
peel k2 with ε hε δ hδ x h
Proof state after:
case h.h.h.h.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)))
k2 : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ : δ > 0
x : ℝ
h : x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
⊢ x ∈ Ici 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
Theorem: hh_integrable_aux
Proof state before:
case h.h.h.h.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)))
k2 : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ : δ > 0
x : ℝ
h : x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
⊢ x ∈ Ici 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
Tactic:
intro (hx : 0 ≤ x)
Proof state after:
case h.h.h.h.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)))
k2 : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ : δ > 0
x : ℝ
h : x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
hx : 0 ≤ x
⊢ dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
Theorem: hh_integrable_aux
Proof state before:
case h.h.h.h.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)))
k2 : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ : δ > 0
x : ℝ
h : x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
hx : 0 ≤ x
⊢ dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
Tactic:
have := le_iff_lt_or_eq.mp hx
Proof state after:
case h.h.h.h.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)))
k2 : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ : δ > 0
x : ℝ
h : x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
hx : 0 ≤ x
this : 0 < x ∨ 0 = x
⊢ dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
Theorem: hh_integrable_aux
Proof state before:
case h.h.h.h.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)))
k2 : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ : δ > 0
x : ℝ
h : x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
hx : 0 ≤ x
this : 0 < x ∨ 0 = x
⊢ dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
Tactic:
cases this with
| inl hx => exact h hx
| inr hx => simp [g₀, hx.symm, hε]
Proof state after:
no goals
Theorem: hh_integrable_aux
Proof state before:
case h.h.h.h.h.inl
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)))
k2 : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ : δ > 0
x : ℝ
h : x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
hx✝ : 0 ≤ x
hx : 0 < x
⊢ dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
Tactic:
exact h hx
Proof state after:
no goals
Theorem: hh_integrable_aux
Proof state before:
case h.h.h.h.h.inr
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)))
k2 : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
ε : ℝ
hε : ε > 0
δ : ℝ
hδ : δ > 0
x : ℝ
h : x ∈ Ioi 0 → dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
hx✝ : 0 ≤ x
hx : 0 = x
⊢ dist x 0 < δ → dist (g₀ x) (g₀ 0) < ε
Tactic:
simp [g₀, hx.symm, hε]
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)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
⊢ ∀ x ∈ Ioi 0, 0 ≤ 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)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
x : ℝ
hx : 0 < x
⊢ 0 ≤ 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)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
x : ℝ
hx : 0 < x
⊢ 0 ≤ g' x
Tactic:
simp [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)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
x : ℝ
hx : 0 < x
⊢ 0 ≤ a * ((1 + (b * (x / c).log) ^ 2)⁻¹ * (c / 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)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
x : ℝ
hx : 0 < x
⊢ 0 ≤ a * ((1 + (b * (x / c).log) ^ 2)⁻¹ * (c / x))
Tactic:
positivity
Proof state after:
no goals
Theorem: hh_integrable_aux
Proof state before:
case left
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)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
k4 : ∀ x ∈ Ioi 0, 0 ≤ g' x
⊢ IntegrableOn (fun t => a * (t / c * (1 + (b * (t / c).log) ^ 2))⁻¹) (Ioi 0) volume
Tactic:
convert_to IntegrableOn g' _
Proof state after:
case left.convert_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)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
k4 : ∀ x ∈ Ioi 0, 0 ≤ g' x
⊢ IntegrableOn g' (Ioi 0) volume
Theorem: hh_integrable_aux
Proof state before:
case left.convert_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)))
k2 : Tendsto g₀ (𝓝[>] 0) (𝓝 (g₀ 0))
k3 : ContinuousWithinAt g₀ (Ici 0) 0
k4 : ∀ x ∈ Ioi 0, 0 ≤ g' x
⊢ IntegrableOn g' (Ioi 0) volume
Tactic:
exact integrableOn_Ioi_deriv_of_nonneg k3 key k4 k1
Proof state after:
no goals