GridAtlasMetric.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Exact metric expansion for the variable grid of phases in a fixed atlas.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.grid_atlas_free_metric line 34

Source documentation

The actual grid phases reconstruct the complete tensor in the fixed atlas.

theorem grid_atlas_free_metric
    {a : A.centers → Finset Index} {h : ℝ} (hh : 0 < h)
    (hcover : ∀ i, (modeSupport (A.chartWeightCompact i) : Set SmallModes.Base) ⊆
      coverRegion (a i) h)
    {n : A.centers → ℕ} {P : ∀ i, Fin 3 → Fin (n i) → Expression}
    {G : A.centers → Base → JetPolynomial.Space} {hG : ∀ i, ContDiff ℝ ∞ (G i)}
    {φ : ∀ i, ((a i) × Fin 3) → Base → ℝ}
    {K : ∀ i, ((a i) × Fin 3) → TopologicalSpace.Compacts Base}
    {τ : ℝ} {s : ℝ≥0}
    {c : ∀ i j, PolynomialSolveData (P i) 0 (G i) (hG i) (φ i j) (K i j) τ s}
    {r : A.centers → ℝ} {ρ R : ℝ}
    {reference : A.centers → SmallModes.Base → Tensor}
…

Mentions: OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space