Integrability

In this file, we prove that the integrands Φⱼ are integrable.

theorem MagicFunction.a.Integrability.Φ₁_integrableOn {r : ℝ} (hr : r ≥ 0) : MeasureTheory.IntegrableOn (RealIntegrands.Φ₁ r) (Set.Ioc 0 1) MeasureTheory.volume

theorem MagicFunction.a.Integrability.Φ₂_integrableOn {r : ℝ} (hr : r ≥ 0) : MeasureTheory.IntegrableOn (RealIntegrands.Φ₂ r) (Set.Icc 0 1) MeasureTheory.volume

theorem MagicFunction.a.Integrability.Φ₃_integrableOn {r : ℝ} (hr : r ≥ 0) : MeasureTheory.IntegrableOn (RealIntegrands.Φ₃ r) (Set.Ioc 0 1) MeasureTheory.volume

theorem MagicFunction.a.Integrability.Φ₄_integrableOn {r : ℝ} (hr : r ≥ 0) : MeasureTheory.IntegrableOn (RealIntegrands.Φ₄ r) (Set.Icc 0 1) MeasureTheory.volume

theorem MagicFunction.a.Integrability.Φ₅_integrableOn {r : ℝ} (hr : r ≥ 0) : MeasureTheory.IntegrableOn (RealIntegrands.Φ₅ r) (Set.Ioc 0 1) MeasureTheory.volume

theorem MagicFunction.a.Integrability.Φ₆_integrableOn {r : ℝ} (hr : r ≥ 0) : MeasureTheory.IntegrableOn (RealIntegrands.Φ₆ r) (Set.Ici 1) MeasureTheory.volume