OAI/Geometry/NearbyLagrangian/RealizationFamilies.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Smooth coupled generating families, their primitives and compact images.

  1. def OAI.NearbyLagrangian.EmbeddedRealization.sourceFamily line 25
  2. theorem OAI.NearbyLagrangian.EmbeddedRealization.contMDiff_sourceFamily line 32
  3. lemma OAI.NearbyLagrangian.EmbeddedRealization.norm_gradient_eq_norm_fderiv line 54
  4. lemma OAI.NearbyLagrangian.EmbeddedRealization.gradient_eq_smul_iff line 59
  5. theorem OAI.NearbyLagrangian.EmbeddedRealization.sourceFamily_critical_iff line 73
  6. theorem OAI.NearbyLagrangian.EmbeddedRealization.sourceFamily_eq_outside line 101
  7. theorem OAI.NearbyLagrangian.EmbeddedRealization.radialSolution_sourceFamily_critical line 109
  8. def OAI.NearbyLagrangian.EmbeddedRealization.sourceGeneratingMap line 134
  9. theorem OAI.NearbyLagrangian.EmbeddedRealization.contMDiff_sourceGeneratingMap line 142
  10. theorem OAI.NearbyLagrangian.EmbeddedRealization.sourceGeneratingMap_primitive line 157
  11. theorem OAI.NearbyLagrangian.EmbeddedRealization.isCompact_range_sourceGeneratingMap line 186