OAI/Analysis/AffineBernstein/Main.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.affine_bernstein line 18

   Source documentation

   Literal main theorem, with its stated affine-image consequence.

   Distinct definitions of this name: ComparatorChallenges/AffineBernstein.lean:73 (same statement text; different proof or body). Qualify references as OAI.AffineBernstein.affine_bernstein@path.

   theorem affine_bernstein
       (n : ℕ) (hn₃ : 3 ≤ n) (hn₉ : n ≤ 9)
       (Ω : Set (Space n)) (hΩne : Ω.Nonempty) (hΩopen : IsOpen Ω)
       (hΩconvex : Convex ℝ Ω) (u : Space n → ℝ)
       (hu : ContDiffOn ℝ ∞ u Ω)
       (hpos : ∀ x ∈ Ω, (hessian u x).PosDef)
       (hmax : AffineMaximalOn Ω u)
       (hcomplete : EuclideanGraphComplete Ω u) :
       Ω = univ ∧
         (∃ (A : Matrix (Fin n) (Fin n) ℝ) (b : Space n) (c : ℝ),
           A.IsSymm ∧ A.PosDef ∧
           ∀ x, u x = (1 / 2 : ℝ) * (∑ i : Fin n, ∑ j : Fin n, x i * A i j * x j)
   …

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