Multi-point Principal Value Infrastructure

Lemmas for multi-point Cauchy principal values: minimum separation, disjoint balls, boundedness, integrability, measurability, and the dominated convergence argument for decomposing multi-point PVs into sums of single-point PVs.

Main Results

• finset_discrete_min_sep — positive minimum separation in a finite set
• disjoint_balls_of_small_epsilon — disjoint balls for small ε
• dominated_convergence_multipoint_helper — dominated convergence for multi-point PV decomposition
• multipointPV_diff_tendsto — difference integrand converges
• multipointPV_eq_sum_of_integral_zero — multi-point PV equals sum of single-point PVs when regular integral vanishes

Measurability Infrastructure

theorem aEStronglyMeasurable_of_continuousOn_off_finite {f : ℝ → ℂ} {a b : ℝ} {P : Finset ℝ} (hf_cont : ContinuousOn f (Set.Icc a b \ ↑P)) : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Icc a b))

theorem aEStronglyMeasurable_pv_integrand_decomposed {g_reg : ℂ → ℂ} {γ : ℝ → ℂ} {a b ε : ℝ} {P : Finset ℝ} (S : Finset ℂ) (coeffs : ℂ → ℂ) (hε : 0 < ε) (hg : ContinuousOn g_reg (γ '' Set.Icc a b)) (hγ : ContinuousOn γ (Set.Icc a b)) (hγ'_off_P : ContinuousOn (deriv γ) (Set.Icc a b \ ↑P)) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => if ∃ s ∈ S, ‖γ t - s‖ ≤ ε then 0 else (g_reg (γ t) + ∑ s ∈ S, coeffs s / (γ t - s)) * deriv γ t) (MeasureTheory.volume.restrict (Set.Icc a b))

theorem integrableOn_of_bounded_aeMeasurable {f : ℝ → ℂ} {a b : ℝ} (M : ℝ) (hf_meas : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Icc a b))) (hf_bound : ∀ x ∈ Set.Icc a b, ‖f x‖ ≤ M) : MeasureTheory.IntegrableOn f (Set.Icc a b) MeasureTheory.volume

theorem tendsto_integral_of_dominated' {a b : ℝ} {F : ℝ → ℝ → ℂ} {f : ℝ → ℂ} {g : ℝ → ℝ} (hF_meas : ∀ ε > 0, MeasureTheory.AEStronglyMeasurable (F ε) (MeasureTheory.volume.restrict (Set.uIoc a b))) (hF_le : ∀ ε > 0, ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → ‖F ε t‖ ≤ g t) (hg_int : IntervalIntegrable g MeasureTheory.volume a b) (hF_lim : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → Filter.Tendsto (fun (ε : ℝ) => F ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f t))) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, F ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (t : ℝ) in a..b, f t))

Finite Set Separation

theorem finset_discrete_min_sep (S0 : Finset ℂ) (hS0_nonempty : S0.Nonempty) (hS0_discrete : ∀ s ∈ S0, ∀ s' ∈ S0, s ≠ s' → 0 < ‖s' - s‖) : ∃ δ > 0, ∀ s ∈ S0, ∀ s' ∈ S0, s ≠ s' → δ ≤ ‖s' - s‖

Positive minimum separation in a finite set.

theorem disjoint_balls_of_small_epsilon (S0 : Finset ℂ) (ε : ℝ) (_hε : 0 < ε) (δ : ℝ) (_hδ : 0 < δ) (hε_small : ε < δ / 2) (h_sep : ∀ s ∈ S0, ∀ s' ∈ S0, s ≠ s' → δ ≤ ‖s' - s‖) (s : ℂ) : s ∈ S0 → ∀ s' ∈ S0, s ≠ s' → Disjoint (Metric.ball s ε) (Metric.ball s' ε)

Disjoint balls for small epsilon.

Boundedness Lemmas

theorem continuousOn_image_bounded {g : ℂ → ℂ} {γ : ℝ → ℂ} {a b : ℝ} (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hg_cont : ContinuousOn g (γ '' Set.Icc a b)) : ∃ (Mg : ℝ), ∀ z ∈ γ '' Set.Icc a b, ‖g z‖ ≤ Mg

Continuous functions on a compact image are bounded.

theorem piecewise_if_bounded {f : ℝ → ℂ} {a b M : ℝ} {cond : ℝ → Prop} [DecidablePred cond] (hf_bound : ∀ t ∈ Set.Icc a b, cond t → ‖f t‖ ≤ M) (hM : 0 ≤ M) (t : ℝ) : t ∈ Set.Icc a b → ‖if cond t then f t else 0‖ ≤ M

Piecewise if-then-else is bounded when the active branch is bounded.

theorem residue_term_bounded_when_separated {γ : ℝ → ℂ} {s c : ℂ} {a b ε : ℝ} (hε : 0 < ε) (h_sep : ∀ t ∈ Set.Icc a b, ε < ‖γ t - s‖) (t : ℝ) : t ∈ Set.Icc a b → ‖c / (γ t - s)‖ ≤ ‖c‖ / ε

Residue term is bounded when separated from the singularity.

noncomputable def residueNormSum (f : ℂ → ℂ) (S : Finset ℂ) : ℝ

The sum of the norms of the simple-pole residues of f over a finite set S.

Equations

• residueNormSum f S = ∑ s ∈ S, ‖residueSimplePole f s‖

theorem A_int_bound_good_set {S0 : Finset ℂ} {f g_reg : ℂ → ℂ} {γ : ℝ → ℂ} {a b ε Mg Mγ : ℝ} (hε : 0 < ε) (hMg : 0 ≤ Mg) (_hMγ : 0 ≤ Mγ) (hg_decomp : ∀ z ∉ ↑S0, f z = g_reg z + ∑ s ∈ S0, residueSimplePole f s / (z - s)) (hg_bound : ∀ t ∈ Set.Icc a b, ‖g_reg (γ t)‖ ≤ Mg) (hγ'_bound : ∀ t ∈ Set.Icc a b, ‖deriv γ t‖ ≤ Mγ) (h_all_far : ∀ t ∈ Set.Icc a b, ∀ s ∈ S0, ε < ‖γ t - s‖) (t : ℝ) : t ∈ Set.Icc a b → ‖cauchyPrincipalValueIntegrandOn S0 f γ ε t - ∑ s ∈ S0, if ‖γ t - s‖ > ε then residueSimplePole f s / (γ t - s) * deriv γ t else 0‖ ≤ Mg * Mγ

Integrability Lemmas

theorem intervalIntegrable_cauchyPrincipalValueIntegrandOn {S0 : Finset ℂ} {f : ℂ → ℂ} {γ : PiecewiseC1Immersion} {ε : ℝ} (_hε : 0 < ε) (hf_cont : ContinuousOn f (γ.toFun '' Set.Icc γ.a γ.b)) : IntervalIntegrable (cauchyPrincipalValueIntegrandOn S0 f γ.toFun ε) MeasureTheory.volume γ.a γ.b

Multi-point PV integrand is interval integrable.

theorem intervalIntegrable_residueTerm {γ : PiecewiseC1Immersion} {s c : ℂ} {ε : ℝ} (hε : 0 < ε) : IntervalIntegrable (fun (t : ℝ) => if ‖γ.toFun t - s‖ > ε then c / (γ.toFun t - s) * deriv γ.toFun t else 0) MeasureTheory.volume γ.a γ.b

Residue term integrand is interval integrable.

Measurability Lemmas

theorem aEStronglyMeasurable_pv_sum_residue (S : Finset ℂ) (f : ℂ → ℂ) (γ : ℝ → ℂ) (ε : ℝ) (hε : 0 < ε) (a b : ℝ) {P : Finset ℝ} (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hγ'_off_P : ContinuousOn (deriv γ) (Set.Icc a b \ ↑P)) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => ∑ s ∈ S, if ‖γ t - s‖ > ε then residueSimplePole f s / (γ t - s) * deriv γ t else 0) (MeasureTheory.volume.restrict (Set.Icc a b))

theorem aEStronglyMeasurable_multipointPV_diff (S0 : Finset ℂ) (f : ℂ → ℂ) (γ : ℝ → ℂ) (ε : ℝ) (hε : 0 < ε) (a b : ℝ) {P : Finset ℝ} (hf_cont : ContinuousOn f (γ '' Set.uIcc a b)) (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγ'_off_P : ContinuousOn (deriv γ) (Set.uIcc a b \ ↑P)) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => cauchyPrincipalValueIntegrandOn S0 f γ ε t - ∑ s ∈ S0, if ‖γ t - s‖ > ε then residueSimplePole f s / (γ t - s) * deriv γ t else 0) (MeasureTheory.volume.restrict (Set.uIoc a b))