OAI/Analysis/AffineBernstein/SupportArea.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.homogeneousSupport_gradient_monotone line 16
2. lemma OAI.AffineBernstein.shiftedGauss_injOn line 34

   Source comment

   The identity-shifted true Gauss map is injective wherever the support is smooth, even though the punctured domain is not convex.

   lemma shiftedGauss_injOn {K : Set (Space n)} (hK : IsCompact K) (hne : K.Nonempty)
       {D : Set (Space n)} (hD : ∀ x ∈ D, DifferentiableAt ℝ (homogeneousSupport K) x) :
       Set.InjOn (fun x => gradient (homogeneousSupport K) x + x) D := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.homogeneousSupport

3. lemma OAI.AffineBernstein.homogeneousSupport_second_nonneg line 45
4. lemma OAI.AffineBernstein.homogeneousSupport_hessian_posSemidef line 84