LocalFinitePeriodicExpansion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact finite periodic expansion with angle-independent lower metric terms.

lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.replace_low_sum line 18

theorem OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.finite_periodic_expansion line 43

Source documentation

The exact finite expansion of the actual pullback metric. This asserts smooth periodic coefficients and removes every low-order oscillation; it does not yet assert the higher-jet order and uniform remainder bounds.

theorem finite_periodic_expansion {F : A → E} (hF : ContDiffOn ℝ ∞ F O)
    (ℓ : A →L[ℝ] ℝ) (dx : A) (hℓx : ℓ dx = 1) (hℓy : ℓ dy = 0)
    (hX : ∀ p ∈ O, fderiv ℝ F p dx = g.X₀ p + average (g.V.val p))
    (hY : ∀ p ∈ O, fderiv ℝ F p dy = g.Y p) (n : ℕ) :
    ∃ 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) ∧
      ∀ z : ℝ, z ≠ 0 → ∀ p ∈ O,
      let L := n + 1
…

Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family