OAI/Analysis/AffineBernstein/GlobalGraphChart.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.exists_smooth_global_diffeomorph line 16

   Source comment

   A one-to-one smooth local diffeomorphism on an open set gives a single global smooth partial chart.

   lemma exists_smooth_global_diffeomorph {E : Type*}
       [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
       [FiniteDimensional ℝ E] {U V : Set E} (hU : IsOpen U) (hV : IsOpen V)
       {f : E → E} (hf : ContDiffOn ℝ ∞ f U) (him : MapsTo f U V)
       (hi : Set.InjOn f U) (hd : ∀ x ∈ U, Function.Bijective (fderiv ℝ f x)) :
       ∃ φ : OpenPartialHomeomorph E E, φ.source = U ∧ φ.target = f '' U ∧
         φ.target ⊆ V ∧ (φ : E → E) = f ∧ ContDiffOn ℝ ∞ φ φ.source ∧
         ContDiffOn ℝ ∞ φ.symm φ.target := by
   …

2. theorem OAI.AffineBernstein.exists_smooth_global_graph_chart line 63

   Source comment

   A globally injective immersion into an actual graph admits a global smooth graph chart on its entire open parameter domain.

   theorem exists_smooth_global_graph_chart {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)
       (hi : Set.InjOn (fun x => (X x).1) U)
       (hd : ∀ x ∈ U, Function.Injective (fderiv ℝ X x)) :
       ∃ φ : OpenPartialHomeomorph (Space n) (Space n), φ.source = U ∧
         φ.target ⊆ Ω ∧ (∀ y ∈ U, X y = (φ y,u (φ y))) ∧
         ContDiffOn ℝ ∞ φ φ.source ∧ ContDiffOn ℝ ∞ φ.symm φ.target := by
   …

   Mentions: OAI.AffineBernstein.Space