GlobalBundleSmoothing.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Boundedness, gain and finite-input tails for bundle smoothing.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundle_smoothing_bounds line 30

Source documentation

No derivative above the stated input order occurs in either bound.

theorem bundle_smoothing_bounds (r m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧
      (∀ (u : ∀ x, E x) (s t C : ℝ), 0 < s → 0 < t → t ≤ 1 → 0 ≤ C →
        ContMDiff planeModel (planeModel.prod 𝓘(ℝ, F)) ∞
          (fun x => TotalSpace.mk' F x (u x)) → A.BundleWeightedBound e t m C u →
        A.BundleWeightedBound e t m (D * (1 + (1 + ∫ y, ‖kernel 0 y‖) ^ r) * C)
          (A.bundleSmooth e r s u)) ∧
      (∀ (u : ∀ x, E x) (s t C : ℝ), 0 < s → s ≤ 1 → 0 ≤ C →
        ContMDiff planeModel (planeModel.prod 𝓘(ℝ, F)) ∞
          (fun x => TotalSpace.mk' F x (u x)) → A.BundleWeightedBound e t 0 C u →
        A.BundleWeightedBound e s m (D * weightedGainConstant r m * C)
          (A.bundleSmooth e r s u)) := by
…

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

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundle_smoothing_tail line 69

Source documentation

The high input norm remains linear after all bundle transition maps.

theorem bundle_smoothing_tail (r m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (u : ∀ x, E x) (s t τ B C : ℝ),
      0 < τ → τ ≤ s → s ≤ t → t ≤ 1 → 0 ≤ B → 0 ≤ C →
      ContMDiff planeModel (planeModel.prod 𝓘(ℝ, F)) ∞
        (fun x => TotalSpace.mk' F x (u x)) →
      A.BundleWeightedBound e t r B u → A.BundleWeightedBound e t m C u →
      A.BundleWeightedBound e τ m
        (D * tailConstant r * (B * (s / t) ^ r + C * (τ / t) ^ r))
        (fun x => u x - A.bundleSmooth e r s u x) := by
…

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