OAI/Geometry/SurfaceImmersion/Primitive/PeriodicMetricCoefficients.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Coefficients of the pullback metric of the finite periodic ansatz.

  1. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.inner_add_left line 19
  2. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.inner_add_right line 24
  3. def OAI.ClosedSurfaceR4.PeriodicExpansion.xCoefficient line 31

    Source documentation

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

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

    Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family

  4. def OAI.ClosedSurfaceR4.PeriodicExpansion.yCoefficient line 35

    Source documentation

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

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

    Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family

  5. def OAI.ClosedSurfaceR4.PeriodicExpansion.xxQuadratic line 38
  6. def OAI.ClosedSurfaceR4.PeriodicExpansion.xyQuadratic line 41
  7. def OAI.ClosedSurfaceR4.PeriodicExpansion.yyQuadratic line 44
  8. def OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.xxCoefficient line 51
  9. def OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.xyCoefficient line 54
  10. def OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.yyCoefficient line 58
  11. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.xCoefficient_congr line 64
  12. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.yCoefficient_congr line 70
  13. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.xxQuadratic_congr line 75
  14. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.xyQuadratic_congr line 84
  15. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.yyQuadratic_congr line 93