OAI/Analysis/AffineBernstein/LocalDet.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.affineMaximal_det_upper_of_section_control line 20

   Source documentation

   A quantitative determinant upper producer using only one finite section modulus and the original PDE. In particular the Hessian determinant is an output, not an ellipticity hypothesis.

   lemma affineMaximal_det_upper_of_section_control {n : ℕ} {O : Set (Space n)}
       (hO : IsOpen O) (hcv : Convex ℝ O) {f : Space n → ℝ}
       (hf : ContDiffOn ℝ ∞ f O) (hp : ∀ x ∈ O, (hessian f x).PosDef)
       (hm : AffineMaximalOn O f) {a : Space n} {r h M : ℝ}
       (hr : 0 < r) (hh : 0 < h) (hM : 0 ≤ M)
       (hball : Metric.closedBall a (2*r) ⊆ O)
       (hb : ∀ x ∈ O, |f x| ≤ M)
       (hsection : tangentSection O f a (2*h) ⊆ Metric.ball a r) :
       (hessian f a).det ≤
         (2*(n:ℝ)*(((n:ℝ)+2)*(2*((4*M/r)^2+1))+(4*M/r)^2))^n * h^2 *
           Real.exp ((4*M/r)^2/(4*((4*M/r)^2+1))) / h^(n+2) := by
   …

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