OAI/Geometry/SurfaceImmersion/Primitive/PeriodicMetricRemainder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.PeriodicExpansion.metricCoefficientFamily line 18
2. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.metricCoefficientFamily_apply line 23
3. def OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.xxRemainder line 39
4. def OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.xyRemainder line 42
5. def OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.yyRemainder line 45
6. theorem OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.exists_angle_independent_coefficients line 50

   Source documentation

   Every finite construction has jointly smooth remainder coefficients. The prescribed lower coefficients are independent of the fast angle.

   theorem exists_angle_independent_coefficients (dx : A) (L : ℕ) :
       ∃ U : ℕ → Family A E,
         U 0 = g.initial ∧ (∀ i p, average ((U i).val p) = 0) ∧
         (∀ O : Set A, IsOpen O → (∀ p ∈ O, g.initial.val p = 0) →
           ∀ i p, p ∈ O → (U i).val p = 0) ∧
         ∀ r, 0 < r → r < L → ∀ p t,
           (g.xxRemainder dx U L r).val p t = average ((g.xxCoefficient dx U r).val p) ∧
           (g.xyRemainder dx U L r).val p t = average ((g.xyCoefficient dx U r).val p) ∧
           (g.yyRemainder U L r).val p t = average ((g.yyCoefficient U r).val p) := by
   …

   Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family