theorem integrable_bessel (x1 x2 : ℝ) : MeasureTheory.IntegrableOn (fun (p : ℝ × ℝ) => (1 - Real.cos (x1 * p.1 * Real.cos (p.2 - x2))) / p.1) (Set.Ioc 0 1 ×ˢ Set.Ioo (-Real.pi) Real.pi) (MeasureTheory.volume.prod MeasureTheory.volume)

Integrability related to Bessel function.

theorem integrable_bessel_slice (x1 x2 : ℝ) : MeasureTheory.IntegrableOn (fun (r : ℝ) => ∫ (θ : ℝ) in Set.Ioo (-Real.pi) Real.pi, (1 - Real.cos (x1 * r * Real.cos (θ - x2))) / r) (Set.Ioc 0 1) MeasureTheory.volume

theorem intervalIntegrable_bessel_slice {x : ℝ} (hx : 0 < x) : IntervalIntegrable (fun (r : ℝ) => ∫ (θ : ℝ) in Set.Ioo (-Real.pi) Real.pi, (1 - Real.cos (r * Real.cos θ)) / r) MeasureTheory.volume 0 x

theorem intervalIntegrable_bessel_slice' {x : ℝ} (hx : 0 < x) : IntervalIntegrable (fun (r : ℝ) => ∫ (θ : ℝ) in -Real.pi..Real.pi, (1 - Real.cos (r * Real.cos θ)) / r) MeasureTheory.volume 0 x

theorem besselJ_bound {r : ℝ} (hr : 1 ≤ r) : |∫ (θ : ℝ) in -Real.pi..Real.pi, Real.cos (r * Real.cos θ)| ≤ (4 + 4 * Real.pi) / √r

theorem asymptotic_bessel : (fun (x : ℝ) => ((2 * Real.pi)⁻¹ * ∫ (r : ℝ) in 0..x, ∫ (θ : ℝ) in -Real.pi..Real.pi, (1 - Real.cos (r * Real.cos θ)) / r) - Real.log x) =O[Filter.atTop] 1