Parametric Differentiation for Homotopy Integrals

Lemmas for differentiating contour integrals under a C² homotopy parameter, including the Schwarz theorem for mixed partial derivatives and the key vanishing-derivative result used in homotopy invariance of contour integrals.

Main Results

• intervalIntegral_continuous_on_param — continuity of a parametric interval integral
• schwarz_partialDeriv_comm — mixed partials of a C² function commute
• hasDerivAt_homotopy_integral_zero — derivative of the homotopy integral vanishes when boundary s-derivatives are zero

theorem intervalIntegral_continuous_on_param (f : ℝ → ℝ → ℂ) (a b : ℝ) (S : Set ℝ) (hab : a ≤ b) (hf_cont : Continuous fun (p : ℝ × ℝ) => f p.1 p.2) (_hf_int : ∀ s ∈ S, IntervalIntegrable (fun (x : ℝ) => f x s) MeasureTheory.volume a b) : ContinuousOn (fun (s : ℝ) => ∫ (t : ℝ) in a..b, f t s) S

Continuity of a parametric interval integral.

theorem contDiff_partialDeriv_snd_of_contDiff_two (H : ℝ × ℝ → ℂ) (hH : ContDiff ℝ 2 H) : ContDiff ℝ 1 fun (p : ℝ × ℝ) => deriv (fun (s : ℝ) => H (p.1, s)) p.2

theorem contDiff_partialDeriv_fst_of_contDiff_two (H : ℝ × ℝ → ℂ) (hH : ContDiff ℝ 2 H) : ContDiff ℝ 1 fun (p : ℝ × ℝ) => deriv (fun (t : ℝ) => H (t, p.2)) p.1

theorem schwarz_partialDeriv_comm (H : ℝ × ℝ → ℂ) (hH : ContDiff ℝ 2 H) (t s : ℝ) : deriv (fun (s' : ℝ) => deriv (fun (t' : ℝ) => H (t', s')) t) s = deriv (fun (t' : ℝ) => deriv (fun (s' : ℝ) => H (t', s')) s) t

Schwarz theorem: mixed partials of a C² function commute.

Shared differentiability helpers for homotopy decomposition

Helpers for hasDerivAt_homotopy_param

Helpers for hasDerivAt_homotopy_integral_zero

theorem hasDerivAt_homotopy_integral_zero (f : ℂ → ℂ) (H : ℝ × ℝ → ℂ) (a b s : ℝ) (hab : a < b) (hH_smooth : ContDiff ℝ 2 H) (hf_diff : ∀ t ∈ Set.Icc a b, ∀ s' ∈ Set.Icc 0 1, DifferentiableAt ℂ f (H (t, s'))) (hfH_cont : Continuous (f ∘ H)) (hs : s ∈ Set.Icc 0 1) (hderiv_a : deriv (fun (s' : ℝ) => H (a, s')) s = 0) (hderiv_b : deriv (fun (s' : ℝ) => H (b, s')) s = 0) (hf_differentiable : Differentiable ℂ f) : HasDerivAt (fun (s' : ℝ) => ∫ (t : ℝ) in a..b, f (H (t, s')) * deriv (fun (t' : ℝ) => H (t', s')) t) 0 s

Derivative of the homotopy integral vanishes.