OAI/Analysis/AffineBernstein/LocalAreaStationarity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.affineMaximal_local_parametric_area_stationary line 15

   Source comment

   Literal affine area is stationary for every compact smooth local ambient variation, with any continuous inward normalized conormal/transverse choices. The equation on the original graph, not an ambient stationary axiom, is used.

   theorem affineMaximal_local_parametric_area_stationary {n : ℕ}
       {Ω K : Set (Space n)} (hΩ : IsOpen Ω) (hK : IsCompact K)
       (φ : OpenPartialHomeomorph (Space n) (Space n))
       (hφ : ContDiffOn ℝ ∞ φ φ.source) (hψ : ContDiffOn ℝ ∞ φ.symm φ.target)
       (hKφ : K ⊆ φ.source) (hφΩ : φ.target ⊆ Ω)
       {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
       {V : Space n → Space n × ℝ} (hV : ContDiffOn ℝ ∞ V φ.source)
       (hVK : tsupport V ⊆ K)
       (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ)
       (ν : ℝ → Space n → (Space n × ℝ) →L[ℝ] ℝ) (ξ : ℝ → Space n → Space n × ℝ)
       (hν : ∀ t x, x ∈ φ.source → (ν t x).comp
   …

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