PV Infrastructure: Gamma Analysis #

Derivative-based bounds on curves near crossing points. These are used in the dyadic PV limit proof for principal value convergence.

Main Results #

theorem integrand_times_t_tendsto_one (γ : ℝ → ℂ) (t₀ : ℝ) (L : ℂ) (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) (hγ_cont_at : ContinuousAt (deriv γ) t₀) :

Filter.Tendsto (fun (t : ℝ) => ↑(t - t₀) * (γ t - γ t₀)⁻¹ * deriv γ t) (nhdsWithin t₀ {t₀}ᶜ) (nhds 1)

The integrand times (t-t₀) tends to 1. This is the key estimate: (t-t₀) * (γ-γ₀)⁻¹ * γ' → 1 as t → t₀.

theorem integrand_asymptotic (γ : ℝ → ℂ) (t₀ : ℝ) (L : ℂ) (_hL : L ≠ 0) (_hγ_hasderiv : HasDerivAt γ L t₀) (_hγ_cont_at : ContinuousAt (deriv γ) t₀) (h_tendsto : Filter.Tendsto (fun (t : ℝ) => ↑(t - t₀) * (γ t - γ t₀)⁻¹ * deriv γ t) (nhdsWithin t₀ {t₀}ᶜ) (nhds 1)) (ε : ℝ) :

ε > 0 → ∃ δ > 0, ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| < δ → ‖(γ t - γ t₀)⁻¹ * deriv γ t - (↑(t - t₀))⁻¹ ‖ ≤ ε / |t - t₀|

Asymptotic control: ‖(γ-γ₀)⁻¹ * γ' - (t-t₀)⁻¹‖ ≤ ε / |t-t₀|.

theorem gamma_lower_bound_of_hasDerivAt {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) :

∃ δ > 0, ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| < δ → ‖γ t - γ t₀‖ ≥ ‖L‖ / 2 * |t - t₀|

Lower bound on ‖γ t - γ t₀‖ from non-zero derivative. Uses hasDerivAt_remainder_bound + reverse triangle inequality.

theorem gamma_upper_bound_of_hasDerivAt {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_hasderiv : HasDerivAt γ L t₀) :

∃ δ > 0, ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| < δ → ‖γ t - γ t₀‖ ≤ 2 * ‖L‖ * |t - t₀|

Upper bound on ‖γ t - γ t₀‖ from non-zero derivative. Uses hasDerivAt_remainder_bound + triangle inequality.

theorem no_return_of_inj_continuous {γ : ℝ → ℂ} {a b t₀ c : ℝ} (hc_pos : 0 < c) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (h_inj : ∀ t ∈ Set.Icc a b, γ t = γ t₀ → t = t₀) :

∃ ρ > 0, ∀ t ∈ Set.Icc a b, c ≤ |t - t₀| → ρ ≤ ‖γ t - γ t₀‖

If γ is continuous on [a,b] and injective at γ(t₀), then γ stays bounded away from γ(t₀) outside any neighborhood of t₀.

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

|t - t₀| ≤ 2 * εC / ‖L‖

From γ-space upper bound to t-space upper bound: If ‖γ t - γ t₀‖ ≤ εC and we have the lower bound, then |t - t₀| ≤ 2*εC/‖L‖.

theorem t_lower_from_gamma_lower {γ : ℝ → ℂ} {t₀ t : ℝ} {L : ℂ} {εC δ : ℝ} (hL : L ≠ 0) (_hδ_pos : 0 < δ) (ht_pos : 0 < |t - t₀|) (ht_lt : |t - t₀| < δ) (h_upper : ∀ (s : ℝ), 0 < |s - t₀| → |s - t₀| < δ → ‖γ s - γ t₀‖ ≤ 2 * ‖L‖ * |s - t₀|) (h_gamma_lower : εC < ‖γ t - γ t₀‖) :

εC / (2 * ‖L‖) < |t - t₀|

From γ-space lower bound to t-space lower bound: If ‖γ t - γ t₀‖ > εC and we have the upper bound, then |t - t₀| > εC/(2*‖L‖).

theorem contAt_deriv_of_contDiffAt_two {γ : ℝ → ℂ} {t₀ : ℝ} (hγ_C2 : ContDiffAt ℝ 2 γ t₀) :

If γ is C² at t₀, then deriv γ is continuous at t₀.