OAI/Geometry/SurfaceImmersion/Primitive/LocalPeriodicMetricRemainder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.metricCoefficientFamily line 23
2. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.metricCoefficientFamily_apply line 28
3. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.xxRemainder line 44
4. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.xyRemainder line 47
5. def OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.yyRemainder line 50
6. theorem OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.exists_angle_independent_coefficients line 55

   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 O E,
         U 0 = g.initial ∧ (∀ i p, p ∈ O → average ((U i).val p) = 0) ∧
         (∀ Z : Set A, IsOpen Z → Z ⊆ O → (∀ p ∈ Z, g.initial.val p = 0) →
           ∀ i p, p ∈ Z → (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.LocalPeriodicExpansion.Family