OAI/Analysis/AffineBernstein/DetInteriorBall.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.normalized_det_interior_ball_producer line 19

   Source documentation

   Uniform two-sided determinant estimates throughout the smaller ball, with constants independent of both solution and evaluation point. This supplies the first regularity stage, but still not uniform ellipticity.

   theorem normalized_det_interior_ball_producer (n : ℕ) (b : ℝ → ℝ)
       (hb : ∀ r : ℝ, 0 < r → 0 < b r) :
       ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ f : Space n → ℝ,
         ContDiffOn ℝ ∞ f (Metric.ball 0 (1/4 : ℝ)) →
         (∀ x ∈ Metric.ball (0 : Space n) (1/4 : ℝ), (hessian f x).PosDef) →
         AffineMaximalOn (Metric.ball 0 (1/4 : ℝ)) f →
         (∀ x ∈ Metric.ball (0 : Space n) (1/4 : ℝ), -1 ≤ f x ∧ f x ≤ 0) →
         HasLowerSectionModulus (Metric.ball 0 (1/4 : ℝ)) f b →
         ∀ a ∈ Metric.ball (0 : Space n) (1/8 : ℝ),
           c ≤ (hessian f a).det ∧ (hessian f a).det ≤ C := by
   …

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