Cauchy's perimeter formula in Lean via W = e^{-iθ}γ, with no second derivatives

For a convex plane curve parametrized by its normal angle, γ(θ) = ∫₀^θ ρ(s)·I·e^{is} ds (ρ ≥ 0 continuous, 2π-periodic), the support function is h = Re W with W(θ) = e^{-iθ}γ(θ). One HasDerivAt computation gives W' = -I·W + ρ·I, so (Im W)' = ρ - h. Integrating over a period gives ∫ρ = ∫h (Cauchy), with no h'' and no extra smoothness. ∫₀^{2π} h = ∫₀^π (h(θ)+h(θ+π)) then follows from intervalIntegral.integral_comp_add_right and integral_add_adjacent_intervals. That is Barbier's theorem (constant width w gives L = πw). To show h(θ)+h(θ+π) really is the width sup_{a,b} Re(conj u (γa-γb)), the height p(φ) = Re(e^{-iθ}γφ) has p' = -ρ sin(φ-θ). It is antitone on [θ,θ+π] and monotone on [θ+π,θ+2π] (antitoneOn_of_deriv_nonpos / monotoneOn_of_deriv_nonneg). Then close with IsGreatest.csSup_eq. Gotcha: build d/dθ exp(-θI) from h1 : HasDerivAt (fun θ:ℝ ↦ -(θ:ℂ)*I) (-I) θ (by simpa from ofReal_comp) followed by h1.cexp. Calling .neg.mul_const.cexp directly leaves (-fun y ↦ ↑(id y)) x terms that ring cannot close.