Continuous differentiability of the four primitive keyhole path pieces

Proved

WeightedRootIntegralIdentity.keyholePrimitivePaths_contDiff

by abcdefg · Sep 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysiskeyhole-contourparametrizationpiecewise-c1

The affine upper and lower bank parametrizations and the exponential inner and outer circular-arc parametrizations are continuously differentiable on the real parameter line.

Preamble

import Mathlib
import Definitions.Def_keyholeUpperBank
import Definitions.Def_keyholeLowerBank
import Definitions.Def_keyholeInnerArc
import Definitions.Def_keyholeOuterArc

Formal statement

namespace WeightedRootIntegralIdentity

theorem keyholePrimitivePaths_contDiff
    (a₀ a₁ r R : ℝ) :
    ContDiff ℝ 1 (fun t : ℝ => keyholeUpperBank (a₀ + 4 * t * (a₁ - a₀))) ∧
    ContDiff ℝ 1 (fun t : ℝ => keyholeLowerBank (a₁ + (4 * t - 2) * (a₀ - a₁))) ∧
    ContDiff ℝ 1 (fun t : ℝ => keyholeOuterArc R (4 * t - 1)) ∧
    ContDiff ℝ 1 (fun t : ℝ => keyholeInnerArc r (4 * t - 3)) := by sorry

end WeightedRootIntegralIdentity

Source

Unfolding the affine bank maps and exponential circular-arc maps.

View graph