PeriodicFiniteMetricIdentity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact finite metric expansion of the actual oscillatory map.

lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.polynomial_zero_coefficients line 24

theorem OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.finite_metric_identity line 46

Source documentation

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

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

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