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

• Φⱼ'_holo: For j = 1…6, Φⱼ' is Complex-differentiable on the upper half-plane.
• Φⱼ'_contDiffOn_ℂ: For j = 1…6, Φⱼ' is Complex-smooth on the upper half-plane.
• Φⱼ'_contDiffOn: For j = 1…6, Φⱼ' is Real-smooth on the upper half-plane.
• φ₀''_holo: φ₀'' is Complex-differentiable on the upper half-plane.
• φ₀''_differentiable: φ₀'' is differentiable on Set.univ ×ℂ Ioi 0.
• φ₀''_continuous: φ₀'' is continuous on the upper half-plane.
• φ₀_continuous: φ₀ : ℍ → ℂ is continuous.

theorem UpperHalfPlane.zero_not_mem_upperHalfPlaneSet : 0 ∉ upperHalfPlaneSet

Complex Differentiability

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

theorem MagicFunction.a.ComplexIntegrands.φ₀''_neg_inv_add_holo {c : ℂ} (hc : c.im = 0) : DifferentiableOn ℂ (fun (z : ℂ) => φ₀'' (-1 / (z + c))) UpperHalfPlane.upperHalfPlaneSet

For a real shift c, z ↦ φ₀''(-1/(z+c)) is holomorphic on ℍ₀: φ₀'' is holomorphic on ℍ₀ and z ↦ -1/(z+c) maps ℍ₀ into ℍ₀ (neg_inv_add_mapsto).

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

Corollaries using alternative set notation

theorem MagicFunction.a.ComplexIntegrands.φ₀''_differentiable : DifferentiableOn ℂ φ₀'' (Set.univ ×ℂ Set.Ioi 0)

φ₀'' is holomorphic on the upper half-plane (using Set.univ ×ℂ Ioi 0 notation). This is equivalent to φ₀''_holo since Set.univ ×ℂ Ioi 0 = ℍ₀.

theorem MagicFunction.a.ComplexIntegrands.φ₀''_continuous : ContinuousOn φ₀'' (Set.univ ×ℂ Set.Ioi 0)

φ₀'' is continuous on the upper half-plane.

theorem MagicFunction.a.ComplexIntegrands.φ₀_continuous : Continuous φ₀

φ₀ : ℍ → ℂ is continuous. Follows from φ₀''_holo.