OAI/Geometry/SurfaceImmersion/Primitive/PeriodicTriangularRecursion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.xxCoefficient_congr line 24
2. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.xyCoefficient_congr line 31
3. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.yyCoefficient_congr line 38
4. theorem OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.advance line 44

   Source documentation

   Add the next corrector while retaining every earlier coefficient.

   theorem advance (dx : A) (U : ℕ → Family A E) (r : ℕ) (hr : 0 < r)
       (hU : ∀ i p, average ((U i).val p) = 0) :
       ∃ W : ℕ → Family A E,
         (∀ i < r, W i = U i) ∧ (∀ i p, average ((W i).val p) = 0) ∧
         (g.xxCoefficient dx W r).fluct = 0 ∧
         (g.xyCoefficient dx W r).fluct = 0 ∧
         (g.yyCoefficient W (r + 1)).fluct = 0 ∧
         (∀ O : Set A, IsOpen O → (∀ i p, p ∈ O → (U i).val p = 0) →
           ∀ i p, p ∈ O → (W i).val p = 0) := by
   …

   Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family

5. theorem OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.exists_coefficients line 123

   Source documentation

   The finite recursion produces mean-zero smooth coefficients with no angle dependence in all prescribed lower metric coefficients.

   theorem exists_coefficients (dx : A) (n : ℕ) :
       ∃ U : ℕ → Family A E,
         U 0 = g.initial ∧ (∀ i p, average ((U i).val p) = 0) ∧
         (g.yyCoefficient U 1).fluct = 0 ∧
         (∀ O : Set A, IsOpen O → (∀ p ∈ O, g.initial.val p = 0) →
           ∀ i p, p ∈ O → (U i).val p = 0) ∧
         ∀ r, 1 ≤ r → r ≤ n →
           (g.xxCoefficient dx U r).fluct = 0 ∧
           (g.xyCoefficient dx U r).fluct = 0 ∧
           (g.yyCoefficient U (r + 1)).fluct = 0 := by
   …

   Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family