LocalPeriodicFiniteMetricIdentity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact finite metric expansion of the actual oscillatory map.

lemma OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.polynomial_zero_coefficients line 29

theorem OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Geometry.finite_metric_identity line 51

Source documentation

The exact metric identity, before replacing low coefficients by their means.

theorem finite_metric_identity {F : A → E} (hF : ContDiffOn ℝ ∞ F O)
    (U : ℕ → Family O E) (hinit : U 0 = g.initial)
    (ℓ : 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 : ℕ) (z : ℝ) (hz : z ≠ 0) {p : A} (hpO : p ∈ O) :
    let f := finiteAnsatz F U ℓ (n + 1) z
…

Mentions: OAI.ClosedSurfaceR4.LocalPeriodicExpansion.Family, OAI.ClosedSurfaceR4.LocalPeriodicExpansion.finiteAnsatz