OAI/Analysis/Mahler/RegularLevelCharts.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MahlerStokes.levelCoordinates line 15

   Source documentation

   Replace the k-th coordinate by the potential itself.

   def levelCoordinates {d : ℕ} (g : (Fin d → ℝ) → ℝ) (k : Fin d)
       (x : Fin d → ℝ) : Fin d → ℝ := Function.update x k (g x)

2. def OAI.MahlerStokes.levelDerivative line 18
3. lemma OAI.MahlerStokes.levelDerivative_apply line 22
4. lemma OAI.MahlerStokes.exists_nonzero_coordinate line 27
5. lemma OAI.MahlerStokes.levelDerivative_injective line 39
6. def OAI.MahlerStokes.levelDerivativeEquiv line 61
7. lemma OAI.MahlerStokes.hasFDerivAt_levelCoordinates line 68
8. lemma OAI.MahlerStokes.contDiffAt_levelCoordinates line 78
9. theorem OAI.MahlerStokes.exists_regular_level_chart line 89

   Source documentation

   A genuine C2 chart flattening a regular level. No boundary decomposition is assumed.

   theorem exists_regular_level_chart {d : ℕ} {g : (Fin d → ℝ) → ℝ}
       {x : Fin d → ℝ} (hg : ContDiffAt ℝ 2 g x) (hreg : fderiv ℝ g x ≠ 0) :
       ∃ (k : Fin d) (e : OpenPartialHomeomorph (Fin d → ℝ) (Fin d → ℝ)),
         x ∈ e.source ∧ (∀ z, e z = levelCoordinates g k z) ∧
         ContDiffOn ℝ 2 e e.source ∧ ContDiffOn ℝ 2 e.symm e.target := by
   …

   Mentions: OAI.MahlerStokes.levelCoordinates