SmoothedMetricIncrement.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

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

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.smoothed_increment line 34

Source documentation

A finite true-input bound supplies every analytic profile used to construct the increment at the smoothed map. All constants and thresholds precede the true input, its higher derivatives, and the three scales.

theorem smoothed_increment (d : MetricGoodPhaseData g F)
    (hF : ContMDiff planeModel spaceModel ∞ F) (r q : ℕ) {B₀ : ℝ} (hB₀ : 0 ≤ B₀) :
    ∃ a ρ η : ℝ, 0 < a ∧ 0 < ρ ∧ 0 < η ∧ η ≤ 1 ∧
    ∃ B T : ℕ → ℝ, (∀ m, 0 ≤ B m) ∧ (∀ m, 0 ≤ T m) ∧
    ∀ (G : M → Space) (H : ∀ p : M, CovariantTwoTensor p),
      ContMDiff planeModel spaceModel ∞ G →
      ContMDiff planeModel (planeModel.prod 𝓘(ℝ, TensorFiber)) ∞
        (fun p => TotalSpace.mk' TensorFiber p (H p)) →
      (∀ p v w, H p v w = H p w v) →
    ∀ t s : ℝ, 0 < t → t ≤ 1 → 0 < s → s ≤ 1 →
      d.A.InputBound t r B₀ G H →
    ∀ b : ℝ, 0 ≤ b → b < ρ → d.A.WeightedBound 1 2 b (d.A.smooth r s G-F) →
…

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

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.smoothed_increment_of_input line 118

Source documentation

The low-norm bootstrap gives the required neighborhoods of the smoothed input, so no smoothed-map hypothesis is needed by the iteration.

theorem smoothed_increment_of_input (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 : ℕ → ℝ, (∀ m, 0 ≤ B m) ∧ (∀ m, 0 ≤ T m) ∧
    ∀ (G : M → Space) (H : ∀ p : M, CovariantTwoTensor p),
      ContMDiff planeModel spaceModel ∞ G →
      ContMDiff planeModel (planeModel.prod 𝓘(ℝ, TensorFiber)) ∞
        (fun p => TotalSpace.mk' TensorFiber p (H p)) →
      (∀ p v w, H p v w = H p w v) →
    ∀ t s : ℝ, 0 < t → t ≤ 1 → 0 < s → s ≤ t →
      d.A.InputBound t r B₀ G H →
      d.A.WeightedBound 1 2 (ρ/4) (G-F) →
…