OAI/Geometry/SurfaceImmersion/Atlas/CenteredAtlasDifferentials.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Centered quadratic phase covectors expressed through actual chart transitions, with the Jacobian nondegeneracy needed for parameter selection.

  1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centered_phaseDerivative_comp line 14
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.coordinateTransition_det_ne line 26
  3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.actual_centered_phase_differential line 34
  4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.actual_centered_phase_at line 45