Cauchy's Theorem and Complex Contour Integration

This file contains signatures and basic results for Cauchy's theorem and complex contour integration, particularly for applications to Gaussian integrals and the Riemann Hypothesis proof.

Main definitions and results

• contour_integral_independent_of_path: For holomorphic functions, the integral is independent of the path between two points
• cauchy_theorem_rectangle: Cauchy's theorem for rectangular contours
• horizontal_shift_invariance: Shifting integration by a purely imaginary constant doesn't change the value for rapidly decaying entire functions
• gaussian_contour_shift_general: General contour shift for Gaussian-like functions

Implementation notes

These are primarily signatures that will be needed for the full proof. The actual implementations require deep complex analysis theory.

theorem Frourio.rectangular_contour_conversion (f : ℂ → ℂ) (z₀ z₁ z₂ : ℂ) : (((∫ (x : ℝ) in z₀.re..z₁.re, f (↑x + ↑z₀.im * Complex.I)) + Complex.I • ∫ (y : ℝ) in z₀.im..z₂.im, f (↑z₁.re + ↑y * Complex.I)) + -∫ (x : ℝ) in z₀.re..z₁.re, f (↑x + ↑z₂.im * Complex.I)) + -Complex.I • ∫ (y : ℝ) in z₀.im..z₂.im, f (↑z₀.re + ↑y * Complex.I) = (((∫ (x : ℝ) in z₀.re..z₁.re, f (↑x + ↑z₀.im * Complex.I)) - ∫ (x : ℝ) in z₀.re..z₁.re, f (↑x + ↑z₂.im * Complex.I)) + Complex.I • ∫ (y : ℝ) in z₀.im..z₂.im, f (↑z₁.re + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in z₀.im..z₂.im, f (↑z₀.re + ↑y * Complex.I)

Equality of parameterized rectangular contour and standard interval representation. This lemma shows that the sum of parameterized integrals along a rectangular path equals the standard Cauchy integral representation.

theorem Frourio.complex_norm_add_mul_I (x y : ℝ) : ‖↑x + ↑y * Complex.I‖ = √(x ^ 2 + y ^ 2)

The norm of a complex number x + yi equals √(x² + y²).

theorem Frourio.integrable_of_gaussian_decay_horizontal {f : ℂ → ℂ} {y : ℝ} (hf_entire : ∀ (z : ℂ), DifferentiableAt ℂ f z) (hf_decay : ∃ (A : ℝ) (B : ℝ) (_ : 0 < A) (_ : 0 < B), ∀ (z : ℂ), ‖f z‖ ≤ A * Real.exp (-B * ‖z‖ ^ 2)) : MeasureTheory.Integrable (fun (x : ℝ) => f (↑x + ↑y * Complex.I)) MeasureTheory.volume

A function with Gaussian decay is integrable along any horizontal line in the complex plane.

theorem Frourio.cauchy_rectangle_formula {f : ℂ → ℂ} {R y₁ y₂ : ℝ} (hf_rect : DifferentiableOn ℂ f (Set.uIcc (-R) R ×ℂ Set.uIcc y₁ y₂)) : (∫ (x : ℝ) in -R..R, f (↑x + ↑y₁ * Complex.I)) - ∫ (x : ℝ) in -R..R, f (↑x + ↑y₂ * Complex.I) = -((Complex.I • ∫ (t : ℝ) in y₁..y₂, f (↑R + ↑t * Complex.I)) - Complex.I • ∫ (t : ℝ) in y₁..y₂, f (-↑R + ↑t * Complex.I))

theorem Frourio.contour_limit_theorem {f : ℂ → ℂ} {y₁ y₂ : ℝ} (hf_integrable_y1 : MeasureTheory.Integrable (fun (x : ℝ) => f (↑x + ↑y₁ * Complex.I)) MeasureTheory.volume) (hf_integrable_y2 : MeasureTheory.Integrable (fun (x : ℝ) => f (↑x + ↑y₂ * Complex.I)) MeasureTheory.volume) (h_vert_vanish : ∀ ε > 0, ∃ R₀ > 0, ∀ R ≥ R₀, ‖(Complex.I • ∫ (t : ℝ) in y₁..y₂, f (↑R + ↑t * Complex.I)) - Complex.I • ∫ (t : ℝ) in y₁..y₂, f (-↑R + ↑t * Complex.I)‖ < ε) (h_rect : ∀ R > 0, (∫ (x : ℝ) in -R..R, f (↑x + ↑y₁ * Complex.I)) - ∫ (x : ℝ) in -R..R, f (↑x + ↑y₂ * Complex.I) = -((Complex.I • ∫ (t : ℝ) in y₁..y₂, f (↑R + ↑t * Complex.I)) - Complex.I • ∫ (t : ℝ) in y₁..y₂, f (-↑R + ↑t * Complex.I))) : ∫ (x : ℝ), f (↑x + ↑y₁ * Complex.I) = ∫ (x : ℝ), f (↑x + ↑y₂ * Complex.I)

theorem Frourio.horizontal_contour_shift {f : ℂ → ℂ} {y₁ y₂ : ℝ} (hf_entire : ∀ (z : ℂ), DifferentiableAt ℂ f z) (hf_decay : ∃ (A : ℝ) (B : ℝ) (_ : 0 < A) (_ : 0 < B), ∀ (z : ℂ), ‖f z‖ ≤ A * Real.exp (-B * ‖z‖ ^ 2)) : ∫ (x : ℝ), f (↑x + ↑y₁ * Complex.I) = ∫ (x : ℝ), f (↑x + ↑y₂ * Complex.I)

For entire functions with Gaussian decay, the integral over any horizontal line has the same value. The decay condition automatically ensures integrability.