OAI/Geometry/SurfaceImmersion/Primitive/LocalPeriodicTriangularRecursion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.xxCoefficient_congr line 25
2. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.xyCoefficient_congr line 32
3. lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.yyCoefficient_congr line 39
4. theorem OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.advance line 45

   Source documentation

   Add the next corrector while retaining every earlier coefficient.

   theorem advance (dx : A) (U : ℕ → Family O E) (r : ℕ) (hr : 0 < r)
       (hU : ∀ i p, p ∈ O → average ((U i).val p) = 0) :
       ∃ W : ℕ → Family O E,
         (∀ i < r, W i = U i) ∧ (∀ i p, p ∈ O → 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 ∧
         (∀ Z : Set A, IsOpen Z → Z ⊆ O → (∀ i p, p ∈ Z → (U i).val p = 0) →
           ∀ i p, p ∈ Z → (W i).val p = 0) := by
   …

   Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family

5. theorem OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.exists_coefficients line 124

   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 O E,
         U 0 = g.initial ∧ (∀ i p, p ∈ O → average ((U i).val p) = 0) ∧
         (g.yyCoefficient U 1).fluct = 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, 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.LocalPeriodicExpansion.Family