OAI/Geometry/SurfaceImmersion/Primitive/PeriodicExpansionInit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The initial coefficient and its transverse cancellation in the periodic expansion.

  1. def OAI.ClosedSurfaceR4.PeriodicExpansion.Family.vectorMean line 20
  2. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.vectorMean_apply line 24
  3. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.centered_mean_zero line 28
  4. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.primitive_mem line 33
  5. def OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.initial line 47
  6. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.initial_mean_zero line 51
  7. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.initial_angle line 55
  8. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.initial_mem line 58
  9. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.initial_pairing line 64
  10. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.initial_transverse_derivative line 70

    Source documentation

    The yy coefficient at order one vanishes before higher correctors are added.

    lemma initial_transverse_derivative : g.transverse.inner (g.initial.slow v) = 0 := by
…