Ehrhart volume inequality: Regularization

Regularization, descent, and positive-Hessian arguments.

theorem Ehrhart.JetEnvelopeTrueRadialHessian.hasDerivAt_intervalIntegral_of_joint_continuous (F F' : ℝ → ℝ → ℝ) (hF : Continuous (Function.uncurry F)) (hF' : Continuous (Function.uncurry F')) (hdiff : ∀ (x θ : ℝ), HasDerivAt (fun (r : ℝ) => F r θ) (F' x θ) x) (x₀ a b : ℝ) : HasDerivAt (fun (x : ℝ) => ∫ (θ : ℝ) in a..b, F x θ) (∫ (θ : ℝ) in a..b, F' x₀ θ) x₀

Differentiate a parameterized interval integral under joint continuity.