convexOn_sinh_Ici
plain-language theorem explainer
Convexity of the hyperbolic sine on the non-negative reals supplies the sublinear bound needed for perturbation control in annular cost estimates. Workers on meromorphic phase charges in the Recognition Science setting cite it when decomposing increments into pure winding plus regular-factor error. The proof applies the standard derivative-monotonicity criterion after checking continuity and differentiability of sinh.
Claim. The function $f(x) = sinh(x)$ is convex on the interval $[0, ∞)$.
background
The MeromorphicCircleOrder module bridges Mathlib meromorphic-order machinery to the RS annular cost framework. It records that a meromorphic function with order n at ρ factors locally as (z−ρ)^n · g(z) with g holomorphic and non-vanishing, yielding additive phase charges that match DefectSensor.charge for ζ^{-1} at zeros. Upstream structures establish that J-cost minimization is strictly convex with global minimum at unity and that physical quantities occupy discrete φ-tiers.
proof idea
The term proof invokes MonotoneOn.convexOn_of_deriv on the closed interval [0, ∞). It supplies the required continuity of sinh on the closed set, differentiability on the interior, and monotonicity of the derivative cosh on the interior by reducing to the known strict increase of cosh.
why it matters
The lemma is invoked directly by the sibling sinh_mul_le_mul_sinh to obtain sinh(t x) ≤ t sinh(x) for t ∈ [0,1]. This sublinearity keeps regular-factor perturbations summable in the log φ scale, closing the analytic input required for canonicalDefectSampledFamily_ringPerturbationControl and for phase-charge calculations that align with the convex J-cost and eight-tick octave of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.