let g' (x : ℝ) := a * (x / c * (1 + (b * Real.log (x / c)) ^ 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
⊢ 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 * π
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))⁻¹
⊢ 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 * π