Basic Definitions for Complex Analysis with Principal Values

Core definitions for piecewise C¹ curves, Cauchy principal value integrals, and generalized winding numbers following Hungerbühler–Wasem.

structure PiecewiseC1Curve : Type

A piecewise continuously differentiable curve γ : [a,b] → ℂ. The curve is C¹ on each subinterval between partition points.

• toFun : ℝ → ℂ

  The underlying parametrization of the curve.

• a : ℝ

  The left endpoint of the parameter interval.

• b : ℝ

  The right endpoint of the parameter interval.

• hab : self.a < self.b
• partition : Finset ℝ

  The finite set of partition points subdividing [a, b].

• partition_subset : ↑self.partition ⊆ Set.Icc self.a self.b
• endpoints_in_partition : self.a ∈ self.partition ∧ self.b ∈ self.partition
• continuous_toFun : ContinuousOn self.toFun (Set.Icc self.a self.b)
• smooth_off_partition (t : ℝ) : t ∈ Set.Icc self.a self.b → t ∉ self.partition → DifferentiableAt ℝ self.toFun t
• deriv_continuous_off_partition (t : ℝ) : t ∈ Set.Ioo self.a self.b → t ∉ self.partition → ContinuousAt (deriv self.toFun) t

@[instance_reducible]

instance instCoeFunPiecewiseC1CurveForallRealComplex : CoeFun PiecewiseC1Curve fun (x : PiecewiseC1Curve) => ℝ → ℂ

Equations

• instCoeFunPiecewiseC1CurveForallRealComplex = { coe := PiecewiseC1Curve.toFun }

def PiecewiseC1Curve.IsClosed (γ : PiecewiseC1Curve) : Prop

A closed curve has γ(a) = γ(b).

Equations

• γ.IsClosed = (γ.toFun γ.a = γ.toFun γ.b)

structure PiecewiseC1Immersionextends PiecewiseC1Curve : Type

A piecewise C¹ immersion: a piecewise C¹ curve with nonzero derivative.

• toFun : ℝ → ℂ
• a : ℝ
• b : ℝ
• hab : self.a < self.b
• partition : Finset ℝ
• partition_subset : ↑self.partition ⊆ Set.Icc self.a self.b
• endpoints_in_partition : self.a ∈ self.partition ∧ self.b ∈ self.partition
• continuous_toFun : ContinuousOn self.toFun (Set.Icc self.a self.b)
• smooth_off_partition (t : ℝ) : t ∈ Set.Icc self.a self.b → t ∉ self.partition → DifferentiableAt ℝ self.toFun t
• deriv_continuous_off_partition (t : ℝ) : t ∈ Set.Ioo self.a self.b → t ∉ self.partition → ContinuousAt (deriv self.toFun) t
• deriv_ne_zero (t : ℝ) : t ∈ Set.Icc self.a self.b → t ∉ self.partition → deriv self.toFun t ≠ 0
• left_deriv_limit (p : ℝ) : p ∈ self.partition → self.a < p → ∃ (L : ℂ), L ≠ 0 ∧ Filter.Tendsto (deriv self.toFun) (nhdsWithin p (Set.Iio p)) (nhds L)
• right_deriv_limit (p : ℝ) : p ∈ self.partition → p < self.b → ∃ (L : ℂ), L ≠ 0 ∧ Filter.Tendsto (deriv self.toFun) (nhdsWithin p (Set.Ioi p)) (nhds L)

noncomputable def cauchyPrincipalValueIntegrand' (f : ℂ → ℂ) (γ : ℝ → ℂ) (z₀ : ℂ) (ε t : ℝ) : ℂ

The Cauchy principal value integrand at cutoff ε.

Equations

• cauchyPrincipalValueIntegrand' f γ z₀ ε t = if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0

@[simp]

theorem cauchyPrincipalValueIntegrand'_of_gt {f : ℂ → ℂ} {γ : ℝ → ℂ} {z₀ : ℂ} {ε t : ℝ} (h : ε < ‖γ t - z₀‖) : cauchyPrincipalValueIntegrand' f γ z₀ ε t = f (γ t) * deriv γ t

@[simp]

theorem cauchyPrincipalValueIntegrand'_of_le {f : ℂ → ℂ} {γ : ℝ → ℂ} {z₀ : ℂ} {ε t : ℝ} (h : ‖γ t - z₀‖ ≤ ε) : cauchyPrincipalValueIntegrand' f γ z₀ ε t = 0

noncomputable def cauchyPrincipalValue' (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) : ℂ

The Cauchy principal value of ∮_γ f(z) dz, excluding ε-neighborhoods of z₀.

Equations

• cauchyPrincipalValue' f γ a b z₀ = (nhdsWithin 0 (Set.Ioi 0)).limUnder fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0

def CauchyPrincipalValueExists' (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) : Prop

The Cauchy principal value exists if the limit exists.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def generalizedWindingNumber' (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) : ℂ

The generalized winding number of γ around z₀, defined via principal value. n_{z₀}(γ) = (1/2πi) · PV ∮_γ dz/(z - z₀).

Equations

• generalizedWindingNumber' γ a b z₀ = (2 * ↑Real.pi * Complex.I)⁻¹ * cauchyPrincipalValue' (fun (x : ℂ) => x⁻¹) (fun (t : ℝ) => γ t - z₀) a b 0

def CurvesHomotopic (Γ γ : ℝ → ℂ) (a b : ℝ) : Prop

Two curves are homotopic relative to endpoints.

Equations

• One or more equations did not get rendered due to their size.

def CurvesHomotopicAvoiding (Γ γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) : Prop

Homotopy avoiding a point z₀.

Equations

• One or more equations did not get rendered due to their size.

theorem intervalIntegrable_of_piecewise_continuousOn_bounded {f : ℝ → ℂ} {a b : ℝ} {P : Finset ℝ} (M : ℝ) (hab : a ≤ b) (hf_cont : ContinuousOn f (Set.Icc a b \ ↑P)) (hf_bound : ∀ t ∈ Set.Icc a b, ‖f t‖ ≤ M) : IntervalIntegrable f MeasureTheory.volume a b

A piecewise continuous bounded function is interval integrable.

theorem hasDerivWithinAt_zero_of_deriv_zero_off_finite {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (a b : ℝ) (P : Finset ℝ) (_hab : a < b) (hf_cont : ContinuousOn f (Set.Icc a b)) (hf_diff : ∀ t ∈ Set.Ioo a b, t ∉ P → DifferentiableAt ℝ f t) (hf_deriv_zero : ∀ t ∈ Set.Ioo a b, t ∉ P → deriv f t = 0) (t : ℝ) : t ∈ Set.Ico a b → HasDerivWithinAt f 0 (Set.Ici t) t

If f is continuous on [a,b], differentiable on (a,b)\P with f'=0 there, then f has zero right derivative at every point of [a,b).

theorem continuousWithinAt_integral_of_dominated_piecewise {X : Type u_1} [TopologicalSpace X] [FirstCountableTopology X] {F : X → ℝ → ℂ} {x₀ : X} {a b : ℝ} {S : Set X} {M : ℝ} (hab : a ≤ b) (hF_meas : ∀ x ∈ S, MeasureTheory.AEStronglyMeasurable (F x) (MeasureTheory.volume.restrict (Set.Icc a b))) (hF_bound : ∀ x ∈ S, ∀ t ∈ Set.Icc a b, ‖F x t‖ ≤ M) (hF_cont : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), ContinuousWithinAt (fun (x : X) => F x t) S x₀) : ContinuousWithinAt (fun (x : X) => ∫ (t : ℝ) in a..b, F x t) S x₀