OAI/Analysis/AffineBernstein/FiberArea.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.sphere_support_cofactor_le_ball line 18

   Source comment

   The full cofactor trace is the genuine Euclidean angular area density of its smooth support function. Its spherical integral is bounded solely by the radius of the compact convex fiber. No surface-area estimate is assumed.

   theorem sphere_support_cofactor_le_ball {K : Set (Space n)} (hn : 1 ≤ n)
       (hK : IsCompact K) (hne : K.Nonempty)
       (hH : ∀ x : Space n, x ≠ 0 → ContDiffAt ℝ ∞ (homogeneousSupport K) x)
       {R : ℝ} (hR : ∀ y ∈ K, ‖y‖ ≤ R) :
       (∫⁻ e : Metric.sphere (0:Space n) 1,
         ENNReal.ofReal (hessian (homogeneousSupport K) e).adjugate.trace ∂volume.toSphere) ≤
         (n:ℝ≥0∞)^2 * volume (Metric.closedBall (0:Space n) (R+1)) := by
   …

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