Smoothness

In this file, we prove that the integrands of all of the REAL integrals making up a are smooth. That is, we translate the complex holomorphicity results into smoothness results by showing first that the parametrisations are smooth and then composing them with the holomorphicity proofs to conclude that the composition of the complex integrands with the parametrisations are smooth real functions.

theorem MagicFunction.Parametrisations.z₁'_contDiffOn : ContDiffOn ℝ (↑⊤) z₁' (Set.Ioc 0 1)

theorem MagicFunction.Parametrisations.z₂'_contDiffOn : ContDiffOn ℝ (↑⊤) z₂' (Set.Icc 0 1)

theorem MagicFunction.Parametrisations.z₃'_contDiffOn : ContDiffOn ℝ (↑⊤) z₃' (Set.Ioc 0 1)

theorem MagicFunction.Parametrisations.z₄'_contDiffOn : ContDiffOn ℝ (↑⊤) z₄' (Set.Icc 0 1)

theorem MagicFunction.Parametrisations.z₅'_contDiffOn : ContDiffOn ℝ (↑⊤) z₅' (Set.Ioc 0 1)

theorem MagicFunction.Parametrisations.z₆'_contDiffOn : ContDiffOn ℝ (↑⊤) z₆' (Set.Ici 1)

theorem MagicFunction.a.RealIntegrands.Φ₁_contDiffOn {r : ℝ} : ContDiffOn ℝ (↑⊤) (Φ₁ r) (Set.Ioc 0 1)

theorem MagicFunction.a.RealIntegrands.Φ₂_contDiffOn {r : ℝ} : ContDiffOn ℝ (↑⊤) (Φ₂ r) (Set.Icc 0 1)

theorem MagicFunction.a.RealIntegrands.Φ₃_contDiffOn {r : ℝ} : ContDiffOn ℝ (↑⊤) (Φ₃ r) (Set.Ioc 0 1)

theorem MagicFunction.a.RealIntegrands.Φ₄_contDiffOn {r : ℝ} : ContDiffOn ℝ (↑⊤) (Φ₄ r) (Set.Icc 0 1)

theorem MagicFunction.a.RealIntegrands.Φ₅_contDiffOn {r : ℝ} : ContDiffOn ℝ (↑⊤) (Φ₅ r) (Set.Ioc 0 1)

theorem MagicFunction.a.RealIntegrands.Φ₆_contDiffOn {r : ℝ} : ContDiffOn ℝ (↑⊤) (Φ₆ r) (Set.Ici 1)