ActualSmoothedStep.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

An actual metric-adapted immersion supplies all the small-increment geometry.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.normalizedStepBound line 34
Source documentation
The explicit normalized metric error of a constructed step. Its dependence on the uncontrolled input norm C is linear.
```
def normalizedStepBound (r q : ℕ) (B₀ D E V W C δ δ' τ s t : ℝ) : ℝ :=
…
```

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.actual_smoothed_step line 41

Source documentation

An actual smooth correction and its all-order normalized defect recurrence, constructed from one fixed finite-order input budget.

theorem actual_smoothed_step (d : MetricGoodPhaseData g F)
    (hF : ContMDiff planeModel spaceModel ∞ F) (r q : ℕ) {B₀ : ℝ} (hB₀ : 0 ≤ B₀) :
    ∃ a ρ η D K : ℝ, 0 < a ∧ 0 < ρ ∧ 0 < η ∧ η ≤ 1 ∧ 0 ≤ D ∧ 0 ≤ K ∧
    ∃ B T Dm Em : ℕ → ℝ,
      (∀ m, 0 ≤ B m) ∧ (∀ m, 0 ≤ T m) ∧ (∀ m, 0 ≤ Dm m) ∧ (∀ m, 0 ≤ Em m) ∧
    ∀ (G : M → Space), ContMDiff planeModel spaceModel ∞ G →
    ∀ δ δ' t s τ : ℝ, 0 < δ → 0 < δ' → δ' ≤ δ →
      0 < t → t ≤ 1 → 0 < s → s ≤ t → 0 < τ → τ ≤ s → τ/s ≤ η → δ ≤ τ →
      d.A.InputBound t r B₀ G (normalizedTensorDefect g.inner δ G) →
      d.A.WeightedBound 1 2 (ρ/4) (G-F) →
      (∀ x, ‖d.A.tensorEncode (normalizedTensorDefect g.inner δ G) x -
        d.A.tensorEncode g.inner x‖ ≤ a/8) →
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalizedTensorDefect