GlobalShiftedSmoothing.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Fixed-atlas smoothing with an unweighted derivative prefix.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.ShiftedBound line 22
Source documentation
Localized norms whose first q derivatives are unweighted.
```
def ShiftedBound (q m : ℕ) (s C : ℝ) (f : M → V) : Prop :=
…
```

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.restoration_shifted_bound line 27

Source documentation

Fixed smooth chart transitions preserve the unweighted prefix.

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

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ShiftedBound, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.restore

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.smoothing_shifted_gain line 52

Source documentation

Global gain of arbitrary higher derivatives uses only the fixed prefix.

theorem smoothing_shifted_gain (r q m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (f : M → V) (s C : ℝ),
      0 < s → s ≤ 1 → 0 ≤ C → ContMDiff planeModel 𝓘(ℝ, V) ∞ f →
      A.ShiftedBound q 0 1 C f → A.ShiftedBound q m s
        (D * ((1 + (1 + ∫ y, ‖kernel 0 y‖) ^ r) + weightedGainConstant r m) * C)
        (A.smooth r s f) := by
…

Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.weightedGainConstant

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.smoothing_shifted_bounded line 74

Source documentation

The same global smoother is bounded at every original shifted order.

theorem smoothing_shifted_bounded (r q m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (f : M → V) (s t C : ℝ),
      0 < s → 0 < t → t ≤ 1 → 0 ≤ C → ContMDiff planeModel 𝓘(ℝ, V) ∞ f →
      A.ShiftedBound q m t C f → A.ShiftedBound q m t
        (D * (1 + (1 + ∫ y, ‖kernel 0 y‖) ^ r) * C) (A.smooth r s f) := by
…

Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.smoothing_shifted_tail line 94

Source documentation

The actual global smoothing error obeys the shifted two-scale estimate.

theorem smoothing_shifted_tail (r q m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (f : M → V) (s t τ B C : ℝ),
      0 < τ → τ ≤ s → s ≤ t → t ≤ 1 → 0 ≤ B → 0 ≤ C →
      ContMDiff planeModel 𝓘(ℝ, V) ∞ f →
      A.ShiftedBound q r t B f → A.ShiftedBound q m t C f →
      A.ShiftedBound q m τ
        (D * tailConstant r * (B * (s / t) ^ r + C * (τ / t) ^ r))
        (f - A.smooth r s f) := by
…

Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tailConstant