OAI/Analysis/AffineBernstein/HessianMinors.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.shiftedGradient_injOn_of_hessian_posSemidef line 15
2. theorem OAI.AffineBernstein.lintegral_hessian_minors_le_ball line 36

   Source comment

   One genuine change of variables for the shifted convex gradient bounds all the large principal minors at once. This is an alternative proof of the source principal-minor estimate, with every quantity the actual Hessian. It does not posit any Hessian or determinant bound.

   theorem lintegral_hessian_minors_le_ball {Ω : Set (Space n)}
       (hcv : Convex ℝ Ω) {u : Space n → ℝ}
       (hu : ∀ x ∈ Ω, ContDiffAt ℝ ∞ u x)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
       {D : Set (Space n)} (hD : MeasurableSet D) (hDO : D ⊆ Ω)
       {G R : ℝ} (hG : ∀ x ∈ D, ‖gradient u x‖ ≤ G)
       (hR : ∀ x ∈ D, ‖x‖ ≤ R) :
       (∫⁻ x in D, ENNReal.ofReal ((hessian u x).det * (1 + (hessian u x)⁻¹.trace))) ≤
         ((n:ℝ≥0∞)+1) * volume (Metric.closedBall (0:Space n) (G+R)) := by
   …

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