OAI/Geometry/NearbyLagrangian/AnalyticObstruction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Localized tube realization and restored endpoints under Hamiltonian isotopy.

  1. def OAI.NearbyLagrangian.Tubes.heightAxis line 18
  2. def OAI.NearbyLagrangian.Tubes.capEquator line 20
  3. lemma OAI.NearbyLagrangian.Tubes.heightAxis_norm line 25
  4. lemma OAI.NearbyLagrangian.Tubes.heightAxis_inner_capEquator line 28
  5. def OAI.NearbyLagrangian.Tubes.realizationFamily line 32
  6. def OAI.NearbyLagrangian.Tubes.HasRestoredEndpoint line 42
  7. theorem OAI.NearbyLagrangian.Tubes.source_analytic_obstruction line 65