OAI/Analysis/AffineBernstein/ConvexSmoothMax.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.hessian_sub_on line 15
2. lemma OAI.AffineBernstein.hessian_convex_smooth_max line 24
3. lemma OAI.AffineBernstein.posDef_convex_combination line 48
4. lemma OAI.AffineBernstein.hessian_convex_smooth_max_posDef line 56
5. def OAI.AffineBernstein.capQuadratic line 72

   Source documentation

   The exact quadratics used in the positive-cap comparison.

   def capQuadratic {n : ℕ} (c : Space n) (b α : ℝ) (x : Space n) : ℝ :=
   …

   Mentions: OAI.AffineBernstein.Space

6. lemma OAI.AffineBernstein.capQuadratic_smooth line 75
7. lemma OAI.AffineBernstein.dirDeriv_capQuadratic line 81
8. lemma OAI.AffineBernstein.hessian_capQuadratic line 89
9. lemma OAI.AffineBernstein.hessian_capQuadratic_posDef line 106
10. lemma OAI.AffineBernstein.affineAreaDensity_capQuadratic line 111