OAI/Geometry/SurfaceImmersion/Atlas/AtlasMetricLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensor_tendsto_zero_of_encode line 38

   Source documentation

   The genuine finite atlas reconstruction carries coordinate convergence to convergence in each tensor fiber.

   lemma tensor_tendsto_zero_of_encode
       {H : ℕ → ∀ p : M, CovariantTwoTensor p}
       (hH : ∀ i x, Tendsto (fun n => A.tensorEncode (H n) x i) atTop (𝓝 0))
       (p : M) : Tendsto (fun n => H n p) atTop (𝓝 0) := by
   …

   Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor

2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.metric_tendsto_of_normalized_coordinates_bound line 56

   Source documentation

   A bounded normalized defect and a vanishing amplitude imply convergence of the actual pullback metrics. No convergence of normalized defects is needed.

   theorem metric_tendsto_of_normalized_coordinates_bound
       {G : ℕ → M → Space} {δ : ℕ → ℝ} {B : ℝ}
       (target : ∀ p : M, CovariantTwoTensor p)
       (hδ : ∀ n, δ n ≠ 0) (hδ0 : Tendsto δ atTop (𝓝 0))
       (hbound : ∀ n i x,
         ‖A.tensorEncode (normalizedTensorDefect target (δ n) (G n)) x i-
           A.tensorEncode target x i‖ ≤ B)
       (p : M) (v w : TangentSpace planeModel p) :
       Tendsto (fun n => inner ℝ (mfderiv planeModel spaceModel (G n) p v)
         (mfderiv planeModel spaceModel (G n) p w)) atTop (𝓝 (target p v w)) := by
   …

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

3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.metric_tendsto_of_normalized_bound line 110

   Source documentation

   The tensor weighted norm used by the correction step supplies the coordinate bound required for metric convergence.

   theorem metric_tendsto_of_normalized_bound
       {G : ℕ → M → Space} {δ s : ℕ → ℝ} {B : ℝ}
       (target : ∀ p : M, CovariantTwoTensor p)
       (hδ : ∀ n, δ n ≠ 0) (hδ0 : Tendsto δ atTop (𝓝 0))
       (hbound : ∀ n, A.TensorWeightedBound (s n) 0 B
         (normalizedTensorDefect target (δ n) (G n)-target))
       (p : M) (v w : TangentSpace planeModel p) :
       Tendsto (fun n => inner ℝ (mfderiv planeModel spaceModel (G n) p v)
         (mfderiv planeModel spaceModel (G n) p w)) atTop (𝓝 (target p v w)) := by
   …

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

4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.metric_tendsto_of_encoded_normalized_bound line 128

   Source documentation

   The encoded zeroth-order invariant of the iteration bounds the normalized metric defect.

   theorem metric_tendsto_of_encoded_normalized_bound
       {G : ℕ → M → Space} {δ : ℕ → ℝ} {B : ℝ}
       (target : ∀ p : M, CovariantTwoTensor p)
       (hδ : ∀ n, δ n ≠ 0) (hδ0 : Tendsto δ atTop (𝓝 0))
       (hbound : ∀ n x,
         ‖A.tensorEncode (normalizedTensorDefect target (δ n) (G n)) x-
           A.tensorEncode target x‖ ≤ B)
       (p : M) (v w : TangentSpace planeModel p) :
       Tendsto (fun n => inner ℝ (mfderiv planeModel spaceModel (G n) p v)
         (mfderiv planeModel spaceModel (G n) p w)) atTop (𝓝 (target p v w)) := by
   …

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

5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.correction_limit_isometric line 144

   Source documentation

   Actual atlas correction bounds and bounded normalized defects suffice for an exact smooth isometric immersion at the series limit.

   theorem correction_limit_isometric
       {F : M → Space} {U : ℕ → M → Space} {ρ δ s : ℕ → ℝ} {B : ℝ}
       (hF : ContMDiff planeModel spaceModel ∞ F)
       (hU : ∀ n, ContMDiff planeModel spaceModel ∞ (U n))
       (hρ : Summable ρ)
       (hbound : ∀ m : ℕ, ∀ᶠ n in atTop, A.WeightedBound 1 m (ρ n) (U n))
       (houter : ∀ i x, x ∈ tsupport (A.weight i) →
         A.outer i =ᶠ[𝓝 x] (fun _ => 1))
       (g : SmoothMetric M) (hδ : ∀ n, δ n ≠ 0) (hδ0 : Tendsto δ atTop (𝓝 0))
       (hdefect : ∀ n, A.TensorWeightedBound (s n) 0 B
         (normalizedTensorDefect g.inner (δ n) (manifoldPartialMap F U n)-g.inner)) :
       IsSmoothIsometricImmersion M g (manifoldLimitMap F U) := by
   …

   Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.SmoothMetric, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalizedTensorDefect, OAI.ClosedSurfaceR4.IsSmoothIsometricImmersion

6. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.correction_limit_isometric_of_encoded_bound line 166

   Source documentation

   The stage invariant in encoded tensor coordinates produces the same isometric limit directly.

   theorem correction_limit_isometric_of_encoded_bound
       {F : M → Space} {U : ℕ → M → Space} {ρ δ : ℕ → ℝ} {B : ℝ}
       (hF : ContMDiff planeModel spaceModel ∞ F)
       (hU : ∀ n, ContMDiff planeModel spaceModel ∞ (U n))
       (hρ : Summable ρ)
       (hbound : ∀ m : ℕ, ∀ᶠ n in atTop, A.WeightedBound 1 m (ρ n) (U n))
       (houter : ∀ i x, x ∈ tsupport (A.weight i) →
         A.outer i =ᶠ[𝓝 x] (fun _ => 1))
       (g : SmoothMetric M) (hδ : ∀ n, δ n ≠ 0) (hδ0 : Tendsto δ atTop (𝓝 0))
       (hdefect : ∀ n x,
         ‖A.tensorEncode (normalizedTensorDefect g.inner (δ n) (manifoldPartialMap F U n)) x-
           A.tensorEncode g.inner x‖ ≤ B) :
   …

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