CoupledSmoothing.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The joint map/tensor input bound and its actual two-scale smoothing tail.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.InputBound line 25
Source documentation
The map carries a two-derivative prefix, while the metric defect has none.
```
def InputBound (t : ℝ) (m : ℕ) (C : ℝ) (G : M → Space)
    (H : ∀ p : M, CovariantTwoTensor p) : Prop :=
…
```
Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.coupled_smoothing_tail line 31

Source documentation

The two smoothing errors obey the finite-input estimate together, with only linear dependence on the possibly large higher input norm.

theorem coupled_smoothing_tail (r m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (G : M → Space) (H : ∀ p : M, CovariantTwoTensor p)
      (s t τ B C : ℝ),
      0 < τ → τ ≤ s → s ≤ t → t ≤ 1 → 0 ≤ B → 0 ≤ C →
      ContMDiff planeModel spaceModel ∞ G →
      ContMDiff planeModel (planeModel.prod 𝓘(ℝ, TensorFiber)) ∞
        (fun p => TotalSpace.mk' TensorFiber p (H p)) →
      A.InputBound t r B G H → A.InputBound t m C G H →
      A.InputBound τ m
        (D * tailConstant r * (B * (s / t) ^ r + C * (τ / t) ^ r))
        (G - A.smooth r s G) (fun p => H p - A.tensorSmooth r s H p) := by
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tailConstant