OAI/Analysis/AffineBernstein/ImmersionStationary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.parametricFrame_derivative_injective line 15
2. theorem OAI.AffineBernstein.affineMaximal_immersed_graph_local_stationary line 39

   Source comment

   Local stationarity on an arbitrary immersed parametrization of the actual solution graph. The smooth inverse chart is produced by the inverse function theorem, not included among the hypotheses.

   theorem affineMaximal_immersed_graph_local_stationary {n : ℕ}
       {U Ω : Set (Space n)} (hU : IsOpen U) (hΩ : IsOpen Ω)
       {X : Space n → Space n × ℝ} {u : Space n → ℝ}
       (hX : ContDiffOn ℝ ∞ X U) (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
       (him : ∀ y ∈ U, (X y).1 ∈ Ω ∧ (X y).2 = u (X y).1)
       {x₀ : Space n} (hx₀ : x₀ ∈ U) (hi : Function.Injective (fderiv ℝ X x₀))
       (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ) :
       ∃ W : Set (Space n), IsOpen W ∧ x₀ ∈ W ∧ W ⊆ U ∧
         ∀ (K : Set (Space n)), IsCompact K → K ⊆ W →
         ∀ (V : Space n → Space n × ℝ), ContDiffOn ℝ ∞ V W → tsupport V ⊆ K →
         ∀ (ν : ℝ → Space n → (Space n × ℝ) →L[ℝ] ℝ) (ξ : ℝ → Space n → Space n × ℝ),
   …

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