UniformRadiusSmoothedMetricIncrement.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

One fixed geometric neighborhood supports smoothed metric correction at every smoothing and cancellation order.

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

Source documentation

The two geometric radii are fixed before all smoothing orders, correction orders, and true-input bounds.

theorem uniform_radius_smoothed_increment (d : MetricGoodPhaseData g F)
    (hF : ContMDiff planeModel spaceModel ∞ F) :
    ∃ a ρ : ℝ, 0 < a ∧ 0 < ρ ∧
    ∀ (r q : ℕ) (B₀ : ℝ), 0 ≤ B₀ →
    ∃ (η : ℝ) (B T : ℕ → ℝ), 0 < η ∧ η ≤ 1 ∧
      (∀ 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 →
…

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

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.uniform_radius_smoothed_increment_of_input line 113

Source documentation

The metric norm bound is fixed once, and the smoothing-tail constant is chosen from the smoothing order before the correction order or input bound.

theorem uniform_radius_smoothed_increment_of_input (d : MetricGoodPhaseData g F)
    (hF : ContMDiff planeModel spaceModel ∞ F) :
    ∃ a ρ K : ℝ, 0 < a ∧ 0 < ρ ∧ 0 ≤ K ∧
    ∀ r : ℕ, ∃ D : ℝ, 0 ≤ D ∧
    ∀ (q : ℕ) (B₀ : ℝ), 0 ≤ B₀ →
    ∃ (η : ℝ) (B T : ℕ → ℝ), 0 < η ∧ η ≤ 1 ∧
      (∀ 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) →
…