OAI/Analysis/AffineBernstein/SmoothGraphChart.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.exists_smooth_local_diffeomorph line 14
2. lemma OAI.AffineBernstein.graph_projection_derivative_bijective line 55

   Source comment

   The graph projection of a smooth immersed parametrization of a graph has nonsingular derivative. This is the differential input to the local chart used in the support-coordinate stationarity calculation.

   lemma graph_projection_derivative_bijective {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 Ω)
       (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)) :
       Function.Bijective (fderiv ℝ (fun y => (X y).1) x) := by
   …

   Mentions: OAI.AffineBernstein.Space

3. theorem OAI.AffineBernstein.exists_smooth_graph_chart line 80