OAI/Analysis/AffineBernstein/NormalizedFamilyDet.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.tangentHeight_tangentShift line 17
2. theorem OAI.AffineBernstein.normalized_balanced_det_bounds line 27

   Source documentation

   All normalized solutions have the same determinant bounds on the fixed inner ball. The constants precede the function; no local analytic estimate is postulated.

   theorem normalized_balanced_det_bounds {n : ℕ} {ρ R : ℝ}
       (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hR : 1 ≤ R) :
       ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ v : Space n → ℝ,
         ContDiff ℝ ∞ v → (∀ x, (hessian v x).PosDef) →
         AffineMaximalOn univ v → v 0=0 → fderiv ℝ v 0=0 →
         SectionBalance univ v ρ →
         Metric.ball 0 1 ⊆ tangentSection univ v 0 1 →
         tangentSection univ v 0 1 ⊆ Metric.ball 0 R →
         ∀ x ∈ Metric.ball (0:Space n) (1/8:ℝ),
           c ≤ (hessian v x).det ∧ (hessian v x).det ≤ C := by
   …

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