Cauchy Principal Value Theory

Theory of Cauchy principal value integrals for piecewise C¹ contour integration. The principal value approach allows contours to pass through singularities.

theorem cauchyPrincipalValueIntegrand_bounded (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (ε : ℝ) (_hε : 0 < ε) (hf_cont : ContinuousOn f (γ '' Set.Icc a b \ Metric.ball z₀ ε)) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hγ'_cont : ContinuousOn (deriv γ) (Set.Icc a b)) : ∃ (M : ℝ), ∀ t ∈ Set.Icc a b, ‖cauchyPrincipalValueIntegrand' f γ z₀ ε t‖ ≤ M

theorem measurableSet_pv_support (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (ε : ℝ) (hγ_cont : ContinuousOn γ (Set.Icc a b)) : MeasurableSet ({t : ℝ | ε < ‖γ t - z₀‖} ∩ Set.Icc a b)

theorem continuousOn_pv_base (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (ε : ℝ) (hf_cont : ContinuousOn f (γ '' Set.Icc a b \ Metric.ball z₀ ε)) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hγ'_cont : ContinuousOn (deriv γ) (Set.Icc a b)) : ContinuousOn (fun (t : ℝ) => f (γ t) * deriv γ t) ({t : ℝ | ε < ‖γ t - z₀‖} ∩ Set.Icc a b)

theorem limUnder_eventually_eq {α : Type u_1} [TopologicalSpace α] [Nonempty α] {f g : ℝ → α} {l : Filter ℝ} [l.NeBot] (h : ∀ᶠ (x : ℝ) in l, f x = g x) : l.limUnder f = l.limUnder g

If f =ᶠ g along a filter, their limUnder values agree.

theorem cauchyPrincipalValueIntegrand_integrable (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (ε : ℝ) (hε : 0 < ε) (hab : a < b) (hf_cont : ContinuousOn f (γ '' Set.Icc a b \ Metric.ball z₀ ε)) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hγ'_cont : ContinuousOn (deriv γ) (Set.Icc a b)) : IntervalIntegrable (cauchyPrincipalValueIntegrand' f γ z₀ ε) MeasureTheory.volume a b

theorem cauchyPrincipalValue_of_dominated (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (hab : a < b) (M : ℝ) (_hM : 0 < M) (h_bound : ∀ ε > 0, ∀ t ∈ Set.Icc a b, ‖cauchyPrincipalValueIntegrand' f γ z₀ ε t‖ ≤ M) (h_ae_limit : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), ∃ (L : ℂ), Filter.Tendsto (fun (ε : ℝ) => cauchyPrincipalValueIntegrand' f γ z₀ ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds L)) (hF_meas : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), MeasureTheory.AEStronglyMeasurable (cauchyPrincipalValueIntegrand' f γ z₀ ε) (MeasureTheory.volume.restrict (Set.uIoc a b))) : CauchyPrincipalValueExists' f γ a b z₀

Dominated convergence for principal value integrals.

theorem cauchyPrincipalValueExists_of_continuous (g : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (hab : a < b) (hg : ContinuousOn g (γ '' Set.Icc a b)) (hγ : ContinuousOn γ (Set.Icc a b)) (hγ' : ContinuousOn (deriv γ) (Set.Icc a b)) : CauchyPrincipalValueExists' g γ a b z₀

PV exists for continuous integrands on C¹ curves.

theorem cauchyPrincipalValueExists_of_singular_inv (γ : PiecewiseC1Immersion) (z₀ : ℂ) (h_crossing_cauchy : (∃ t ∈ Set.Icc γ.a γ.b, γ.toFun t = z₀) → Cauchy (Filter.map (fun (ε : ℝ) => ∫ (t : ℝ) in γ.a..γ.b, if ε < ‖γ.toFun t - z₀‖ then (γ.toFun t - z₀)⁻¹ * deriv γ.toFun t else 0) (nhdsWithin 0 (Set.Ioi 0)))) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - z₀)⁻¹) γ.toFun γ.a γ.b z₀

PV exists for singular 1/(z-z₀) integrands on C¹ immersions.

theorem uniform_avoidance_on_compact (γ : ℝ → ℂ) (K : Set ℝ) (z₀ : ℂ) (hK_compact : IsCompact K) (hK_nonempty : K.Nonempty) (hγ_cont : ContinuousOn γ K) (h_avoid : ∀ t ∈ K, γ t ≠ z₀) : ∃ δ > 0, ∀ t ∈ K, δ ≤ ‖γ t - z₀‖

Uniform avoidance on compact sets.