Complex integrands Φ₁'–Φ₆' are holomorphic on the upper half-plane

In this file, we prove that all the complex integrands Φ₁' through Φ₆' that appear in our integrals I₁-I₆ are holomorphic on the upper half-plane.

Main Results:

This file includes the following (families of) theorems:

• [PROVED] Φⱼ'_holo: For j = 1…6, Φⱼ' is Complex-differentiable on the upper half-plane.
• [PROVED] Φⱼ'_contDiffOn_ℂ: For j = 1…6, Φⱼ' is Complex-smooth on the upper half-plane.
• [TODO] Φⱼ'_contDiffOn: For j = 1…6, Φⱼ' is Real-smooth on the upper half-plane.
• [TODO] φ₀''_holo: φ₀'' is Complex-differentiable on the upper half-plane.

theorem UpperHalfPlane.range_upperHalfPlane_coe : Set.range UpperHalfPlane.coe = upperHalfPlaneSet

theorem UpperHalfPlane.zero_not_mem_upperHalfPlaneSet : 0 ∉ upperHalfPlaneSet

Complex Differentiability

theorem MagicFunction.a.ComplexIntegrands.φ₀''_holo : DifferentiableOn ℂ φ₀'' UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₁'_holo {r : ℝ} : DifferentiableOn ℂ (Φ₁' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₁'_contDiffOn_ℂ {r : ℝ} : ContDiffOn ℂ (↑⊤) (Φ₁' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₂'_holo {r : ℝ} : DifferentiableOn ℂ (Φ₂' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₂'_contDiffOn_ℂ {r : ℝ} : ContDiffOn ℂ (↑⊤) (Φ₂' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₃'_holo {r : ℝ} : DifferentiableOn ℂ (Φ₃' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₃'_contDiffOn_ℂ {r : ℝ} : ContDiffOn ℂ (↑⊤) (Φ₃' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₄'_holo {r : ℝ} : DifferentiableOn ℂ (Φ₄' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₄'_contDiffOn_ℂ {r : ℝ} : ContDiffOn ℂ (↑⊤) (Φ₄' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₅'_holo {r : ℝ} : DifferentiableOn ℂ (Φ₅' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₅'_contDiffOn_ℂ {r : ℝ} : ContDiffOn ℂ (↑⊤) (Φ₅' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₆'_holo {r : ℝ} : DifferentiableOn ℂ (Φ₆' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₆'_contDiffOn_ℂ {r : ℝ} : ContDiffOn ℂ (↑⊤) (Φ₆' r) UpperHalfPlane.upperHalfPlaneSet

Real Differentiability

theorem MagicFunction.a.ComplexIntegrands.Φ₁'_contDiffOn {r : ℝ} : ContDiffOn ℝ (↑⊤) (Φ₁' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₂'_contDiffOn {r : ℝ} : ContDiffOn ℝ (↑⊤) (Φ₂' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₃'_contDiffOn {r : ℝ} : ContDiffOn ℝ (↑⊤) (Φ₃' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₄'_contDiffOn {r : ℝ} : ContDiffOn ℝ (↑⊤) (Φ₄' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₅'_contDiffOn {r : ℝ} : ContDiffOn ℝ (↑⊤) (Φ₅' r) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.a.ComplexIntegrands.Φ₆'_contDiffOn {r : ℝ} : ContDiffOn ℝ (↑⊤) (Φ₆' r) UpperHalfPlane.upperHalfPlaneSet