PV Infrastructure: Singular Annulus Bounds

Bounds on singular annular integrals, including the linearized model, symmetric cancellation, measurability, and the explicit epsilon-independent bound used in the dyadic PV convergence proof.

Main Results

• singular_tAnnLin_cancel — linearized annular integrand cancels symmetrically
• singular_annulus_lin_integral_zero — linearized annular integral vanishes
• singular_annulus_bound_explicit — epsilon-independent bound on singular integral

Reusable API: norm-annulus rescaling, indicator bundles, integral splitting

theorem norm_annulus_condition_iff {t₀ : ℝ} {L : ℂ} {ε₁ ε₂ : ℝ} (hL_pos : 0 < ‖L‖) (t : ℝ) : ε₂ < ‖L‖ * |t - t₀| ∧ ‖L‖ * |t - t₀| ≤ ε₁ ↔ ε₂ / ‖L‖ < |t - t₀| ∧ |t - t₀| ≤ ε₁ / ‖L‖

The annulus condition ε₂ < ‖L‖ * |t - t₀| ∧ ‖L‖ * |t - t₀| ≤ ε₁ is equivalent to c₁ < |t - t₀| ∧ |t - t₀| ≤ c₂ where c₁ = ε₂/‖L‖ and c₂ = ε₁/‖L‖.

theorem intervalIntegral_eq_zero_of_ae_eq_zero {a b : ℝ} {φ : ℝ → ℂ} (_hI : IntervalIntegrable φ MeasureTheory.volume a b) (h_ae : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → φ t = 0) : ∫ (t : ℝ) in a..b, φ t = 0

When an integrand is a.e. zero on an interval, its interval integral is zero.

theorem integral_split_five {a p₁ p₂ p₃ p₄ b : ℝ} {φ : ℝ → ℂ} (h₁ : IntervalIntegrable φ MeasureTheory.volume a p₁) (h₂ : IntervalIntegrable φ MeasureTheory.volume p₁ p₂) (h₃ : IntervalIntegrable φ MeasureTheory.volume p₂ p₃) (h₄ : IntervalIntegrable φ MeasureTheory.volume p₃ p₄) (h₅ : IntervalIntegrable φ MeasureTheory.volume p₄ b) : ∫ (t : ℝ) in a..b, φ t = ((((∫ (t : ℝ) in a..p₁, φ t) + ∫ (t : ℝ) in p₁..p₂, φ t) + ∫ (t : ℝ) in p₂..p₃, φ t) + ∫ (t : ℝ) in p₃..p₄, φ t) + ∫ (t : ℝ) in p₄..b, φ t

Split ∫ a..b f into five consecutive sub-integrals at four ordered intermediate points.

End API section

theorem singular_tAnnLin_inside_interval {t₀ a b : ℝ} (hat₀ : t₀ ∈ Set.Ioo a b) {L : ℂ} (hL_pos : 0 < ‖L‖) {ε₁ : ℝ} (hε₁_small : ε₁ < ‖L‖ * min (t₀ - a) (b - t₀)) {t : ℝ} (ht_bound : ‖L‖ * |t - t₀| ≤ ε₁) : t ∈ Set.Icc a b

theorem singular_tAnnLin_cancel (t₀ : ℝ) {L : ℂ} (hL_pos : 0 < ‖L‖) (ε₁ ε₂ : ℝ) (hε₂_pos : 0 < ε₂) (hε₂_le : ε₂ ≤ ε₁) : have c₁ := ε₂ / ‖L‖; have c₂ := ε₁ / ‖L‖; (∫ (t : ℝ) in t₀ - c₂..t₀ - c₁, (↑(t - t₀))⁻¹) + ∫ (t : ℝ) in t₀ + c₁..t₀ + c₂, (↑(t - t₀))⁻¹ = 0

theorem singular_symmDiff_sup_bound {t₀ c : ℝ} (hc_pos : 0 < c) {t : ℝ} (ht_lower : c ≤ |t - t₀|) : ‖(↑(t - t₀))⁻¹‖ ≤ 1 / c

Helper: measurability, bound, and integrability for the linearized indicator

theorem singular_annulus_f_lin_intervalIntegrable {t₀ : ℝ} {L : ℂ} {ε₁ ε₂ : ℝ} (hL_pos : 0 < ‖L‖) (hε₂_pos : 0 < ε₂) (u v : ℝ) : IntervalIntegrable (fun (t : ℝ) => if ε₂ < ‖L‖ * |t - t₀| ∧ ‖L‖ * |t - t₀| ≤ ε₁ then (↑(t - t₀))⁻¹ else 0) MeasureTheory.volume u v

The linearized annular indicator is integrable on any interval.

Helper: linearized annular integral vanishes by symmetric cancellation

Helper: pointwise bound on difference between gamma and linearized indicators

Helper: symmetric difference volume bound via a.e. correction

theorem singular_annulus_bound_explicit {γ : ℝ → ℂ} {a b t₀ : ℝ} {L : ℂ} (hab : a < b) (hat₀ : t₀ ∈ Set.Ioo a b) (hγ_C2 : ContDiffAt ℝ 2 γ t₀) (hγ_deriv : deriv γ t₀ = L) (hL : L ≠ 0) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (h_inj : ∀ t ∈ Set.Icc a b, γ t = γ t₀ → t = t₀) : ∃ Csing > 0, ∃ δ > 0, ∀ (ε₁ ε₂ : ℝ), 0 < ε₂ → ε₂ ≤ ε₁ → ε₁ ≤ 2 * ε₂ → ε₁ < δ → ‖∫ (t : ℝ) in a..b, if ε₂ < ‖γ t - γ t₀‖ ∧ ‖γ t - γ t₀‖ ≤ ε₁ then (↑(t - t₀))⁻¹ else 0‖ ≤ Csing * ε₁