PV Infrastructure: Uniform Step Bound

The main uniform step bound for dyadic PV convergence. Combines the remainder analysis, gamma bounds, and singular annulus bound into a single epsilon-independent estimate.

Main Results

• pv_step_bound_ratio_two_uniform — uniform step bound with epsilon-independent constant

theorem pv_step_bound_ratio_two_uniform {γ : ℝ → ℂ} {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γ_meas : Measurable γ) (hγ_cont_deriv : ContinuousOn (deriv γ) (Set.Icc a b)) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (h_inj : ∀ t ∈ Set.Icc a b, γ t = γ t₀ → t = t₀) : ∃ Kstep > 0, ∃ δ > 0, ∀ (ε₁ ε₂ : ℝ), 0 < ε₂ → ε₂ ≤ ε₁ → ε₁ ≤ 2 * ε₂ → ε₁ < δ → have I := fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ε < ‖γ t - γ t₀‖ then (γ t - γ t₀)⁻¹ * deriv γ t else 0; ‖I ε₂ - I ε₁‖ ≤ Kstep * ε₁

Uniform step bound with epsilon-independent constant.