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
k4 : ∀ x ∈ Ioi 0, 0 ≤ g' x
⊢ IntegrableOn (fun t => a * (t / c * (1 + (b * (t / c).log) ^ 2))⁻¹) (Ioi 0) volume ∧
    ∫ (t : ℝ) in Ioi 0, a * (t / c * (1 + (b * (t / c).log) ^ 2))⁻¹ = a * c / b * π
Tactic:
constructor
Proof state after:
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

case right
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
⊢ ∫ (t : ℝ) in Ioi 0, a * (t / c * (1 + (b * (t / c).log) ^ 2))⁻¹ = a * c / b * π