FinitePeriodicExpansion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

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

lemma OAI.ClosedSurfaceR4.PeriodicExpansion.replace_low_sum line 14

theorem OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.finite_periodic_expansion line 38

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

Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family