OAI/Analysis/AffineBernstein/AmbientImmersion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.parametricAreaDensity_volume_pullback line 16
2. theorem OAI.AffineBernstein.affineMaximal_ambient_immersed_local_stationary line 43

   Source comment

   Literal local affine stationarity in any ambient vector coordinates. The reference volume basis is transported exactly, not replaced by a coordinate-free area axiom.

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

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