EntireGlobalDet.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.sectionBalance_tangentShift line 16
theorem OAI.AffineBernstein.balanced_global_det_bounds line 29
Source documentation
Once genuine balance is produced, the whole Hessian determinant is bounded above and below by positive constants. The proof uses only that balance and the original affine maximal equation.
```
theorem balanced_global_det_bounds {n : ℕ} (hn : 1 ≤ n)
    {u : Space n → ℝ} (hu : ContDiff ℝ ∞ u) (hp : ∀ x, (hessian u x).PosDef)
    (hm : AffineMaximalOn univ u)
    {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hbal : SectionBalance univ u ρ) :
    ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ x, c ≤ (hessian u x).det ∧ (hessian u x).det ≤ C := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.SectionBalance

theorem OAI.AffineBernstein.affineMaximal_entire_global_det_bounds line 53

Source documentation

Further consequence of the unchanged EXACT main hypotheses: the domain is entire and its Hessian determinant has global positive lower and upper bounds. Quadratic rigidity is still a separate obligation.

theorem affineMaximal_entire_global_det_bounds {n : ℕ} (hn : 3 ≤ n) (hn9 : n ≤ 9)
    {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hne : Ω.Nonempty) (hcv : Convex ℝ Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
    (hc : EuclideanGraphComplete Ω u) :
    Ω = univ ∧ ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ x, c ≤ (hessian u x).det ∧ (hessian u x).det ≤ C := by
…

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