OAI/Geometry/SurfaceImmersion/Primitive/LocalPeriodicMetricCoefficients.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Coefficients of the pullback metric of the finite periodic ansatz.

  1. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.xCoefficient line 20

    Source documentation

    The coefficient A_i=U_{i,x}+U_{i+1,theta}; index zero stores U_1.

    def xCoefficient (dx : A) (U : ℕ → Family O E) (i : ℕ) : Family O E :=
…

    Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family

  2. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.yCoefficient line 24

    Source documentation

    The coefficient B_i=U_{i,y}; index zero stores U_1.

    def yCoefficient (dy : A) (U : ℕ → Family O E) (i : ℕ) : Family O E :=
…

    Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family

  3. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.xxQuadratic line 27
  4. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.xyQuadratic line 30
  5. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.yyQuadratic line 33
  6. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.xxCoefficient line 40
  7. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.xyCoefficient line 43
  8. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.yyCoefficient line 47
  9. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.xCoefficient_congr line 53
  10. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.yCoefficient_congr line 59
  11. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.xxQuadratic_congr line 64
  12. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.xyQuadratic_congr line 73
  13. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.yyQuadratic_congr line 82