OAI/Analysis/AffineBernstein/ParametricChartStationarity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.affineMaximal_coordinate_parametric_area_stationary line 15

   Source comment

   The stationarity functional in any smooth nonsingular injective coordinate chart. The change of variables uses the literal Lebesgue Jacobian, and positivity for the full parameter family is derived uniformly from the original Hessian.

   theorem affineMaximal_coordinate_parametric_area_stationary {n : ℕ}
       {Ω K : Set (Space n)} (hΩ : IsOpen Ω) (hK : IsCompact K)
       {φ : Space n → Space n} (hφ : ∀ x ∈ K, ContDiffAt ℝ ∞ φ x)
       (hinj : InjOn φ K) (hφJ : ∀ x ∈ K, (parametricJacobian φ x).det ≠ 0)
       (hKΩ : φ '' K ⊆ Ω) {u β : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
       (hβ : ContDiff ℝ ∞ β) (hβK : tsupport β ⊆ φ '' K)
       {a : Fin n → Space n → ℝ} (ha : ∀ k, ContDiff ℝ ∞ (a k))
       (haK : ∀ k, tsupport (a k) ⊆ φ '' K)
       (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ) :
       HasDerivAt (fun t : ℝ => ∫ x in K, coordinateAffineVariationArea L v φ u β a x t) 0 0 := by
   …

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