FTC for Log-Derivative Integrals

Fundamental theorem of calculus for integrals of f'/f along curves, generalizing the specific computations used in winding number calculations.

Main results

• intervalIntegrable_logDeriv_of_slitPlane - ∫ f'/f is interval integrable when f stays in slitPlane
• integral_logDeriv_eq_log_sub - ∫ f'/f = log f(b) - log f(a) when f stays in slitPlane
• ftc_log_on_segment - combined integrability + FTC for a single C¹ function in slitPlane
• ftc_log_neg_on_segment - combined integrability + FTC when -f stays in slitPlane
• ftc_log_piece - combined integrability + FTC when f and g agree a.e. (generalizes Common.lean version)

Basic integrability and FTC for C¹ curves staying in the slit plane

theorem LogDerivFTC.intervalIntegrable_logDeriv_of_slitPlane {f : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hf_cont : ContinuousOn f (Set.Icc a b)) (hf_deriv_cont : ContinuousOn (deriv f) (Set.Icc a b)) (hf_slit : ∀ t ∈ Set.Icc a b, f t ∈ Complex.slitPlane) : IntervalIntegrable (fun (t : ℝ) => deriv f t / f t) MeasureTheory.volume a b

If f : ℝ → ℂ is C¹ on [a,b] with f(t) ∈ slitPlane for all t ∈ [a,b], then the log-derivative t ↦ deriv f t / f t is interval integrable on [a,b].

theorem LogDerivFTC.integral_logDeriv_eq_log_sub {f : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hf_cont : ContinuousOn f (Set.Icc a b)) (hf_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ f t) (hf_deriv_cont : ContinuousOn (deriv f) (Set.Icc a b)) (hf_slit : ∀ t ∈ Set.Icc a b, f t ∈ Complex.slitPlane) : ∫ (t : ℝ) in a..b, deriv f t / f t = Complex.log (f b) - Complex.log (f a)

Fundamental theorem of calculus for log-derivative integrals: If f : ℝ → ℂ is differentiable on (a,b) with derivative continuous on [a,b], and f(t) ∈ slitPlane for all t ∈ [a,b], then ∫ t in a..b, deriv f t / f t = Complex.log (f b) - Complex.log (f a).

Combined integrability + FTC for a.e.-equal pairs of curves

This is the general version of ftc_log_piece from ValenceFormula.WindingWeights.Common, allowing g to differ from f on a null set (e.g. finitely many points).

theorem LogDerivFTC.ftc_log_piece {g h : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hh_cont : ContinuousOn h (Set.Icc a b)) (hh_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ h t) (hh_deriv_cont : ContinuousOn (deriv h) (Set.Icc a b)) (hh_slit : ∀ t ∈ Set.Icc a b, h t ∈ Complex.slitPlane) (heq : ∀ t ∈ Set.Ioo a b, g t = h t ∧ deriv g t = deriv h t) (heq_a : g a = h a) (heq_b : 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)

Combined integrability and FTC for log-derivative integrals.

Given a "reference" function h (C¹ with values in slitPlane) and a function g that agrees with h on (a,b) up to a null set (with matching endpoint values), both ∫ g'/g and ∫ h'/h are interval integrable and equal Complex.log(g b) - Complex.log(g a).

This generalizes the ftc_log_piece lemma in ValenceFormula.WindingWeights.Common to the setting where h serves as the smooth comparison function.

theorem LogDerivFTC.ftc_log_on_segment {f : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hf_cont : ContinuousOn f (Set.Icc a b)) (hf_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ f t) (hf_deriv_cont : ContinuousOn (deriv f) (Set.Icc a b)) (hf_slit : ∀ t ∈ Set.Icc a b, f t ∈ Complex.slitPlane) : IntervalIntegrable (fun (t : ℝ) => deriv f t / f t) MeasureTheory.volume a b ∧ ∫ (t : ℝ) in a..b, deriv f t / f t = Complex.log (f b) - Complex.log (f a)

Combined integrability and FTC for a single C¹ function staying in slitPlane.

Returns both IntervalIntegrable (f'/f) and ∫ f'/f = log(f(b)) - log(f(a)). This is the direct-function version of ftc_log_piece (no g/h a.e.-equal pair needed).

theorem LogDerivFTC.ftc_log_neg_on_segment {f : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hf_cont : ContinuousOn f (Set.Icc a b)) (hf_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ f t) (hf_deriv_cont : ContinuousOn (deriv f) (Set.Icc a b)) (hf_slit : ∀ t ∈ Set.Icc a b, -f t ∈ Complex.slitPlane) : IntervalIntegrable (fun (t : ℝ) => deriv f t / f t) MeasureTheory.volume a b ∧ ∫ (t : ℝ) in a..b, deriv f t / f t = Complex.log (-f b) - Complex.log (-f a)

Combined integrability and FTC when -f stays in slitPlane.

Returns both IntervalIntegrable (f'/f) and ∫ f'/f = log(-f(b)) - log(-f(a)). This is the negation variant of ftc_log_on_segment.

theorem LogDerivFTC.integral_logDeriv_eq_neg_log_sub {f : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hf_cont : ContinuousOn f (Set.Icc a b)) (hf_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ f t) (hf_deriv_cont : ContinuousOn (deriv f) (Set.Icc a b)) (hf_neg_slit : ∀ t ∈ Set.Icc a b, -f t ∈ Complex.slitPlane) : ∫ (t : ℝ) in a..b, deriv f t / f t = Complex.log (-f b) - Complex.log (-f a)

FTC for log-derivative when the negated function stays in slitPlane: ∫ f'/f = log(-f(b)) - log(-f(a)) when -f ∈ slitPlane on [a,b].