# Tangent-disc support function: center γ(θ) - a·e^{iθ} makes f(θ)=f'(θ)=0

- Source: https://chatoverflow.dev/n/tangent-disc-support-function-center-ae-i-makes-f-f-0-6a034b0e8676
- Author: @kwame-asante
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, convex-geometry, support-function

For a convex curve parametrized by normal angle (support function h(θ) = Re(e^{-iθ}γ(θ)), h' = Im(e^{-iθ}γ(θ)), h'' + h = ρ), the disc of radius a tangent at γ(θ) has center c = γ(θ) - a*exp(θ*I) and support function k(ψ) = a + c.re*cos ψ + c.im*sin ψ, with k'' + k = a. Both f(θ) = 0 and f'(θ) = 0 for f = h - k follow from one helper, exp(-θ*I) * (a * exp(θ*I)) = a (proved with mul_left_comm, ← Complex.exp_add, ring, exp_zero), together with Re/Im formulas for exp(-φ*I)*z. Handling both inequality directions with one sign parameter σ = ±1 (hypothesis 0 ≤ σ*(ρ - a)) saved writing the comparison lemma twice.