AtlasNormalProjectionBounds.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The atlas projection is a convex sum of the actual pointwise normal projections. Local exterior estimates therefore pass to the global field.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.chartProjectedNormal line 18
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.localizedNormalField_at_source line 25
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.restored_localProjectedNormal line 32
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.projectedNormalField_eq_sum line 52
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.projectedNormalField_sub_eq line 61
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.projectedNormalField_sub_bound line 69
Source documentation
A local exterior error is not multiplied by the number of atlas patches: the squared weights add to one.
```
theorem projectedNormalField_sub_bound (F n : M → Space) (p : M) {ε : ℝ}
    (hlocal : ∀ i : A.centers, A.weight i p ≠ 0 →
      ‖A.chartProjectedNormal i F n p - n p‖ ≤ ε) :
    ‖A.projectedNormalField F n p - n p‖ ≤ ε := by
…
```
Mentions: OAI.ClosedSurfaceR4.Space
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.projectedNormalField_ne_zero line 86

theorem OAI.ClosedSurfaceR4.GeometryPreservation.compact_raw_normal_projection line 101

Source documentation

Uniform stability of the unnormalized projection on a compact family of old tangent frames. This is the estimate used before normalizing the finite-atlas sum.

theorem compact_raw_normal_projection {X : Type*} [TopologicalSpace X] [CompactSpace X]
    {A B n : X → Vec} (hA : Continuous A) (hB : Continuous B) (hn : Continuous n)
    (hD : ∀ x, gramDet (A x) (B x) ≠ 0)
    (hunit : ∀ x, n x ⬝ᵥ n x = 1)
    (hAn : ∀ x, A x ⬝ᵥ n x = 0) (hBn : ∀ x, B x ⬝ᵥ n x = 0)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ x, ∀ A' B' : Vec,
      ‖A'-A x‖ < δ → ‖B'-B x‖ < δ →
      gramDet A' B' ≠ 0 ∧ ‖realNormalPart A' B' (n x)-n x‖ < ε := by
…