PV Infrastructure: Step Bounds

Dyadic step bounds and subsequence selection for principal value convergence. These combine the gamma analysis (lower/upper bounds) with the remainder analysis (C² bounded remainder) to show that cutoff integrals converge along dyadic subsequences.

Main Results

• remainder_integral_O_eps — O(ε) step bound from bounded remainder
• integral_inv_symm — symmetric cancellation of 1/(t-t₀)
• remainder_annulus_bound — integral of remainder over annulus is O(log ratio)
• exists_summable_subseq — summable subsequence construction
• cutoff_integrand_intervalIntegrable — integrability of cutoff
• cutoff_diff_eq_annulus_integral — difference equals annulus integral

theorem remainder_integral_O_eps {r : ℝ → ℂ} {t₀ ε C : ℝ} (hε_pos : 0 < ε) (_hC_pos : 0 < C) (hr_bound : ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| ≤ 2 * ε → ‖r t‖ ≤ C) : ‖∫ (t : ℝ) in t₀ - 2 * ε..t₀ - ε, r t‖ + ‖∫ (t : ℝ) in t₀ + ε..t₀ + 2 * ε, r t‖ ≤ 2 * C * ε

O(ε) step bound from bounded remainder.

theorem integral_inv_symm (t₀ ε₁ ε₂ : ℝ) (_hε₁ : 0 < ε₁) (_hε₂ : 0 < ε₂) (_hε₁₂ : ε₁ ≤ ε₂) : (∫ (t : ℝ) in t₀ - ε₂..t₀ - ε₁, (↑(t - t₀))⁻¹) + ∫ (t : ℝ) in t₀ + ε₁..t₀ + ε₂, (↑(t - t₀))⁻¹ = 0

Symmetric cancellation of 1/(t-t₀).

theorem remainder_annulus_bound {r : ℝ → ℂ} {t₀ c₁ c₂ η : ℝ} (hc₁_pos : 0 < c₁) (hc₂_pos : 0 < c₂) (hc₁₂ : c₁ < c₂) (_hη_pos : 0 < η) (hr_bound : ∀ (t : ℝ), c₁ < |t - t₀| → |t - t₀| < c₂ → ‖r t‖ ≤ η / |t - t₀|) : ‖∫ (t : ℝ) in t₀ - c₂..t₀ - c₁, r t‖ + ‖∫ (t : ℝ) in t₀ + c₁..t₀ + c₂, r t‖ ≤ 2 * η * Real.log (c₂ / c₁)

Remainder annulus bound: O(log ratio).

theorem exists_eta_delta {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_deriv : ContinuousAt (deriv γ) t₀) (η : ℝ) (hη : 0 < η) : ∃ δ > 0, ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| < δ → ‖(γ t - γ t₀)⁻¹ * deriv γ t - (↑(t - t₀))⁻¹‖ ≤ η / |t - t₀|

Scale-dependent η from asymptotic control.

theorem step_bound_with_eta {r : ℝ → ℂ} {t₀ ε η : ℝ} (hε_pos : 0 < ε) (hη_pos : 0 < η) (hr_bound : ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| ≤ ε → ‖r t‖ ≤ η / |t - t₀|) : ‖∫ (t : ℝ) in t₀ - ε..t₀ - ε / 2, r t‖ + ‖∫ (t : ℝ) in t₀ + ε / 2..t₀ + ε, r t‖ ≤ 2 * η * Real.log 2

Dyadic step [ε/2, ε] contributes ≤ 2η*log(2).

theorem error_at_smaller_scale {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_deriv : ContinuousAt (deriv γ) t₀) (η' : ℝ) : η' > 0 → ∃ δ > 0, ∀ (ε : ℝ), 0 < ε → ε < δ → ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| ≤ ε → ‖(γ t - γ t₀)⁻¹ * deriv γ t - (↑(t - t₀))⁻¹‖ ≤ η' / |t - t₀|

Error bound extends to smaller scales.

@[reducible, inline]

noncomputable abbrev cutoffIntegral (γ : ℝ → ℂ) (a b t₀ ε : ℝ) : ℂ

Cutoff integral I(ε).

Equations

• cutoffIntegral γ a b t₀ ε = ∫ (t : ℝ) in a..b, if ε < ‖γ t - γ t₀‖ then (γ t - γ t₀)⁻¹ * deriv γ t else 0

theorem exists_delta_for_error_bound {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_deriv : ContinuousAt (deriv γ) t₀) (n : ℕ) : ∃ δ > 0, ∀ (ε : ℝ), 0 < ε → ε < δ → ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| ≤ ε → ‖(γ t - γ t₀)⁻¹ * deriv γ t - (↑(t - t₀))⁻¹‖ ≤ (1 / 2) ^ n / |t - t₀|

δ giving error bound (1/2)^n at scale ε < δ.

noncomputable def summableSubseqAux {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_deriv : ContinuousAt (deriv γ) t₀) (δ₀ : ℝ) : ℕ → ℝ

An auxiliary summable subsequence used in the step-bound estimates.

Equations

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

theorem summableSubseqAux_zero {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_deriv : ContinuousAt (deriv γ) t₀) (δ₀ : ℝ) : summableSubseqAux hL hγ_hasderiv hγ_cont_deriv δ₀ 0 = min δ₀ ⋯.choose / 2

theorem summableSubseqAux_succ {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_deriv : ContinuousAt (deriv γ) t₀) (δ₀ : ℝ) (n : ℕ) : have ε := summableSubseqAux hL hγ_hasderiv hγ_cont_deriv δ₀; have δ := fun (m : ℕ) => ⋯.choose; ε (n + 1) = min (ε n / 2) (δ (n + 1)) / 2

theorem summableSubseqAux_pos {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_deriv : ContinuousAt (deriv γ) t₀) (δ₀ : ℝ) (hδ₀_pos : 0 < δ₀) (n : ℕ) : 0 < summableSubseqAux hL hγ_hasderiv hγ_cont_deriv δ₀ n

theorem summableSubseqAux_halving {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_deriv : ContinuousAt (deriv γ) t₀) (δ₀ : ℝ) (hδ₀_pos : 0 < δ₀) (n : ℕ) : summableSubseqAux hL hγ_hasderiv hγ_cont_deriv δ₀ (n + 1) ≤ summableSubseqAux hL hγ_hasderiv hγ_cont_deriv δ₀ n / 2

theorem summableSubseqAux_lt_delta {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_deriv : ContinuousAt (deriv γ) t₀) (δ₀ : ℝ) (hδ₀_pos : 0 < δ₀) (n : ℕ) : have δ := fun (m : ℕ) => ⋯.choose; summableSubseqAux hL hγ_hasderiv hγ_cont_deriv δ₀ n < δ n

theorem summableSubseqAux_error_bound {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_deriv : ContinuousAt (deriv γ) t₀) (δ₀ : ℝ) (hδ₀_pos : 0 < δ₀) (n : ℕ) : have ε_n := summableSubseqAux hL hγ_hasderiv hγ_cont_deriv δ₀ n; ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| ≤ ε_n → ‖(γ t - γ t₀)⁻¹ * deriv γ t - (↑(t - t₀))⁻¹‖ ≤ (1 / 2) ^ n / |t - t₀|

theorem exists_summable_subseq {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_deriv : ContinuousAt (deriv γ) t₀) (δ₀ : ℝ) (hδ₀_pos : 0 < δ₀) : ∃ (ε : ℕ → ℝ), (∀ (n : ℕ), 0 < ε n) ∧ (∀ (n : ℕ), ε (n + 1) ≤ ε n / 2) ∧ ∀ (n : ℕ) (t : ℝ), 0 < |t - t₀| → |t - t₀| ≤ ε n → ‖(γ t - γ t₀)⁻¹ * deriv γ t - (↑(t - t₀))⁻¹‖ ≤ (1 / 2) ^ n / |t - t₀|

theorem summableSubseqAux_le_geometric {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_deriv : ContinuousAt (deriv γ) t₀) (δ₀ : ℝ) (hδ₀_pos : 0 < δ₀) (n : ℕ) : summableSubseqAux hL hγ_hasderiv hγ_cont_deriv δ₀ n ≤ summableSubseqAux hL hγ_hasderiv hγ_cont_deriv δ₀ 0 / 2 ^ n

ε_n ≤ ε_0 / 2^n for the summable subsequence.

theorem summableSubseqAux_tendsto_zero {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_deriv : ContinuousAt (deriv γ) t₀) (δ₀ : ℝ) (hδ₀_pos : 0 < δ₀) : Filter.Tendsto (summableSubseqAux hL hγ_hasderiv hγ_cont_deriv δ₀) Filter.atTop (nhds 0)

The summable subsequence tends to 0.

theorem cutoff_integrand_intervalIntegrable {γ : ℝ → ℂ} {a b t₀ : ℝ} {L : ℂ} (hat₀ : t₀ ∈ Set.Ioo a b) (_hL : L ≠ 0) (hγ_meas : Measurable γ) (hγ_cont_deriv : ContinuousOn (deriv γ) (Set.Icc a b)) (ε : ℝ) (hε_pos : 0 < ε) : IntervalIntegrable (fun (t : ℝ) => if ε < ‖γ t - γ t₀‖ then (γ t - γ t₀)⁻¹ * deriv γ t else 0) MeasureTheory.volume a b

Cutoff integrand is interval integrable.

theorem cutoff_diff_eq_annulus_integral {f γ : ℝ → ℂ} {a b t₀ ε₁ ε₂ : ℝ} (h_le : ε₁ ≤ ε₂) (h_int₁ : IntervalIntegrable (fun (t : ℝ) => if ε₁ < ‖γ t - γ t₀‖ then f t else 0) MeasureTheory.volume a b) (h_int₂ : IntervalIntegrable (fun (t : ℝ) => if ε₂ < ‖γ t - γ t₀‖ then f t else 0) MeasureTheory.volume a b) : ((∫ (t : ℝ) in a..b, if ε₁ < ‖γ t - γ t₀‖ then f t else 0) - ∫ (t : ℝ) in a..b, if ε₂ < ‖γ t - γ t₀‖ then f t else 0) = ∫ (t : ℝ) in a..b, if ε₁ < ‖γ t - γ t₀‖ ∧ ‖γ t - γ t₀‖ ≤ ε₂ then f t else 0

Cutoff difference equals annulus integral.

theorem pv_singular_cancels (t₀ ε δ : ℝ) (hε_pos : 0 < ε) (hδ_pos : 0 < δ) (hεδ : ε < δ) : (∫ (t : ℝ) in t₀ - δ..t₀ - ε, (↑(t - t₀))⁻¹) + ∫ (t : ℝ) in t₀ + ε..t₀ + δ, (↑(t - t₀))⁻¹ = 0

Singular part cancellation via odd symmetry.

theorem remainder_step_bound {r : ℝ → ℂ} {t₀ ε η : ℝ} (hε_pos : 0 < ε) (_hη_pos : 0 < η) (hr_bound : ∀ (t : ℝ), ε / 2 < |t - t₀| → |t - t₀| < ε → ‖r t‖ ≤ η / |t - t₀|) : ‖∫ (t : ℝ) in t₀ - ε..t₀ - ε / 2, r t‖ + ‖∫ (t : ℝ) in t₀ + ε / 2..t₀ + ε, r t‖ ≤ 2 * η * Real.log 2

Remainder step bound for dyadic step.

theorem remainder_bounded_ratio {r : ℝ → ℂ} {t₀ ε₁ ε₂ η K : ℝ} (hε₁_pos : 0 < ε₁) (hε₁₂ : ε₁ < ε₂) (hη_pos : 0 < η) (_hK : 1 < K) (h_ratio : ε₂ / ε₁ ≤ K) (hr_bound : ∀ (t : ℝ), ε₁ < |t - t₀| → |t - t₀| < ε₂ → ‖r t‖ ≤ η / |t - t₀|) : ‖∫ (t : ℝ) in t₀ - ε₂..t₀ - ε₁, r t‖ + ‖∫ (t : ℝ) in t₀ + ε₁..t₀ + ε₂, r t‖ ≤ 2 * η * Real.log K

Remainder bounded ratio for annuli.

theorem remainder_dyadic_step {r : ℝ → ℂ} {t₀ ε₀ η : ℝ} (n : ℕ) (hε₀_pos : 0 < ε₀) (hη_pos : 0 < η) (hr_bound : ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| < ε₀ → ‖r t‖ ≤ η / |t - t₀|) : ‖∫ (t : ℝ) in t₀ - ε₀ / 2 ^ n..t₀ - ε₀ / 2 ^ (n + 1), r t‖ + ‖∫ (t : ℝ) in t₀ + ε₀ / 2 ^ (n + 1)..t₀ + ε₀ / 2 ^ n, r t‖ ≤ 2 * η * Real.log 2

Dyadic step bound for remainder.

theorem pv_dyadic_step_O_eps {r : ℝ → ℂ} {t₀ δ₀ C : ℝ} (n : ℕ) (hδ₀_pos : 0 < δ₀) (_hC_pos : 0 < C) (hr_bounded : ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| ≤ δ₀ → ‖r t‖ ≤ C) : have ε_n := δ₀ / 2 ^ n; ‖∫ (t : ℝ) in t₀ - ε_n..t₀ - ε_n / 2, r t‖ + ‖∫ (t : ℝ) in t₀ + ε_n / 2..t₀ + ε_n, r t‖ ≤ C * ε_n

Dyadic step O(ε) with bounded remainder.

theorem cauchySeq_pv_dyadic {I : ℝ → ℂ} {δ₀ C : ℝ} (_hδ₀_pos : 0 < δ₀) (_hC_pos : 0 < C) (h_step : ∀ (n : ℕ), ‖I (δ₀ / 2 ^ (n + 1)) - I (δ₀ / 2 ^ n)‖ ≤ C * δ₀ / 2 ^ n) : CauchySeq fun (n : ℕ) => I (δ₀ / 2 ^ n)

Dyadic sequence is Cauchy with bounded remainder.

theorem t_bound_from_gamma_annulus {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} {δ₁ ε : ℝ} (hL : L ≠ 0) (_hε_pos : 0 < ε) (h_lower : ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| < δ₁ → ‖γ t - γ t₀‖ ≥ ‖L‖ / 2 * |t - t₀|) (t : ℝ) (ht_pos : 0 < |t - t₀|) (ht_lt : |t - t₀| < δ₁) (hγ_bound : ‖γ t - γ t₀‖ ≤ ε) : |t - t₀| ≤ 2 * ε / ‖L‖

t-space bound from γ-annulus.

theorem integrand_bound_on_annulus {γ : ℝ → ℂ} {t₀ C δ₀ : ℝ} (hr_bounded : ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| < δ₀ → ‖(γ t - γ t₀)⁻¹ * deriv γ t - (↑(t - t₀))⁻¹‖ ≤ C) (t : ℝ) (ht_pos : 0 < |t - t₀|) (ht_lt : |t - t₀| < δ₀) : ‖(γ t - γ t₀)⁻¹ * deriv γ t‖ ≤ |t - t₀|⁻¹ + C

Integrand bound on γ-annulus.

theorem annulus_implies_t_local {γ : ℝ → ℂ} {a b t₀ ε₁ δ₀ δ₁ : ℝ} (h_localize : ∀ t ∈ Set.Icc a b, ‖γ t - γ t₀‖ ≤ ε₁ → |t - t₀| < min δ₀ δ₁) (t : ℝ) (ht_ab : t ∈ Set.Icc a b) (hγ_bound : ‖γ t - γ t₀‖ ≤ ε₁) : |t - t₀| < δ₀ ∧ |t - t₀| < δ₁

Annulus localization: γ-annulus points are local.

theorem exists_dyadic_bracket {δ ε : ℝ} (hδ_pos : 0 < δ) (hε_pos : 0 < ε) (hε_le : ε ≤ δ) : ∃ (n : ℕ), δ / 2 ^ (n + 1) < ε ∧ ε ≤ δ / 2 ^ n

Bracket ε between dyadic points: for ε ∈ (0, δ], find n with δ/2^(n+1) < ε ≤ δ/2^n.

theorem telescoping_sum_bound {X : Type u_1} [SeminormedAddCommGroup X] {I : ℕ → X} {K δ : ℝ} (_hK_pos : 0 < K) (_hδ_pos : 0 < δ) (h_step : ∀ (n : ℕ), ‖I (n + 1) - I n‖ ≤ K * δ / 2 ^ n) (N M : ℕ) : M > N → ‖I M - I N‖ ≤ 2 * K * δ / 2 ^ N - 2 * K * δ / 2 ^ M

Telescoping sum bound for geometric step bounds.