dslope as a parameter integral

For f : ℂ → ℂ differentiable on an open set and points c, w there, the divided slope dslope f c w is a fundamental-theorem-of-calculus average of the derivative of f along the segment [c, w] — on a convex set,

dslope f c w = ∫ t in 0..1, deriv f (c + t • (w - c)).

The representation unifies the two branches of dslope (deriv f c at c = w, the slope (f w - f c) / (w - c) otherwise) into a single integral that is manifestly continuous through the diagonal. From it we read off the analytic inputs the Dixon homology Cauchy theorem needs about the map (c, w) ↦ dslope f c w: joint continuity and a Cauchy bound on its w-derivative.

Main results

• TauCeti.dslope_eq_integral_deriv — the integral representation on an open convex set.
• TauCeti.continuousOn_dslope_prod — joint continuity of (c, w) ↦ dslope f c w on U ×ˢ U for arbitrary open U.
• TauCeti.continuousOn_dslope_first_arg — continuity of c ↦ dslope f c w₀ on open U.
• TauCeti.deriv_dslope_bounded_on_compact — a uniform bound on ‖deriv (dslope f c) w‖ for c in a compact subset of U and w near a point of U.

Provenance

Adapted from DslopeIntegral.lean in the AINTLIB LeanModularForms development. Prerequisite for the holomorphy of the Dixon dslope integral, hence for the homology Cauchy theorem and the generalized residue theorem on the roadmap.

theorem TauCeti.dslope_eq_integral_deriv {f : ℂ → ℂ} {U : Set ℂ} (hU : Convex ℝ U) (hU_open : IsOpen U) (hf : DifferentiableOn ℂ f U) {c w : ℂ} (hc : c ∈ U) (hw : w ∈ U) : dslope f c w = ∫ (t : ℝ) in 0..1, deriv f (c + t • (w - c))

The dslope integral representation on a convex open set: when f is differentiable on U and both c, w ∈ U (so the segment [c, w] ⊆ U), then dslope f c w equals the integral of the derivative of f along the segment.

theorem TauCeti.continuousOn_dslope_prod {f : ℂ → ℂ} {U : Set ℂ} (hU_open : IsOpen U) (hf : DifferentiableOn ℂ f U) : ContinuousOn (fun (p : ℂ × ℂ) => dslope f p.1 p.2) (U ×ˢ U)

Joint continuity of (c, w) ↦ dslope f c w on U ×ˢ U for f differentiable on an arbitrary open set U (no convexity assumption).

theorem TauCeti.continuousOn_dslope_first_arg {f : ℂ → ℂ} {U : Set ℂ} (hU_open : IsOpen U) (hf : DifferentiableOn ℂ f U) {w₀ : ℂ} (hw₀ : w₀ ∈ U) : ContinuousOn (fun (c : ℂ) => dslope f c w₀) U

Continuity of c ↦ dslope f c w₀ on any open set U (no convexity). Follows from continuousOn_dslope_prod by partial application.

theorem TauCeti.deriv_dslope_bounded_on_compact {f : ℂ → ℂ} {U : Set ℂ} (hU_open : IsOpen U) (hf : DifferentiableOn ℂ f U) {K_c : Set ℂ} (hK_compact : IsCompact K_c) (hK_sub : K_c ⊆ U) {w₀ : ℂ} (hw₀ : w₀ ∈ U) : ∃ C > 0, ∃ δ > 0, ∀ c ∈ K_c, ∀ w ∈ Metric.ball w₀ δ, ‖deriv (dslope f c) w‖ ≤ C

Uniform bound on deriv (dslope f c) w. For f differentiable on an open set U, with c ranging over a compact subset of U and w over a small ball around a point w₀ ∈ U, the norm ‖deriv (dslope f c) w‖ is bounded by a single constant.