OAI/Analysis/PathSelection/IdentityDetection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Analytic identity detection by strict submersions and pathwise eventual vanishing.

  1. def OAI.PathSelection.Detection.IsStrictSubmersionAt line 19
  2. lemma OAI.PathSelection.Detection.IsStrictSubmersionAt.continuousAt line 23
  3. lemma OAI.PathSelection.Detection.IsStrictSubmersionAt.map_nhds_eq line 28
  4. theorem OAI.PathSelection.Detection.nowhereDense_zeros_of_submersion line 35
  5. theorem OAI.PathSelection.Detection.eqOn_zero_of_integer_evaluations line 75
  6. theorem OAI.PathSelection.Detection.eqOn_zero_of_pathwise_eventually_zero line 96
  7. theorem OAI.PathSelection.Detection.eqOn_zero_of_analytic_evaluations line 110
  8. theorem OAI.PathSelection.Detection.family_zero_of_pathwise_eventually_zero line 126
  9. lemma OAI.PathSelection.Detection.IsStrictSubmersionAt.triangular line 143