On-Curve Principal Value: General Infrastructure

General PV convergence machinery for piecewise C¹ curves: dyadic PV limits, measurability of cutout integrands, arc angle injectivity, CPV avoidance and concatenation lemmas. These results work for arbitrary curves and functions.

theorem pv_limit_via_dyadic {γ : ℝ → ℂ} {a b t₀ : ℝ} {L : ℂ} (hat₀ : t₀ ∈ Set.Ioo a b) (hL : L ≠ 0) (hγ_C2 : ContDiffAt ℝ 2 γ t₀) (hγ_deriv : deriv γ t₀ = L) (hγ_cont_deriv : ContinuousOn (deriv γ) (Set.Icc a b)) (hγ_meas : Measurable γ) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (h_inj : ∀ t ∈ Set.Icc a b, γ t = γ t₀ → t = t₀) : ∃ (limit : ℂ), Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ε < ‖γ t - γ t₀‖ then (γ t - γ t₀)⁻¹ * deriv γ t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds limit)

theorem measurableSet_norm_gt_of_continuousOn {f : ℝ → ℂ} {s : Set ℝ} (ε : ℝ) (hf : ContinuousOn f s) (hs : MeasurableSet s) : MeasurableSet ({t : ℝ | ε < ‖f t‖} ∩ s)

theorem measurableSet_norm_gt_Icc {f : ℝ → ℂ} {a b : ℝ} (ε : ℝ) (hf : ContinuousOn f (Set.Icc a b)) : MeasurableSet ({t : ℝ | ε < ‖f t‖} ∩ Set.Icc a b)

theorem aEStronglyMeasurable_pv_integrand_piecewiseC1 {f : ℂ → ℂ} {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} {ε : ℝ} {P : Finset ℝ} (hf : ContinuousOn f (γ '' Set.Icc a b \ Metric.ball z₀ ε)) (hγ : ContinuousOn γ (Set.Icc a b)) (hγ'_off_P : ContinuousOn (deriv γ) (Set.Icc a b \ ↑P)) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => if ε < ‖γ t - z₀‖ then f (γ t) * deriv γ t else 0) (MeasureTheory.volume.restrict (Set.Icc a b))

theorem indicator_integrand_deriv_eq (γ : ℝ → ℂ) (c : ℂ) (ε t : ℝ) : (if ‖γ t - c‖ > ε then (γ t - c)⁻¹ * deriv (fun (s : ℝ) => γ s - c) t else 0) = if ‖γ t - c‖ > ε then (γ t - c)⁻¹ * deriv γ t else 0

theorem cpv_exists_from_shifted_tendsto (γ : ℝ → ℂ) (a b : ℝ) (c L : ℂ) (h : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ‖γ t - c‖ > ε then (γ t - c)⁻¹ * deriv (fun (s : ℝ) => γ s - c) t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds L)) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - c)⁻¹) γ a b c

theorem arc_angle_injective {t t' : ℝ} (ht : t ∈ Set.Ioo 1 3) (ht' : t' ∈ Set.Ioo 1 3) (h_eq : Complex.exp (↑(Real.pi * (1 + t) / 6) * Complex.I) = Complex.exp (↑(Real.pi * (1 + t') / 6) * Complex.I)) : t = t'

theorem cpv_avoidance (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (h_cont : ContinuousOn γ (Set.Icc a b)) (hab : a ≤ b) (h_avoid : ∀ t ∈ Set.Icc a b, γ t ≠ z₀) : CauchyPrincipalValueExists' f γ a b z₀

CPV trivially exists when the curve avoids z₀ on [a, b].

theorem cpv_concat (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b c : ℝ) (z₀ : ℂ) (h_ab : CauchyPrincipalValueExists' f γ a b z₀) (h_bc : CauchyPrincipalValueExists' f γ b c z₀) (hab : a ≤ b) (hbc : b ≤ c) (h_int : ∀ ε > 0, IntervalIntegrable (fun (t : ℝ) => if ε < ‖γ t - z₀‖ then f (γ t) * deriv γ t else 0) MeasureTheory.volume a c) : CauchyPrincipalValueExists' f γ a c z₀

CPV on adjacent intervals can be concatenated (when a ≤ b ≤ c).