AtlasWeightedBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Fixed-atlas weighted norms and bounds for the actual restoration operator.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize_sum line 18
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.WeightedBound line 28
Source documentation
A fixed finite family of localized coordinate norms.
```
def WeightedBound (t : ℝ) (m : ℕ) (C : ℝ) (f : M → V) : Prop :=
…
```

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.restoration_bound line 36

Source documentation

Restoring finitely many coordinate functions is bounded in every fixed weighted atlas norm, uniformly in the input and the scale.

theorem restoration_bound (m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (h : A.centers → Base → V) (s C : ℝ),
      0 < s → s ≤ 1 → 0 ≤ C → (∀ i, ContDiff ℝ ∞ (h i)) →
      (∀ i, WeightedEstimates.WeightedBound Set.univ s m C (h i)) →
      A.WeightedBound s m (D * C) (∑ i : A.centers, restore (i : M) (A.outer i) (h i)) := by
…

Mentions: OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.restore