OAI/Analysis/AffineBernstein/SupportAnnulus.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.toMatrix_fderiv_gradient_eq_hessian_transpose line 15
2. lemma OAI.AffineBernstein.det_fderiv_shiftedGradient line 28
3. lemma OAI.AffineBernstein.lintegral_support_cofactor_le_ball line 50

   Source comment

   On any bounded measurable annular set, the cofactor trace of the literal support Hessian has a bound depending only on the radius of the convex fiber. The proof uses the injective shifted Gauss map and genuine change of variables.

   lemma lintegral_support_cofactor_le_ball {K D : Set (Space n)}
       (hK : IsCompact K) (hne : K.Nonempty) (hD : MeasurableSet D)
       (hH : ∀ x ∈ D, ContDiffAt ℝ ∞ (homogeneousSupport K) x)
       {R r : ℝ} (hR : ∀ y ∈ K, ‖y‖ ≤ R) (hr : ∀ x ∈ D, ‖x‖ ≤ r) :
       (∫⁻ x in D, ENNReal.ofReal (hessian (homogeneousSupport K) x).adjugate.trace) ≤
         (n : ℝ≥0∞) * volume (Metric.closedBall (0 : Space n) (R+r)) := by
   …

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