OAI/Analysis/AffineBernstein/ABPCriticalDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.linearizedMA_critical_density line 20

   Source documentation

   Critical density for a positive supersolution of the actual linearized Monge--Ampère operator. The touching paraboloid is replaced by the genuine convex tangent section, so no ellipticity-ratio bound is presupposed.

   theorem linearizedMA_critical_density {n : ℕ} {u s : Space n → ℝ}
       (hu : ContDiff ℝ ∞ u) (hs : ContDiff ℝ ∞ s)
       (hp : ∀ x, (hessian u x).PosDef)
       {a : Space n} {h ε R D : ℝ} (hh : 0 < h) (hε : 0 < ε) (hR : 0 < R)
       (hD : 0 ≤ D)
       (hK : IsCompact {x | tangentHeight u a x ≤ h})
       (hKR : {x | tangentHeight u a x ≤ h} ⊆ Metric.closedBall a R)
       (hspos : ∀ x, 0 ≤ s x) (hsa : s a ≤ ε)
       (hLs : ∀ x, inverseHessianTrace u s x ≤ 0)
       (hdet : ∀ x, tangentHeight u a x ≤ h → (hessian u x).det ≤ D) :
       volume (Metric.ball (0 : Space n) (1/(2*R))) ≤
         ENNReal.ofReal (D * (2*(n:ℝ)/h)^n) *
   …

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