OAI/Analysis/AffineBernstein/ParametricChoiceTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.affineParametric_conormal_null line 12
2. theorem OAI.AffineBernstein.coordinateAffineVariationArea_choices line 33

   Source comment

   The ambient conormal/transverse choices in the local chart stationarity functional may be replaced by any other inward normalized choices.

   theorem coordinateAffineVariationArea_choices {n : ℕ}
       {Ω U : Set (Space n)} (hΩ : IsOpen Ω) (hU : IsOpen U)
       {u β : Space n → ℝ} {a : Fin n → Space n → ℝ}
       (hu : ContDiffOn ℝ ∞ u Ω) (hβ : ContDiff ℝ ∞ β)
       (ha : ∀ k, ContDiff ℝ ∞ (a k))
       (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ)
       {φ : Space n → Space n} (hφ : ContDiffOn ℝ ∞ φ U) (hφΩ : φ '' U ⊆ Ω)
       {x : Space n} (hx : x ∈ U) (hφJ : (parametricJacobian φ x).det ≠ 0) (t : ℝ)
       (hJ : (graphVariationJacobian a (t,φ x)).det ≠ 0)
       (hH : 0 ≤ (graphVariationSecond u β a (t,φ x)).det)
       (ν : (Space n × ℝ) →L[ℝ] ℝ) (ξ : Space n × ℝ)
       (hν : ν.comp (fderiv ℝ ((fun y => L (graphParamVariation u β a t y)+v) ∘ φ) x) = 0)
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.parametricJacobian, OAI.AffineBernstein.graphVariationJacobian, OAI.AffineBernstein.graphVariationSecond, OAI.AffineBernstein.graphParamVariation