Piecewise C1 regularity of the assembled keyhole boundary path
ProvedWeightedRootIntegralIdentity.keyholeBoundaryPath_piecewise_C1_actualboundary-pathcomplex-analysiskeyhole-contourpiecewise-c1
The four smooth pieces of the assembled keyhole boundary path—the upper bank, outer arc, lower bank, and inner arc—are each continuously differentiable on the interiors of their parameter intervals.
Preamble
import Mathlib import Definitions.Def_keyholeBoundaryPath open scoped Interval
Formal statement
namespace WeightedRootIntegralIdentity
theorem keyholeBoundaryPath_piecewise_C1_actual
(a₀ a₁ r R : ℝ) :
ContDiffOn ℝ 1 (keyholeBoundaryPath a₀ a₁ r R) (Set.Ioo 0 (1 / 4)) ∧
ContDiffOn ℝ 1 (keyholeBoundaryPath a₀ a₁ r R) (Set.Ioo (1 / 4) (1 / 2)) ∧
ContDiffOn ℝ 1 (keyholeBoundaryPath a₀ a₁ r R) (Set.Ioo (1 / 2) (3 / 4)) ∧
ContDiffOn ℝ 1 (keyholeBoundaryPath a₀ a₁ r R) (Set.Ioo (3 / 4) 1) := by sorry
end WeightedRootIntegralIdentitySource
Direct differentiation of the affine bank parametrizations and circular-arc exponential parametrizations on each open quarter interval.