OAI/Analysis/AffineBernstein/BaseConcavity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.support_base_hessian_neg line 18

   Source comment

   Strict curvature of the actual level hypersurface forces strict concavity of its support value in the base variables.

   theorem support_base_hessian_neg {F : S × E → ℝ} {Y : S → E} {s : S} {e : E} {lam : ℝ}
       (hF : ContDiffAt ℝ ∞ F (s,Y s)) (hY : ContDiffAt ℝ ∞ Y s)
       (hlevel : (fun r => F (r,Y r)) =ᶠ[𝓝 s] (fun _ => (0 : ℝ)))
       (hlam : 0 < lam)
       (hconormal : ∀ z : E, fderiv ℝ F (s,Y s) (0,z) = lam * inner ℝ e z)
       (hcurv : ∀ z : S × E, z ≠ 0 → fderiv ℝ F (s,Y s) z = 0 →
         0 < fderiv ℝ (fderiv ℝ F) (s,Y s) z z)
       {v : S} (hv : v ≠ 0) :
       fderiv ℝ (fderiv ℝ (fun r => inner ℝ e (Y r))) s v v < 0 := by
   …