Telescoping FTC for Log-Derivative on Piecewise Segments

When FTC-for-log is applied to consecutive segments sharing endpoints, the log terms telescope. For a closed curve split at a crossing t₀ ± δ, the total integral reduces to log(g(t₀-δ)) - log(g(t₀+δ)).

Main results

• ftc_telescope_two — FTC on two consecutive segments telescopes
• ftc_telescope_closed_split — for closed curves, the full integral telescopes to the log difference at the crossing boundary

theorem ContourIntegral.ftc_telescope_two {f : ℝ → ℂ} {a b c : ℝ} (_hab : a ≤ b) (_hbc : b ≤ c) (hint_ab : IntervalIntegrable (fun (t : ℝ) => deriv f t / f t) MeasureTheory.volume a b) (hint_bc : IntervalIntegrable (fun (t : ℝ) => deriv f t / f t) MeasureTheory.volume b c) (h_ab : ∫ (t : ℝ) in a..b, deriv f t / f t = Complex.log (f b) - Complex.log (f a)) (h_bc : ∫ (t : ℝ) in b..c, deriv f t / f t = Complex.log (f c) - Complex.log (f b)) : ∫ (t : ℝ) in a..c, deriv f t / f t = Complex.log (f c) - Complex.log (f a)

FTC on two consecutive segments telescopes: if the integral over [a,b] is log(f b) - log(f a) and the integral over [b,c] is log(f c) - log(f b), then the integral over [a,c] is log(f c) - log(f a).

theorem ContourIntegral.ftc_telescope_closed_split {f : ℝ → ℂ} {a b t₀ δ : ℝ} (h_closed : f a = f b) (_hint_left : IntervalIntegrable (fun (t : ℝ) => deriv f t / f t) MeasureTheory.volume a (t₀ - δ)) (_hint_right : IntervalIntegrable (fun (t : ℝ) => deriv f t / f t) MeasureTheory.volume (t₀ + δ) b) (h_left : ∫ (t : ℝ) in a..t₀ - δ, deriv f t / f t = Complex.log (f (t₀ - δ)) - Complex.log (f a)) (h_right : ∫ (t : ℝ) in t₀ + δ..b, deriv f t / f t = Complex.log (f b) - Complex.log (f (t₀ + δ))) : (∫ (t : ℝ) in a..t₀ - δ, deriv f t / f t) + ∫ (t : ℝ) in t₀ + δ..b, deriv f t / f t = Complex.log (f (t₀ - δ)) - Complex.log (f (t₀ + δ))

For a closed curve (f a = f b), the integral from a to (t₀ - δ) plus from (t₀ + δ) to b telescopes to log(f(t₀ - δ)) - log(f(t₀ + δ)), because the log terms at a and b cancel by closedness.

theorem ContourIntegral.ftc_telescope_three {f : ℝ → ℂ} {a b c d : ℝ} (hint_ab : IntervalIntegrable (fun (t : ℝ) => deriv f t / f t) MeasureTheory.volume a b) (hint_bc : IntervalIntegrable (fun (t : ℝ) => deriv f t / f t) MeasureTheory.volume b c) (hint_cd : IntervalIntegrable (fun (t : ℝ) => deriv f t / f t) MeasureTheory.volume c d) (h_ab : ∫ (t : ℝ) in a..b, deriv f t / f t = Complex.log (f b) - Complex.log (f a)) (h_bc : ∫ (t : ℝ) in b..c, deriv f t / f t = Complex.log (f c) - Complex.log (f b)) (h_cd : ∫ (t : ℝ) in c..d, deriv f t / f t = Complex.log (f d) - Complex.log (f c)) : ∫ (t : ℝ) in a..d, deriv f t / f t = Complex.log (f d) - Complex.log (f a)

FTC on three consecutive segments telescopes: the integral over [a,d] is log(f d) - log(f a) if each sub-interval satisfies the FTC-for-log.

theorem ContourIntegral.ftc_telescope_integrability {g h : ℝ → ℂ} {a b : ℝ} (hint_h : IntervalIntegrable (fun (t : ℝ) => deriv h t / h t) MeasureTheory.volume a b) (h_ae : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → deriv g t / g t = deriv h t / h t) : IntervalIntegrable (fun (t : ℝ) => deriv g t / g t) MeasureTheory.volume a b

Transfer integrability from a local function h to g given that their log-derivatives agree almost everywhere on the interval. The h_ae hypothesis has the direction deriv g / g = deriv h / h pointwise a.e., which is reversed internally to match the congr_ae requirement.

theorem ContourIntegral.ftc_telescope_transfer {g h : ℝ → ℂ} {a b : ℝ} (hint_h : IntervalIntegrable (fun (t : ℝ) => deriv h t / h t) MeasureTheory.volume a b) (h_ftc : ∫ (t : ℝ) in a..b, deriv h t / h t = Complex.log (h b) - Complex.log (h a)) (h_ae : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → deriv g t / g t = deriv h t / h t) (h_ga : g a = h a) (h_gb : g b = h b) : IntervalIntegrable (fun (t : ℝ) => deriv g t / g t) MeasureTheory.volume a b ∧ ∫ (t : ℝ) in a..b, deriv g t / g t = Complex.log (g b) - Complex.log (g a)

Transfer an FTC result from a local function h to g given that their log-derivatives agree a.e. and their values agree at the endpoints. Produces both integrability and the FTC equality for g.

theorem ContourIntegral.ftc_telescope_piecewise_two {g h₁ h₂ : ℝ → ℂ} {a p b : ℝ} (hap : a ≤ p) (hpb : p ≤ b) (hint₁ : IntervalIntegrable (fun (t : ℝ) => deriv h₁ t / h₁ t) MeasureTheory.volume a p) (hint₂ : IntervalIntegrable (fun (t : ℝ) => deriv h₂ t / h₂ t) MeasureTheory.volume p b) (h_ftc₁ : ∫ (t : ℝ) in a..p, deriv h₁ t / h₁ t = Complex.log (h₁ p) - Complex.log (h₁ a)) (h_ftc₂ : ∫ (t : ℝ) in p..b, deriv h₂ t / h₂ t = Complex.log (h₂ b) - Complex.log (h₂ p)) (h_ae₁ : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a p → deriv g t / g t = deriv h₁ t / h₁ t) (h_ae₂ : ∀ᵐ (t : ℝ), t ∈ Set.uIoc p b → deriv g t / g t = deriv h₂ t / h₂ t) (h_ga : g a = h₁ a) (h_gp_left : g p = h₁ p) (h_gp_right : g p = h₂ p) (h_gb : g b = h₂ b) : IntervalIntegrable (fun (t : ℝ) => deriv g t / g t) MeasureTheory.volume a b ∧ ∫ (t : ℝ) in a..b, deriv g t / g t = Complex.log (g b) - Complex.log (g a)

General piecewise FTC telescope for a function g on [a, b] that is split at a single interior breakpoint p. Given FTC results on [a, p] and [p, b] for local functions h₁ and h₂ respectively, together with a.e. agreement of log-derivatives and matching endpoints, the combined integral telescopes to log(g b) - log(g a).

theorem ContourIntegral.ftc_telescope_piecewise_three {g h₁ h₂ h₃ : ℝ → ℂ} {a p q b : ℝ} (hint₁ : IntervalIntegrable (fun (t : ℝ) => deriv h₁ t / h₁ t) MeasureTheory.volume a p) (hint₂ : IntervalIntegrable (fun (t : ℝ) => deriv h₂ t / h₂ t) MeasureTheory.volume p q) (hint₃ : IntervalIntegrable (fun (t : ℝ) => deriv h₃ t / h₃ t) MeasureTheory.volume q b) (h_ftc₁ : ∫ (t : ℝ) in a..p, deriv h₁ t / h₁ t = Complex.log (h₁ p) - Complex.log (h₁ a)) (h_ftc₂ : ∫ (t : ℝ) in p..q, deriv h₂ t / h₂ t = Complex.log (h₂ q) - Complex.log (h₂ p)) (h_ftc₃ : ∫ (t : ℝ) in q..b, deriv h₃ t / h₃ t = Complex.log (h₃ b) - Complex.log (h₃ q)) (h_ae₁ : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a p → deriv g t / g t = deriv h₁ t / h₁ t) (h_ae₂ : ∀ᵐ (t : ℝ), t ∈ Set.uIoc p q → deriv g t / g t = deriv h₂ t / h₂ t) (h_ae₃ : ∀ᵐ (t : ℝ), t ∈ Set.uIoc q b → deriv g t / g t = deriv h₃ t / h₃ t) (h_ga : g a = h₁ a) (h_gp : g p = h₁ p) (h_gp' : g p = h₂ p) (h_gq : g q = h₂ q) (h_gq' : g q = h₃ q) (h_gb : g b = h₃ b) : IntervalIntegrable (fun (t : ℝ) => deriv g t / g t) MeasureTheory.volume a b ∧ ∫ (t : ℝ) in a..b, deriv g t / g t = Complex.log (g b) - Complex.log (g a)

Piecewise FTC telescope with three local functions (two interior breakpoints).

theorem ContourIntegral.ftc_telescope_closed_split_five {g h₁ h₂ h₃ h₄ h₅ : ℝ → ℂ} {a p₁ p₂ tₗ tᵣ p₃ b : ℝ} (hint₁ : IntervalIntegrable (fun (t : ℝ) => deriv h₁ t / h₁ t) MeasureTheory.volume a p₁) (hint₂ : IntervalIntegrable (fun (t : ℝ) => deriv h₂ t / h₂ t) MeasureTheory.volume p₁ p₂) (hint₃ : IntervalIntegrable (fun (t : ℝ) => deriv h₃ t / h₃ t) MeasureTheory.volume p₂ tₗ) (hint₄ : IntervalIntegrable (fun (t : ℝ) => deriv h₄ t / h₄ t) MeasureTheory.volume tᵣ p₃) (hint₅ : IntervalIntegrable (fun (t : ℝ) => deriv h₅ t / h₅ t) MeasureTheory.volume p₃ b) (h_ftc₁ : ∫ (t : ℝ) in a..p₁, deriv h₁ t / h₁ t = Complex.log (h₁ p₁) - Complex.log (h₁ a)) (h_ftc₂ : ∫ (t : ℝ) in p₁..p₂, deriv h₂ t / h₂ t = Complex.log (h₂ p₂) - Complex.log (h₂ p₁)) (h_ftc₃ : ∫ (t : ℝ) in p₂..tₗ, deriv h₃ t / h₃ t = Complex.log (h₃ tₗ) - Complex.log (h₃ p₂)) (h_ftc₄ : ∫ (t : ℝ) in tᵣ..p₃, deriv h₄ t / h₄ t = Complex.log (h₄ p₃) - Complex.log (h₄ tᵣ)) (h_ftc₅ : ∫ (t : ℝ) in p₃..b, deriv h₅ t / h₅ t = Complex.log (h₅ b) - Complex.log (h₅ p₃)) (h_ae₁ : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a p₁ → deriv g t / g t = deriv h₁ t / h₁ t) (h_ae₂ : ∀ᵐ (t : ℝ), t ∈ Set.uIoc p₁ p₂ → deriv g t / g t = deriv h₂ t / h₂ t) (h_ae₃ : ∀ᵐ (t : ℝ), t ∈ Set.uIoc p₂ tₗ → deriv g t / g t = deriv h₃ t / h₃ t) (h_ae₄ : ∀ᵐ (t : ℝ), t ∈ Set.uIoc tᵣ p₃ → deriv g t / g t = deriv h₄ t / h₄ t) (h_ae₅ : ∀ᵐ (t : ℝ), t ∈ Set.uIoc p₃ b → deriv g t / g t = deriv h₅ t / h₅ t) (h_ga : g a = h₁ a) (h_gp₁ : g p₁ = h₁ p₁) (h_gp₁' : g p₁ = h₂ p₁) (h_gp₂ : g p₂ = h₂ p₂) (h_gp₂' : g p₂ = h₃ p₂) (h_gtₗ : g tₗ = h₃ tₗ) (h_gtᵣ : g tᵣ = h₄ tᵣ) (h_gp₃ : g p₃ = h₄ p₃) (h_gp₃' : g p₃ = h₅ p₃) (h_gb : g b = h₅ b) (h_closed : h₁ a = h₅ b) : IntervalIntegrable (fun (t : ℝ) => deriv g t / g t) MeasureTheory.volume a tₗ ∧ IntervalIntegrable (fun (t : ℝ) => deriv g t / g t) MeasureTheory.volume tᵣ b ∧ (∫ (t : ℝ) in a..tₗ, deriv g t / g t) + ∫ (t : ℝ) in tᵣ..b, deriv g t / g t = Complex.log (g tₗ) - Complex.log (g tᵣ)

For a closed curve with a crossing gap, the FTC telescopes across five piecewise segments [a, p₁], [p₁, p₂], [p₂, tₗ] (left of gap) and [tᵣ, p₃], [p₃, b] (right of gap). Each segment has a local function satisfying FTC, and g agrees a.e. with each. The closed-curve condition h₁ a = h₅ b (implying g a = g b) means the outer log terms cancel, telescoping to log(g tₗ) - log(g tᵣ).