OAI/Geometry/SurfaceImmersion/Correction/PairModelCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.pairCoordinateMap line 13
2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.pairCoordinateInverse line 14
3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.pairCoordinateMap_smooth line 16
4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.pairCoordinateInverse_smooth line 20
5. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.pairCoordinates line 25
6. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalPairScale line 49
7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalPairScale_apply line 54
8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalPairScale_injective line 59
9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalPairScale_axis line 69
10. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.pullback_model_filling line 76

    Source documentation

    Pull a compact model filling back by an affine chart and rescale its two normal coordinates. The support is the actual inverse image of the model support.

    theorem pullback_model_filling {Q : Base → Base →L[ℝ] FrameTarget}
        {B : Base → Base →L[ℝ] FrameTarget} (hB : ContDiff ℝ ∞ B)
        (hBI : ∀ x, Function.Injective (B x)) {K : Set Base} (hK : IsCompact K)
        (hBe : ∀ x ∉ K, B =ᶠ[𝓝 x] Q)
        (c h k a b : ℝ) (hh : h ≠ 0) (hk : k ≠ 0) (ha : a ≠ 0) (hb : b ≠ 0) :
        ∃ A : Base → Base →L[ℝ] FrameTarget,
          ContDiff ℝ ∞ A ∧ (∀ x, Function.Injective (A x)) ∧
          IsCompact ((pairCoordinates c h k hh hk) ⁻¹' K) ∧
          ∀ x ∉ (pairCoordinates c h k hh hk) ⁻¹' K,
            A x = (normalPairScale a b).comp (Q (pairCoordinateMap c h k x)) := by
    …

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.FrameTarget, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.pairCoordinates, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalPairScale, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.pairCoordinateMap