PV Infrastructure: Remainder Analysis

Taylor expansion and C² remainder bounds for the PV integrand. The key result remainder_bounded_of_C2 shows that the remainder r(t) = (γ-γ₀)⁻¹γ' - (t-t₀)⁻¹ is bounded (O(1)) near t₀.

Main Results

• remainder_bounded_of_C2 — bounded remainder from C² smoothness
• numerator_quadratic_bound — numerator is O(|t-t₀|²)
• quadratic_approx_of_contDiffAt_two — quadratic Taylor approximation

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

C¹ regularity of deriv γ from C² regularity of γ.

theorem deriv_deviation_bound_of_C2 {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hγ_C2 : ContDiffAt ℝ 2 γ t₀) (hγ_deriv : deriv γ t₀ = L) : ∃ (K : ℝ) (δ : ℝ), 0 < δ ∧ ∀ (t : ℝ), |t - t₀| < δ → ‖deriv γ t - L‖ ≤ K * |t - t₀|

Lipschitz-type bound on deriv γ deviation from C².

theorem quadratic_approx_of_contDiffAt_two {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hγ_C2 : ContDiffAt ℝ 2 γ t₀) (hγ_deriv : deriv γ t₀ = L) : ∃ (K : ℝ) (δ : ℝ), 0 < δ ∧ 0 < K ∧ ∀ (t : ℝ), |t - t₀| < δ → ‖γ t - γ t₀ - (t - t₀) • L‖ ≤ K * |t - t₀| ^ 2

Quadratic Taylor approximation from C² smoothness.

theorem bounded_slope_deviation_of_contDiffAt_two {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hγ_C2 : ContDiffAt ℝ 2 γ t₀) (hγ_deriv : deriv γ t₀ = L) : ∃ (K : ℝ) (δ : ℝ), 0 < δ ∧ 0 < K ∧ ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| < δ → ‖(γ t - γ t₀) / ↑(t - t₀) - L‖ ≤ K * |t - t₀|

Bounded slope deviation from C² smoothness.

theorem numerator_quadratic_bound {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hγ_C2 : ContDiffAt ℝ 2 γ t₀) (hγ_deriv : deriv γ t₀ = L) : ∃ (K : ℝ) (δ : ℝ), 0 < δ ∧ ∀ (t : ℝ), |t - t₀| < δ → ‖↑(t - t₀) * deriv γ t - (γ t - γ t₀)‖ ≤ K * |t - t₀| ^ 2

Numerator quadratic bound for (t-t₀)γ'(t) - (γt - γt₀).

theorem remainder_bounded_of_C2 {γ : ℝ → ℂ} {t₀ : ℝ} {L : ℂ} (hL : L ≠ 0) (hγ_C2 : ContDiffAt ℝ 2 γ t₀) (hγ_deriv : deriv γ t₀ = L) : ∃ (C : ℝ) (δ : ℝ), 0 < δ ∧ ∀ (t : ℝ), 0 < |t - t₀| → |t - t₀| < δ → ‖(γ t - γ t₀)⁻¹ * deriv γ t - (↑(t - t₀))⁻¹‖ ≤ C

Bounded remainder from C² smoothness.