OAI/Analysis/AffineBernstein/GraphPatchArea.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.jacobian_geometric_mean_image_bound line 15
2. lemma OAI.AffineBernstein.det_fderiv_reciprocal_gradient line 45
3. lemma OAI.AffineBernstein.graph_area_jacobian_factor line 59
4. lemma OAI.AffineBernstein.graph_area_dominant_patch_bound line 80
5. theorem OAI.AffineBernstein.convexOn_of_hessian_posSemidef line 123

   Source documentation

   The standing positive-Hessian hypothesis implies genuine convexity on the original open convex domain; this is not an additional hypothesis.

   theorem convexOn_of_hessian_posSemidef {n : ℕ} {Ω : Set (Space n)}
       (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
       (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosSemidef) :
       ConvexOn ℝ Ω u := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian