ConstantDet.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.balanced_bounded_harmonic_constant line 17
theorem OAI.AffineBernstein.balanced_affineMaximal_constant_det line 40
Source documentation
Constant determinant is produced by the original equation and actual balanced normalization family, rather than inserted as a hypothesis.
```
theorem balanced_affineMaximal_constant_det {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 ρ) :
    ∀ x y, (hessian u x).det=(hessian u y).det := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.SectionBalance
theorem OAI.AffineBernstein.affineMaximal_entire_and_constant_det line 67
Source documentation
Consequence of every unchanged main hypothesis: the domain is all of space and the full Hessian determinant is one positive constant. The remaining Jörgens--Calabi--Pogorelov rigidity is not claimed here.
```
theorem affineMaximal_entire_and_constant_det {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 ∧ ∃ D : ℝ, 0 < D ∧ ∀ x, (hessian u x).det=D := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.EuclideanGraphComplete